algextdeglem5 - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > algextdeglem5		Structured version Visualization version GIF version

Theorem algextdeglem5 33389

Description: Lemma for algextdeg 33393. The subspace 𝑍 of annihilators of 𝐴 is a principal ideal generated by the minimal polynomial. (Contributed by Thierry Arnoux, 2-Apr-2025.)

**Hypotheses**
Ref	Expression
algextdeg.k	⊢ 𝐾 = (𝐸 ↾_s 𝐹)
algextdeg.l	⊢ 𝐿 = (𝐸 ↾_s (𝐸 fldGen (𝐹 ∪ {𝐴})))
algextdeg.d	⊢ 𝐷 = ( deg₁ ‘𝐸)
algextdeg.m	⊢ 𝑀 = (𝐸 minPoly 𝐹)
algextdeg.f	⊢ (𝜑 → 𝐸 ∈ Field)
algextdeg.e	⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))
algextdeg.a	⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))
algextdeglem.o	⊢ 𝑂 = (𝐸 evalSub₁ 𝐹)
algextdeglem.y	⊢ 𝑃 = (Poly₁‘𝐾)
algextdeglem.u	⊢ 𝑈 = (Base‘𝑃)
algextdeglem.g	⊢ 𝐺 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴))
algextdeglem.n	⊢ 𝑁 = (𝑥 ∈ 𝑈 ↦ [𝑥](𝑃 ~_QG 𝑍))
algextdeglem.z	⊢ 𝑍 = (^◡𝐺 “ {(0_g‘𝐿)})
algextdeglem.q	⊢ 𝑄 = (𝑃 /_s (𝑃 ~_QG 𝑍))
algextdeglem.j	⊢ 𝐽 = (𝑝 ∈ (Base‘𝑄) ↦ ∪ (𝐺 “ 𝑝))

**Assertion**
Ref	Expression
algextdeglem5	⊢ (𝜑 → 𝑍 = ((RSpan‘𝑃)‘{(𝑀‘𝐴)}))

Distinct variable groups: 𝐴,𝑝 𝐸,𝑝 𝐹,𝑝,𝑥 𝐺,𝑝,𝑥 𝐽,𝑝,𝑥 𝐾,𝑝 𝐿,𝑝,𝑥 𝑥,𝑁 𝑂,𝑝 𝑃,𝑝,𝑥 𝑄,𝑝,𝑥 𝑈,𝑝,𝑥 𝑍,𝑝,𝑥 𝜑,𝑝,𝑥 Allowed substitution hints: 𝐴(𝑥) 𝐷(𝑥,𝑝) 𝐸(𝑥) 𝐾(𝑥) 𝑀(𝑥,𝑝) 𝑁(𝑝) 𝑂(𝑥)

Proof of Theorem algextdeglem5 Dummy variable 𝑞 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		algextdeglem.o	. . 3 ⊢ 𝑂 = (𝐸 evalSub₁ 𝐹)
2		algextdeglem.y	. . . 4 ⊢ 𝑃 = (Poly₁‘𝐾)
3		algextdeg.k	. . . . 5 ⊢ 𝐾 = (𝐸 ↾_s 𝐹)
4	3	fveq2i 6900	. . . 4 ⊢ (Poly₁‘𝐾) = (Poly₁‘(𝐸 ↾_s 𝐹))
5	2, 4	eqtri 2756	. . 3 ⊢ 𝑃 = (Poly₁‘(𝐸 ↾_s 𝐹))
6		eqid 2728	. . 3 ⊢ (Base‘𝐸) = (Base‘𝐸)
7		algextdeg.f	. . 3 ⊢ (𝜑 → 𝐸 ∈ Field)
8		algextdeg.e	. . 3 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))
9		eqid 2728	. . . . 5 ⊢ (0_g‘𝐸) = (0_g‘𝐸)
10	7	fldcrngd 20637	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ CRing)
11		issdrg 20676	. . . . . . 7 ⊢ (𝐹 ∈ (SubDRing‘𝐸) ↔ (𝐸 ∈ DivRing ∧ 𝐹 ∈ (SubRing‘𝐸) ∧ (𝐸 ↾_s 𝐹) ∈ DivRing))
12	8, 11	sylib 217	. . . . . 6 ⊢ (𝜑 → (𝐸 ∈ DivRing ∧ 𝐹 ∈ (SubRing‘𝐸) ∧ (𝐸 ↾_s 𝐹) ∈ DivRing))
13	12	simp2d 1141	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸))
14	1, 3, 6, 9, 10, 13	irngssv 33366	. . . 4 ⊢ (𝜑 → (𝐸 IntgRing 𝐹) ⊆ (Base‘𝐸))
15		algextdeg.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))
16	14, 15	sseldd 3981	. . 3 ⊢ (𝜑 → 𝐴 ∈ (Base‘𝐸))
17		eqid 2728	. . 3 ⊢ {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0_g‘𝐸)} = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0_g‘𝐸)}
18		eqid 2728	. . 3 ⊢ (RSpan‘𝑃) = (RSpan‘𝑃)
19		eqid 2728	. . 3 ⊢ (idlGen_1p‘(𝐸 ↾_s 𝐹)) = (idlGen_1p‘(𝐸 ↾_s 𝐹))
20	1, 5, 6, 7, 8, 16, 9, 17, 18, 19	ply1annig1p 33375	. 2 ⊢ (𝜑 → {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0_g‘𝐸)} = ((RSpan‘𝑃)‘{((idlGen_1p‘(𝐸 ↾_s 𝐹))‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0_g‘𝐸)})}))
21		algextdeglem.z	. . . 4 ⊢ 𝑍 = (^◡𝐺 “ {(0_g‘𝐿)})
22	10	crnggrpd 20187	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ Grp)
23	22	grpmndd 18903	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ Mnd)
24	7	flddrngd 20636	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∈ DivRing)
25		subrgsubg 20516	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (SubRing‘𝐸) → 𝐹 ∈ (SubGrp‘𝐸))
26	6	subgss 19082	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (SubGrp‘𝐸) → 𝐹 ⊆ (Base‘𝐸))
27	13, 25, 26	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐸))
28	16	snssd 4813	. . . . . . . . . . 11 ⊢ (𝜑 → {𝐴} ⊆ (Base‘𝐸))
29	27, 28	unssd 4186	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹 ∪ {𝐴}) ⊆ (Base‘𝐸))
30	6, 24, 29	fldgensdrg 33014	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubDRing‘𝐸))
31		sdrgsubrg 20679	. . . . . . . . 9 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubDRing‘𝐸) → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸))
32		subrgsubg 20516	. . . . . . . . 9 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubGrp‘𝐸))
33	30, 31, 32	3syl 18	. . . . . . . 8 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubGrp‘𝐸))
34	9	subg0cl 19089	. . . . . . . 8 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubGrp‘𝐸) → (0_g‘𝐸) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})))
35	33, 34	syl 17	. . . . . . 7 ⊢ (𝜑 → (0_g‘𝐸) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})))
36	6, 24, 29	fldgenssv 33015	. . . . . . 7 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ⊆ (Base‘𝐸))
37		algextdeg.l	. . . . . . . 8 ⊢ 𝐿 = (𝐸 ↾_s (𝐸 fldGen (𝐹 ∪ {𝐴})))
38	37, 6, 9	ress0g 18722	. . . . . . 7 ⊢ ((𝐸 ∈ Mnd ∧ (0_g‘𝐸) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∧ (𝐸 fldGen (𝐹 ∪ {𝐴})) ⊆ (Base‘𝐸)) → (0_g‘𝐸) = (0_g‘𝐿))
39	23, 35, 36, 38	syl3anc 1369	. . . . . 6 ⊢ (𝜑 → (0_g‘𝐸) = (0_g‘𝐿))
40	39	sneqd 4641	. . . . 5 ⊢ (𝜑 → {(0_g‘𝐸)} = {(0_g‘𝐿)})
41	40	imaeq2d 6063	. . . 4 ⊢ (𝜑 → (^◡𝐺 “ {(0_g‘𝐸)}) = (^◡𝐺 “ {(0_g‘𝐿)}))
42	21, 41	eqtr4id 2787	. . 3 ⊢ (𝜑 → 𝑍 = (^◡𝐺 “ {(0_g‘𝐸)}))
43		algextdeglem.g	. . . . 5 ⊢ 𝐺 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴))
44		algextdeglem.u	. . . . . 6 ⊢ 𝑈 = (Base‘𝑃)
45	44	mpteq1i 5244	. . . . 5 ⊢ (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴)) = (𝑝 ∈ (Base‘𝑃) ↦ ((𝑂‘𝑝)‘𝐴))
46	43, 45	eqtri 2756	. . . 4 ⊢ 𝐺 = (𝑝 ∈ (Base‘𝑃) ↦ ((𝑂‘𝑝)‘𝐴))
47	1, 5, 6, 10, 13, 16, 9, 17, 46	ply1annidllem 33372	. . 3 ⊢ (𝜑 → {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0_g‘𝐸)} = (^◡𝐺 “ {(0_g‘𝐸)}))
48	42, 47	eqtr4d 2771	. 2 ⊢ (𝜑 → 𝑍 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0_g‘𝐸)})
49		algextdeg.m	. . . . 5 ⊢ 𝑀 = (𝐸 minPoly 𝐹)
50	1, 5, 6, 7, 8, 16, 9, 17, 18, 19, 49	minplyval 33376	. . . 4 ⊢ (𝜑 → (𝑀‘𝐴) = ((idlGen_1p‘(𝐸 ↾_s 𝐹))‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0_g‘𝐸)}))
51	50	sneqd 4641	. . 3 ⊢ (𝜑 → {(𝑀‘𝐴)} = {((idlGen_1p‘(𝐸 ↾_s 𝐹))‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0_g‘𝐸)})})
52	51	fveq2d 6901	. 2 ⊢ (𝜑 → ((RSpan‘𝑃)‘{(𝑀‘𝐴)}) = ((RSpan‘𝑃)‘{((idlGen_1p‘(𝐸 ↾_s 𝐹))‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0_g‘𝐸)})}))
53	20, 48, 52	3eqtr4d 2778	1 ⊢ (𝜑 → 𝑍 = ((RSpan‘𝑃)‘{(𝑀‘𝐴)}))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ w3a 1085 = wceq 1534 ∈ wcel 2099 {crab 3429 ∪ cun 3945 ⊆ wss 3947 {csn 4629 ∪ cuni 4908 ↦ cmpt 5231 ^◡ccnv 5677 dom cdm 5678 “ cima 5681 ‘cfv 6548 (class class class)co 7420 [cec 8723 Basecbs 17180 ↾_s cress 17209 0_gc0g 17421 /_s cqus 17487 Mndcmnd 18694 SubGrpcsubg 19075 ~_QG cqg 19077 SubRingcsubrg 20506 DivRingcdr 20624 Fieldcfield 20625 SubDRingcsdrg 20674 RSpancrsp 21103 Poly₁cpl1 22096 evalSub₁ ces1 22232 deg₁ cdg1 26000 idlGen_1pcig1p 26078 fldGen cfldgen 33010 IntgRing cirng 33361 minPoly cminply 33370

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2699 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5365 ax-pr 5429 ax-un 7740 ax-cnex 11195 ax-resscn 11196 ax-1cn 11197 ax-icn 11198 ax-addcl 11199 ax-addrcl 11200 ax-mulcl 11201 ax-mulrcl 11202 ax-mulcom 11203 ax-addass 11204 ax-mulass 11205 ax-distr 11206 ax-i2m1 11207 ax-1ne0 11208 ax-1rid 11209 ax-rnegex 11210 ax-rrecex 11211 ax-cnre 11212 ax-pre-lttri 11213 ax-pre-lttrn 11214 ax-pre-ltadd 11215 ax-pre-mulgt0 11216 ax-pre-sup 11217 ax-addf 11218

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2530 df-eu 2559 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-ne 2938 df-nel 3044 df-ral 3059 df-rex 3068 df-rmo 3373 df-reu 3374 df-rab 3430 df-v 3473 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-tp 4634 df-op 4636 df-uni 4909 df-int 4950 df-iun 4998 df-iin 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5576 df-eprel 5582 df-po 5590 df-so 5591 df-fr 5633 df-se 5634 df-we 5635 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 df-pred 6305 df-ord 6372 df-on 6373 df-lim 6374 df-suc 6375 df-iota 6500 df-fun 6550 df-fn 6551 df-f 6552 df-f1 6553 df-fo 6554 df-f1o 6555 df-fv 6556 df-isom 6557 df-riota 7376 df-ov 7423 df-oprab 7424 df-mpo 7425 df-of 7685 df-ofr 7686 df-om 7871 df-1st 7993 df-2nd 7994 df-supp 8166 df-tpos 8232 df-frecs 8287 df-wrecs 8318 df-recs 8392 df-rdg 8431 df-1o 8487 df-er 8725 df-map 8847 df-pm 8848 df-ixp 8917 df-en 8965 df-dom 8966 df-sdom 8967 df-fin 8968 df-fsupp 9387 df-sup 9466 df-inf 9467 df-oi 9534 df-card 9963 df-pnf 11281 df-mnf 11282 df-xr 11283 df-ltxr 11284 df-le 11285 df-sub 11477 df-neg 11478 df-nn 12244 df-2 12306 df-3 12307 df-4 12308 df-5 12309 df-6 12310 df-7 12311 df-8 12312 df-9 12313 df-n0 12504 df-z 12590 df-dec 12709 df-uz 12854 df-fz 13518 df-fzo 13661 df-seq 14000 df-hash 14323 df-struct 17116 df-sets 17133 df-slot 17151 df-ndx 17163 df-base 17181 df-ress 17210 df-plusg 17246 df-mulr 17247 df-starv 17248 df-sca 17249 df-vsca 17250 df-ip 17251 df-tset 17252 df-ple 17253 df-ds 17255 df-unif 17256 df-hom 17257 df-cco 17258 df-0g 17423 df-gsum 17424 df-prds 17429 df-pws 17431 df-mre 17566 df-mrc 17567 df-acs 17569 df-mgm 18600 df-sgrp 18679 df-mnd 18695 df-mhm 18740 df-submnd 18741 df-grp 18893 df-minusg 18894 df-sbg 18895 df-mulg 19024 df-subg 19078 df-ghm 19168 df-cntz 19268 df-cmn 19737 df-abl 19738 df-mgp 20075 df-rng 20093 df-ur 20122 df-srg 20127 df-ring 20175 df-cring 20176 df-oppr 20273 df-dvdsr 20296 df-unit 20297 df-invr 20327 df-dvr 20340 df-rhm 20411 df-subrng 20483 df-subrg 20508 df-drng 20626 df-field 20627 df-sdrg 20675 df-lmod 20745 df-lss 20816 df-lsp 20856 df-sra 21058 df-rgmod 21059 df-lidl 21104 df-rsp 21105 df-rlreg 21230 df-cnfld 21280 df-assa 21787 df-asp 21788 df-ascl 21789 df-psr 21842 df-mvr 21843 df-mpl 21844 df-opsr 21846 df-evls 22018 df-evl 22019 df-psr1 22099 df-vr1 22100 df-ply1 22101 df-coe1 22102 df-evls1 22234 df-evl1 22235 df-mdeg 26001 df-deg1 26002 df-mon1 26079 df-uc1p 26080 df-q1p 26081 df-r1p 26082 df-ig1p 26083 df-fldgen 33011 df-irng 33362 df-minply 33371

This theorem is referenced by: algextdeglem6 33390

W3C validator

	
		OSZAR »