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 33065

Description: Lemma for algextdeg 33070. (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 20547	. . . . . . . 8 ⊢ (𝐹 ∈ (SubDRing‘𝐸) ↔ (𝐸 ∈ DivRing ∧ 𝐹 ∈ (SubRing‘𝐸) ∧ (𝐸 ↾_s 𝐹) ∈ DivRing))
3	1, 2	sylib 217	. . . . . . 7 ⊢ (𝜑 → (𝐸 ∈ DivRing ∧ 𝐹 ∈ (SubRing‘𝐸) ∧ (𝐸 ↾_s 𝐹) ∈ DivRing))
4	3	simp2d 1141	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸))
5		subrgsubg 20467	. . . . . 6 ⊢ (𝐹 ∈ (SubRing‘𝐸) → 𝐹 ∈ (SubGrp‘𝐸))
6		eqid 2730	. . . . . . 7 ⊢ (Base‘𝐸) = (Base‘𝐸)
7	6	subgss 19043	. . . . . 6 ⊢ (𝐹 ∈ (SubGrp‘𝐸) → 𝐹 ⊆ (Base‘𝐸))
8	4, 5, 7	3syl 18	. . . . 5 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐸))
9		algextdeg.k	. . . . . 6 ⊢ 𝐾 = (𝐸 ↾_s 𝐹)
10	9, 6	ressbas2 17186	. . . . 5 ⊢ (𝐹 ⊆ (Base‘𝐸) → 𝐹 = (Base‘𝐾))
11	8, 10	syl 17	. . . 4 ⊢ (𝜑 → 𝐹 = (Base‘𝐾))
12	11	fveq2d 6894	. . 3 ⊢ (𝜑 → ((subringAlg ‘𝐿)‘𝐹) = ((subringAlg ‘𝐿)‘(Base‘𝐾)))
13	12	fveq2d 6894	. 2 ⊢ (𝜑 → (dim‘((subringAlg ‘𝐿)‘𝐹)) = (dim‘((subringAlg ‘𝐿)‘(Base‘𝐾))))
14		eqid 2730	. . . . 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 33063	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ (𝑃 LMHom ((subringAlg ‘𝐿)‘𝐹)))
29		eqid 2730	. . . . 5 ⊢ (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))}) = (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))})
30		eqid 2730	. . . . 5 ⊢ (𝑃 /_s (𝑃 ~_QG (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))}))) = (𝑃 /_s (𝑃 ~_QG (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))})))
31	9	fveq2i 6893	. . . . . . . . . . 11 ⊢ (Poly₁‘𝐾) = (Poly₁‘(𝐸 ↾_s 𝐹))
32	21, 31	eqtri 2758	. . . . . . . . . 10 ⊢ 𝑃 = (Poly₁‘(𝐸 ↾_s 𝐹))
33	18	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝐸 ∈ Field)
34	1	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝐹 ∈ (SubDRing‘𝐸))
35		eqid 2730	. . . . . . . . . . . . 13 ⊢ (0_g‘𝐸) = (0_g‘𝐸)
36	18	fldcrngd 20513	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸 ∈ CRing)
37	20, 9, 6, 35, 36, 4	irngssv 33041	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸 IntgRing 𝐹) ⊆ (Base‘𝐸))
38	37, 19	sseldd 3982	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ (Base‘𝐸))
39	38	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝐴 ∈ (Base‘𝐸))
40		simpr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝑝 ∈ 𝑈)
41	6, 20, 32, 22, 33, 34, 39, 40	evls1fldgencl 33033	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → ((𝑂‘𝑝)‘𝐴) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})))
42	41	ralrimiva 3144	. . . . . . . 8 ⊢ (𝜑 → ∀𝑝 ∈ 𝑈 ((𝑂‘𝑝)‘𝐴) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})))
43	23	rnmptss 7123	. . . . . . . 8 ⊢ (∀𝑝 ∈ 𝑈 ((𝑂‘𝑝)‘𝐴) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})) → ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))
44	42, 43	syl 17	. . . . . . 7 ⊢ (𝜑 → ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))
45	18	flddrngd 20512	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ DivRing)
46	20, 32, 6, 22, 36, 4, 38, 23	evls1maprhm 33048	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ (𝑃 RingHom 𝐸))
47		rnrhmsubrg 20495	. . . . . . . . . 10 ⊢ (𝐺 ∈ (𝑃 RingHom 𝐸) → ran 𝐺 ∈ (SubRing‘𝐸))
48	46, 47	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐺 ∈ (SubRing‘𝐸))
49	15	oveq1i 7421	. . . . . . . . . . 11 ⊢ (𝐿 ↾_s ran 𝐺) = ((𝐸 ↾_s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ↾_s ran 𝐺)
50		ovex 7444	. . . . . . . . . . . 12 ⊢ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ V
51		ressabs 17198	. . . . . . . . . . . 12 ⊢ (((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ V ∧ ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴}))) → ((𝐸 ↾_s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ↾_s ran 𝐺) = (𝐸 ↾_s ran 𝐺))
52	50, 44, 51	sylancr 585	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 ↾_s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ↾_s ran 𝐺) = (𝐸 ↾_s ran 𝐺))
53	49, 52	eqtrid 2782	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿 ↾_s ran 𝐺) = (𝐸 ↾_s ran 𝐺))
54		eqid 2730	. . . . . . . . . . . . . . 15 ⊢ (0_g‘𝐿) = (0_g‘𝐿)
55	38	snssd 4811	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → {𝐴} ⊆ (Base‘𝐸))
56	8, 55	unssd 4185	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐹 ∪ {𝐴}) ⊆ (Base‘𝐸))
57	6, 45, 56	fldgensdrg 32674	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubDRing‘𝐸))
58		issdrg 20547	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubDRing‘𝐸) ↔ (𝐸 ∈ DivRing ∧ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ (𝐸 ↾_s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ∈ DivRing))
59	57, 58	sylib 217	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 ∈ DivRing ∧ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ (𝐸 ↾_s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ∈ DivRing))
60	59	simp2d 1141	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸))
61	15	resrhm2b 20492	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴}))) → (𝐺 ∈ (𝑃 RingHom 𝐸) ↔ 𝐺 ∈ (𝑃 RingHom 𝐿)))
62	61	biimpa 475	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴}))) ∧ 𝐺 ∈ (𝑃 RingHom 𝐸)) → 𝐺 ∈ (𝑃 RingHom 𝐿))
63	60, 44, 46, 62	syl21anc 834	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐺 ∈ (𝑃 RingHom 𝐿))
64		rhmghm 20375	. . . . . . . . . . . . . . . 16 ⊢ (𝐺 ∈ (𝑃 RingHom 𝐿) → 𝐺 ∈ (𝑃 GrpHom 𝐿))
65	63, 64	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺 ∈ (𝑃 GrpHom 𝐿))
66	54, 65, 25, 26, 27, 22, 24	ghmquskerco 32803	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺 = (𝐽 ∘ 𝑁))
67	66	rneqd 5936	. . . . . . . . . . . . 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 1142	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸 ↾_s 𝐹) ∈ DivRing)
72	32, 71	ply1lvec 32912	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ LVec)
73	68, 69, 70, 72	qusbas 17495	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 / (𝑃 ~_QG 𝑍)) = (Base‘𝑄))
74		eqid 2730	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 / (𝑃 ~_QG 𝑍)) = (𝑈 / (𝑃 ~_QG 𝑍))
75	54	ghmker 19156	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 ∈ (𝑃 GrpHom 𝐿) → (^◡𝐺 “ {(0_g‘𝐿)}) ∈ (NrmSGrp‘𝑃))
76	65, 75	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (^◡𝐺 “ {(0_g‘𝐿)}) ∈ (NrmSGrp‘𝑃))
77	25, 76	eqeltrid 2835	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑍 ∈ (NrmSGrp‘𝑃))
78	22, 74, 24, 77	qusrn 32794	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ran 𝑁 = (𝑈 / (𝑃 ~_QG 𝑍)))
79		eqid 2730	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((subringAlg ‘𝐸)‘𝐹) = ((subringAlg ‘𝐸)‘𝐹)
80	20, 32, 6, 22, 36, 4, 38, 23, 79	evls1maplmhm 33049	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐺 ∈ (𝑃 LMHom ((subringAlg ‘𝐸)‘𝐹)))
81	80	elexd 3493	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐺 ∈ V)
82	81	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘𝑄)) → 𝐺 ∈ V)
83	82	imaexd 32171	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘𝑄)) → (𝐺 “ 𝑝) ∈ V)
84	83	uniexd 7734	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘𝑄)) → ∪ (𝐺 “ 𝑝) ∈ V)
85	27, 84	dmmptd 6694	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom 𝐽 = (Base‘𝑄))
86	73, 78, 85	3eqtr4rd 2781	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom 𝐽 = ran 𝑁)
87		rncoeq 5973	. . . . . . . . . . . . . 14 ⊢ (dom 𝐽 = ran 𝑁 → ran (𝐽 ∘ 𝑁) = ran 𝐽)
88	86, 87	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran (𝐽 ∘ 𝑁) = ran 𝐽)
89	67, 88	eqtrd 2770	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝐺 = ran 𝐽)
90	89	oveq2d 7427	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐿 ↾_s ran 𝐺) = (𝐿 ↾_s ran 𝐽))
91		eqid 2730	. . . . . . . . . . . 12 ⊢ (𝐿 ↾_s ran 𝐽) = (𝐿 ↾_s ran 𝐽)
92	9	subrgcrng 20465	. . . . . . . . . . . . . . 15 ⊢ ((𝐸 ∈ CRing ∧ 𝐹 ∈ (SubRing‘𝐸)) → 𝐾 ∈ CRing)
93	36, 4, 92	syl2anc 582	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ CRing)
94	21	ply1crng 21941	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ CRing → 𝑃 ∈ CRing)
95	93, 94	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ CRing)
96	54, 63, 25, 26, 27, 95	rhmquskerlem 32817	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ (𝑄 RingHom 𝐿))
97	20, 32, 6, 22, 36, 4, 38, 23	evls1maprnss 33050	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 ⊆ ran 𝐺)
98		eqid 2730	. . . . . . . . . . . . . . . . . 18 ⊢ (1_r‘𝐸) = (1_r‘𝐸)
99	9, 98	subrg1 20472	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (SubRing‘𝐸) → (1_r‘𝐸) = (1_r‘𝐾))
100	4, 99	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1_r‘𝐸) = (1_r‘𝐾))
101	98	subrg1cl 20470	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (SubRing‘𝐸) → (1_r‘𝐸) ∈ 𝐹)
102	4, 101	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1_r‘𝐸) ∈ 𝐹)
103	100, 102	eqeltrrd 2832	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1_r‘𝐾) ∈ 𝐹)
104	97, 103	sseldd 3982	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1_r‘𝐾) ∈ ran 𝐺)
105		drngnzr 20520	. . . . . . . . . . . . . . . . 17 ⊢ (𝐸 ∈ DivRing → 𝐸 ∈ NzRing)
106	98, 35	nzrnz 20406	. . . . . . . . . . . . . . . . 17 ⊢ (𝐸 ∈ NzRing → (1_r‘𝐸) ≠ (0_g‘𝐸))
107	45, 105, 106	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1_r‘𝐸) ≠ (0_g‘𝐸))
108	36	crnggrpd 20141	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐸 ∈ Grp)
109	108	grpmndd 18868	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐸 ∈ Mnd)
110		sdrgsubrg 20550	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubDRing‘𝐸) → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸))
111		subrgsubg 20467	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubGrp‘𝐸))
112	57, 110, 111	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubGrp‘𝐸))
113	35	subg0cl 19050	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubGrp‘𝐸) → (0_g‘𝐸) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})))
114	112, 113	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0_g‘𝐸) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})))
115	6, 45, 56	fldgenssv 32675	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ⊆ (Base‘𝐸))
116	15, 6, 35	ress0g 18687	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐸 ∈ Mnd ∧ (0_g‘𝐸) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∧ (𝐸 fldGen (𝐹 ∪ {𝐴})) ⊆ (Base‘𝐸)) → (0_g‘𝐸) = (0_g‘𝐿))
117	109, 114, 115, 116	syl3anc 1369	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0_g‘𝐸) = (0_g‘𝐿))
118	107, 100, 117	3netr3d 3015	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1_r‘𝐾) ≠ (0_g‘𝐿))
119		nelsn 4667	. . . . . . . . . . . . . . 15 ⊢ ((1_r‘𝐾) ≠ (0_g‘𝐿) → ¬ (1_r‘𝐾) ∈ {(0_g‘𝐿)})
120	118, 119	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ¬ (1_r‘𝐾) ∈ {(0_g‘𝐿)})
121		nelne1 3037	. . . . . . . . . . . . . 14 ⊢ (((1_r‘𝐾) ∈ ran 𝐺 ∧ ¬ (1_r‘𝐾) ∈ {(0_g‘𝐿)}) → ran 𝐺 ≠ {(0_g‘𝐿)})
122	104, 120, 121	syl2anc 582	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝐺 ≠ {(0_g‘𝐿)})
123	89, 122	eqnetrrd 3007	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝐽 ≠ {(0_g‘𝐿)})
124		eqid 2730	. . . . . . . . . . . . 13 ⊢ (opp_r‘𝑃) = (opp_r‘𝑃)
125	9	sdrgdrng 20549	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐾 ∈ DivRing)
126		drngnzr 20520	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ DivRing → 𝐾 ∈ NzRing)
127	1, 125, 126	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ NzRing)
128	21	ply1nz 25874	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ NzRing → 𝑃 ∈ NzRing)
129	127, 128	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ NzRing)
130		eqid 2730	. . . . . . . . . . . . . . . 16 ⊢ {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0_g‘𝐸)} = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0_g‘𝐸)}
131		eqid 2730	. . . . . . . . . . . . . . . 16 ⊢ (RSpan‘𝑃) = (RSpan‘𝑃)
132	9	fveq2i 6893	. . . . . . . . . . . . . . . 16 ⊢ (idlGen_1p‘𝐾) = (idlGen_1p‘(𝐸 ↾_s 𝐹))
133	20, 32, 6, 18, 1, 38, 35, 130, 131, 132	ply1annig1p 33054	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0_g‘𝐸)} = ((RSpan‘𝑃)‘{((idlGen_1p‘𝐾)‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0_g‘𝐸)})}))
134	117	sneqd 4639	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → {(0_g‘𝐸)} = {(0_g‘𝐿)})
135	134	imaeq2d 6058	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (^◡𝐺 “ {(0_g‘𝐸)}) = (^◡𝐺 “ {(0_g‘𝐿)}))
136	25, 135	eqtr4id 2789	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑍 = (^◡𝐺 “ {(0_g‘𝐸)}))
137	22	mpteq1i 5243	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴)) = (𝑝 ∈ (Base‘𝑃) ↦ ((𝑂‘𝑝)‘𝐴))
138	23, 137	eqtri 2758	. . . . . . . . . . . . . . . . 17 ⊢ 𝐺 = (𝑝 ∈ (Base‘𝑃) ↦ ((𝑂‘𝑝)‘𝐴))
139	20, 32, 6, 36, 4, 38, 35, 130, 138	ply1annidllem 33051	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0_g‘𝐸)} = (^◡𝐺 “ {(0_g‘𝐸)}))
140	136, 139	eqtr4d 2773	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑍 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0_g‘𝐸)})
141		eqid 2730	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐸 minPoly 𝐹) = (𝐸 minPoly 𝐹)
142	20, 32, 6, 18, 1, 38, 35, 130, 131, 132, 141	minplyval 33055	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) = ((idlGen_1p‘𝐾)‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0_g‘𝐸)}))
143	142	sneqd 4639	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {((𝐸 minPoly 𝐹)‘𝐴)} = {((idlGen_1p‘𝐾)‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0_g‘𝐸)})})
144	143	fveq2d 6894	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) = ((RSpan‘𝑃)‘{((idlGen_1p‘𝐾)‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0_g‘𝐸)})}))
145	133, 140, 144	3eqtr4d 2780	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑍 = ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}))
146		eqid 2730	. . . . . . . . . . . . . . . 16 ⊢ (0_g‘𝑃) = (0_g‘𝑃)
147		eqid 2730	. . . . . . . . . . . . . . . . . 18 ⊢ (0_g‘(Poly₁‘𝐸)) = (0_g‘(Poly₁‘𝐸))
148	147, 18, 1, 141, 19	irngnminplynz 33060	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ≠ (0_g‘(Poly₁‘𝐸)))
149		eqid 2730	. . . . . . . . . . . . . . . . . 18 ⊢ (Poly₁‘𝐸) = (Poly₁‘𝐸)
150	149, 9, 21, 22, 4, 147	ressply10g 32930	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0_g‘(Poly₁‘𝐸)) = (0_g‘𝑃))
151	148, 150	neeqtrd 3008	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ≠ (0_g‘𝑃))
152	20, 32, 6, 18, 1, 38, 141, 146, 151	minplyirred 33059	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ∈ (Irred‘𝑃))
153		eqid 2730	. . . . . . . . . . . . . . . 16 ⊢ ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) = ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)})
154		fldsdrgfld 20557	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ (SubDRing‘𝐸)) → (𝐸 ↾_s 𝐹) ∈ Field)
155	18, 1, 154	syl2anc 582	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 ↾_s 𝐹) ∈ Field)
156	9, 155	eqeltrid 2835	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 ∈ Field)
157	21	ply1pid 25932	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ Field → 𝑃 ∈ PID)
158	156, 157	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ PID)
159	20, 32, 6, 18, 1, 38, 35, 130, 131, 132, 141	minplycl 33056	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ∈ (Base‘𝑃))
160	159, 22	eleqtrrdi 2842	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ∈ 𝑈)
161	95	crngringd 20140	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ Ring)
162	160	snssd 4811	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → {((𝐸 minPoly 𝐹)‘𝐴)} ⊆ 𝑈)
163		eqid 2730	. . . . . . . . . . . . . . . . . 18 ⊢ (LIdeal‘𝑃) = (LIdeal‘𝑃)
164	131, 22, 163	rspcl 20996	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ Ring ∧ {((𝐸 minPoly 𝐹)‘𝐴)} ⊆ 𝑈) → ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) ∈ (LIdeal‘𝑃))
165	161, 162, 164	syl2anc 582	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) ∈ (LIdeal‘𝑃))
166	22, 131, 146, 153, 158, 160, 151, 165	mxidlirred 32862	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) ∈ (MaxIdeal‘𝑃) ↔ ((𝐸 minPoly 𝐹)‘𝐴) ∈ (Irred‘𝑃)))
167	152, 166	mpbird 256	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) ∈ (MaxIdeal‘𝑃))
168	145, 167	eqeltrd 2831	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑍 ∈ (MaxIdeal‘𝑃))
169		eqid 2730	. . . . . . . . . . . . . . . 16 ⊢ (MaxIdeal‘𝑃) = (MaxIdeal‘𝑃)
170	169, 124	crngmxidl 32859	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ CRing → (MaxIdeal‘𝑃) = (MaxIdeal‘(opp_r‘𝑃)))
171	95, 170	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (MaxIdeal‘𝑃) = (MaxIdeal‘(opp_r‘𝑃)))
172	168, 171	eleqtrd 2833	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑍 ∈ (MaxIdeal‘(opp_r‘𝑃)))
173	124, 26, 129, 168, 172	qsdrngi 32883	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∈ DivRing)
174	91, 54, 96, 123, 173	rndrhmcl 32666	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐿 ↾_s ran 𝐽) ∈ DivRing)
175	90, 174	eqeltrd 2831	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿 ↾_s ran 𝐺) ∈ DivRing)
176	53, 175	eqeltrrd 2832	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 ↾_s ran 𝐺) ∈ DivRing)
177		issdrg 20547	. . . . . . . . 9 ⊢ (ran 𝐺 ∈ (SubDRing‘𝐸) ↔ (𝐸 ∈ DivRing ∧ ran 𝐺 ∈ (SubRing‘𝐸) ∧ (𝐸 ↾_s ran 𝐺) ∈ DivRing))
178	45, 48, 176, 177	syl3anbrc 1341	. . . . . . . 8 ⊢ (𝜑 → ran 𝐺 ∈ (SubDRing‘𝐸))
179		fveq2 6890	. . . . . . . . . . . . . 14 ⊢ (𝑝 = (var₁‘𝐾) → (𝑂‘𝑝) = (𝑂‘(var₁‘𝐾)))
180	179	fveq1d 6892	. . . . . . . . . . . . 13 ⊢ (𝑝 = (var₁‘𝐾) → ((𝑂‘𝑝)‘𝐴) = ((𝑂‘(var₁‘𝐾))‘𝐴))
181	180	eqeq2d 2741	. . . . . . . . . . . 12 ⊢ (𝑝 = (var₁‘𝐾) → (𝐴 = ((𝑂‘𝑝)‘𝐴) ↔ 𝐴 = ((𝑂‘(var₁‘𝐾))‘𝐴)))
182	9, 71	eqeltrid 2835	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ DivRing)
183	182	drngringd 20508	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐾 ∈ Ring)
184		eqid 2730	. . . . . . . . . . . . . 14 ⊢ (var₁‘𝐾) = (var₁‘𝐾)
185	184, 21, 22	vr1cl 21960	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ Ring → (var₁‘𝐾) ∈ 𝑈)
186	183, 185	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (var₁‘𝐾) ∈ 𝑈)
187	20, 184, 9, 6, 36, 4	evls1var 22077	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑂‘(var₁‘𝐾)) = ( I ↾ (Base‘𝐸)))
188	187	fveq1d 6892	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑂‘(var₁‘𝐾))‘𝐴) = (( I ↾ (Base‘𝐸))‘𝐴))
189		fvresi 7172	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (Base‘𝐸) → (( I ↾ (Base‘𝐸))‘𝐴) = 𝐴)
190	38, 189	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (( I ↾ (Base‘𝐸))‘𝐴) = 𝐴)
191	188, 190	eqtr2d 2771	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 = ((𝑂‘(var₁‘𝐾))‘𝐴))
192	181, 186, 191	rspcedvdw 3614	. . . . . . . . . . 11 ⊢ (𝜑 → ∃𝑝 ∈ 𝑈 𝐴 = ((𝑂‘𝑝)‘𝐴))
193	23, 192, 19	elrnmptd 5959	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ran 𝐺)
194	193	snssd 4811	. . . . . . . . 9 ⊢ (𝜑 → {𝐴} ⊆ ran 𝐺)
195	97, 194	unssd 4185	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ∪ {𝐴}) ⊆ ran 𝐺)
196	6, 45, 178, 195	fldgenssp 32678	. . . . . . 7 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ⊆ ran 𝐺)
197	44, 196	eqssd 3998	. . . . . 6 ⊢ (𝜑 → ran 𝐺 = (𝐸 fldGen (𝐹 ∪ {𝐴})))
198	15, 6	ressbas2 17186	. . . . . . 7 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ⊆ (Base‘𝐸) → (𝐸 fldGen (𝐹 ∪ {𝐴})) = (Base‘𝐿))
199	115, 198	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) = (Base‘𝐿))
200		eqidd 2731	. . . . . . 7 ⊢ (𝜑 → ((subringAlg ‘𝐿)‘𝐹) = ((subringAlg ‘𝐿)‘𝐹))
201	6, 45, 56	fldgenssid 32673	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 ∪ {𝐴}) ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))
202	201	unssad 4186	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))
203	202, 199	sseqtrd 4021	. . . . . . 7 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐿))
204	200, 203	srabase 20937	. . . . . 6 ⊢ (𝜑 → (Base‘𝐿) = (Base‘((subringAlg ‘𝐿)‘𝐹)))
205	197, 199, 204	3eqtrd 2774	. . . . 5 ⊢ (𝜑 → ran 𝐺 = (Base‘((subringAlg ‘𝐿)‘𝐹)))
206		imaeq2 6054	. . . . . . 7 ⊢ (𝑞 = 𝑝 → (𝐺 “ 𝑞) = (𝐺 “ 𝑝))
207	206	unieqd 4921	. . . . . 6 ⊢ (𝑞 = 𝑝 → ∪ (𝐺 “ 𝑞) = ∪ (𝐺 “ 𝑝))
208	207	cbvmptv 5260	. . . . 5 ⊢ (𝑞 ∈ (Base‘(𝑃 /_s (𝑃 ~_QG (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺 “ 𝑞)) = (𝑝 ∈ (Base‘(𝑃 /_s (𝑃 ~_QG (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺 “ 𝑝))
209	14, 28, 29, 30, 205, 208	lmhmqusker 32808	. . . 4 ⊢ (𝜑 → (𝑞 ∈ (Base‘(𝑃 /_s (𝑃 ~_QG (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺 “ 𝑞)) ∈ ((𝑃 /_s (𝑃 ~_QG (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))}))) LMIso ((subringAlg ‘𝐿)‘𝐹)))
210		eqidd 2731	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘𝐿) = (0_g‘𝐿))
211	200, 210, 203	sralmod0 20955	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0_g‘𝐿) = (0_g‘((subringAlg ‘𝐿)‘𝐹)))
212	211	sneqd 4639	. . . . . . . . . . . 12 ⊢ (𝜑 → {(0_g‘𝐿)} = {(0_g‘((subringAlg ‘𝐿)‘𝐹))})
213	212	imaeq2d 6058	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐺 “ {(0_g‘𝐿)}) = (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))}))
214	25, 213	eqtrid 2782	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 = (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))}))
215	214	oveq2d 7427	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 ~_QG 𝑍) = (𝑃 ~_QG (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))})))
216	215	oveq2d 7427	. . . . . . . 8 ⊢ (𝜑 → (𝑃 /_s (𝑃 ~_QG 𝑍)) = (𝑃 /_s (𝑃 ~_QG (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))}))))
217	26, 216	eqtrid 2782	. . . . . . 7 ⊢ (𝜑 → 𝑄 = (𝑃 /_s (𝑃 ~_QG (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))}))))
218	217	fveq2d 6894	. . . . . 6 ⊢ (𝜑 → (Base‘𝑄) = (Base‘(𝑃 /_s (𝑃 ~_QG (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))})))))
219	218	mpteq1d 5242	. . . . 5 ⊢ (𝜑 → (𝑝 ∈ (Base‘𝑄) ↦ ∪ (𝐺 “ 𝑝)) = (𝑝 ∈ (Base‘(𝑃 /_s (𝑃 ~_QG (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺 “ 𝑝)))
220	219, 27, 208	3eqtr4g 2795	. . . 4 ⊢ (𝜑 → 𝐽 = (𝑞 ∈ (Base‘(𝑃 /_s (𝑃 ~_QG (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺 “ 𝑞)))
221	217	oveq1d 7426	. . . 4 ⊢ (𝜑 → (𝑄 LMIso ((subringAlg ‘𝐿)‘𝐹)) = ((𝑃 /_s (𝑃 ~_QG (^◡𝐺 “ {(0_g‘((subringAlg ‘𝐿)‘𝐹))}))) LMIso ((subringAlg ‘𝐿)‘𝐹)))
222	209, 220, 221	3eltr4d 2846	. . 3 ⊢ (𝜑 → 𝐽 ∈ (𝑄 LMIso ((subringAlg ‘𝐿)‘𝐹)))
223	9, 15, 16, 17, 18, 1, 19, 20, 21, 22, 23, 24, 25, 26, 27	algextdeglem3 33064	. . 3 ⊢ (𝜑 → 𝑄 ∈ LVec)
224	222, 223	lmimdim 32976	. 2 ⊢ (𝜑 → (dim‘𝑄) = (dim‘((subringAlg ‘𝐿)‘𝐹)))
225	6, 18, 56	fldgenfld 32680	. . . . 5 ⊢ (𝜑 → (𝐸 ↾_s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ∈ Field)
226	15, 225	eqeltrid 2835	. . . 4 ⊢ (𝜑 → 𝐿 ∈ Field)
227	9, 15, 16, 17, 18, 1, 19	algextdeglem1 33062	. . . . 5 ⊢ (𝜑 → (𝐿 ↾_s 𝐹) = 𝐾)
228	11	oveq2d 7427	. . . . 5 ⊢ (𝜑 → (𝐿 ↾_s 𝐹) = (𝐿 ↾_s (Base‘𝐾)))
229	227, 228	eqtr3d 2772	. . . 4 ⊢ (𝜑 → 𝐾 = (𝐿 ↾_s (Base‘𝐾)))
230	15	subsubrg 20488	. . . . . . 7 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) → (𝐹 ∈ (SubRing‘𝐿) ↔ (𝐹 ∈ (SubRing‘𝐸) ∧ 𝐹 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))))
231	230	biimpar 476	. . . . . 6 ⊢ (((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ (𝐹 ∈ (SubRing‘𝐸) ∧ 𝐹 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))) → 𝐹 ∈ (SubRing‘𝐿))
232	60, 4, 202, 231	syl12anc 833	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐿))
233	11, 232	eqeltrrd 2832	. . . 4 ⊢ (𝜑 → (Base‘𝐾) ∈ (SubRing‘𝐿))
234		brfldext 33014	. . . . 5 ⊢ ((𝐿 ∈ Field ∧ 𝐾 ∈ Field) → (𝐿/_FldExt𝐾 ↔ (𝐾 = (𝐿 ↾_s (Base‘𝐾)) ∧ (Base‘𝐾) ∈ (SubRing‘𝐿))))
235	234	biimpar 476	. . . 4 ⊢ (((𝐿 ∈ Field ∧ 𝐾 ∈ Field) ∧ (𝐾 = (𝐿 ↾_s (Base‘𝐾)) ∧ (Base‘𝐾) ∈ (SubRing‘𝐿))) → 𝐿/_FldExt𝐾)
236	226, 156, 229, 233, 235	syl22anc 835	. . 3 ⊢ (𝜑 → 𝐿/_FldExt𝐾)
237		extdgval 33021	. . 3 ⊢ (𝐿/_FldExt𝐾 → (𝐿[:]𝐾) = (dim‘((subringAlg ‘𝐿)‘(Base‘𝐾))))
238	236, 237	syl 17	. 2 ⊢ (𝜑 → (𝐿[:]𝐾) = (dim‘((subringAlg ‘𝐿)‘(Base‘𝐾))))
239	13, 224, 238	3eqtr4d 2780	1 ⊢ (𝜑 → (dim‘𝑄) = (𝐿[:]𝐾))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 394 ∧ w3a 1085 = wceq 1539 ∈ wcel 2104 ≠ wne 2938 ∀wral 3059 {crab 3430 Vcvv 3472 ∪ cun 3945 ⊆ wss 3947 {csn 4627 ∪ cuni 4907 class class class wbr 5147 ↦ cmpt 5230 I cid 5572 ^◡ccnv 5674 dom cdm 5675 ran crn 5676 ↾ cres 5677 “ cima 5678 ∘ ccom 5679 ‘cfv 6542 (class class class)co 7411 [cec 8703 / cqs 8704 Basecbs 17148 ↾_s cress 17177 0_gc0g 17389 /_s cqus 17455 Mndcmnd 18659 SubGrpcsubg 19036 NrmSGrpcnsg 19037 ~_QG cqg 19038 GrpHom cghm 19127 1_rcur 20075 Ringcrg 20127 CRingccrg 20128 opp_rcoppr 20224 Irredcir 20247 RingHom crh 20360 NzRingcnzr 20403 SubRingcsubrg 20457 DivRingcdr 20500 Fieldcfield 20501 SubDRingcsdrg 20545 LMHom clmhm 20774 LMIso clmim 20775 LVecclvec 20857 subringAlg csra 20926 LIdealclidl 20928 RSpancrsp 20929 PIDcpid 21098 var₁cv1 21919 Poly₁cpl1 21920 evalSub₁ ces1 22052 deg₁ cdg1 25804 idlGen_1pcig1p 25882 fldGen cfldgen 32670 MaxIdealcmxidl 32849 dimcldim 32971 /_FldExtcfldext 33005 [:]cextdg 33008 IntgRing cirng 33036 minPoly cminply 33045

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 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7727 ax-reg 9589 ax-inf2 9638 ax-ac2 10460 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189 ax-pre-sup 11190 ax-addf 11191 ax-mulf 11192

This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3374 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-tp 4632 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-iin 4999 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-se 5631 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-isom 6551 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-of 7672 df-ofr 7673 df-rpss 7715 df-om 7858 df-1st 7977 df-2nd 7978 df-supp 8149 df-tpos 8213 df-frecs 8268 df-wrecs 8299 df-recs 8373 df-rdg 8412 df-1o 8468 df-2o 8469 df-oadd 8472 df-er 8705 df-ec 8707 df-qs 8711 df-map 8824 df-pm 8825 df-ixp 8894 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-fsupp 9364 df-sup 9439 df-inf 9440 df-oi 9507 df-r1 9761 df-rank 9762 df-dju 9898 df-card 9936 df-acn 9939 df-ac 10113 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-sub 11450 df-neg 11451 df-nn 12217 df-2 12279 df-3 12280 df-4 12281 df-5 12282 df-6 12283 df-7 12284 df-8 12285 df-9 12286 df-n0 12477 df-xnn0 12549 df-z 12563 df-dec 12682 df-uz 12827 df-fz 13489 df-fzo 13632 df-seq 13971 df-hash 14295 df-struct 17084 df-sets 17101 df-slot 17119 df-ndx 17131 df-base 17149 df-ress 17178 df-plusg 17214 df-mulr 17215 df-starv 17216 df-sca 17217 df-vsca 17218 df-ip 17219 df-tset 17220 df-ple 17221 df-ocomp 17222 df-ds 17223 df-unif 17224 df-hom 17225 df-cco 17226 df-0g 17391 df-gsum 17392 df-prds 17397 df-pws 17399 df-imas 17458 df-qus 17459 df-mre 17534 df-mrc 17535 df-mri 17536 df-acs 17537 df-proset 18252 df-drs 18253 df-poset 18270 df-ipo 18485 df-mgm 18565 df-sgrp 18644 df-mnd 18660 df-mhm 18705 df-submnd 18706 df-grp 18858 df-minusg 18859 df-sbg 18860 df-mulg 18987 df-subg 19039 df-nsg 19040 df-eqg 19041 df-ghm 19128 df-gim 19173 df-cntz 19222 df-oppg 19251 df-lsm 19545 df-cmn 19691 df-abl 19692 df-mgp 20029 df-rng 20047 df-ur 20076 df-srg 20081 df-ring 20129 df-cring 20130 df-oppr 20225 df-dvdsr 20248 df-unit 20249 df-irred 20250 df-invr 20279 df-dvr 20292 df-rhm 20363 df-nzr 20404 df-subrng 20434 df-subrg 20459 df-drng 20502 df-field 20503 df-sdrg 20546 df-lmod 20616 df-lss 20687 df-lsp 20727 df-lmhm 20777 df-lmim 20778 df-lbs 20830 df-lvec 20858 df-sra 20930 df-rgmod 20931 df-lidl 20932 df-rsp 20933 df-2idl 21006 df-lpidl 21081 df-lpir 21082 df-rlreg 21099 df-domn 21100 df-idom 21101 df-pid 21102 df-cnfld 21145 df-dsmm 21506 df-frlm 21521 df-uvc 21557 df-lindf 21580 df-linds 21581 df-assa 21627 df-asp 21628 df-ascl 21629 df-psr 21681 df-mvr 21682 df-mpl 21683 df-opsr 21685 df-evls 21854 df-evl 21855 df-psr1 21923 df-vr1 21924 df-ply1 21925 df-coe1 21926 df-evls1 22054 df-evl1 22055 df-mdeg 25805 df-deg1 25806 df-mon1 25883 df-uc1p 25884 df-q1p 25885 df-r1p 25886 df-ig1p 25887 df-fldgen 32671 df-mxidl 32850 df-dim 32972 df-fldext 33009 df-extdg 33010 df-irng 33037 df-minply 33046

This theorem is referenced by: algextdeg 33070

W3C validator