Theorem algextdeglem4 34054

Description: Lemma for algextdeg 34059. By lmhmqusker 33669, the surjective module homomorphism 𝐺 described in algextdeglem2 34052 induces an isomorphism with the quotient space. Therefore, the dimension of that quotient space 𝑃 / 𝑍 is the degree of the algebraic field extension. (Contributed by Thierry Arnoux, 2-Apr-2025.)

Hypotheses

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

Assertion

Ref	Expression
algextdeglem4	⊢ (𝜑 → (dim‘𝑄) = (𝐿[:]𝐾))

Distinct variable groups:   𝐴,𝑝   𝐸,𝑝   𝐹,𝑝,𝑥   𝐺,𝑝,𝑥   𝐽,𝑝,𝑥   𝐾,𝑝   𝐿,𝑝,𝑥   𝑥,𝑁   𝑂,𝑝   𝑃,𝑝,𝑥   𝑄,𝑝,𝑥   𝑈,𝑝,𝑥   𝑍,𝑝,𝑥   𝜑,𝑝,𝑥

Allowed substitution hints:   𝐴(𝑥)   𝐷(𝑥,𝑝)   𝐸(𝑥)   𝐾(𝑥)   𝑀(𝑥,𝑝)   𝑁(𝑝)   𝑂(𝑥)

Proof of Theorem algextdeglem4

Dummy variable 𝑞 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		algextdeg.e	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))
2		issdrg 20868	. . . . . . . 8 ⊢ (𝐹 ∈ (SubDRing‘𝐸) ↔ (𝐸 ∈ DivRing ∧ 𝐹 ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s 𝐹) ∈ DivRing))
3	1, 2	sylib 221	. . . . . . 7 ⊢ (𝜑 → (𝐸 ∈ DivRing ∧ 𝐹 ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s 𝐹) ∈ DivRing))
4	3	simp2d 1159	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸))
5		subrgsubg 20661	. . . . . 6 ⊢ (𝐹 ∈ (SubRing‘𝐸) → 𝐹 ∈ (SubGrp‘𝐸))
6		eqid 2769	. . . . . . 7 ⊢ (Base‘𝐸) = (Base‘𝐸)
7	6	subgss 19192	. . . . . 6 ⊢ (𝐹 ∈ (SubGrp‘𝐸) → 𝐹 ⊆ (Base‘𝐸))
8	4, 5, 7	3syl 19	. . . . 5 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐸))
9		algextdeg.k	. . . . . 6 ⊢ 𝐾 = (𝐸 ↾s 𝐹)
10	9, 6	ressbas2 17297	. . . . 5 ⊢ (𝐹 ⊆ (Base‘𝐸) → 𝐹 = (Base‘𝐾))
11	8, 10	syl 18	. . . 4 ⊢ (𝜑 → 𝐹 = (Base‘𝐾))
12	11	fveq2d 6886	. . 3 ⊢ (𝜑 → ((subringAlg ‘𝐿)‘𝐹) = ((subringAlg ‘𝐿)‘(Base‘𝐾)))
13	12	fveq2d 6886	. 2 ⊢ (𝜑 → (dim‘((subringAlg ‘𝐿)‘𝐹)) = (dim‘((subringAlg ‘𝐿)‘(Base‘𝐾))))
14		eqid 2769	. . . . 5 ⊢ (0g‘((subringAlg ‘𝐿)‘𝐹)) = (0g‘((subringAlg ‘𝐿)‘𝐹))
15		algextdeg.l	. . . . . 6 ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴})))
16		algextdeg.d	. . . . . 6 ⊢ 𝐷 = (deg1‘𝐸)
17		algextdeg.m	. . . . . 6 ⊢ 𝑀 = (𝐸 minPoly 𝐹)
18		algextdeg.f	. . . . . 6 ⊢ (𝜑 → 𝐸 ∈ Field)
19		algextdeg.a	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))
20		algextdeglem.o	. . . . . 6 ⊢ 𝑂 = (𝐸 evalSub1 𝐹)
21		algextdeglem.y	. . . . . 6 ⊢ 𝑃 = (Poly1‘𝐾)
22		algextdeglem.u	. . . . . 6 ⊢ 𝑈 = (Base‘𝑃)
23		algextdeglem.g	. . . . . 6 ⊢ 𝐺 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴))
24		algextdeglem.n	. . . . . 6 ⊢ 𝑁 = (𝑥 ∈ 𝑈 ↦ [𝑥](𝑃 ~QG 𝑍))
25		algextdeglem.z	. . . . . 6 ⊢ 𝑍 = (◡𝐺 “ {(0g‘𝐿)})
26		algextdeglem.q	. . . . . 6 ⊢ 𝑄 = (𝑃 /s (𝑃 ~QG 𝑍))
27		algextdeglem.j	. . . . . 6 ⊢ 𝐽 = (𝑝 ∈ (Base‘𝑄) ↦ ∪ (𝐺 “ 𝑝))
28	9, 15, 16, 17, 18, 1, 19, 20, 21, 22, 23, 24, 25, 26, 27	algextdeglem2 34052	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ (𝑃 LMHom ((subringAlg ‘𝐿)‘𝐹)))
29		eqid 2769	. . . . 5 ⊢ (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}) = (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})
30		eqid 2769	. . . . 5 ⊢ (𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}))) = (𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))
31	9	fveq2i 6885	. . . . . . . . . . 11 ⊢ (Poly1‘𝐾) = (Poly1‘(𝐸 ↾s 𝐹))
32	21, 31	eqtri 2792	. . . . . . . . . 10 ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))
33	18	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝐸 ∈ Field)
34	1	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝐹 ∈ (SubDRing‘𝐸))
35		eqid 2769	. . . . . . . . . . . . 13 ⊢ (0g‘𝐸) = (0g‘𝐸)
36	18	fldcrngd 20825	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸 ∈ CRing)
37	20, 9, 6, 35, 36, 4	irngssv 34022	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸 IntgRing 𝐹) ⊆ (Base‘𝐸))
38	37, 19	sseldd 3946	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ (Base‘𝐸))
39	38	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝐴 ∈ (Base‘𝐸))
40		simpr 489	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝑝 ∈ 𝑈)
41	6, 20, 32, 22, 33, 34, 39, 40	evls1fldgencl 34004	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → ((𝑂‘𝑝)‘𝐴) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})))
42	41	ralrimiva 3163	. . . . . . . 8 ⊢ (𝜑 → ∀𝑝 ∈ 𝑈 ((𝑂‘𝑝)‘𝐴) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})))
43	23	rnmptss 7119	. . . . . . . 8 ⊢ (∀𝑝 ∈ 𝑈 ((𝑂‘𝑝)‘𝐴) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})) → ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))
44	42, 43	syl 18	. . . . . . 7 ⊢ (𝜑 → ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))
45	18	flddrngd 20824	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ DivRing)
46	20, 32, 6, 22, 36, 4, 38, 23	evls1maprhm 22504	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ (𝑃 RingHom 𝐸))
47		rnrhmsubrg 20689	. . . . . . . . . 10 ⊢ (𝐺 ∈ (𝑃 RingHom 𝐸) → ran 𝐺 ∈ (SubRing‘𝐸))
48	46, 47	syl 18	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐺 ∈ (SubRing‘𝐸))
49	15	oveq1i 7421	. . . . . . . . . . 11 ⊢ (𝐿 ↾s ran 𝐺) = ((𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ↾s ran 𝐺)
50		ovex 7444	. . . . . . . . . . . 12 ⊢ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ V
51		ressabs 17307	. . . . . . . . . . . 12 ⊢ (((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ V ∧ ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴}))) → ((𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ↾s ran 𝐺) = (𝐸 ↾s ran 𝐺))
52	50, 44, 51	sylancr 598	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ↾s ran 𝐺) = (𝐸 ↾s ran 𝐺))
53	49, 52	eqtrid 2816	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿 ↾s ran 𝐺) = (𝐸 ↾s ran 𝐺))
54		eqid 2769	. . . . . . . . . . . . . . 15 ⊢ (0g‘𝐿) = (0g‘𝐿)
55	38	snssd 4757	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → {𝐴} ⊆ (Base‘𝐸))
56	8, 55	unssd 4153	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐹 ∪ {𝐴}) ⊆ (Base‘𝐸))
57	6, 45, 56	fldgensdrg 33577	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubDRing‘𝐸))
58		issdrg 20868	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubDRing‘𝐸) ↔ (𝐸 ∈ DivRing ∧ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ∈ DivRing))
59	57, 58	sylib 221	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 ∈ DivRing ∧ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ∈ DivRing))
60	59	simp2d 1159	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸))
61	15	resrhm2b 20686	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴}))) → (𝐺 ∈ (𝑃 RingHom 𝐸) ↔ 𝐺 ∈ (𝑃 RingHom 𝐿)))
62	61	biimpa 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴}))) ∧ 𝐺 ∈ (𝑃 RingHom 𝐸)) → 𝐺 ∈ (𝑃 RingHom 𝐿))
63	60, 44, 46, 62	syl21anc 850	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐺 ∈ (𝑃 RingHom 𝐿))
64		rhmghm 20564	. . . . . . . . . . . . . . . 16 ⊢ (𝐺 ∈ (𝑃 RingHom 𝐿) → 𝐺 ∈ (𝑃 GrpHom 𝐿))
65	63, 64	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺 ∈ (𝑃 GrpHom 𝐿))
66	54, 65, 25, 26, 27, 22, 24	ghmquskerco 19353	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺 = (𝐽 ∘ 𝑁))
67	66	rneqd 5929	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝐺 = ran (𝐽 ∘ 𝑁))
68	26	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑄 = (𝑃 /s (𝑃 ~QG 𝑍)))
69	22	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑈 = (Base‘𝑃))
70		ovexd 7446	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃 ~QG 𝑍) ∈ V)
71	3	simp3d 1160	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ DivRing)
72	32, 71	ply1lvec 33793	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ LVec)
73	68, 69, 70, 72	qusbas 17598	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 / (𝑃 ~QG 𝑍)) = (Base‘𝑄))
74		eqid 2769	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 / (𝑃 ~QG 𝑍)) = (𝑈 / (𝑃 ~QG 𝑍))
75	54	ghmker 19311	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 ∈ (𝑃 GrpHom 𝐿) → (◡𝐺 “ {(0g‘𝐿)}) ∈ (NrmSGrp‘𝑃))
76	65, 75	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (◡𝐺 “ {(0g‘𝐿)}) ∈ (NrmSGrp‘𝑃))
77	25, 76	eqeltrid 2873	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑍 ∈ (NrmSGrp‘𝑃))
78	22, 74, 24, 77	qusrn 33661	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ran 𝑁 = (𝑈 / (𝑃 ~QG 𝑍)))
79		eqid 2769	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((subringAlg ‘𝐸)‘𝐹) = ((subringAlg ‘𝐸)‘𝐹)
80	20, 32, 6, 22, 36, 4, 38, 23, 79	evls1maplmhm 22505	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐺 ∈ (𝑃 LMHom ((subringAlg ‘𝐸)‘𝐹)))
81	80	elexd 3486	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐺 ∈ V)
82	81	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘𝑄)) → 𝐺 ∈ V)
83	82	imaexd 7912	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘𝑄)) → (𝐺 “ 𝑝) ∈ V)
84	83	uniexd 7740	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘𝑄)) → ∪ (𝐺 “ 𝑝) ∈ V)
85	27, 84	dmmptd 6681	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom 𝐽 = (Base‘𝑄))
86	73, 78, 85	3eqtr4rd 2815	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom 𝐽 = ran 𝑁)
87		rncoeq 5972	. . . . . . . . . . . . . 14 ⊢ (dom 𝐽 = ran 𝑁 → ran (𝐽 ∘ 𝑁) = ran 𝐽)
88	86, 87	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran (𝐽 ∘ 𝑁) = ran 𝐽)
89	67, 88	eqtrd 2804	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝐺 = ran 𝐽)
90	89	oveq2d 7427	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐿 ↾s ran 𝐺) = (𝐿 ↾s ran 𝐽))
91		eqid 2769	. . . . . . . . . . . 12 ⊢ (𝐿 ↾s ran 𝐽) = (𝐿 ↾s ran 𝐽)
92	9	subrgcrng 20659	. . . . . . . . . . . . . . 15 ⊢ ((𝐸 ∈ CRing ∧ 𝐹 ∈ (SubRing‘𝐸)) → 𝐾 ∈ CRing)
93	36, 4, 92	syl2anc 595	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ CRing)
94	21	ply1crng 22326	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ CRing → 𝑃 ∈ CRing)
95	93, 94	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ CRing)
96	54, 63, 25, 26, 27, 95	rhmquskerlem 33676	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ (𝑄 RingHom 𝐿))
97	20, 32, 6, 22, 36, 4, 38, 23	evls1maprnss 22506	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 ⊆ ran 𝐺)
98		eqid 2769	. . . . . . . . . . . . . . . . . 18 ⊢ (1r‘𝐸) = (1r‘𝐸)
99	9, 98	subrg1 20666	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (SubRing‘𝐸) → (1r‘𝐸) = (1r‘𝐾))
100	4, 99	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1r‘𝐸) = (1r‘𝐾))
101	98	subrg1cl 20664	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (SubRing‘𝐸) → (1r‘𝐸) ∈ 𝐹)
102	4, 101	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1r‘𝐸) ∈ 𝐹)
103	100, 102	eqeltrrd 2870	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1r‘𝐾) ∈ 𝐹)
104	97, 103	sseldd 3946	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1r‘𝐾) ∈ ran 𝐺)
105		drngnzr 20831	. . . . . . . . . . . . . . . . 17 ⊢ (𝐸 ∈ DivRing → 𝐸 ∈ NzRing)
106	98, 35	nzrnz 20597	. . . . . . . . . . . . . . . . 17 ⊢ (𝐸 ∈ NzRing → (1r‘𝐸) ≠ (0g‘𝐸))
107	45, 105, 106	3syl 19	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1r‘𝐸) ≠ (0g‘𝐸))
108	36	crnggrpd 20328	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐸 ∈ Grp)
109	108	grpmndd 19012	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐸 ∈ Mnd)
110		sdrgsubrg 20871	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubDRing‘𝐸) → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸))
111		subrgsubg 20661	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubGrp‘𝐸))
112	57, 110, 111	3syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubGrp‘𝐸))
113	35	subg0cl 19199	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubGrp‘𝐸) → (0g‘𝐸) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})))
114	112, 113	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0g‘𝐸) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})))
115	6, 45, 56	fldgenssv 33578	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ⊆ (Base‘𝐸))
116	15, 6, 35	ress0g 18819	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐸 ∈ Mnd ∧ (0g‘𝐸) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∧ (𝐸 fldGen (𝐹 ∪ {𝐴})) ⊆ (Base‘𝐸)) → (0g‘𝐸) = (0g‘𝐿))
117	109, 114, 115, 116	syl3anc 1396	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐿))
118	107, 100, 117	3netr3d 3040	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1r‘𝐾) ≠ (0g‘𝐿))
119		nelsn 4637	. . . . . . . . . . . . . . 15 ⊢ ((1r‘𝐾) ≠ (0g‘𝐿) → ¬ (1r‘𝐾) ∈ {(0g‘𝐿)})
120	118, 119	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ¬ (1r‘𝐾) ∈ {(0g‘𝐿)})
121		nelne1 3061	. . . . . . . . . . . . . 14 ⊢ (((1r‘𝐾) ∈ ran 𝐺 ∧ ¬ (1r‘𝐾) ∈ {(0g‘𝐿)}) → ran 𝐺 ≠ {(0g‘𝐿)})
122	104, 120, 121	syl2anc 595	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝐺 ≠ {(0g‘𝐿)})
123	89, 122	eqnetrrd 3032	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝐽 ≠ {(0g‘𝐿)})
124		eqid 2769	. . . . . . . . . . . . 13 ⊢ (oppr‘𝑃) = (oppr‘𝑃)
125	9	sdrgdrng 20870	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐾 ∈ DivRing)
126		drngnzr 20831	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ DivRing → 𝐾 ∈ NzRing)
127	1, 125, 126	3syl 19	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ NzRing)
128	21	ply1nz 26247	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ NzRing → 𝑃 ∈ NzRing)
129	127, 128	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ NzRing)
130		eqid 2769	. . . . . . . . . . . . . . . 16 ⊢ {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)} = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)}
131		eqid 2769	. . . . . . . . . . . . . . . 16 ⊢ (RSpan‘𝑃) = (RSpan‘𝑃)
132	9	fveq2i 6885	. . . . . . . . . . . . . . . 16 ⊢ (idlGen1p‘𝐾) = (idlGen1p‘(𝐸 ↾s 𝐹))
133	20, 32, 6, 18, 1, 38, 35, 130, 131, 132	ply1annig1p 34038	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)} = ((RSpan‘𝑃)‘{((idlGen1p‘𝐾)‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)})}))
134	117	sneqd 4606	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → {(0g‘𝐸)} = {(0g‘𝐿)})
135	134	imaeq2d 6063	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (◡𝐺 “ {(0g‘𝐸)}) = (◡𝐺 “ {(0g‘𝐿)}))
136	25, 135	eqtr4id 2823	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑍 = (◡𝐺 “ {(0g‘𝐸)}))
137	22	mpteq1i 5206	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴)) = (𝑝 ∈ (Base‘𝑃) ↦ ((𝑂‘𝑝)‘𝐴))
138	23, 137	eqtri 2792	. . . . . . . . . . . . . . . . 17 ⊢ 𝐺 = (𝑝 ∈ (Base‘𝑃) ↦ ((𝑂‘𝑝)‘𝐴))
139	20, 32, 6, 36, 4, 38, 35, 130, 138	ply1annidllem 34035	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)} = (◡𝐺 “ {(0g‘𝐸)}))
140	136, 139	eqtr4d 2807	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑍 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)})
141		eqid 2769	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐸 minPoly 𝐹) = (𝐸 minPoly 𝐹)
142	20, 32, 6, 18, 1, 38, 35, 130, 131, 132, 141	minplyval 34039	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) = ((idlGen1p‘𝐾)‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)}))
143	142	sneqd 4606	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {((𝐸 minPoly 𝐹)‘𝐴)} = {((idlGen1p‘𝐾)‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)})})
144	143	fveq2d 6886	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) = ((RSpan‘𝑃)‘{((idlGen1p‘𝐾)‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)})}))
145	133, 140, 144	3eqtr4d 2814	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑍 = ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}))
146		eqid 2769	. . . . . . . . . . . . . . . 16 ⊢ (0g‘𝑃) = (0g‘𝑃)
147		eqid 2769	. . . . . . . . . . . . . . . . . 18 ⊢ (0g‘(Poly1‘𝐸)) = (0g‘(Poly1‘𝐸))
148	147, 18, 1, 141, 19	irngnminplynz 34046	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ≠ (0g‘(Poly1‘𝐸)))
149		eqid 2769	. . . . . . . . . . . . . . . . . 18 ⊢ (Poly1‘𝐸) = (Poly1‘𝐸)
150	149, 9, 21, 22, 4, 147	ressply10g 33801	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0g‘(Poly1‘𝐸)) = (0g‘𝑃))
151	148, 150	neeqtrd 3033	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ≠ (0g‘𝑃))
152	20, 32, 6, 18, 1, 38, 141, 146, 151	minplyirred 34045	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ∈ (Irred‘𝑃))
153		eqid 2769	. . . . . . . . . . . . . . . 16 ⊢ ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) = ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)})
154		fldsdrgfld 20878	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ (SubDRing‘𝐸)) → (𝐸 ↾s 𝐹) ∈ Field)
155	18, 1, 154	syl2anc 595	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ Field)
156	9, 155	eqeltrid 2873	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 ∈ Field)
157	21	ply1pid 26308	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ Field → 𝑃 ∈ PID)
158	156, 157	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ PID)
159	20, 32, 6, 18, 1, 38, 35, 130, 131, 132, 141	minplycl 34040	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ∈ (Base‘𝑃))
160	159, 22	eleqtrrdi 2880	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ∈ 𝑈)
161	95	crngringd 20327	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ Ring)
162	160	snssd 4757	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → {((𝐸 minPoly 𝐹)‘𝐴)} ⊆ 𝑈)
163		eqid 2769	. . . . . . . . . . . . . . . . . 18 ⊢ (LIdeal‘𝑃) = (LIdeal‘𝑃)
164	131, 22, 163	rspcl 21341	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ Ring ∧ {((𝐸 minPoly 𝐹)‘𝐴)} ⊆ 𝑈) → ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) ∈ (LIdeal‘𝑃))
165	161, 162, 164	syl2anc 595	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) ∈ (LIdeal‘𝑃))
166	22, 131, 146, 153, 158, 160, 151, 165	mxidlirred 33699	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) ∈ (MaxIdeal‘𝑃) ↔ ((𝐸 minPoly 𝐹)‘𝐴) ∈ (Irred‘𝑃)))
167	152, 166	mpbird 260	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) ∈ (MaxIdeal‘𝑃))
168	145, 167	eqeltrd 2869	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑍 ∈ (MaxIdeal‘𝑃))
169		eqid 2769	. . . . . . . . . . . . . . . 16 ⊢ (MaxIdeal‘𝑃) = (MaxIdeal‘𝑃)
170	169, 124	crngmxidl 33696	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ CRing → (MaxIdeal‘𝑃) = (MaxIdeal‘(oppr‘𝑃)))
171	95, 170	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (MaxIdeal‘𝑃) = (MaxIdeal‘(oppr‘𝑃)))
172	168, 171	eleqtrd 2871	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑍 ∈ (MaxIdeal‘(oppr‘𝑃)))
173	124, 26, 129, 168, 172	qsdrngi 33721	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∈ DivRing)
174	91, 54, 96, 123, 173	rndrhmcl 33559	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐿 ↾s ran 𝐽) ∈ DivRing)
175	90, 174	eqeltrd 2869	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿 ↾s ran 𝐺) ∈ DivRing)
176	53, 175	eqeltrrd 2870	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 ↾s ran 𝐺) ∈ DivRing)
177		issdrg 20868	. . . . . . . . 9 ⊢ (ran 𝐺 ∈ (SubDRing‘𝐸) ↔ (𝐸 ∈ DivRing ∧ ran 𝐺 ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s ran 𝐺) ∈ DivRing))
178	45, 48, 176, 177	syl3anbrc 1360	. . . . . . . 8 ⊢ (𝜑 → ran 𝐺 ∈ (SubDRing‘𝐸))
179		fveq2 6882	. . . . . . . . . . . . . 14 ⊢ (𝑝 = (var1‘𝐾) → (𝑂‘𝑝) = (𝑂‘(var1‘𝐾)))
180	179	fveq1d 6884	. . . . . . . . . . . . 13 ⊢ (𝑝 = (var1‘𝐾) → ((𝑂‘𝑝)‘𝐴) = ((𝑂‘(var1‘𝐾))‘𝐴))
181	180	eqeq2d 2780	. . . . . . . . . . . 12 ⊢ (𝑝 = (var1‘𝐾) → (𝐴 = ((𝑂‘𝑝)‘𝐴) ↔ 𝐴 = ((𝑂‘(var1‘𝐾))‘𝐴)))
182	9, 71	eqeltrid 2873	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ DivRing)
183	182	drngringd 20820	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐾 ∈ Ring)
184		eqid 2769	. . . . . . . . . . . . . 14 ⊢ (var1‘𝐾) = (var1‘𝐾)
185	184, 21, 22	vr1cl 22345	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ Ring → (var1‘𝐾) ∈ 𝑈)
186	183, 185	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (var1‘𝐾) ∈ 𝑈)
187	20, 184, 9, 6, 36, 4	evls1var 22466	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑂‘(var1‘𝐾)) = ( I ↾ (Base‘𝐸)))
188	187	fveq1d 6884	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑂‘(var1‘𝐾))‘𝐴) = (( I ↾ (Base‘𝐸))‘𝐴))
189		fvresi 7172	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (Base‘𝐸) → (( I ↾ (Base‘𝐸))‘𝐴) = 𝐴)
190	38, 189	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (( I ↾ (Base‘𝐸))‘𝐴) = 𝐴)
191	188, 190	eqtr2d 2805	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 = ((𝑂‘(var1‘𝐾))‘𝐴))
192	181, 186, 191	rspcedvdw 3593	. . . . . . . . . . 11 ⊢ (𝜑 → ∃𝑝 ∈ 𝑈 𝐴 = ((𝑂‘𝑝)‘𝐴))
193	23, 192, 19	elrnmptd 5954	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ran 𝐺)
194	193	snssd 4757	. . . . . . . . 9 ⊢ (𝜑 → {𝐴} ⊆ ran 𝐺)
195	97, 194	unssd 4153	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ∪ {𝐴}) ⊆ ran 𝐺)
196	6, 45, 178, 195	fldgenssp 33581	. . . . . . 7 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ⊆ ran 𝐺)
197	44, 196	eqssd 3962	. . . . . 6 ⊢ (𝜑 → ran 𝐺 = (𝐸 fldGen (𝐹 ∪ {𝐴})))
198	15, 6	ressbas2 17297	. . . . . . 7 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ⊆ (Base‘𝐸) → (𝐸 fldGen (𝐹 ∪ {𝐴})) = (Base‘𝐿))
199	115, 198	syl 18	. . . . . 6 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) = (Base‘𝐿))
200		eqidd 2770	. . . . . . 7 ⊢ (𝜑 → ((subringAlg ‘𝐿)‘𝐹) = ((subringAlg ‘𝐿)‘𝐹))
201	6, 45, 56	fldgenssid 33576	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 ∪ {𝐴}) ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))
202	201	unssad 4154	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))
203	202, 199	sseqtrd 3981	. . . . . . 7 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐿))
204	200, 203	srabase 21275	. . . . . 6 ⊢ (𝜑 → (Base‘𝐿) = (Base‘((subringAlg ‘𝐿)‘𝐹)))
205	197, 199, 204	3eqtrd 2808	. . . . 5 ⊢ (𝜑 → ran 𝐺 = (Base‘((subringAlg ‘𝐿)‘𝐹)))
206		imaeq2 6059	. . . . . . 7 ⊢ (𝑞 = 𝑝 → (𝐺 “ 𝑞) = (𝐺 “ 𝑝))
207	206	unieqd 4889	. . . . . 6 ⊢ (𝑞 = 𝑝 → ∪ (𝐺 “ 𝑞) = ∪ (𝐺 “ 𝑝))
208	207	cbvmptv 5219	. . . . 5 ⊢ (𝑞 ∈ (Base‘(𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺 “ 𝑞)) = (𝑝 ∈ (Base‘(𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺 “ 𝑝))
209	14, 28, 29, 30, 205, 208	lmhmqusker 33669	. . . 4 ⊢ (𝜑 → (𝑞 ∈ (Base‘(𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺 “ 𝑞)) ∈ ((𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}))) LMIso ((subringAlg ‘𝐿)‘𝐹)))
210		eqidd 2770	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0g‘𝐿) = (0g‘𝐿))
211	200, 210, 203	sralmod0 21286	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0g‘𝐿) = (0g‘((subringAlg ‘𝐿)‘𝐹)))
212	211	sneqd 4606	. . . . . . . . . . . 12 ⊢ (𝜑 → {(0g‘𝐿)} = {(0g‘((subringAlg ‘𝐿)‘𝐹))})
213	212	imaeq2d 6063	. . . . . . . . . . 11 ⊢ (𝜑 → (◡𝐺 “ {(0g‘𝐿)}) = (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}))
214	25, 213	eqtrid 2816	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 = (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}))
215	214	oveq2d 7427	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 ~QG 𝑍) = (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))
216	215	oveq2d 7427	. . . . . . . 8 ⊢ (𝜑 → (𝑃 /s (𝑃 ~QG 𝑍)) = (𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}))))
217	26, 216	eqtrid 2816	. . . . . . 7 ⊢ (𝜑 → 𝑄 = (𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}))))
218	217	fveq2d 6886	. . . . . 6 ⊢ (𝜑 → (Base‘𝑄) = (Base‘(𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))))
219	218	mpteq1d 5205	. . . . 5 ⊢ (𝜑 → (𝑝 ∈ (Base‘𝑄) ↦ ∪ (𝐺 “ 𝑝)) = (𝑝 ∈ (Base‘(𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺 “ 𝑝)))
220	219, 27, 208	3eqtr4g 2829	. . . 4 ⊢ (𝜑 → 𝐽 = (𝑞 ∈ (Base‘(𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺 “ 𝑞)))
221	217	oveq1d 7426	. . . 4 ⊢ (𝜑 → (𝑄 LMIso ((subringAlg ‘𝐿)‘𝐹)) = ((𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}))) LMIso ((subringAlg ‘𝐿)‘𝐹)))
222	209, 220, 221	3eltr4d 2884	. . 3 ⊢ (𝜑 → 𝐽 ∈ (𝑄 LMIso ((subringAlg ‘𝐿)‘𝐹)))
223	9, 15, 16, 17, 18, 1, 19, 20, 21, 22, 23, 24, 25, 26, 27	algextdeglem3 34053	. . 3 ⊢ (𝜑 → 𝑄 ∈ LVec)
224	222, 223	lmimdim 33938	. 2 ⊢ (𝜑 → (dim‘𝑄) = (dim‘((subringAlg ‘𝐿)‘𝐹)))
225	6, 18, 56	fldgenfld 33583	. . . . 5 ⊢ (𝜑 → (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ∈ Field)
226	15, 225	eqeltrid 2873	. . . 4 ⊢ (𝜑 → 𝐿 ∈ Field)
227	9, 15, 16, 17, 18, 1, 19	algextdeglem1 34051	. . . . 5 ⊢ (𝜑 → (𝐿 ↾s 𝐹) = 𝐾)
228	11	oveq2d 7427	. . . . 5 ⊢ (𝜑 → (𝐿 ↾s 𝐹) = (𝐿 ↾s (Base‘𝐾)))
229	227, 228	eqtr3d 2806	. . . 4 ⊢ (𝜑 → 𝐾 = (𝐿 ↾s (Base‘𝐾)))
230	15	subsubrg 20682	. . . . . . 7 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) → (𝐹 ∈ (SubRing‘𝐿) ↔ (𝐹 ∈ (SubRing‘𝐸) ∧ 𝐹 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))))
231	230	biimpar 482	. . . . . 6 ⊢ (((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ (𝐹 ∈ (SubRing‘𝐸) ∧ 𝐹 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))) → 𝐹 ∈ (SubRing‘𝐿))
232	60, 4, 202, 231	syl12anc 849	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐿))
233	11, 232	eqeltrrd 2870	. . . 4 ⊢ (𝜑 → (Base‘𝐾) ∈ (SubRing‘𝐿))
234		brfldext 33979	. . . . 5 ⊢ ((𝐿 ∈ Field ∧ 𝐾 ∈ Field) → (𝐿/FldExt𝐾 ↔ (𝐾 = (𝐿 ↾s (Base‘𝐾)) ∧ (Base‘𝐾) ∈ (SubRing‘𝐿))))
235	234	biimpar 482	. . . 4 ⊢ (((𝐿 ∈ Field ∧ 𝐾 ∈ Field) ∧ (𝐾 = (𝐿 ↾s (Base‘𝐾)) ∧ (Base‘𝐾) ∈ (SubRing‘𝐿))) → 𝐿/FldExt𝐾)
236	226, 156, 229, 233, 235	syl22anc 851	. . 3 ⊢ (𝜑 → 𝐿/FldExt𝐾)
237		extdgval 33987	. . 3 ⊢ (𝐿/FldExt𝐾 → (𝐿[:]𝐾) = (dim‘((subringAlg ‘𝐿)‘(Base‘𝐾))))
238	236, 237	syl 18	. 2 ⊢ (𝜑 → (𝐿[:]𝐾) = (dim‘((subringAlg ‘𝐿)‘(Base‘𝐾))))
239	13, 224, 238	3eqtr4d 2814	1 ⊢ (𝜑 → (dim‘𝑄) = (𝐿[:]𝐾))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149   ≠ wne 2964  ∀wral 3085  {crab 3423  Vcvv 3463   ∪ cun 3911   ⊆ wss 3913  {csn 4594  ∪ cuni 4876   class class class wbr 5113   ↦ cmpt 5196   I cid 5556  ^◡ccnv 5661  dom cdm 5662  ran crn 5663   ↾ cres 5664   “ cima 5665   ∘ ccom 5666  ‘cfv 6537  (class class class)co 7411  [cec 8691   / cqs 8692  Basecbs 17268   ↾_s cress 17289  0_gc0g 17491   /_s cqus 17558  Mndcmnd 18791  SubGrpcsubg 19185  NrmSGrpcnsg 19186   ~_QG cqg 19187   GrpHom cghm 19282  1_rcur 20262  Ringcrg 20314  CRingccrg 20315  opp_rcoppr 20417  Irredcir 20437   RingHom crh 20550  NzRingcnzr 20594  SubRingcsubrg 20653  DivRingcdr 20812  Fieldcfield 20813  SubDRingcsdrg 20866   LMHom clmhm 21117   LMIso clmim 21118  LVecclvec 21200  subringAlg csra 21269  LIdealclidl 21307  RSpancrsp 21308  PIDcpid 21472  var₁cv1 22304  Poly₁cpl1 22305   evalSub₁ ces1 22441  deg₁cdg1 26179  idlGen_1pcig1p 26255   fldGen cfldgen 33573  MaxIdealcmxidl 33686  dimcldim 33933  /_FldExtcfldext 33972  [:]cextdg 33974   IntgRing cirng 34017   minPoly cminply 34033

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5242  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-reg 9553  ax-inf2 9609  ax-ac2 10446  ax-cnex 11155  ax-resscn 11156  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-mulcom 11163  ax-addass 11164  ax-mulass 11165  ax-distr 11166  ax-i2m1 11167  ax-1ne0 11168  ax-1rid 11169  ax-rnegex 11170  ax-rrecex 11171  ax-cnre 11172  ax-pre-lttri 11173  ax-pre-lttrn 11174  ax-pre-ltadd 11175  ax-pre-mulgt0 11176  ax-pre-sup 11177  ax-addf 11178

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-tp 4599  df-op 4601  df-uni 4877  df-int 4917  df-iun 4962  df-iin 4963  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-se 5616  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7675  df-ofr 7676  df-rpss 7721  df-om 7862  df-1st 7985  df-2nd 7986  df-supp 8156  df-tpos 8221  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-1o 8452  df-2o 8453  df-oadd 8456  df-er 8693  df-ec 8695  df-qs 8699  df-map 8825  df-pm 8826  df-ixp 8895  df-en 8943  df-dom 8944  df-sdom 8945  df-fin 8946  df-fsupp 9321  df-sup 9401  df-inf 9402  df-oi 9471  df-r1 9735  df-rank 9736  df-dju 9886  df-card 9924  df-acn 9927  df-ac 10099  df-pnf 11244  df-mnf 11245  df-xr 11246  df-ltxr 11247  df-le 11248  df-sub 11442  df-neg 11443  df-nn 12233  df-2 12302  df-3 12303  df-4 12304  df-5 12305  df-6 12306  df-7 12307  df-8 12308  df-9 12309  df-n0 12504  df-xnn0 12577  df-z 12591  df-dec 12711  df-uz 12862  df-fz 13535  df-fzo 13682  df-seq 14037  df-hash 14366  df-struct 17206  df-sets 17223  df-slot 17241  df-ndx 17253  df-base 17269  df-ress 17290  df-plusg 17322  df-mulr 17323  df-starv 17324  df-sca 17325  df-vsca 17326  df-ip 17327  df-tset 17328  df-ple 17329  df-ocomp 17330  df-ds 17331  df-unif 17332  df-hom 17333  df-cco 17334  df-0g 17493  df-gsum 17494  df-prds 17499  df-pws 17501  df-imas 17561  df-qus 17562  df-mre 17637  df-mrc 17638  df-mri 17639  df-acs 17640  df-proset 18349  df-drs 18350  df-poset 18368  df-ipo 18583  df-mgm 18697  df-sgrp 18776  df-mnd 18792  df-mhm 18840  df-submnd 18841  df-grp 19002  df-minusg 19003  df-sbg 19004  df-mulg 19133  df-subg 19188  df-nsg 19189  df-eqg 19190  df-ghm 19283  df-gim 19328  df-cntz 19386  df-oppg 19415  df-lsm 19705  df-cmn 19851  df-abl 19852  df-mgp 20216  df-rng 20230  df-ur 20263  df-srg 20268  df-ring 20316  df-cring 20317  df-oppr 20418  df-dvdsr 20438  df-unit 20439  df-irred 20440  df-invr 20469  df-dvr 20482  df-rhm 20553  df-nzr 20595  df-subrng 20630  df-subrg 20654  df-rlreg 20778  df-domn 20779  df-idom 20780  df-drng 20814  df-field 20815  df-sdrg 20867  df-lmod 20960  df-lss 21030  df-lsp 21070  df-lmhm 21120  df-lmim 21121  df-lbs 21173  df-lvec 21201  df-sra 21271  df-rgmod 21272  df-lidl 21309  df-rsp 21310  df-2idl 21359  df-lpidl 21458  df-lpir 21459  df-pid 21473  df-cnfld 21491  df-dsmm 21850  df-frlm 21865  df-uvc 21901  df-lindf 21924  df-linds 21925  df-assa 21971  df-asp 21972  df-ascl 21973  df-psr 22027  df-mvr 22028  df-mpl 22029  df-opsr 22031  df-evls 22193  df-evl 22194  df-psr1 22308  df-vr1 22309  df-ply1 22310  df-coe1 22311  df-evls1 22443  df-evl1 22444  df-mdeg 26180  df-deg1 26181  df-mon1 26256  df-uc1p 26257  df-q1p 26258  df-r1p 26259  df-ig1p 26260  df-fldgen 33574  df-mxidl 33687  df-dim 33934  df-fldext 33975  df-extdg 33976  df-irng 34018  df-minply 34034

This theorem is referenced by:  algextdeg  34059