Theorem algextdeglem4 33883

Description: Lemma for algextdeg 33888. By lmhmqusker 33495, the surjective module homomorphism 𝐺 described in algextdeglem2 33881 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 20759	. . . . . . . 8 ⊢ (𝐹 ∈ (SubDRing‘𝐸) ↔ (𝐸 ∈ DivRing ∧ 𝐹 ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s 𝐹) ∈ DivRing))
3	1, 2	sylib 218	. . . . . . 7 ⊢ (𝜑 → (𝐸 ∈ DivRing ∧ 𝐹 ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s 𝐹) ∈ DivRing))
4	3	simp2d 1144	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸))
5		subrgsubg 20548	. . . . . 6 ⊢ (𝐹 ∈ (SubRing‘𝐸) → 𝐹 ∈ (SubGrp‘𝐸))
6		eqid 2737	. . . . . . 7 ⊢ (Base‘𝐸) = (Base‘𝐸)
7	6	subgss 19097	. . . . . 6 ⊢ (𝐹 ∈ (SubGrp‘𝐸) → 𝐹 ⊆ (Base‘𝐸))
8	4, 5, 7	3syl 18	. . . . 5 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐸))
9		algextdeg.k	. . . . . 6 ⊢ 𝐾 = (𝐸 ↾s 𝐹)
10	9, 6	ressbas2 17202	. . . . 5 ⊢ (𝐹 ⊆ (Base‘𝐸) → 𝐹 = (Base‘𝐾))
11	8, 10	syl 17	. . . 4 ⊢ (𝜑 → 𝐹 = (Base‘𝐾))
12	11	fveq2d 6839	. . 3 ⊢ (𝜑 → ((subringAlg ‘𝐿)‘𝐹) = ((subringAlg ‘𝐿)‘(Base‘𝐾)))
13	12	fveq2d 6839	. 2 ⊢ (𝜑 → (dim‘((subringAlg ‘𝐿)‘𝐹)) = (dim‘((subringAlg ‘𝐿)‘(Base‘𝐾))))
14		eqid 2737	. . . . 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 33881	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ (𝑃 LMHom ((subringAlg ‘𝐿)‘𝐹)))
29		eqid 2737	. . . . 5 ⊢ (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}) = (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})
30		eqid 2737	. . . . 5 ⊢ (𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}))) = (𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))
31	9	fveq2i 6838	. . . . . . . . . . 11 ⊢ (Poly1‘𝐾) = (Poly1‘(𝐸 ↾s 𝐹))
32	21, 31	eqtri 2760	. . . . . . . . . 10 ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))
33	18	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝐸 ∈ Field)
34	1	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝐹 ∈ (SubDRing‘𝐸))
35		eqid 2737	. . . . . . . . . . . . 13 ⊢ (0g‘𝐸) = (0g‘𝐸)
36	18	fldcrngd 20713	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸 ∈ CRing)
37	20, 9, 6, 35, 36, 4	irngssv 33851	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸 IntgRing 𝐹) ⊆ (Base‘𝐸))
38	37, 19	sseldd 3923	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ (Base‘𝐸))
39	38	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝐴 ∈ (Base‘𝐸))
40		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝑝 ∈ 𝑈)
41	6, 20, 32, 22, 33, 34, 39, 40	evls1fldgencl 33833	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → ((𝑂‘𝑝)‘𝐴) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})))
42	41	ralrimiva 3130	. . . . . . . 8 ⊢ (𝜑 → ∀𝑝 ∈ 𝑈 ((𝑂‘𝑝)‘𝐴) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})))
43	23	rnmptss 7070	. . . . . . . 8 ⊢ (∀𝑝 ∈ 𝑈 ((𝑂‘𝑝)‘𝐴) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})) → ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))
44	42, 43	syl 17	. . . . . . 7 ⊢ (𝜑 → ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))
45	18	flddrngd 20712	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ DivRing)
46	20, 32, 6, 22, 36, 4, 38, 23	evls1maprhm 22354	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ (𝑃 RingHom 𝐸))
47		rnrhmsubrg 20576	. . . . . . . . . 10 ⊢ (𝐺 ∈ (𝑃 RingHom 𝐸) → ran 𝐺 ∈ (SubRing‘𝐸))
48	46, 47	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐺 ∈ (SubRing‘𝐸))
49	15	oveq1i 7371	. . . . . . . . . . 11 ⊢ (𝐿 ↾s ran 𝐺) = ((𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ↾s ran 𝐺)
50		ovex 7394	. . . . . . . . . . . 12 ⊢ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ V
51		ressabs 17212	. . . . . . . . . . . 12 ⊢ (((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ V ∧ ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴}))) → ((𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ↾s ran 𝐺) = (𝐸 ↾s ran 𝐺))
52	50, 44, 51	sylancr 588	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ↾s ran 𝐺) = (𝐸 ↾s ran 𝐺))
53	49, 52	eqtrid 2784	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿 ↾s ran 𝐺) = (𝐸 ↾s ran 𝐺))
54		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ (0g‘𝐿) = (0g‘𝐿)
55	38	snssd 4753	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → {𝐴} ⊆ (Base‘𝐸))
56	8, 55	unssd 4133	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐹 ∪ {𝐴}) ⊆ (Base‘𝐸))
57	6, 45, 56	fldgensdrg 33393	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubDRing‘𝐸))
58		issdrg 20759	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubDRing‘𝐸) ↔ (𝐸 ∈ DivRing ∧ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ∈ DivRing))
59	57, 58	sylib 218	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 ∈ DivRing ∧ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ∈ DivRing))
60	59	simp2d 1144	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸))
61	15	resrhm2b 20573	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴}))) → (𝐺 ∈ (𝑃 RingHom 𝐸) ↔ 𝐺 ∈ (𝑃 RingHom 𝐿)))
62	61	biimpa 476	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴}))) ∧ 𝐺 ∈ (𝑃 RingHom 𝐸)) → 𝐺 ∈ (𝑃 RingHom 𝐿))
63	60, 44, 46, 62	syl21anc 838	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐺 ∈ (𝑃 RingHom 𝐿))
64		rhmghm 20457	. . . . . . . . . . . . . . . 16 ⊢ (𝐺 ∈ (𝑃 RingHom 𝐿) → 𝐺 ∈ (𝑃 GrpHom 𝐿))
65	63, 64	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺 ∈ (𝑃 GrpHom 𝐿))
66	54, 65, 25, 26, 27, 22, 24	ghmquskerco 19253	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺 = (𝐽 ∘ 𝑁))
67	66	rneqd 5888	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝐺 = ran (𝐽 ∘ 𝑁))
68	26	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑄 = (𝑃 /s (𝑃 ~QG 𝑍)))
69	22	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑈 = (Base‘𝑃))
70		ovexd 7396	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃 ~QG 𝑍) ∈ V)
71	3	simp3d 1145	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ DivRing)
72	32, 71	ply1lvec 33637	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ LVec)
73	68, 69, 70, 72	qusbas 17503	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 / (𝑃 ~QG 𝑍)) = (Base‘𝑄))
74		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 / (𝑃 ~QG 𝑍)) = (𝑈 / (𝑃 ~QG 𝑍))
75	54	ghmker 19211	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 ∈ (𝑃 GrpHom 𝐿) → (◡𝐺 “ {(0g‘𝐿)}) ∈ (NrmSGrp‘𝑃))
76	65, 75	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (◡𝐺 “ {(0g‘𝐿)}) ∈ (NrmSGrp‘𝑃))
77	25, 76	eqeltrid 2841	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑍 ∈ (NrmSGrp‘𝑃))
78	22, 74, 24, 77	qusrn 33487	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ran 𝑁 = (𝑈 / (𝑃 ~QG 𝑍)))
79		eqid 2737	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((subringAlg ‘𝐸)‘𝐹) = ((subringAlg ‘𝐸)‘𝐹)
80	20, 32, 6, 22, 36, 4, 38, 23, 79	evls1maplmhm 22355	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐺 ∈ (𝑃 LMHom ((subringAlg ‘𝐸)‘𝐹)))
81	80	elexd 3454	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐺 ∈ V)
82	81	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘𝑄)) → 𝐺 ∈ V)
83	82	imaexd 7861	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘𝑄)) → (𝐺 “ 𝑝) ∈ V)
84	83	uniexd 7690	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘𝑄)) → ∪ (𝐺 “ 𝑝) ∈ V)
85	27, 84	dmmptd 6638	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom 𝐽 = (Base‘𝑄))
86	73, 78, 85	3eqtr4rd 2783	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom 𝐽 = ran 𝑁)
87		rncoeq 5932	. . . . . . . . . . . . . 14 ⊢ (dom 𝐽 = ran 𝑁 → ran (𝐽 ∘ 𝑁) = ran 𝐽)
88	86, 87	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran (𝐽 ∘ 𝑁) = ran 𝐽)
89	67, 88	eqtrd 2772	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝐺 = ran 𝐽)
90	89	oveq2d 7377	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐿 ↾s ran 𝐺) = (𝐿 ↾s ran 𝐽))
91		eqid 2737	. . . . . . . . . . . 12 ⊢ (𝐿 ↾s ran 𝐽) = (𝐿 ↾s ran 𝐽)
92	9	subrgcrng 20546	. . . . . . . . . . . . . . 15 ⊢ ((𝐸 ∈ CRing ∧ 𝐹 ∈ (SubRing‘𝐸)) → 𝐾 ∈ CRing)
93	36, 4, 92	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ CRing)
94	21	ply1crng 22175	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ CRing → 𝑃 ∈ CRing)
95	93, 94	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ CRing)
96	54, 63, 25, 26, 27, 95	rhmquskerlem 33503	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ (𝑄 RingHom 𝐿))
97	20, 32, 6, 22, 36, 4, 38, 23	evls1maprnss 22356	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 ⊆ ran 𝐺)
98		eqid 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (1r‘𝐸) = (1r‘𝐸)
99	9, 98	subrg1 20553	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (SubRing‘𝐸) → (1r‘𝐸) = (1r‘𝐾))
100	4, 99	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1r‘𝐸) = (1r‘𝐾))
101	98	subrg1cl 20551	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (SubRing‘𝐸) → (1r‘𝐸) ∈ 𝐹)
102	4, 101	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1r‘𝐸) ∈ 𝐹)
103	100, 102	eqeltrrd 2838	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1r‘𝐾) ∈ 𝐹)
104	97, 103	sseldd 3923	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1r‘𝐾) ∈ ran 𝐺)
105		drngnzr 20719	. . . . . . . . . . . . . . . . 17 ⊢ (𝐸 ∈ DivRing → 𝐸 ∈ NzRing)
106	98, 35	nzrnz 20486	. . . . . . . . . . . . . . . . 17 ⊢ (𝐸 ∈ NzRing → (1r‘𝐸) ≠ (0g‘𝐸))
107	45, 105, 106	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1r‘𝐸) ≠ (0g‘𝐸))
108	36	crnggrpd 20222	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐸 ∈ Grp)
109	108	grpmndd 18916	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐸 ∈ Mnd)
110		sdrgsubrg 20762	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubDRing‘𝐸) → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸))
111		subrgsubg 20548	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubGrp‘𝐸))
112	57, 110, 111	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubGrp‘𝐸))
113	35	subg0cl 19104	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubGrp‘𝐸) → (0g‘𝐸) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})))
114	112, 113	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0g‘𝐸) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})))
115	6, 45, 56	fldgenssv 33394	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ⊆ (Base‘𝐸))
116	15, 6, 35	ress0g 18724	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐸 ∈ Mnd ∧ (0g‘𝐸) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∧ (𝐸 fldGen (𝐹 ∪ {𝐴})) ⊆ (Base‘𝐸)) → (0g‘𝐸) = (0g‘𝐿))
117	109, 114, 115, 116	syl3anc 1374	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐿))
118	107, 100, 117	3netr3d 3009	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1r‘𝐾) ≠ (0g‘𝐿))
119		nelsn 4611	. . . . . . . . . . . . . . 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 585	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝐺 ≠ {(0g‘𝐿)})
123	89, 122	eqnetrrd 3001	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝐽 ≠ {(0g‘𝐿)})
124		eqid 2737	. . . . . . . . . . . . 13 ⊢ (oppr‘𝑃) = (oppr‘𝑃)
125	9	sdrgdrng 20761	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐾 ∈ DivRing)
126		drngnzr 20719	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ DivRing → 𝐾 ∈ NzRing)
127	1, 125, 126	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ NzRing)
128	21	ply1nz 26100	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ NzRing → 𝑃 ∈ NzRing)
129	127, 128	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ NzRing)
130		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)} = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)}
131		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (RSpan‘𝑃) = (RSpan‘𝑃)
132	9	fveq2i 6838	. . . . . . . . . . . . . . . 16 ⊢ (idlGen1p‘𝐾) = (idlGen1p‘(𝐸 ↾s 𝐹))
133	20, 32, 6, 18, 1, 38, 35, 130, 131, 132	ply1annig1p 33867	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)} = ((RSpan‘𝑃)‘{((idlGen1p‘𝐾)‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)})}))
134	117	sneqd 4580	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → {(0g‘𝐸)} = {(0g‘𝐿)})
135	134	imaeq2d 6020	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (◡𝐺 “ {(0g‘𝐸)}) = (◡𝐺 “ {(0g‘𝐿)}))
136	25, 135	eqtr4id 2791	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑍 = (◡𝐺 “ {(0g‘𝐸)}))
137	22	mpteq1i 5177	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴)) = (𝑝 ∈ (Base‘𝑃) ↦ ((𝑂‘𝑝)‘𝐴))
138	23, 137	eqtri 2760	. . . . . . . . . . . . . . . . 17 ⊢ 𝐺 = (𝑝 ∈ (Base‘𝑃) ↦ ((𝑂‘𝑝)‘𝐴))
139	20, 32, 6, 36, 4, 38, 35, 130, 138	ply1annidllem 33864	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)} = (◡𝐺 “ {(0g‘𝐸)}))
140	136, 139	eqtr4d 2775	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑍 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)})
141		eqid 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐸 minPoly 𝐹) = (𝐸 minPoly 𝐹)
142	20, 32, 6, 18, 1, 38, 35, 130, 131, 132, 141	minplyval 33868	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) = ((idlGen1p‘𝐾)‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)}))
143	142	sneqd 4580	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {((𝐸 minPoly 𝐹)‘𝐴)} = {((idlGen1p‘𝐾)‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)})})
144	143	fveq2d 6839	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) = ((RSpan‘𝑃)‘{((idlGen1p‘𝐾)‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)})}))
145	133, 140, 144	3eqtr4d 2782	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑍 = ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}))
146		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (0g‘𝑃) = (0g‘𝑃)
147		eqid 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (0g‘(Poly1‘𝐸)) = (0g‘(Poly1‘𝐸))
148	147, 18, 1, 141, 19	irngnminplynz 33875	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ≠ (0g‘(Poly1‘𝐸)))
149		eqid 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (Poly1‘𝐸) = (Poly1‘𝐸)
150	149, 9, 21, 22, 4, 147	ressply10g 33645	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0g‘(Poly1‘𝐸)) = (0g‘𝑃))
151	148, 150	neeqtrd 3002	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ≠ (0g‘𝑃))
152	20, 32, 6, 18, 1, 38, 141, 146, 151	minplyirred 33874	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ∈ (Irred‘𝑃))
153		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) = ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)})
154		fldsdrgfld 20769	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ (SubDRing‘𝐸)) → (𝐸 ↾s 𝐹) ∈ Field)
155	18, 1, 154	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ Field)
156	9, 155	eqeltrid 2841	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 ∈ Field)
157	21	ply1pid 26161	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ Field → 𝑃 ∈ PID)
158	156, 157	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ PID)
159	20, 32, 6, 18, 1, 38, 35, 130, 131, 132, 141	minplycl 33869	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ∈ (Base‘𝑃))
160	159, 22	eleqtrrdi 2848	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ∈ 𝑈)
161	95	crngringd 20221	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ Ring)
162	160	snssd 4753	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → {((𝐸 minPoly 𝐹)‘𝐴)} ⊆ 𝑈)
163		eqid 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (LIdeal‘𝑃) = (LIdeal‘𝑃)
164	131, 22, 163	rspcl 21228	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ Ring ∧ {((𝐸 minPoly 𝐹)‘𝐴)} ⊆ 𝑈) → ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) ∈ (LIdeal‘𝑃))
165	161, 162, 164	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) ∈ (LIdeal‘𝑃))
166	22, 131, 146, 153, 158, 160, 151, 165	mxidlirred 33550	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) ∈ (MaxIdeal‘𝑃) ↔ ((𝐸 minPoly 𝐹)‘𝐴) ∈ (Irred‘𝑃)))
167	152, 166	mpbird 257	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) ∈ (MaxIdeal‘𝑃))
168	145, 167	eqeltrd 2837	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑍 ∈ (MaxIdeal‘𝑃))
169		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (MaxIdeal‘𝑃) = (MaxIdeal‘𝑃)
170	169, 124	crngmxidl 33547	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ CRing → (MaxIdeal‘𝑃) = (MaxIdeal‘(oppr‘𝑃)))
171	95, 170	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (MaxIdeal‘𝑃) = (MaxIdeal‘(oppr‘𝑃)))
172	168, 171	eleqtrd 2839	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑍 ∈ (MaxIdeal‘(oppr‘𝑃)))
173	124, 26, 129, 168, 172	qsdrngi 33573	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∈ DivRing)
174	91, 54, 96, 123, 173	rndrhmcl 33375	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐿 ↾s ran 𝐽) ∈ DivRing)
175	90, 174	eqeltrd 2837	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿 ↾s ran 𝐺) ∈ DivRing)
176	53, 175	eqeltrrd 2838	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 ↾s ran 𝐺) ∈ DivRing)
177		issdrg 20759	. . . . . . . . 9 ⊢ (ran 𝐺 ∈ (SubDRing‘𝐸) ↔ (𝐸 ∈ DivRing ∧ ran 𝐺 ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s ran 𝐺) ∈ DivRing))
178	45, 48, 176, 177	syl3anbrc 1345	. . . . . . . 8 ⊢ (𝜑 → ran 𝐺 ∈ (SubDRing‘𝐸))
179		fveq2 6835	. . . . . . . . . . . . . 14 ⊢ (𝑝 = (var1‘𝐾) → (𝑂‘𝑝) = (𝑂‘(var1‘𝐾)))
180	179	fveq1d 6837	. . . . . . . . . . . . 13 ⊢ (𝑝 = (var1‘𝐾) → ((𝑂‘𝑝)‘𝐴) = ((𝑂‘(var1‘𝐾))‘𝐴))
181	180	eqeq2d 2748	. . . . . . . . . . . 12 ⊢ (𝑝 = (var1‘𝐾) → (𝐴 = ((𝑂‘𝑝)‘𝐴) ↔ 𝐴 = ((𝑂‘(var1‘𝐾))‘𝐴)))
182	9, 71	eqeltrid 2841	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ DivRing)
183	182	drngringd 20708	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐾 ∈ Ring)
184		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (var1‘𝐾) = (var1‘𝐾)
185	184, 21, 22	vr1cl 22194	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ Ring → (var1‘𝐾) ∈ 𝑈)
186	183, 185	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (var1‘𝐾) ∈ 𝑈)
187	20, 184, 9, 6, 36, 4	evls1var 22316	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑂‘(var1‘𝐾)) = ( I ↾ (Base‘𝐸)))
188	187	fveq1d 6837	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑂‘(var1‘𝐾))‘𝐴) = (( I ↾ (Base‘𝐸))‘𝐴))
189		fvresi 7122	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (Base‘𝐸) → (( I ↾ (Base‘𝐸))‘𝐴) = 𝐴)
190	38, 189	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (( I ↾ (Base‘𝐸))‘𝐴) = 𝐴)
191	188, 190	eqtr2d 2773	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 = ((𝑂‘(var1‘𝐾))‘𝐴))
192	181, 186, 191	rspcedvdw 3568	. . . . . . . . . . 11 ⊢ (𝜑 → ∃𝑝 ∈ 𝑈 𝐴 = ((𝑂‘𝑝)‘𝐴))
193	23, 192, 19	elrnmptd 5913	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ran 𝐺)
194	193	snssd 4753	. . . . . . . . 9 ⊢ (𝜑 → {𝐴} ⊆ ran 𝐺)
195	97, 194	unssd 4133	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ∪ {𝐴}) ⊆ ran 𝐺)
196	6, 45, 178, 195	fldgenssp 33397	. . . . . . 7 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ⊆ ran 𝐺)
197	44, 196	eqssd 3940	. . . . . 6 ⊢ (𝜑 → ran 𝐺 = (𝐸 fldGen (𝐹 ∪ {𝐴})))
198	15, 6	ressbas2 17202	. . . . . . 7 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ⊆ (Base‘𝐸) → (𝐸 fldGen (𝐹 ∪ {𝐴})) = (Base‘𝐿))
199	115, 198	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) = (Base‘𝐿))
200		eqidd 2738	. . . . . . 7 ⊢ (𝜑 → ((subringAlg ‘𝐿)‘𝐹) = ((subringAlg ‘𝐿)‘𝐹))
201	6, 45, 56	fldgenssid 33392	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 ∪ {𝐴}) ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))
202	201	unssad 4134	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))
203	202, 199	sseqtrd 3959	. . . . . . 7 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐿))
204	200, 203	srabase 21167	. . . . . 6 ⊢ (𝜑 → (Base‘𝐿) = (Base‘((subringAlg ‘𝐿)‘𝐹)))
205	197, 199, 204	3eqtrd 2776	. . . . 5 ⊢ (𝜑 → ran 𝐺 = (Base‘((subringAlg ‘𝐿)‘𝐹)))
206		imaeq2 6016	. . . . . . 7 ⊢ (𝑞 = 𝑝 → (𝐺 “ 𝑞) = (𝐺 “ 𝑝))
207	206	unieqd 4864	. . . . . 6 ⊢ (𝑞 = 𝑝 → ∪ (𝐺 “ 𝑞) = ∪ (𝐺 “ 𝑝))
208	207	cbvmptv 5190	. . . . 5 ⊢ (𝑞 ∈ (Base‘(𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺 “ 𝑞)) = (𝑝 ∈ (Base‘(𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺 “ 𝑝))
209	14, 28, 29, 30, 205, 208	lmhmqusker 33495	. . . 4 ⊢ (𝜑 → (𝑞 ∈ (Base‘(𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺 “ 𝑞)) ∈ ((𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}))) LMIso ((subringAlg ‘𝐿)‘𝐹)))
210		eqidd 2738	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0g‘𝐿) = (0g‘𝐿))
211	200, 210, 203	sralmod0 21178	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0g‘𝐿) = (0g‘((subringAlg ‘𝐿)‘𝐹)))
212	211	sneqd 4580	. . . . . . . . . . . 12 ⊢ (𝜑 → {(0g‘𝐿)} = {(0g‘((subringAlg ‘𝐿)‘𝐹))})
213	212	imaeq2d 6020	. . . . . . . . . . 11 ⊢ (𝜑 → (◡𝐺 “ {(0g‘𝐿)}) = (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}))
214	25, 213	eqtrid 2784	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 = (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}))
215	214	oveq2d 7377	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 ~QG 𝑍) = (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))
216	215	oveq2d 7377	. . . . . . . 8 ⊢ (𝜑 → (𝑃 /s (𝑃 ~QG 𝑍)) = (𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}))))
217	26, 216	eqtrid 2784	. . . . . . 7 ⊢ (𝜑 → 𝑄 = (𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}))))
218	217	fveq2d 6839	. . . . . 6 ⊢ (𝜑 → (Base‘𝑄) = (Base‘(𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))))
219	218	mpteq1d 5176	. . . . 5 ⊢ (𝜑 → (𝑝 ∈ (Base‘𝑄) ↦ ∪ (𝐺 “ 𝑝)) = (𝑝 ∈ (Base‘(𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺 “ 𝑝)))
220	219, 27, 208	3eqtr4g 2797	. . . 4 ⊢ (𝜑 → 𝐽 = (𝑞 ∈ (Base‘(𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺 “ 𝑞)))
221	217	oveq1d 7376	. . . 4 ⊢ (𝜑 → (𝑄 LMIso ((subringAlg ‘𝐿)‘𝐹)) = ((𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}))) LMIso ((subringAlg ‘𝐿)‘𝐹)))
222	209, 220, 221	3eltr4d 2852	. . 3 ⊢ (𝜑 → 𝐽 ∈ (𝑄 LMIso ((subringAlg ‘𝐿)‘𝐹)))
223	9, 15, 16, 17, 18, 1, 19, 20, 21, 22, 23, 24, 25, 26, 27	algextdeglem3 33882	. . 3 ⊢ (𝜑 → 𝑄 ∈ LVec)
224	222, 223	lmimdim 33766	. 2 ⊢ (𝜑 → (dim‘𝑄) = (dim‘((subringAlg ‘𝐿)‘𝐹)))
225	6, 18, 56	fldgenfld 33399	. . . . 5 ⊢ (𝜑 → (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ∈ Field)
226	15, 225	eqeltrid 2841	. . . 4 ⊢ (𝜑 → 𝐿 ∈ Field)
227	9, 15, 16, 17, 18, 1, 19	algextdeglem1 33880	. . . . 5 ⊢ (𝜑 → (𝐿 ↾s 𝐹) = 𝐾)
228	11	oveq2d 7377	. . . . 5 ⊢ (𝜑 → (𝐿 ↾s 𝐹) = (𝐿 ↾s (Base‘𝐾)))
229	227, 228	eqtr3d 2774	. . . 4 ⊢ (𝜑 → 𝐾 = (𝐿 ↾s (Base‘𝐾)))
230	15	subsubrg 20569	. . . . . . 7 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) → (𝐹 ∈ (SubRing‘𝐿) ↔ (𝐹 ∈ (SubRing‘𝐸) ∧ 𝐹 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))))
231	230	biimpar 477	. . . . . 6 ⊢ (((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ (𝐹 ∈ (SubRing‘𝐸) ∧ 𝐹 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))) → 𝐹 ∈ (SubRing‘𝐿))
232	60, 4, 202, 231	syl12anc 837	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐿))
233	11, 232	eqeltrrd 2838	. . . 4 ⊢ (𝜑 → (Base‘𝐾) ∈ (SubRing‘𝐿))
234		brfldext 33808	. . . . 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 839	. . 3 ⊢ (𝜑 → 𝐿/FldExt𝐾)
237		extdgval 33816	. . 3 ⊢ (𝐿/FldExt𝐾 → (𝐿[:]𝐾) = (dim‘((subringAlg ‘𝐿)‘(Base‘𝐾))))
238	236, 237	syl 17	. 2 ⊢ (𝜑 → (𝐿[:]𝐾) = (dim‘((subringAlg ‘𝐿)‘(Base‘𝐾))))
239	13, 224, 238	3eqtr4d 2782	1 ⊢ (𝜑 → (dim‘𝑄) = (𝐿[:]𝐾))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  ∀wral 3052  {crab 3390  Vcvv 3430   ∪ cun 3888   ⊆ wss 3890  {csn 4568  ∪ cuni 4851   class class class wbr 5086   ↦ cmpt 5167   I cid 5519  ^◡ccnv 5624  dom cdm 5625  ran crn 5626   ↾ cres 5627   “ cima 5628   ∘ ccom 5629  ‘cfv 6493  (class class class)co 7361  [cec 8635   / cqs 8636  Basecbs 17173   ↾_s cress 17194  0_gc0g 17396   /_s cqus 17463  Mndcmnd 18696  SubGrpcsubg 19090  NrmSGrpcnsg 19091   ~_QG cqg 19092   GrpHom cghm 19181  1_rcur 20156  Ringcrg 20208  CRingccrg 20209  opp_rcoppr 20310  Irredcir 20330   RingHom crh 20443  NzRingcnzr 20483  SubRingcsubrg 20540  DivRingcdr 20700  Fieldcfield 20701  SubDRingcsdrg 20757   LMHom clmhm 21009   LMIso clmim 21010  LVecclvec 21092  subringAlg csra 21161  LIdealclidl 21199  RSpancrsp 21200  PIDcpid 21329  var₁cv1 22152  Poly₁cpl1 22153   evalSub₁ ces1 22291  deg₁cdg1 26032  idlGen_1pcig1p 26108   fldGen cfldgen 33389  MaxIdealcmxidl 33537  dimcldim 33761  /_FldExtcfldext 33801  [:]cextdg 33803   IntgRing cirng 33846   minPoly cminply 33862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-reg 9501  ax-inf2 9556  ax-ac2 10379  ax-cnex 11088  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108  ax-pre-mulgt0 11109  ax-pre-sup 11110  ax-addf 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-tp 4573  df-op 4575  df-uni 4852  df-int 4891  df-iun 4936  df-iin 4937  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-se 5579  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-isom 6502  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-of 7625  df-ofr 7626  df-rpss 7671  df-om 7812  df-1st 7936  df-2nd 7937  df-supp 8105  df-tpos 8170  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-1o 8399  df-2o 8400  df-oadd 8403  df-er 8637  df-ec 8639  df-qs 8643  df-map 8769  df-pm 8770  df-ixp 8840  df-en 8888  df-dom 8889  df-sdom 8890  df-fin 8891  df-fsupp 9269  df-sup 9349  df-inf 9350  df-oi 9419  df-r1 9682  df-rank 9683  df-dju 9819  df-card 9857  df-acn 9860  df-ac 10032  df-pnf 11175  df-mnf 11176  df-xr 11177  df-ltxr 11178  df-le 11179  df-sub 11373  df-neg 11374  df-nn 12169  df-2 12238  df-3 12239  df-4 12240  df-5 12241  df-6 12242  df-7 12243  df-8 12244  df-9 12245  df-n0 12432  df-xnn0 12505  df-z 12519  df-dec 12639  df-uz 12783  df-fz 13456  df-fzo 13603  df-seq 13958  df-hash 14287  df-struct 17111  df-sets 17128  df-slot 17146  df-ndx 17158  df-base 17174  df-ress 17195  df-plusg 17227  df-mulr 17228  df-starv 17229  df-sca 17230  df-vsca 17231  df-ip 17232  df-tset 17233  df-ple 17234  df-ocomp 17235  df-ds 17236  df-unif 17237  df-hom 17238  df-cco 17239  df-0g 17398  df-gsum 17399  df-prds 17404  df-pws 17406  df-imas 17466  df-qus 17467  df-mre 17542  df-mrc 17543  df-mri 17544  df-acs 17545  df-proset 18254  df-drs 18255  df-poset 18273  df-ipo 18488  df-mgm 18602  df-sgrp 18681  df-mnd 18697  df-mhm 18745  df-submnd 18746  df-grp 18906  df-minusg 18907  df-sbg 18908  df-mulg 19038  df-subg 19093  df-nsg 19094  df-eqg 19095  df-ghm 19182  df-gim 19228  df-cntz 19286  df-oppg 19315  df-lsm 19605  df-cmn 19751  df-abl 19752  df-mgp 20116  df-rng 20128  df-ur 20157  df-srg 20162  df-ring 20210  df-cring 20211  df-oppr 20311  df-dvdsr 20331  df-unit 20332  df-irred 20333  df-invr 20362  df-dvr 20375  df-rhm 20446  df-nzr 20484  df-subrng 20517  df-subrg 20541  df-rlreg 20665  df-domn 20666  df-idom 20667  df-drng 20702  df-field 20703  df-sdrg 20758  df-lmod 20851  df-lss 20921  df-lsp 20961  df-lmhm 21012  df-lmim 21013  df-lbs 21065  df-lvec 21093  df-sra 21163  df-rgmod 21164  df-lidl 21201  df-rsp 21202  df-2idl 21243  df-lpidl 21315  df-lpir 21316  df-pid 21330  df-cnfld 21348  df-dsmm 21725  df-frlm 21740  df-uvc 21776  df-lindf 21799  df-linds 21800  df-assa 21846  df-asp 21847  df-ascl 21848  df-psr 21902  df-mvr 21903  df-mpl 21904  df-opsr 21906  df-evls 22065  df-evl 22066  df-psr1 22156  df-vr1 22157  df-ply1 22158  df-coe1 22159  df-evls1 22293  df-evl1 22294  df-mdeg 26033  df-deg1 26034  df-mon1 26109  df-uc1p 26110  df-q1p 26111  df-r1p 26112  df-ig1p 26113  df-fldgen 33390  df-mxidl 33538  df-dim 33762  df-fldext 33804  df-extdg 33805  df-irng 33847  df-minply 33863

This theorem is referenced by:  algextdeg  33888