Theorem algextdeglem4 33759

Description: Lemma for algextdeg 33764. By lmhmqusker 33437, the surjective module homomorphism 𝐺 described in algextdeglem2 33757 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 20753	. . . . . . . 8 ⊢ (𝐹 ∈ (SubDRing‘𝐸) ↔ (𝐸 ∈ DivRing ∧ 𝐹 ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s 𝐹) ∈ DivRing))
3	1, 2	sylib 218	. . . . . . 7 ⊢ (𝜑 → (𝐸 ∈ DivRing ∧ 𝐹 ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s 𝐹) ∈ DivRing))
4	3	simp2d 1143	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸))
5		subrgsubg 20542	. . . . . 6 ⊢ (𝐹 ∈ (SubRing‘𝐸) → 𝐹 ∈ (SubGrp‘𝐸))
6		eqid 2736	. . . . . . 7 ⊢ (Base‘𝐸) = (Base‘𝐸)
7	6	subgss 19115	. . . . . 6 ⊢ (𝐹 ∈ (SubGrp‘𝐸) → 𝐹 ⊆ (Base‘𝐸))
8	4, 5, 7	3syl 18	. . . . 5 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐸))
9		algextdeg.k	. . . . . 6 ⊢ 𝐾 = (𝐸 ↾s 𝐹)
10	9, 6	ressbas2 17264	. . . . 5 ⊢ (𝐹 ⊆ (Base‘𝐸) → 𝐹 = (Base‘𝐾))
11	8, 10	syl 17	. . . 4 ⊢ (𝜑 → 𝐹 = (Base‘𝐾))
12	11	fveq2d 6885	. . 3 ⊢ (𝜑 → ((subringAlg ‘𝐿)‘𝐹) = ((subringAlg ‘𝐿)‘(Base‘𝐾)))
13	12	fveq2d 6885	. 2 ⊢ (𝜑 → (dim‘((subringAlg ‘𝐿)‘𝐹)) = (dim‘((subringAlg ‘𝐿)‘(Base‘𝐾))))
14		eqid 2736	. . . . 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 33757	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ (𝑃 LMHom ((subringAlg ‘𝐿)‘𝐹)))
29		eqid 2736	. . . . 5 ⊢ (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}) = (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})
30		eqid 2736	. . . . 5 ⊢ (𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}))) = (𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))
31	9	fveq2i 6884	. . . . . . . . . . 11 ⊢ (Poly1‘𝐾) = (Poly1‘(𝐸 ↾s 𝐹))
32	21, 31	eqtri 2759	. . . . . . . . . 10 ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))
33	18	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝐸 ∈ Field)
34	1	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝐹 ∈ (SubDRing‘𝐸))
35		eqid 2736	. . . . . . . . . . . . 13 ⊢ (0g‘𝐸) = (0g‘𝐸)
36	18	fldcrngd 20707	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸 ∈ CRing)
37	20, 9, 6, 35, 36, 4	irngssv 33734	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸 IntgRing 𝐹) ⊆ (Base‘𝐸))
38	37, 19	sseldd 3964	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ (Base‘𝐸))
39	38	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝐴 ∈ (Base‘𝐸))
40		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝑝 ∈ 𝑈)
41	6, 20, 32, 22, 33, 34, 39, 40	evls1fldgencl 33716	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → ((𝑂‘𝑝)‘𝐴) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})))
42	41	ralrimiva 3133	. . . . . . . 8 ⊢ (𝜑 → ∀𝑝 ∈ 𝑈 ((𝑂‘𝑝)‘𝐴) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})))
43	23	rnmptss 7118	. . . . . . . 8 ⊢ (∀𝑝 ∈ 𝑈 ((𝑂‘𝑝)‘𝐴) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})) → ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))
44	42, 43	syl 17	. . . . . . 7 ⊢ (𝜑 → ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))
45	18	flddrngd 20706	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ DivRing)
46	20, 32, 6, 22, 36, 4, 38, 23	evls1maprhm 22319	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ (𝑃 RingHom 𝐸))
47		rnrhmsubrg 20570	. . . . . . . . . 10 ⊢ (𝐺 ∈ (𝑃 RingHom 𝐸) → ran 𝐺 ∈ (SubRing‘𝐸))
48	46, 47	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐺 ∈ (SubRing‘𝐸))
49	15	oveq1i 7420	. . . . . . . . . . 11 ⊢ (𝐿 ↾s ran 𝐺) = ((𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ↾s ran 𝐺)
50		ovex 7443	. . . . . . . . . . . 12 ⊢ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ V
51		ressabs 17274	. . . . . . . . . . . 12 ⊢ (((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ V ∧ ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴}))) → ((𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ↾s ran 𝐺) = (𝐸 ↾s ran 𝐺))
52	50, 44, 51	sylancr 587	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ↾s ran 𝐺) = (𝐸 ↾s ran 𝐺))
53	49, 52	eqtrid 2783	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿 ↾s ran 𝐺) = (𝐸 ↾s ran 𝐺))
54		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ (0g‘𝐿) = (0g‘𝐿)
55	38	snssd 4790	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → {𝐴} ⊆ (Base‘𝐸))
56	8, 55	unssd 4172	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐹 ∪ {𝐴}) ⊆ (Base‘𝐸))
57	6, 45, 56	fldgensdrg 33313	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubDRing‘𝐸))
58		issdrg 20753	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubDRing‘𝐸) ↔ (𝐸 ∈ DivRing ∧ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ∈ DivRing))
59	57, 58	sylib 218	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 ∈ DivRing ∧ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ∈ DivRing))
60	59	simp2d 1143	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸))
61	15	resrhm2b 20567	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴}))) → (𝐺 ∈ (𝑃 RingHom 𝐸) ↔ 𝐺 ∈ (𝑃 RingHom 𝐿)))
62	61	biimpa 476	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴}))) ∧ 𝐺 ∈ (𝑃 RingHom 𝐸)) → 𝐺 ∈ (𝑃 RingHom 𝐿))
63	60, 44, 46, 62	syl21anc 837	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐺 ∈ (𝑃 RingHom 𝐿))
64		rhmghm 20449	. . . . . . . . . . . . . . . 16 ⊢ (𝐺 ∈ (𝑃 RingHom 𝐿) → 𝐺 ∈ (𝑃 GrpHom 𝐿))
65	63, 64	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺 ∈ (𝑃 GrpHom 𝐿))
66	54, 65, 25, 26, 27, 22, 24	ghmquskerco 19272	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺 = (𝐽 ∘ 𝑁))
67	66	rneqd 5923	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝐺 = ran (𝐽 ∘ 𝑁))
68	26	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑄 = (𝑃 /s (𝑃 ~QG 𝑍)))
69	22	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑈 = (Base‘𝑃))
70		ovexd 7445	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃 ~QG 𝑍) ∈ V)
71	3	simp3d 1144	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ DivRing)
72	32, 71	ply1lvec 33577	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ LVec)
73	68, 69, 70, 72	qusbas 17564	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 / (𝑃 ~QG 𝑍)) = (Base‘𝑄))
74		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 / (𝑃 ~QG 𝑍)) = (𝑈 / (𝑃 ~QG 𝑍))
75	54	ghmker 19230	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 ∈ (𝑃 GrpHom 𝐿) → (◡𝐺 “ {(0g‘𝐿)}) ∈ (NrmSGrp‘𝑃))
76	65, 75	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (◡𝐺 “ {(0g‘𝐿)}) ∈ (NrmSGrp‘𝑃))
77	25, 76	eqeltrid 2839	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑍 ∈ (NrmSGrp‘𝑃))
78	22, 74, 24, 77	qusrn 33429	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ran 𝑁 = (𝑈 / (𝑃 ~QG 𝑍)))
79		eqid 2736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((subringAlg ‘𝐸)‘𝐹) = ((subringAlg ‘𝐸)‘𝐹)
80	20, 32, 6, 22, 36, 4, 38, 23, 79	evls1maplmhm 22320	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐺 ∈ (𝑃 LMHom ((subringAlg ‘𝐸)‘𝐹)))
81	80	elexd 3488	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐺 ∈ V)
82	81	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘𝑄)) → 𝐺 ∈ V)
83	82	imaexd 7917	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘𝑄)) → (𝐺 “ 𝑝) ∈ V)
84	83	uniexd 7741	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘𝑄)) → ∪ (𝐺 “ 𝑝) ∈ V)
85	27, 84	dmmptd 6688	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom 𝐽 = (Base‘𝑄))
86	73, 78, 85	3eqtr4rd 2782	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom 𝐽 = ran 𝑁)
87		rncoeq 5964	. . . . . . . . . . . . . 14 ⊢ (dom 𝐽 = ran 𝑁 → ran (𝐽 ∘ 𝑁) = ran 𝐽)
88	86, 87	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran (𝐽 ∘ 𝑁) = ran 𝐽)
89	67, 88	eqtrd 2771	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝐺 = ran 𝐽)
90	89	oveq2d 7426	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐿 ↾s ran 𝐺) = (𝐿 ↾s ran 𝐽))
91		eqid 2736	. . . . . . . . . . . 12 ⊢ (𝐿 ↾s ran 𝐽) = (𝐿 ↾s ran 𝐽)
92	9	subrgcrng 20540	. . . . . . . . . . . . . . 15 ⊢ ((𝐸 ∈ CRing ∧ 𝐹 ∈ (SubRing‘𝐸)) → 𝐾 ∈ CRing)
93	36, 4, 92	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ CRing)
94	21	ply1crng 22139	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ CRing → 𝑃 ∈ CRing)
95	93, 94	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ CRing)
96	54, 63, 25, 26, 27, 95	rhmquskerlem 33445	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ (𝑄 RingHom 𝐿))
97	20, 32, 6, 22, 36, 4, 38, 23	evls1maprnss 22321	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 ⊆ ran 𝐺)
98		eqid 2736	. . . . . . . . . . . . . . . . . 18 ⊢ (1r‘𝐸) = (1r‘𝐸)
99	9, 98	subrg1 20547	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (SubRing‘𝐸) → (1r‘𝐸) = (1r‘𝐾))
100	4, 99	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1r‘𝐸) = (1r‘𝐾))
101	98	subrg1cl 20545	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (SubRing‘𝐸) → (1r‘𝐸) ∈ 𝐹)
102	4, 101	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1r‘𝐸) ∈ 𝐹)
103	100, 102	eqeltrrd 2836	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1r‘𝐾) ∈ 𝐹)
104	97, 103	sseldd 3964	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1r‘𝐾) ∈ ran 𝐺)
105		drngnzr 20713	. . . . . . . . . . . . . . . . 17 ⊢ (𝐸 ∈ DivRing → 𝐸 ∈ NzRing)
106	98, 35	nzrnz 20480	. . . . . . . . . . . . . . . . 17 ⊢ (𝐸 ∈ NzRing → (1r‘𝐸) ≠ (0g‘𝐸))
107	45, 105, 106	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1r‘𝐸) ≠ (0g‘𝐸))
108	36	crnggrpd 20212	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐸 ∈ Grp)
109	108	grpmndd 18934	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐸 ∈ Mnd)
110		sdrgsubrg 20756	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubDRing‘𝐸) → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸))
111		subrgsubg 20542	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubGrp‘𝐸))
112	57, 110, 111	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubGrp‘𝐸))
113	35	subg0cl 19122	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubGrp‘𝐸) → (0g‘𝐸) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})))
114	112, 113	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0g‘𝐸) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})))
115	6, 45, 56	fldgenssv 33314	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ⊆ (Base‘𝐸))
116	15, 6, 35	ress0g 18745	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐸 ∈ Mnd ∧ (0g‘𝐸) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∧ (𝐸 fldGen (𝐹 ∪ {𝐴})) ⊆ (Base‘𝐸)) → (0g‘𝐸) = (0g‘𝐿))
117	109, 114, 115, 116	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐿))
118	107, 100, 117	3netr3d 3009	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1r‘𝐾) ≠ (0g‘𝐿))
119		nelsn 4647	. . . . . . . . . . . . . . 15 ⊢ ((1r‘𝐾) ≠ (0g‘𝐿) → ¬ (1r‘𝐾) ∈ {(0g‘𝐿)})
120	118, 119	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ¬ (1r‘𝐾) ∈ {(0g‘𝐿)})
121		nelne1 3030	. . . . . . . . . . . . . 14 ⊢ (((1r‘𝐾) ∈ ran 𝐺 ∧ ¬ (1r‘𝐾) ∈ {(0g‘𝐿)}) → ran 𝐺 ≠ {(0g‘𝐿)})
122	104, 120, 121	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝐺 ≠ {(0g‘𝐿)})
123	89, 122	eqnetrrd 3001	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝐽 ≠ {(0g‘𝐿)})
124		eqid 2736	. . . . . . . . . . . . 13 ⊢ (oppr‘𝑃) = (oppr‘𝑃)
125	9	sdrgdrng 20755	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐾 ∈ DivRing)
126		drngnzr 20713	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ DivRing → 𝐾 ∈ NzRing)
127	1, 125, 126	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ NzRing)
128	21	ply1nz 26084	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ NzRing → 𝑃 ∈ NzRing)
129	127, 128	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ NzRing)
130		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)} = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)}
131		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (RSpan‘𝑃) = (RSpan‘𝑃)
132	9	fveq2i 6884	. . . . . . . . . . . . . . . 16 ⊢ (idlGen1p‘𝐾) = (idlGen1p‘(𝐸 ↾s 𝐹))
133	20, 32, 6, 18, 1, 38, 35, 130, 131, 132	ply1annig1p 33743	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)} = ((RSpan‘𝑃)‘{((idlGen1p‘𝐾)‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)})}))
134	117	sneqd 4618	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → {(0g‘𝐸)} = {(0g‘𝐿)})
135	134	imaeq2d 6052	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (◡𝐺 “ {(0g‘𝐸)}) = (◡𝐺 “ {(0g‘𝐿)}))
136	25, 135	eqtr4id 2790	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑍 = (◡𝐺 “ {(0g‘𝐸)}))
137	22	mpteq1i 5216	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴)) = (𝑝 ∈ (Base‘𝑃) ↦ ((𝑂‘𝑝)‘𝐴))
138	23, 137	eqtri 2759	. . . . . . . . . . . . . . . . 17 ⊢ 𝐺 = (𝑝 ∈ (Base‘𝑃) ↦ ((𝑂‘𝑝)‘𝐴))
139	20, 32, 6, 36, 4, 38, 35, 130, 138	ply1annidllem 33740	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)} = (◡𝐺 “ {(0g‘𝐸)}))
140	136, 139	eqtr4d 2774	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑍 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)})
141		eqid 2736	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐸 minPoly 𝐹) = (𝐸 minPoly 𝐹)
142	20, 32, 6, 18, 1, 38, 35, 130, 131, 132, 141	minplyval 33744	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) = ((idlGen1p‘𝐾)‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)}))
143	142	sneqd 4618	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {((𝐸 minPoly 𝐹)‘𝐴)} = {((idlGen1p‘𝐾)‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)})})
144	143	fveq2d 6885	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) = ((RSpan‘𝑃)‘{((idlGen1p‘𝐾)‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)})}))
145	133, 140, 144	3eqtr4d 2781	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑍 = ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}))
146		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (0g‘𝑃) = (0g‘𝑃)
147		eqid 2736	. . . . . . . . . . . . . . . . . 18 ⊢ (0g‘(Poly1‘𝐸)) = (0g‘(Poly1‘𝐸))
148	147, 18, 1, 141, 19	irngnminplynz 33751	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ≠ (0g‘(Poly1‘𝐸)))
149		eqid 2736	. . . . . . . . . . . . . . . . . 18 ⊢ (Poly1‘𝐸) = (Poly1‘𝐸)
150	149, 9, 21, 22, 4, 147	ressply10g 33585	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0g‘(Poly1‘𝐸)) = (0g‘𝑃))
151	148, 150	neeqtrd 3002	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ≠ (0g‘𝑃))
152	20, 32, 6, 18, 1, 38, 141, 146, 151	minplyirred 33750	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ∈ (Irred‘𝑃))
153		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) = ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)})
154		fldsdrgfld 20763	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ (SubDRing‘𝐸)) → (𝐸 ↾s 𝐹) ∈ Field)
155	18, 1, 154	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ Field)
156	9, 155	eqeltrid 2839	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 ∈ Field)
157	21	ply1pid 26145	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ Field → 𝑃 ∈ PID)
158	156, 157	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ PID)
159	20, 32, 6, 18, 1, 38, 35, 130, 131, 132, 141	minplycl 33745	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ∈ (Base‘𝑃))
160	159, 22	eleqtrrdi 2846	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ∈ 𝑈)
161	95	crngringd 20211	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ Ring)
162	160	snssd 4790	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → {((𝐸 minPoly 𝐹)‘𝐴)} ⊆ 𝑈)
163		eqid 2736	. . . . . . . . . . . . . . . . . 18 ⊢ (LIdeal‘𝑃) = (LIdeal‘𝑃)
164	131, 22, 163	rspcl 21201	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ Ring ∧ {((𝐸 minPoly 𝐹)‘𝐴)} ⊆ 𝑈) → ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) ∈ (LIdeal‘𝑃))
165	161, 162, 164	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) ∈ (LIdeal‘𝑃))
166	22, 131, 146, 153, 158, 160, 151, 165	mxidlirred 33492	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) ∈ (MaxIdeal‘𝑃) ↔ ((𝐸 minPoly 𝐹)‘𝐴) ∈ (Irred‘𝑃)))
167	152, 166	mpbird 257	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) ∈ (MaxIdeal‘𝑃))
168	145, 167	eqeltrd 2835	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑍 ∈ (MaxIdeal‘𝑃))
169		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (MaxIdeal‘𝑃) = (MaxIdeal‘𝑃)
170	169, 124	crngmxidl 33489	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ CRing → (MaxIdeal‘𝑃) = (MaxIdeal‘(oppr‘𝑃)))
171	95, 170	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (MaxIdeal‘𝑃) = (MaxIdeal‘(oppr‘𝑃)))
172	168, 171	eleqtrd 2837	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑍 ∈ (MaxIdeal‘(oppr‘𝑃)))
173	124, 26, 129, 168, 172	qsdrngi 33515	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∈ DivRing)
174	91, 54, 96, 123, 173	rndrhmcl 33295	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐿 ↾s ran 𝐽) ∈ DivRing)
175	90, 174	eqeltrd 2835	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿 ↾s ran 𝐺) ∈ DivRing)
176	53, 175	eqeltrrd 2836	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 ↾s ran 𝐺) ∈ DivRing)
177		issdrg 20753	. . . . . . . . 9 ⊢ (ran 𝐺 ∈ (SubDRing‘𝐸) ↔ (𝐸 ∈ DivRing ∧ ran 𝐺 ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s ran 𝐺) ∈ DivRing))
178	45, 48, 176, 177	syl3anbrc 1344	. . . . . . . 8 ⊢ (𝜑 → ran 𝐺 ∈ (SubDRing‘𝐸))
179		fveq2 6881	. . . . . . . . . . . . . 14 ⊢ (𝑝 = (var1‘𝐾) → (𝑂‘𝑝) = (𝑂‘(var1‘𝐾)))
180	179	fveq1d 6883	. . . . . . . . . . . . 13 ⊢ (𝑝 = (var1‘𝐾) → ((𝑂‘𝑝)‘𝐴) = ((𝑂‘(var1‘𝐾))‘𝐴))
181	180	eqeq2d 2747	. . . . . . . . . . . 12 ⊢ (𝑝 = (var1‘𝐾) → (𝐴 = ((𝑂‘𝑝)‘𝐴) ↔ 𝐴 = ((𝑂‘(var1‘𝐾))‘𝐴)))
182	9, 71	eqeltrid 2839	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ DivRing)
183	182	drngringd 20702	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐾 ∈ Ring)
184		eqid 2736	. . . . . . . . . . . . . 14 ⊢ (var1‘𝐾) = (var1‘𝐾)
185	184, 21, 22	vr1cl 22158	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ Ring → (var1‘𝐾) ∈ 𝑈)
186	183, 185	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (var1‘𝐾) ∈ 𝑈)
187	20, 184, 9, 6, 36, 4	evls1var 22281	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑂‘(var1‘𝐾)) = ( I ↾ (Base‘𝐸)))
188	187	fveq1d 6883	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑂‘(var1‘𝐾))‘𝐴) = (( I ↾ (Base‘𝐸))‘𝐴))
189		fvresi 7170	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (Base‘𝐸) → (( I ↾ (Base‘𝐸))‘𝐴) = 𝐴)
190	38, 189	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (( I ↾ (Base‘𝐸))‘𝐴) = 𝐴)
191	188, 190	eqtr2d 2772	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 = ((𝑂‘(var1‘𝐾))‘𝐴))
192	181, 186, 191	rspcedvdw 3609	. . . . . . . . . . 11 ⊢ (𝜑 → ∃𝑝 ∈ 𝑈 𝐴 = ((𝑂‘𝑝)‘𝐴))
193	23, 192, 19	elrnmptd 5948	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ran 𝐺)
194	193	snssd 4790	. . . . . . . . 9 ⊢ (𝜑 → {𝐴} ⊆ ran 𝐺)
195	97, 194	unssd 4172	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ∪ {𝐴}) ⊆ ran 𝐺)
196	6, 45, 178, 195	fldgenssp 33317	. . . . . . 7 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ⊆ ran 𝐺)
197	44, 196	eqssd 3981	. . . . . 6 ⊢ (𝜑 → ran 𝐺 = (𝐸 fldGen (𝐹 ∪ {𝐴})))
198	15, 6	ressbas2 17264	. . . . . . 7 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ⊆ (Base‘𝐸) → (𝐸 fldGen (𝐹 ∪ {𝐴})) = (Base‘𝐿))
199	115, 198	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) = (Base‘𝐿))
200		eqidd 2737	. . . . . . 7 ⊢ (𝜑 → ((subringAlg ‘𝐿)‘𝐹) = ((subringAlg ‘𝐿)‘𝐹))
201	6, 45, 56	fldgenssid 33312	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 ∪ {𝐴}) ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))
202	201	unssad 4173	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))
203	202, 199	sseqtrd 4000	. . . . . . 7 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐿))
204	200, 203	srabase 21140	. . . . . 6 ⊢ (𝜑 → (Base‘𝐿) = (Base‘((subringAlg ‘𝐿)‘𝐹)))
205	197, 199, 204	3eqtrd 2775	. . . . 5 ⊢ (𝜑 → ran 𝐺 = (Base‘((subringAlg ‘𝐿)‘𝐹)))
206		imaeq2 6048	. . . . . . 7 ⊢ (𝑞 = 𝑝 → (𝐺 “ 𝑞) = (𝐺 “ 𝑝))
207	206	unieqd 4901	. . . . . 6 ⊢ (𝑞 = 𝑝 → ∪ (𝐺 “ 𝑞) = ∪ (𝐺 “ 𝑝))
208	207	cbvmptv 5230	. . . . 5 ⊢ (𝑞 ∈ (Base‘(𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺 “ 𝑞)) = (𝑝 ∈ (Base‘(𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺 “ 𝑝))
209	14, 28, 29, 30, 205, 208	lmhmqusker 33437	. . . 4 ⊢ (𝜑 → (𝑞 ∈ (Base‘(𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺 “ 𝑞)) ∈ ((𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}))) LMIso ((subringAlg ‘𝐿)‘𝐹)))
210		eqidd 2737	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0g‘𝐿) = (0g‘𝐿))
211	200, 210, 203	sralmod0 21151	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0g‘𝐿) = (0g‘((subringAlg ‘𝐿)‘𝐹)))
212	211	sneqd 4618	. . . . . . . . . . . 12 ⊢ (𝜑 → {(0g‘𝐿)} = {(0g‘((subringAlg ‘𝐿)‘𝐹))})
213	212	imaeq2d 6052	. . . . . . . . . . 11 ⊢ (𝜑 → (◡𝐺 “ {(0g‘𝐿)}) = (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}))
214	25, 213	eqtrid 2783	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 = (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}))
215	214	oveq2d 7426	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 ~QG 𝑍) = (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))
216	215	oveq2d 7426	. . . . . . . 8 ⊢ (𝜑 → (𝑃 /s (𝑃 ~QG 𝑍)) = (𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}))))
217	26, 216	eqtrid 2783	. . . . . . 7 ⊢ (𝜑 → 𝑄 = (𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}))))
218	217	fveq2d 6885	. . . . . 6 ⊢ (𝜑 → (Base‘𝑄) = (Base‘(𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))))
219	218	mpteq1d 5215	. . . . 5 ⊢ (𝜑 → (𝑝 ∈ (Base‘𝑄) ↦ ∪ (𝐺 “ 𝑝)) = (𝑝 ∈ (Base‘(𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺 “ 𝑝)))
220	219, 27, 208	3eqtr4g 2796	. . . 4 ⊢ (𝜑 → 𝐽 = (𝑞 ∈ (Base‘(𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺 “ 𝑞)))
221	217	oveq1d 7425	. . . 4 ⊢ (𝜑 → (𝑄 LMIso ((subringAlg ‘𝐿)‘𝐹)) = ((𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}))) LMIso ((subringAlg ‘𝐿)‘𝐹)))
222	209, 220, 221	3eltr4d 2850	. . 3 ⊢ (𝜑 → 𝐽 ∈ (𝑄 LMIso ((subringAlg ‘𝐿)‘𝐹)))
223	9, 15, 16, 17, 18, 1, 19, 20, 21, 22, 23, 24, 25, 26, 27	algextdeglem3 33758	. . 3 ⊢ (𝜑 → 𝑄 ∈ LVec)
224	222, 223	lmimdim 33648	. 2 ⊢ (𝜑 → (dim‘𝑄) = (dim‘((subringAlg ‘𝐿)‘𝐹)))
225	6, 18, 56	fldgenfld 33319	. . . . 5 ⊢ (𝜑 → (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ∈ Field)
226	15, 225	eqeltrid 2839	. . . 4 ⊢ (𝜑 → 𝐿 ∈ Field)
227	9, 15, 16, 17, 18, 1, 19	algextdeglem1 33756	. . . . 5 ⊢ (𝜑 → (𝐿 ↾s 𝐹) = 𝐾)
228	11	oveq2d 7426	. . . . 5 ⊢ (𝜑 → (𝐿 ↾s 𝐹) = (𝐿 ↾s (Base‘𝐾)))
229	227, 228	eqtr3d 2773	. . . 4 ⊢ (𝜑 → 𝐾 = (𝐿 ↾s (Base‘𝐾)))
230	15	subsubrg 20563	. . . . . . 7 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) → (𝐹 ∈ (SubRing‘𝐿) ↔ (𝐹 ∈ (SubRing‘𝐸) ∧ 𝐹 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))))
231	230	biimpar 477	. . . . . 6 ⊢ (((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ (𝐹 ∈ (SubRing‘𝐸) ∧ 𝐹 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))) → 𝐹 ∈ (SubRing‘𝐿))
232	60, 4, 202, 231	syl12anc 836	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐿))
233	11, 232	eqeltrrd 2836	. . . 4 ⊢ (𝜑 → (Base‘𝐾) ∈ (SubRing‘𝐿))
234		brfldext 33692	. . . . 5 ⊢ ((𝐿 ∈ Field ∧ 𝐾 ∈ Field) → (𝐿/FldExt𝐾 ↔ (𝐾 = (𝐿 ↾s (Base‘𝐾)) ∧ (Base‘𝐾) ∈ (SubRing‘𝐿))))
235	234	biimpar 477	. . . 4 ⊢ (((𝐿 ∈ Field ∧ 𝐾 ∈ Field) ∧ (𝐾 = (𝐿 ↾s (Base‘𝐾)) ∧ (Base‘𝐾) ∈ (SubRing‘𝐿))) → 𝐿/FldExt𝐾)
236	226, 156, 229, 233, 235	syl22anc 838	. . 3 ⊢ (𝜑 → 𝐿/FldExt𝐾)
237		extdgval 33700	. . 3 ⊢ (𝐿/FldExt𝐾 → (𝐿[:]𝐾) = (dim‘((subringAlg ‘𝐿)‘(Base‘𝐾))))
238	236, 237	syl 17	. 2 ⊢ (𝜑 → (𝐿[:]𝐾) = (dim‘((subringAlg ‘𝐿)‘(Base‘𝐾))))
239	13, 224, 238	3eqtr4d 2781	1 ⊢ (𝜑 → (dim‘𝑄) = (𝐿[:]𝐾))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ≠ wne 2933  ∀wral 3052  {crab 3420  Vcvv 3464   ∪ cun 3929   ⊆ wss 3931  {csn 4606  ∪ cuni 4888   class class class wbr 5124   ↦ cmpt 5206   I cid 5552  ^◡ccnv 5658  dom cdm 5659  ran crn 5660   ↾ cres 5661   “ cima 5662   ∘ ccom 5663  ‘cfv 6536  (class class class)co 7410  [cec 8722   / cqs 8723  Basecbs 17233   ↾_s cress 17256  0_gc0g 17458   /_s cqus 17524  Mndcmnd 18717  SubGrpcsubg 19108  NrmSGrpcnsg 19109   ~_QG cqg 19110   GrpHom cghm 19200  1_rcur 20146  Ringcrg 20198  CRingccrg 20199  opp_rcoppr 20301  Irredcir 20321   RingHom crh 20434  NzRingcnzr 20477  SubRingcsubrg 20534  DivRingcdr 20694  Fieldcfield 20695  SubDRingcsdrg 20751   LMHom clmhm 20982   LMIso clmim 20983  LVecclvec 21065  subringAlg csra 21134  LIdealclidl 21172  RSpancrsp 21173  PIDcpid 21302  var₁cv1 22116  Poly₁cpl1 22117   evalSub₁ ces1 22256  deg₁cdg1 26016  idlGen_1pcig1p 26092   fldGen cfldgen 33309  MaxIdealcmxidl 33479  dimcldim 33643  /_FldExtcfldext 33683  [:]cextdg 33686   IntgRing cirng 33729   minPoly cminply 33738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-rep 5254  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-reg 9611  ax-inf2 9660  ax-ac2 10482  ax-cnex 11190  ax-resscn 11191  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-mulcom 11198  ax-addass 11199  ax-mulass 11200  ax-distr 11201  ax-i2m1 11202  ax-1ne0 11203  ax-1rid 11204  ax-rnegex 11205  ax-rrecex 11206  ax-cnre 11207  ax-pre-lttri 11208  ax-pre-lttrn 11209  ax-pre-ltadd 11210  ax-pre-mulgt0 11211  ax-pre-sup 11212  ax-addf 11213

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rmo 3364  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-tp 4611  df-op 4613  df-uni 4889  df-int 4928  df-iun 4974  df-iin 4975  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-se 5612  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-isom 6545  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-of 7676  df-ofr 7677  df-rpss 7722  df-om 7867  df-1st 7993  df-2nd 7994  df-supp 8165  df-tpos 8230  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-1o 8485  df-2o 8486  df-oadd 8489  df-er 8724  df-ec 8726  df-qs 8730  df-map 8847  df-pm 8848  df-ixp 8917  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-fsupp 9379  df-sup 9459  df-inf 9460  df-oi 9529  df-r1 9783  df-rank 9784  df-dju 9920  df-card 9958  df-acn 9961  df-ac 10135  df-pnf 11276  df-mnf 11277  df-xr 11278  df-ltxr 11279  df-le 11280  df-sub 11473  df-neg 11474  df-nn 12246  df-2 12308  df-3 12309  df-4 12310  df-5 12311  df-6 12312  df-7 12313  df-8 12314  df-9 12315  df-n0 12507  df-xnn0 12580  df-z 12594  df-dec 12714  df-uz 12858  df-fz 13530  df-fzo 13677  df-seq 14025  df-hash 14354  df-struct 17171  df-sets 17188  df-slot 17206  df-ndx 17218  df-base 17234  df-ress 17257  df-plusg 17289  df-mulr 17290  df-starv 17291  df-sca 17292  df-vsca 17293  df-ip 17294  df-tset 17295  df-ple 17296  df-ocomp 17297  df-ds 17298  df-unif 17299  df-hom 17300  df-cco 17301  df-0g 17460  df-gsum 17461  df-prds 17466  df-pws 17468  df-imas 17527  df-qus 17528  df-mre 17603  df-mrc 17604  df-mri 17605  df-acs 17606  df-proset 18311  df-drs 18312  df-poset 18330  df-ipo 18543  df-mgm 18623  df-sgrp 18702  df-mnd 18718  df-mhm 18766  df-submnd 18767  df-grp 18924  df-minusg 18925  df-sbg 18926  df-mulg 19056  df-subg 19111  df-nsg 19112  df-eqg 19113  df-ghm 19201  df-gim 19247  df-cntz 19305  df-oppg 19334  df-lsm 19622  df-cmn 19768  df-abl 19769  df-mgp 20106  df-rng 20118  df-ur 20147  df-srg 20152  df-ring 20200  df-cring 20201  df-oppr 20302  df-dvdsr 20322  df-unit 20323  df-irred 20324  df-invr 20353  df-dvr 20366  df-rhm 20437  df-nzr 20478  df-subrng 20511  df-subrg 20535  df-rlreg 20659  df-domn 20660  df-idom 20661  df-drng 20696  df-field 20697  df-sdrg 20752  df-lmod 20824  df-lss 20894  df-lsp 20934  df-lmhm 20985  df-lmim 20986  df-lbs 21038  df-lvec 21066  df-sra 21136  df-rgmod 21137  df-lidl 21174  df-rsp 21175  df-2idl 21216  df-lpidl 21288  df-lpir 21289  df-pid 21303  df-cnfld 21321  df-dsmm 21697  df-frlm 21712  df-uvc 21748  df-lindf 21771  df-linds 21772  df-assa 21818  df-asp 21819  df-ascl 21820  df-psr 21874  df-mvr 21875  df-mpl 21876  df-opsr 21878  df-evls 22037  df-evl 22038  df-psr1 22120  df-vr1 22121  df-ply1 22122  df-coe1 22123  df-evls1 22258  df-evl1 22259  df-mdeg 26017  df-deg1 26018  df-mon1 26093  df-uc1p 26094  df-q1p 26095  df-r1p 26096  df-ig1p 26097  df-fldgen 33310  df-mxidl 33480  df-dim 33644  df-fldext 33687  df-extdg 33688  df-irng 33730  df-minply 33739

This theorem is referenced by:  algextdeg  33764