algextdeglem4 - Mathbox for Thierry Arnoux

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

Theorem algextdeglem4 33080

Description: Lemma for algextdeg 33085. (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
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 20551	. . . . . . . 8 ⊢ (𝐹 ∈ (SubDRing‘𝐸) ↔ (𝐸 ∈ DivRing ∧ 𝐹 ∈ (SubRing‘𝐸) ∧ (𝐸 ↾_s 𝐹) ∈ DivRing))
3	1, 2	sylib 217	. . . . . . 7 ⊢ (𝜑 → (𝐸 ∈ DivRing ∧ 𝐹 ∈ (SubRing‘𝐸) ∧ (𝐸 ↾_s 𝐹) ∈ DivRing))
4	3	simp2d 1142	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸))
5		subrgsubg 20471	. . . . . 6 ⊢ (𝐹 ∈ (SubRing‘𝐸) → 𝐹 ∈ (SubGrp‘𝐸))
6		eqid 2731	. . . . . . 7 ⊢ (Base‘𝐸) = (Base‘𝐸)
7	6	subgss 19047	. . . . . 6 ⊢ (𝐹 ∈ (SubGrp‘𝐸) → 𝐹 ⊆ (Base‘𝐸))
8	4, 5, 7	3syl 18	. . . . 5 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐸))
9		algextdeg.k	. . . . . 6 ⊢ 𝐾 = (𝐸 ↾_s 𝐹)
10	9, 6	ressbas2 17189	. . . . 5 ⊢ (𝐹 ⊆ (Base‘𝐸) → 𝐹 = (Base‘𝐾))
11	8, 10	syl 17	. . . 4 ⊢ (𝜑 → 𝐹 = (Base‘𝐾))
12	11	fveq2d 6895	. . 3 ⊢ (𝜑 → ((subringAlg ‘𝐿)‘𝐹) = ((subringAlg ‘𝐿)‘(Base‘𝐾)))
13	12	fveq2d 6895	. 2 ⊢ (𝜑 → (dim‘((subringAlg ‘𝐿)‘𝐹)) = (dim‘((subringAlg ‘𝐿)‘(Base‘𝐾))))
14		eqid 2731	. . . . 5 ⊢ (0_g‘((subringAlg ‘𝐿)‘𝐹)) = (0_g‘((subringAlg ‘𝐿)‘𝐹))
15		algextdeg.l	. . . . . 6 ⊢ 𝐿 = (𝐸 ↾_s (𝐸 fldGen (𝐹 ∪ {𝐴})))
16		algextdeg.d	. . . . . 6 ⊢ 𝐷 = ( deg₁ ‘𝐸)
17		algextdeg.m	. . . . . 6 ⊢ 𝑀 = (𝐸 minPoly 𝐹)
18		algextdeg.f	. . . . . 6 ⊢ (𝜑 → 𝐸 ∈ Field)
19		algextdeg.a	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))
20		algextdeglem.o	. . . . . 6 ⊢ 𝑂 = (𝐸 evalSub₁ 𝐹)
21		algextdeglem.y	. . . . . 6 ⊢ 𝑃 = (Poly₁‘𝐾)
22		algextdeglem.u	. . . . . 6 ⊢ 𝑈 = (Base‘𝑃)
23		algextdeglem.g	. . . . . 6 ⊢ 𝐺 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴))
24		algextdeglem.n	. . . . . 6 ⊢ 𝑁 = (𝑥 ∈ 𝑈 ↦ [𝑥](𝑃 ~_QG 𝑍))
25		algextdeglem.z	. . . . . 6 ⊢ 𝑍 = (^◡𝐺 “ {(0_g‘𝐿)})
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 33078	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ (𝑃 LMHom ((subringAlg ‘𝐿)‘𝐹)))
29		eqid 2731	. . . . 5 ⊢ (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))}) = (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))})
30		eqid 2731	. . . . 5 ⊢ (𝑃 /_s (𝑃 ~_QG (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))}))) = (𝑃 /_s (𝑃 ~_QG (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))})))
31	9	fveq2i 6894	. . . . . . . . . . 11 ⊢ (Poly₁‘𝐾) = (Poly₁‘(𝐸 ↾_s 𝐹))
32	21, 31	eqtri 2759	. . . . . . . . . 10 ⊢ 𝑃 = (Poly₁‘(𝐸 ↾_s 𝐹))
33	18	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝐸 ∈ Field)
34	1	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝐹 ∈ (SubDRing‘𝐸))
35		eqid 2731	. . . . . . . . . . . . 13 ⊢ (0_g‘𝐸) = (0_g‘𝐸)
36	18	fldcrngd 20517	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸 ∈ CRing)
37	20, 9, 6, 35, 36, 4	irngssv 33056	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸 IntgRing 𝐹) ⊆ (Base‘𝐸))
38	37, 19	sseldd 3983	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ (Base‘𝐸))
39	38	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝐴 ∈ (Base‘𝐸))
40		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝑝 ∈ 𝑈)
41	6, 20, 32, 22, 33, 34, 39, 40	evls1fldgencl 33048	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → ((𝑂‘𝑝)‘𝐴) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})))
42	41	ralrimiva 3145	. . . . . . . 8 ⊢ (𝜑 → ∀𝑝 ∈ 𝑈 ((𝑂‘𝑝)‘𝐴) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})))
43	23	rnmptss 7124	. . . . . . . 8 ⊢ (∀𝑝 ∈ 𝑈 ((𝑂‘𝑝)‘𝐴) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})) → ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))
44	42, 43	syl 17	. . . . . . 7 ⊢ (𝜑 → ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))
45	18	flddrngd 20516	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ DivRing)
46	20, 32, 6, 22, 36, 4, 38, 23	evls1maprhm 33063	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ (𝑃 RingHom 𝐸))
47		rnrhmsubrg 20499	. . . . . . . . . 10 ⊢ (𝐺 ∈ (𝑃 RingHom 𝐸) → ran 𝐺 ∈ (SubRing‘𝐸))
48	46, 47	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐺 ∈ (SubRing‘𝐸))
49	15	oveq1i 7422	. . . . . . . . . . 11 ⊢ (𝐿 ↾_s ran 𝐺) = ((𝐸 ↾_s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ↾_s ran 𝐺)
50		ovex 7445	. . . . . . . . . . . 12 ⊢ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ V
51		ressabs 17201	. . . . . . . . . . . 12 ⊢ (((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ V ∧ ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴}))) → ((𝐸 ↾_s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ↾_s ran 𝐺) = (𝐸 ↾_s ran 𝐺))
52	50, 44, 51	sylancr 586	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 ↾_s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ↾_s ran 𝐺) = (𝐸 ↾_s ran 𝐺))
53	49, 52	eqtrid 2783	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿 ↾_s ran 𝐺) = (𝐸 ↾_s ran 𝐺))
54		eqid 2731	. . . . . . . . . . . . . . 15 ⊢ (0_g‘𝐿) = (0_g‘𝐿)
55	38	snssd 4812	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → {𝐴} ⊆ (Base‘𝐸))
56	8, 55	unssd 4186	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐹 ∪ {𝐴}) ⊆ (Base‘𝐸))
57	6, 45, 56	fldgensdrg 32689	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubDRing‘𝐸))
58		issdrg 20551	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubDRing‘𝐸) ↔ (𝐸 ∈ DivRing ∧ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ (𝐸 ↾_s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ∈ DivRing))
59	57, 58	sylib 217	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 ∈ DivRing ∧ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ (𝐸 ↾_s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ∈ DivRing))
60	59	simp2d 1142	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸))
61	15	resrhm2b 20496	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴}))) → (𝐺 ∈ (𝑃 RingHom 𝐸) ↔ 𝐺 ∈ (𝑃 RingHom 𝐿)))
62	61	biimpa 476	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴}))) ∧ 𝐺 ∈ (𝑃 RingHom 𝐸)) → 𝐺 ∈ (𝑃 RingHom 𝐿))
63	60, 44, 46, 62	syl21anc 835	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐺 ∈ (𝑃 RingHom 𝐿))
64		rhmghm 20379	. . . . . . . . . . . . . . . 16 ⊢ (𝐺 ∈ (𝑃 RingHom 𝐿) → 𝐺 ∈ (𝑃 GrpHom 𝐿))
65	63, 64	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺 ∈ (𝑃 GrpHom 𝐿))
66	54, 65, 25, 26, 27, 22, 24	ghmquskerco 32818	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺 = (𝐽 ∘ 𝑁))
67	66	rneqd 5937	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝐺 = ran (𝐽 ∘ 𝑁))
68	26	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑄 = (𝑃 /_s (𝑃 ~_QG 𝑍)))
69	22	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑈 = (Base‘𝑃))
70		ovexd 7447	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃 ~_QG 𝑍) ∈ V)
71	3	simp3d 1143	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸 ↾_s 𝐹) ∈ DivRing)
72	32, 71	ply1lvec 32927	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ LVec)
73	68, 69, 70, 72	qusbas 17498	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 / (𝑃 ~_QG 𝑍)) = (Base‘𝑄))
74		eqid 2731	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 / (𝑃 ~_QG 𝑍)) = (𝑈 / (𝑃 ~_QG 𝑍))
75	54	ghmker 19160	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 ∈ (𝑃 GrpHom 𝐿) → (^◡𝐺 “ {(0_g‘𝐿)}) ∈ (NrmSGrp‘𝑃))
76	65, 75	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (^◡𝐺 “ {(0_g‘𝐿)}) ∈ (NrmSGrp‘𝑃))
77	25, 76	eqeltrid 2836	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑍 ∈ (NrmSGrp‘𝑃))
78	22, 74, 24, 77	qusrn 32809	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ran 𝑁 = (𝑈 / (𝑃 ~_QG 𝑍)))
79		eqid 2731	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((subringAlg ‘𝐸)‘𝐹) = ((subringAlg ‘𝐸)‘𝐹)
80	20, 32, 6, 22, 36, 4, 38, 23, 79	evls1maplmhm 33064	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐺 ∈ (𝑃 LMHom ((subringAlg ‘𝐸)‘𝐹)))
81	80	elexd 3494	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐺 ∈ V)
82	81	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘𝑄)) → 𝐺 ∈ V)
83	82	imaexd 32186	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘𝑄)) → (𝐺 “ 𝑝) ∈ V)
84	83	uniexd 7736	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘𝑄)) → ∪ (𝐺 “ 𝑝) ∈ V)
85	27, 84	dmmptd 6695	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom 𝐽 = (Base‘𝑄))
86	73, 78, 85	3eqtr4rd 2782	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom 𝐽 = ran 𝑁)
87		rncoeq 5974	. . . . . . . . . . . . . 14 ⊢ (dom 𝐽 = ran 𝑁 → ran (𝐽 ∘ 𝑁) = ran 𝐽)
88	86, 87	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran (𝐽 ∘ 𝑁) = ran 𝐽)
89	67, 88	eqtrd 2771	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝐺 = ran 𝐽)
90	89	oveq2d 7428	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐿 ↾_s ran 𝐺) = (𝐿 ↾_s ran 𝐽))
91		eqid 2731	. . . . . . . . . . . 12 ⊢ (𝐿 ↾_s ran 𝐽) = (𝐿 ↾_s ran 𝐽)
92	9	subrgcrng 20469	. . . . . . . . . . . . . . 15 ⊢ ((𝐸 ∈ CRing ∧ 𝐹 ∈ (SubRing‘𝐸)) → 𝐾 ∈ CRing)
93	36, 4, 92	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ CRing)
94	21	ply1crng 21954	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ CRing → 𝑃 ∈ CRing)
95	93, 94	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ CRing)
96	54, 63, 25, 26, 27, 95	rhmquskerlem 32832	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ (𝑄 RingHom 𝐿))
97	20, 32, 6, 22, 36, 4, 38, 23	evls1maprnss 33065	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 ⊆ ran 𝐺)
98		eqid 2731	. . . . . . . . . . . . . . . . . 18 ⊢ (1_r‘𝐸) = (1_r‘𝐸)
99	9, 98	subrg1 20476	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (SubRing‘𝐸) → (1_r‘𝐸) = (1_r‘𝐾))
100	4, 99	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1_r‘𝐸) = (1_r‘𝐾))
101	98	subrg1cl 20474	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (SubRing‘𝐸) → (1_r‘𝐸) ∈ 𝐹)
102	4, 101	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1_r‘𝐸) ∈ 𝐹)
103	100, 102	eqeltrrd 2833	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1_r‘𝐾) ∈ 𝐹)
104	97, 103	sseldd 3983	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1_r‘𝐾) ∈ ran 𝐺)
105		drngnzr 20524	. . . . . . . . . . . . . . . . 17 ⊢ (𝐸 ∈ DivRing → 𝐸 ∈ NzRing)
106	98, 35	nzrnz 20410	. . . . . . . . . . . . . . . . 17 ⊢ (𝐸 ∈ NzRing → (1_r‘𝐸) ≠ (0_g‘𝐸))
107	45, 105, 106	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1_r‘𝐸) ≠ (0_g‘𝐸))
108	36	crnggrpd 20145	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐸 ∈ Grp)
109	108	grpmndd 18871	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐸 ∈ Mnd)
110		sdrgsubrg 20554	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubDRing‘𝐸) → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸))
111		subrgsubg 20471	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubGrp‘𝐸))
112	57, 110, 111	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubGrp‘𝐸))
113	35	subg0cl 19054	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubGrp‘𝐸) → (0_g‘𝐸) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})))
114	112, 113	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0_g‘𝐸) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})))
115	6, 45, 56	fldgenssv 32690	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ⊆ (Base‘𝐸))
116	15, 6, 35	ress0g 18690	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐸 ∈ Mnd ∧ (0_g‘𝐸) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∧ (𝐸 fldGen (𝐹 ∪ {𝐴})) ⊆ (Base‘𝐸)) → (0_g‘𝐸) = (0_g‘𝐿))
117	109, 114, 115, 116	syl3anc 1370	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0_g‘𝐸) = (0_g‘𝐿))
118	107, 100, 117	3netr3d 3016	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1_r‘𝐾) ≠ (0_g‘𝐿))
119		nelsn 4668	. . . . . . . . . . . . . . 15 ⊢ ((1_r‘𝐾) ≠ (0_g‘𝐿) → ¬ (1_r‘𝐾) ∈ {(0_g‘𝐿)})
120	118, 119	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ¬ (1_r‘𝐾) ∈ {(0_g‘𝐿)})
121		nelne1 3038	. . . . . . . . . . . . . 14 ⊢ (((1_r‘𝐾) ∈ ran 𝐺 ∧ ¬ (1_r‘𝐾) ∈ {(0_g‘𝐿)}) → ran 𝐺 ≠ {(0_g‘𝐿)})
122	104, 120, 121	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝐺 ≠ {(0_g‘𝐿)})
123	89, 122	eqnetrrd 3008	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝐽 ≠ {(0_g‘𝐿)})
124		eqid 2731	. . . . . . . . . . . . 13 ⊢ (opp_r‘𝑃) = (opp_r‘𝑃)
125	9	sdrgdrng 20553	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐾 ∈ DivRing)
126		drngnzr 20524	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ DivRing → 𝐾 ∈ NzRing)
127	1, 125, 126	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ NzRing)
128	21	ply1nz 25888	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ NzRing → 𝑃 ∈ NzRing)
129	127, 128	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ NzRing)
130		eqid 2731	. . . . . . . . . . . . . . . 16 ⊢ {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0_g‘𝐸)} = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0_g‘𝐸)}
131		eqid 2731	. . . . . . . . . . . . . . . 16 ⊢ (RSpan‘𝑃) = (RSpan‘𝑃)
132	9	fveq2i 6894	. . . . . . . . . . . . . . . 16 ⊢ (idlGen_1p‘𝐾) = (idlGen_1p‘(𝐸 ↾_s 𝐹))
133	20, 32, 6, 18, 1, 38, 35, 130, 131, 132	ply1annig1p 33069	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0_g‘𝐸)} = ((RSpan‘𝑃)‘{((idlGen_1p‘𝐾)‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0_g‘𝐸)})}))
134	117	sneqd 4640	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → {(0_g‘𝐸)} = {(0_g‘𝐿)})
135	134	imaeq2d 6059	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (^◡𝐺 “ {(0_g‘𝐸)}) = (^◡𝐺 “ {(0_g‘𝐿)}))
136	25, 135	eqtr4id 2790	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑍 = (^◡𝐺 “ {(0_g‘𝐸)}))
137	22	mpteq1i 5244	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴)) = (𝑝 ∈ (Base‘𝑃) ↦ ((𝑂‘𝑝)‘𝐴))
138	23, 137	eqtri 2759	. . . . . . . . . . . . . . . . 17 ⊢ 𝐺 = (𝑝 ∈ (Base‘𝑃) ↦ ((𝑂‘𝑝)‘𝐴))
139	20, 32, 6, 36, 4, 38, 35, 130, 138	ply1annidllem 33066	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0_g‘𝐸)} = (^◡𝐺 “ {(0_g‘𝐸)}))
140	136, 139	eqtr4d 2774	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑍 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0_g‘𝐸)})
141		eqid 2731	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐸 minPoly 𝐹) = (𝐸 minPoly 𝐹)
142	20, 32, 6, 18, 1, 38, 35, 130, 131, 132, 141	minplyval 33070	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) = ((idlGen_1p‘𝐾)‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0_g‘𝐸)}))
143	142	sneqd 4640	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {((𝐸 minPoly 𝐹)‘𝐴)} = {((idlGen_1p‘𝐾)‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0_g‘𝐸)})})
144	143	fveq2d 6895	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) = ((RSpan‘𝑃)‘{((idlGen_1p‘𝐾)‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0_g‘𝐸)})}))
145	133, 140, 144	3eqtr4d 2781	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑍 = ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}))
146		eqid 2731	. . . . . . . . . . . . . . . 16 ⊢ (0_g‘𝑃) = (0_g‘𝑃)
147		eqid 2731	. . . . . . . . . . . . . . . . . 18 ⊢ (0_g‘(Poly₁‘𝐸)) = (0_g‘(Poly₁‘𝐸))
148	147, 18, 1, 141, 19	irngnminplynz 33075	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ≠ (0_g‘(Poly₁‘𝐸)))
149		eqid 2731	. . . . . . . . . . . . . . . . . 18 ⊢ (Poly₁‘𝐸) = (Poly₁‘𝐸)
150	149, 9, 21, 22, 4, 147	ressply10g 32945	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0_g‘(Poly₁‘𝐸)) = (0_g‘𝑃))
151	148, 150	neeqtrd 3009	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ≠ (0_g‘𝑃))
152	20, 32, 6, 18, 1, 38, 141, 146, 151	minplyirred 33074	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ∈ (Irred‘𝑃))
153		eqid 2731	. . . . . . . . . . . . . . . 16 ⊢ ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) = ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)})
154		fldsdrgfld 20561	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ (SubDRing‘𝐸)) → (𝐸 ↾_s 𝐹) ∈ Field)
155	18, 1, 154	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 ↾_s 𝐹) ∈ Field)
156	9, 155	eqeltrid 2836	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 ∈ Field)
157	21	ply1pid 25946	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ Field → 𝑃 ∈ PID)
158	156, 157	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ PID)
159	20, 32, 6, 18, 1, 38, 35, 130, 131, 132, 141	minplycl 33071	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ∈ (Base‘𝑃))
160	159, 22	eleqtrrdi 2843	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ∈ 𝑈)
161	95	crngringd 20144	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ Ring)
162	160	snssd 4812	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → {((𝐸 minPoly 𝐹)‘𝐴)} ⊆ 𝑈)
163		eqid 2731	. . . . . . . . . . . . . . . . . 18 ⊢ (LIdeal‘𝑃) = (LIdeal‘𝑃)
164	131, 22, 163	rspcl 21000	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ Ring ∧ {((𝐸 minPoly 𝐹)‘𝐴)} ⊆ 𝑈) → ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) ∈ (LIdeal‘𝑃))
165	161, 162, 164	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) ∈ (LIdeal‘𝑃))
166	22, 131, 146, 153, 158, 160, 151, 165	mxidlirred 32877	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) ∈ (MaxIdeal‘𝑃) ↔ ((𝐸 minPoly 𝐹)‘𝐴) ∈ (Irred‘𝑃)))
167	152, 166	mpbird 257	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) ∈ (MaxIdeal‘𝑃))
168	145, 167	eqeltrd 2832	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑍 ∈ (MaxIdeal‘𝑃))
169		eqid 2731	. . . . . . . . . . . . . . . 16 ⊢ (MaxIdeal‘𝑃) = (MaxIdeal‘𝑃)
170	169, 124	crngmxidl 32874	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ CRing → (MaxIdeal‘𝑃) = (MaxIdeal‘(opp_r‘𝑃)))
171	95, 170	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (MaxIdeal‘𝑃) = (MaxIdeal‘(opp_r‘𝑃)))
172	168, 171	eleqtrd 2834	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑍 ∈ (MaxIdeal‘(opp_r‘𝑃)))
173	124, 26, 129, 168, 172	qsdrngi 32898	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∈ DivRing)
174	91, 54, 96, 123, 173	rndrhmcl 32681	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐿 ↾_s ran 𝐽) ∈ DivRing)
175	90, 174	eqeltrd 2832	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿 ↾_s ran 𝐺) ∈ DivRing)
176	53, 175	eqeltrrd 2833	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 ↾_s ran 𝐺) ∈ DivRing)
177		issdrg 20551	. . . . . . . . 9 ⊢ (ran 𝐺 ∈ (SubDRing‘𝐸) ↔ (𝐸 ∈ DivRing ∧ ran 𝐺 ∈ (SubRing‘𝐸) ∧ (𝐸 ↾_s ran 𝐺) ∈ DivRing))
178	45, 48, 176, 177	syl3anbrc 1342	. . . . . . . 8 ⊢ (𝜑 → ran 𝐺 ∈ (SubDRing‘𝐸))
179		fveq2 6891	. . . . . . . . . . . . . 14 ⊢ (𝑝 = (var₁‘𝐾) → (𝑂‘𝑝) = (𝑂‘(var₁‘𝐾)))
180	179	fveq1d 6893	. . . . . . . . . . . . 13 ⊢ (𝑝 = (var₁‘𝐾) → ((𝑂‘𝑝)‘𝐴) = ((𝑂‘(var₁‘𝐾))‘𝐴))
181	180	eqeq2d 2742	. . . . . . . . . . . 12 ⊢ (𝑝 = (var₁‘𝐾) → (𝐴 = ((𝑂‘𝑝)‘𝐴) ↔ 𝐴 = ((𝑂‘(var₁‘𝐾))‘𝐴)))
182	9, 71	eqeltrid 2836	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ DivRing)
183	182	drngringd 20512	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐾 ∈ Ring)
184		eqid 2731	. . . . . . . . . . . . . 14 ⊢ (var₁‘𝐾) = (var₁‘𝐾)
185	184, 21, 22	vr1cl 21973	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ Ring → (var₁‘𝐾) ∈ 𝑈)
186	183, 185	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (var₁‘𝐾) ∈ 𝑈)
187	20, 184, 9, 6, 36, 4	evls1var 22090	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑂‘(var₁‘𝐾)) = ( I ↾ (Base‘𝐸)))
188	187	fveq1d 6893	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑂‘(var₁‘𝐾))‘𝐴) = (( I ↾ (Base‘𝐸))‘𝐴))
189		fvresi 7173	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (Base‘𝐸) → (( I ↾ (Base‘𝐸))‘𝐴) = 𝐴)
190	38, 189	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (( I ↾ (Base‘𝐸))‘𝐴) = 𝐴)
191	188, 190	eqtr2d 2772	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 = ((𝑂‘(var₁‘𝐾))‘𝐴))
192	181, 186, 191	rspcedvdw 3615	. . . . . . . . . . 11 ⊢ (𝜑 → ∃𝑝 ∈ 𝑈 𝐴 = ((𝑂‘𝑝)‘𝐴))
193	23, 192, 19	elrnmptd 5960	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ran 𝐺)
194	193	snssd 4812	. . . . . . . . 9 ⊢ (𝜑 → {𝐴} ⊆ ran 𝐺)
195	97, 194	unssd 4186	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ∪ {𝐴}) ⊆ ran 𝐺)
196	6, 45, 178, 195	fldgenssp 32693	. . . . . . 7 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ⊆ ran 𝐺)
197	44, 196	eqssd 3999	. . . . . 6 ⊢ (𝜑 → ran 𝐺 = (𝐸 fldGen (𝐹 ∪ {𝐴})))
198	15, 6	ressbas2 17189	. . . . . . 7 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ⊆ (Base‘𝐸) → (𝐸 fldGen (𝐹 ∪ {𝐴})) = (Base‘𝐿))
199	115, 198	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) = (Base‘𝐿))
200		eqidd 2732	. . . . . . 7 ⊢ (𝜑 → ((subringAlg ‘𝐿)‘𝐹) = ((subringAlg ‘𝐿)‘𝐹))
201	6, 45, 56	fldgenssid 32688	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 ∪ {𝐴}) ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))
202	201	unssad 4187	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))
203	202, 199	sseqtrd 4022	. . . . . . 7 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐿))
204	200, 203	srabase 20941	. . . . . 6 ⊢ (𝜑 → (Base‘𝐿) = (Base‘((subringAlg ‘𝐿)‘𝐹)))
205	197, 199, 204	3eqtrd 2775	. . . . 5 ⊢ (𝜑 → ran 𝐺 = (Base‘((subringAlg ‘𝐿)‘𝐹)))
206		imaeq2 6055	. . . . . . 7 ⊢ (𝑞 = 𝑝 → (𝐺 “ 𝑞) = (𝐺 “ 𝑝))
207	206	unieqd 4922	. . . . . 6 ⊢ (𝑞 = 𝑝 → ∪ (𝐺 “ 𝑞) = ∪ (𝐺 “ 𝑝))
208	207	cbvmptv 5261	. . . . 5 ⊢ (𝑞 ∈ (Base‘(𝑃 /_s (𝑃 ~_QG (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺 “ 𝑞)) = (𝑝 ∈ (Base‘(𝑃 /_s (𝑃 ~_QG (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺 “ 𝑝))
209	14, 28, 29, 30, 205, 208	lmhmqusker 32823	. . . 4 ⊢ (𝜑 → (𝑞 ∈ (Base‘(𝑃 /_s (𝑃 ~_QG (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺 “ 𝑞)) ∈ ((𝑃 /_s (𝑃 ~_QG (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))}))) LMIso ((subringAlg ‘𝐿)‘𝐹)))
210		eqidd 2732	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘𝐿) = (0_g‘𝐿))
211	200, 210, 203	sralmod0 20959	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0_g‘𝐿) = (0_g‘((subringAlg ‘𝐿)‘𝐹)))
212	211	sneqd 4640	. . . . . . . . . . . 12 ⊢ (𝜑 → {(0_g‘𝐿)} = {(0_g‘((subringAlg ‘𝐿)‘𝐹))})
213	212	imaeq2d 6059	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐺 “ {(0_g‘𝐿)}) = (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))}))
214	25, 213	eqtrid 2783	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 = (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))}))
215	214	oveq2d 7428	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 ~_QG 𝑍) = (𝑃 ~_QG (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))})))
216	215	oveq2d 7428	. . . . . . . 8 ⊢ (𝜑 → (𝑃 /_s (𝑃 ~_QG 𝑍)) = (𝑃 /_s (𝑃 ~_QG (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))}))))
217	26, 216	eqtrid 2783	. . . . . . 7 ⊢ (𝜑 → 𝑄 = (𝑃 /_s (𝑃 ~_QG (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))}))))
218	217	fveq2d 6895	. . . . . 6 ⊢ (𝜑 → (Base‘𝑄) = (Base‘(𝑃 /_s (𝑃 ~_QG (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))})))))
219	218	mpteq1d 5243	. . . . 5 ⊢ (𝜑 → (𝑝 ∈ (Base‘𝑄) ↦ ∪ (𝐺 “ 𝑝)) = (𝑝 ∈ (Base‘(𝑃 /_s (𝑃 ~_QG (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺 “ 𝑝)))
220	219, 27, 208	3eqtr4g 2796	. . . 4 ⊢ (𝜑 → 𝐽 = (𝑞 ∈ (Base‘(𝑃 /_s (𝑃 ~_QG (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺 “ 𝑞)))
221	217	oveq1d 7427	. . . 4 ⊢ (𝜑 → (𝑄 LMIso ((subringAlg ‘𝐿)‘𝐹)) = ((𝑃 /_s (𝑃 ~_QG (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))}))) LMIso ((subringAlg ‘𝐿)‘𝐹)))
222	209, 220, 221	3eltr4d 2847	. . 3 ⊢ (𝜑 → 𝐽 ∈ (𝑄 LMIso ((subringAlg ‘𝐿)‘𝐹)))
223	9, 15, 16, 17, 18, 1, 19, 20, 21, 22, 23, 24, 25, 26, 27	algextdeglem3 33079	. . 3 ⊢ (𝜑 → 𝑄 ∈ LVec)
224	222, 223	lmimdim 32991	. 2 ⊢ (𝜑 → (dim‘𝑄) = (dim‘((subringAlg ‘𝐿)‘𝐹)))
225	6, 18, 56	fldgenfld 32695	. . . . 5 ⊢ (𝜑 → (𝐸 ↾_s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ∈ Field)
226	15, 225	eqeltrid 2836	. . . 4 ⊢ (𝜑 → 𝐿 ∈ Field)
227	9, 15, 16, 17, 18, 1, 19	algextdeglem1 33077	. . . . 5 ⊢ (𝜑 → (𝐿 ↾_s 𝐹) = 𝐾)
228	11	oveq2d 7428	. . . . 5 ⊢ (𝜑 → (𝐿 ↾_s 𝐹) = (𝐿 ↾_s (Base‘𝐾)))
229	227, 228	eqtr3d 2773	. . . 4 ⊢ (𝜑 → 𝐾 = (𝐿 ↾_s (Base‘𝐾)))
230	15	subsubrg 20492	. . . . . . 7 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) → (𝐹 ∈ (SubRing‘𝐿) ↔ (𝐹 ∈ (SubRing‘𝐸) ∧ 𝐹 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))))
231	230	biimpar 477	. . . . . 6 ⊢ (((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ (𝐹 ∈ (SubRing‘𝐸) ∧ 𝐹 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))) → 𝐹 ∈ (SubRing‘𝐿))
232	60, 4, 202, 231	syl12anc 834	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐿))
233	11, 232	eqeltrrd 2833	. . . 4 ⊢ (𝜑 → (Base‘𝐾) ∈ (SubRing‘𝐿))
234		brfldext 33029	. . . . 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 836	. . 3 ⊢ (𝜑 → 𝐿/_FldExt𝐾)
237		extdgval 33036	. . 3 ⊢ (𝐿/_FldExt𝐾 → (𝐿[:]𝐾) = (dim‘((subringAlg ‘𝐿)‘(Base‘𝐾))))
238	236, 237	syl 17	. 2 ⊢ (𝜑 → (𝐿[:]𝐾) = (dim‘((subringAlg ‘𝐿)‘(Base‘𝐾))))
239	13, 224, 238	3eqtr4d 2781	1 ⊢ (𝜑 → (dim‘𝑄) = (𝐿[:]𝐾))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2105 ≠ wne 2939 ∀wral 3060 {crab 3431 Vcvv 3473 ∪ cun 3946 ⊆ wss 3948 {csn 4628 ∪ cuni 4908 class class class wbr 5148 ↦ cmpt 5231 I cid 5573 ^◡ccnv 5675 dom cdm 5676 ran crn 5677 ↾ cres 5678 “ cima 5679 ∘ ccom 5680 ‘cfv 6543 (class class class)co 7412 [cec 8707 / cqs 8708 Basecbs 17151 ↾_s cress 17180 0_gc0g 17392 /_s cqus 17458 Mndcmnd 18662 SubGrpcsubg 19040 NrmSGrpcnsg 19041 ~_QG cqg 19042 GrpHom cghm 19131 1_rcur 20079 Ringcrg 20131 CRingccrg 20132 opp_rcoppr 20228 Irredcir 20251 RingHom crh 20364 NzRingcnzr 20407 SubRingcsubrg 20461 DivRingcdr 20504 Fieldcfield 20505 SubDRingcsdrg 20549 LMHom clmhm 20778 LMIso clmim 20779 LVecclvec 20861 subringAlg csra 20930 LIdealclidl 20932 RSpancrsp 20933 PIDcpid 21102 var₁cv1 21932 Poly₁cpl1 21933 evalSub₁ ces1 22065 deg₁ cdg1 25818 idlGen_1pcig1p 25896 fldGen cfldgen 32685 MaxIdealcmxidl 32864 dimcldim 32986 /_FldExtcfldext 33020 [:]cextdg 33023 IntgRing cirng 33051 minPoly cminply 33060

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7729 ax-reg 9593 ax-inf2 9642 ax-ac2 10464 ax-cnex 11172 ax-resscn 11173 ax-1cn 11174 ax-icn 11175 ax-addcl 11176 ax-addrcl 11177 ax-mulcl 11178 ax-mulrcl 11179 ax-mulcom 11180 ax-addass 11181 ax-mulass 11182 ax-distr 11183 ax-i2m1 11184 ax-1ne0 11185 ax-1rid 11186 ax-rnegex 11187 ax-rrecex 11188 ax-cnre 11189 ax-pre-lttri 11190 ax-pre-lttrn 11191 ax-pre-ltadd 11192 ax-pre-mulgt0 11193 ax-pre-sup 11194 ax-addf 11195 ax-mulf 11196

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3375 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-tp 4633 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-iin 5000 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-se 5632 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7368 df-ov 7415 df-oprab 7416 df-mpo 7417 df-of 7674 df-ofr 7675 df-rpss 7717 df-om 7860 df-1st 7979 df-2nd 7980 df-supp 8152 df-tpos 8217 df-frecs 8272 df-wrecs 8303 df-recs 8377 df-rdg 8416 df-1o 8472 df-2o 8473 df-oadd 8476 df-er 8709 df-ec 8711 df-qs 8715 df-map 8828 df-pm 8829 df-ixp 8898 df-en 8946 df-dom 8947 df-sdom 8948 df-fin 8949 df-fsupp 9368 df-sup 9443 df-inf 9444 df-oi 9511 df-r1 9765 df-rank 9766 df-dju 9902 df-card 9940 df-acn 9943 df-ac 10117 df-pnf 11257 df-mnf 11258 df-xr 11259 df-ltxr 11260 df-le 11261 df-sub 11453 df-neg 11454 df-nn 12220 df-2 12282 df-3 12283 df-4 12284 df-5 12285 df-6 12286 df-7 12287 df-8 12288 df-9 12289 df-n0 12480 df-xnn0 12552 df-z 12566 df-dec 12685 df-uz 12830 df-fz 13492 df-fzo 13635 df-seq 13974 df-hash 14298 df-struct 17087 df-sets 17104 df-slot 17122 df-ndx 17134 df-base 17152 df-ress 17181 df-plusg 17217 df-mulr 17218 df-starv 17219 df-sca 17220 df-vsca 17221 df-ip 17222 df-tset 17223 df-ple 17224 df-ocomp 17225 df-ds 17226 df-unif 17227 df-hom 17228 df-cco 17229 df-0g 17394 df-gsum 17395 df-prds 17400 df-pws 17402 df-imas 17461 df-qus 17462 df-mre 17537 df-mrc 17538 df-mri 17539 df-acs 17540 df-proset 18255 df-drs 18256 df-poset 18273 df-ipo 18488 df-mgm 18568 df-sgrp 18647 df-mnd 18663 df-mhm 18708 df-submnd 18709 df-grp 18861 df-minusg 18862 df-sbg 18863 df-mulg 18991 df-subg 19043 df-nsg 19044 df-eqg 19045 df-ghm 19132 df-gim 19177 df-cntz 19226 df-oppg 19255 df-lsm 19549 df-cmn 19695 df-abl 19696 df-mgp 20033 df-rng 20051 df-ur 20080 df-srg 20085 df-ring 20133 df-cring 20134 df-oppr 20229 df-dvdsr 20252 df-unit 20253 df-irred 20254 df-invr 20283 df-dvr 20296 df-rhm 20367 df-nzr 20408 df-subrng 20438 df-subrg 20463 df-drng 20506 df-field 20507 df-sdrg 20550 df-lmod 20620 df-lss 20691 df-lsp 20731 df-lmhm 20781 df-lmim 20782 df-lbs 20834 df-lvec 20862 df-sra 20934 df-rgmod 20935 df-lidl 20936 df-rsp 20937 df-2idl 21010 df-lpidl 21085 df-lpir 21086 df-rlreg 21103 df-domn 21104 df-idom 21105 df-pid 21106 df-cnfld 21149 df-dsmm 21510 df-frlm 21525 df-uvc 21561 df-lindf 21584 df-linds 21585 df-assa 21631 df-asp 21632 df-ascl 21633 df-psr 21685 df-mvr 21686 df-mpl 21687 df-opsr 21689 df-evls 21859 df-evl 21860 df-psr1 21936 df-vr1 21937 df-ply1 21938 df-coe1 21939 df-evls1 22067 df-evl1 22068 df-mdeg 25819 df-deg1 25820 df-mon1 25897 df-uc1p 25898 df-q1p 25899 df-r1p 25900 df-ig1p 25901 df-fldgen 32686 df-mxidl 32865 df-dim 32987 df-fldext 33024 df-extdg 33025 df-irng 33052 df-minply 33061

This theorem is referenced by: algextdeg 33085

W3C validator