algextdeglem4

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

	Ref	Expression
Hypotheses	algextdeg.k	$⊢ K = E ↾_{𝑠} F$
	algextdeg.l	$⊢ L = E ↾_{𝑠} (E fldGen (F \cup \{A\}))$
	algextdeg.d	$⊢ D = \deg_{1} (E)$
	algextdeg.m	$⊢ M = E minPoly F$
	algextdeg.f	$⊢ φ \to E \in Field$
	algextdeg.e	$⊢ φ \to F \in SubDRing (E)$
	algextdeg.a	$⊢ φ \to A \in (E IntgRing F)$
	algextdeglem.o	$⊢ O = E {evalSub}_{1} F$
	algextdeglem.y	$⊢ P = {Poly}_{1} (K)$
	algextdeglem.u	$⊢ U = {Base}_{P}$
	algextdeglem.g	$⊢ G = (p \in U ⟼ O (p) (A))$
	algextdeglem.n	$⊢ N = (x \in U ⟼ [x] (P ~_{QG} Z))$
	algextdeglem.z	$⊢ Z = G^{-1} [\{0_{L}\}]$
	algextdeglem.q	$⊢ Q = P /_{𝑠} (P ~_{QG} Z)$
	algextdeglem.j	$⊢ J = (p \in {Base}_{Q} ⟼ ⋃ G [p])$
Assertion	algextdeglem4	$⊢ φ \to \dim (Q) = L [. : .] K$

Proof

Step	Hyp	Ref	Expression
1		algextdeg.k	$⊢ K = E ↾_{𝑠} F$
2		algextdeg.l	$⊢ L = E ↾_{𝑠} (E fldGen (F \cup \{A\}))$
3		algextdeg.d	$⊢ D = \deg_{1} (E)$
4		algextdeg.m	$⊢ M = E minPoly F$
5		algextdeg.f	$⊢ φ \to E \in Field$
6		algextdeg.e	$⊢ φ \to F \in SubDRing (E)$
7		algextdeg.a	$⊢ φ \to A \in (E IntgRing F)$
8		algextdeglem.o	$⊢ O = E {evalSub}_{1} F$
9		algextdeglem.y	$⊢ P = {Poly}_{1} (K)$
10		algextdeglem.u	$⊢ U = {Base}_{P}$
11		algextdeglem.g	$⊢ G = (p \in U ⟼ O (p) (A))$
12		algextdeglem.n	$⊢ N = (x \in U ⟼ [x] (P ~_{QG} Z))$
13		algextdeglem.z	$⊢ Z = G^{-1} [\{0_{L}\}]$
14		algextdeglem.q	$⊢ Q = P /_{𝑠} (P ~_{QG} Z)$
15		algextdeglem.j	$⊢ J = (p \in {Base}_{Q} ⟼ ⋃ G [p])$
16		issdrg	$⊢ F \in SubDRing (E) \leftrightarrow (E \in DivRing \land F \in SubRing (E) \land E ↾_{𝑠} F \in DivRing)$
17	6 16	sylib	$⊢ φ \to (E \in DivRing \land F \in SubRing (E) \land E ↾_{𝑠} F \in DivRing)$
18	17	simp2d	$⊢ φ \to F \in SubRing (E)$
19		subrgsubg	$⊢ F \in SubRing (E) \to F \in SubGrp (E)$
20		eqid	$⊢ {Base}_{E} = {Base}_{E}$
21	20	subgss	$⊢ F \in SubGrp (E) \to F \subseteq {Base}_{E}$
22	18 19 21	3syl	$⊢ φ \to F \subseteq {Base}_{E}$
23	1 20	ressbas2	$⊢ F \subseteq {Base}_{E} \to F = {Base}_{K}$
24	22 23	syl	$⊢ φ \to F = {Base}_{K}$
25	24	fveq2d	$⊢ φ \to subringAlg (L) (F) = subringAlg (L) ({Base}_{K})$
26	25	fveq2d	$⊢ φ \to \dim (subringAlg (L) (F)) = \dim (subringAlg (L) ({Base}_{K}))$
27		eqid	$⊢ 0_{subringAlg (L) (F)} = 0_{subringAlg (L) (F)}$
28	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	algextdeglem2	$⊢ φ \to G \in (P LMHom subringAlg (L) (F))$
29		eqid	$⊢ G^{-1} [\{0_{subringAlg (L) (F)}\}] = G^{-1} [\{0_{subringAlg (L) (F)}\}]$
30		eqid	$⊢ P /_{𝑠} (P ~_{QG} G^{-1} [\{0_{subringAlg (L) (F)}\}]) = P /_{𝑠} (P ~_{QG} G^{-1} [\{0_{subringAlg (L) (F)}\}])$
31	1	fveq2i	$⊢ {Poly}_{1} (K) = {Poly}_{1} (E ↾_{𝑠} F)$
32	9 31	eqtri	$⊢ P = {Poly}_{1} (E ↾_{𝑠} F)$
33	5	adantr	$⊢ (φ \land p \in U) \to E \in Field$
34	6	adantr	$⊢ (φ \land p \in U) \to F \in SubDRing (E)$
35		eqid	$⊢ 0_{E} = 0_{E}$
36	5	fldcrngd	$⊢ φ \to E \in CRing$
37	8 1 20 35 36 18	irngssv	$⊢ φ \to E IntgRing F \subseteq {Base}_{E}$
38	37 7	sseldd	$⊢ φ \to A \in {Base}_{E}$
39	38	adantr	$⊢ (φ \land p \in U) \to A \in {Base}_{E}$
40		simpr	$⊢ (φ \land p \in U) \to p \in U$
41	20 8 32 10 33 34 39 40	evls1fldgencl	$⊢ (φ \land p \in U) \to O (p) (A) \in (E fldGen (F \cup \{A\}))$
42	41	ralrimiva	$⊢ φ \to \forall p \in U O (p) (A) \in (E fldGen (F \cup \{A\}))$
43	11	rnmptss	$⊢ \forall p \in U O (p) (A) \in (E fldGen (F \cup \{A\})) \to ran G \subseteq E fldGen (F \cup \{A\})$
44	42 43	syl	$⊢ φ \to ran G \subseteq E fldGen (F \cup \{A\})$
45	5	flddrngd	$⊢ φ \to E \in DivRing$
46	8 32 20 10 36 18 38 11	evls1maprhm	$⊢ φ \to G \in (P RingHom E)$
47		rnrhmsubrg	$⊢ G \in (P RingHom E) \to ran G \in SubRing (E)$
48	46 47	syl	$⊢ φ \to ran G \in SubRing (E)$
49	2	oveq1i	$⊢ L ↾_{𝑠} ran G = (E ↾_{𝑠} (E fldGen (F \cup \{A\}))) ↾_{𝑠} ran G$
50		ovex	$⊢ E fldGen (F \cup \{A\}) \in V$
51		ressabs	$⊢ (E fldGen (F \cup \{A\}) \in V \land ran G \subseteq E fldGen (F \cup \{A\})) \to (E ↾_{𝑠} (E fldGen (F \cup \{A\}))) ↾_{𝑠} ran G = E ↾_{𝑠} ran G$
52	50 44 51	sylancr	$⊢ φ \to (E ↾_{𝑠} (E fldGen (F \cup \{A\}))) ↾_{𝑠} ran G = E ↾_{𝑠} ran G$
53	49 52	eqtrid	$⊢ φ \to L ↾_{𝑠} ran G = E ↾_{𝑠} ran G$
54		eqid	$⊢ 0_{L} = 0_{L}$
55	38	snssd	$⊢ φ \to \{A\} \subseteq {Base}_{E}$
56	22 55	unssd	$⊢ φ \to F \cup \{A\} \subseteq {Base}_{E}$
57	20 45 56	fldgensdrg	$⊢ φ \to E fldGen (F \cup \{A\}) \in SubDRing (E)$
58		issdrg	$⊢ E fldGen (F \cup \{A\}) \in SubDRing (E) \leftrightarrow (E \in DivRing \land E fldGen (F \cup \{A\}) \in SubRing (E) \land E ↾_{𝑠} (E fldGen (F \cup \{A\})) \in DivRing)$
59	57 58	sylib	$⊢ φ \to (E \in DivRing \land E fldGen (F \cup \{A\}) \in SubRing (E) \land E ↾_{𝑠} (E fldGen (F \cup \{A\})) \in DivRing)$
60	59	simp2d	$⊢ φ \to E fldGen (F \cup \{A\}) \in SubRing (E)$
61	2	resrhm2b	$⊢ (E fldGen (F \cup \{A\}) \in SubRing (E) \land ran G \subseteq E fldGen (F \cup \{A\})) \to (G \in (P RingHom E) \leftrightarrow G \in (P RingHom L))$
62	61	biimpa	$⊢ ((E fldGen (F \cup \{A\}) \in SubRing (E) \land ran G \subseteq E fldGen (F \cup \{A\})) \land G \in (P RingHom E)) \to G \in (P RingHom L)$
63	60 44 46 62	syl21anc	$⊢ φ \to G \in (P RingHom L)$
64		rhmghm	$⊢ G \in (P RingHom L) \to G \in (P GrpHom L)$
65	63 64	syl	$⊢ φ \to G \in (P GrpHom L)$
66	54 65 13 14 15 10 12	ghmquskerco	$⊢ φ \to G = J \circ N$
67	66	rneqd	$⊢ φ \to ran G = ran (J \circ N)$
68	14	a1i	$⊢ φ \to Q = P /_{𝑠} (P ~_{QG} Z)$
69	10	a1i	$⊢ φ \to U = {Base}_{P}$
70		ovexd	$⊢ φ \to P ~_{QG} Z \in V$
71	17	simp3d	$⊢ φ \to E ↾_{𝑠} F \in DivRing$
72	32 71	ply1lvec	$⊢ φ \to P \in LVec$
73	68 69 70 72	qusbas	$⊢ φ \to U / (P ~_{QG} Z) = {Base}_{Q}$
74		eqid	$⊢ U / (P ~_{QG} Z) = U / (P ~_{QG} Z)$
75	54	ghmker	$⊢ G \in (P GrpHom L) \to G^{-1} [\{0_{L}\}] \in NrmSGrp (P)$
76	65 75	syl	$⊢ φ \to G^{-1} [\{0_{L}\}] \in NrmSGrp (P)$
77	13 76	eqeltrid	$⊢ φ \to Z \in NrmSGrp (P)$
78	10 74 12 77	qusrn	$⊢ φ \to ran N = U / (P ~_{QG} Z)$
79		eqid	$⊢ subringAlg (E) (F) = subringAlg (E) (F)$
80	8 32 20 10 36 18 38 11 79	evls1maplmhm	$⊢ φ \to G \in (P LMHom subringAlg (E) (F))$
81	80	elexd	$⊢ φ \to G \in V$
82	81	adantr	$⊢ (φ \land p \in {Base}_{Q}) \to G \in V$
83	82	imaexd	$⊢ (φ \land p \in {Base}_{Q}) \to G [p] \in V$
84	83	uniexd	$⊢ (φ \land p \in {Base}_{Q}) \to ⋃ G [p] \in V$
85	15 84	dmmptd	$⊢ φ \to dom J = {Base}_{Q}$
86	73 78 85	3eqtr4rd	$⊢ φ \to dom J = ran N$
87		rncoeq	$⊢ dom J = ran N \to ran (J \circ N) = ran J$
88	86 87	syl	$⊢ φ \to ran (J \circ N) = ran J$
89	67 88	eqtrd	$⊢ φ \to ran G = ran J$
90	89	oveq2d	$⊢ φ \to L ↾_{𝑠} ran G = L ↾_{𝑠} ran J$
91		eqid	$⊢ L ↾_{𝑠} ran J = L ↾_{𝑠} ran J$
92	1	subrgcrng	$⊢ (E \in CRing \land F \in SubRing (E)) \to K \in CRing$
93	36 18 92	syl2anc	$⊢ φ \to K \in CRing$
94	9	ply1crng	$⊢ K \in CRing \to P \in CRing$
95	93 94	syl	$⊢ φ \to P \in CRing$
96	54 63 13 14 15 95	rhmquskerlem	$⊢ φ \to J \in (Q RingHom L)$
97	8 32 20 10 36 18 38 11	evls1maprnss	$⊢ φ \to F \subseteq ran G$
98		eqid	$⊢ 1_{E} = 1_{E}$
99	1 98	subrg1	$⊢ F \in SubRing (E) \to 1_{E} = 1_{K}$
100	18 99	syl	$⊢ φ \to 1_{E} = 1_{K}$
101	98	subrg1cl	$⊢ F \in SubRing (E) \to 1_{E} \in F$
102	18 101	syl	$⊢ φ \to 1_{E} \in F$
103	100 102	eqeltrrd	$⊢ φ \to 1_{K} \in F$
104	97 103	sseldd	$⊢ φ \to 1_{K} \in ran G$
105		drngnzr	$⊢ E \in DivRing \to E \in NzRing$
106	98 35	nzrnz	$⊢ E \in NzRing \to 1_{E} \neq 0_{E}$
107	45 105 106	3syl	$⊢ φ \to 1_{E} \neq 0_{E}$
108	36	crnggrpd	$⊢ φ \to E \in Grp$
109	108	grpmndd	$⊢ φ \to E \in Mnd$
110		sdrgsubrg	$⊢ E fldGen (F \cup \{A\}) \in SubDRing (E) \to E fldGen (F \cup \{A\}) \in SubRing (E)$
111		subrgsubg	$⊢ E fldGen (F \cup \{A\}) \in SubRing (E) \to E fldGen (F \cup \{A\}) \in SubGrp (E)$
112	57 110 111	3syl	$⊢ φ \to E fldGen (F \cup \{A\}) \in SubGrp (E)$
113	35	subg0cl	$⊢ E fldGen (F \cup \{A\}) \in SubGrp (E) \to 0_{E} \in (E fldGen (F \cup \{A\}))$
114	112 113	syl	$⊢ φ \to 0_{E} \in (E fldGen (F \cup \{A\}))$
115	20 45 56	fldgenssv	$⊢ φ \to E fldGen (F \cup \{A\}) \subseteq {Base}_{E}$
116	2 20 35	ress0g	$⊢ (E \in Mnd \land 0_{E} \in (E fldGen (F \cup \{A\})) \land E fldGen (F \cup \{A\}) \subseteq {Base}_{E}) \to 0_{E} = 0_{L}$
117	109 114 115 116	syl3anc	$⊢ φ \to 0_{E} = 0_{L}$
118	107 100 117	3netr3d	$⊢ φ \to 1_{K} \neq 0_{L}$
119		nelsn	$⊢ 1_{K} \neq 0_{L} \to \neg 1_{K} \in \{0_{L}\}$
120	118 119	syl	$⊢ φ \to \neg 1_{K} \in \{0_{L}\}$
121		nelne1	$⊢ (1_{K} \in ran G \land \neg 1_{K} \in \{0_{L}\}) \to ran G \neq \{0_{L}\}$
122	104 120 121	syl2anc	$⊢ φ \to ran G \neq \{0_{L}\}$
123	89 122	eqnetrrd	$⊢ φ \to ran J \neq \{0_{L}\}$
124		eqid	$⊢ {opp}_{r} (P) = {opp}_{r} (P)$
125	1	sdrgdrng	$⊢ F \in SubDRing (E) \to K \in DivRing$
126		drngnzr	$⊢ K \in DivRing \to K \in NzRing$
127	6 125 126	3syl	$⊢ φ \to K \in NzRing$
128	9	ply1nz	$⊢ K \in NzRing \to P \in NzRing$
129	127 128	syl	$⊢ φ \to P \in NzRing$
130		eqid	$⊢ \{q \in dom O \| O (q) (A) = 0_{E}\} = \{q \in dom O \| O (q) (A) = 0_{E}\}$
131		eqid	$⊢ RSpan (P) = RSpan (P)$
132	1	fveq2i	$⊢ {idlGen}_{1p} (K) = {idlGen}_{1p} (E ↾_{𝑠} F)$
133	8 32 20 5 6 38 35 130 131 132	ply1annig1p	$⊢ φ \to \{q \in dom O \| O (q) (A) = 0_{E}\} = RSpan (P) (\{{idlGen}_{1p} (K) (\{q \in dom O \| O (q) (A) = 0_{E}\})\})$
134	117	sneqd	$⊢ φ \to \{0_{E}\} = \{0_{L}\}$
135	134	imaeq2d	$⊢ φ \to G^{-1} [\{0_{E}\}] = G^{-1} [\{0_{L}\}]$
136	13 135	eqtr4id	$⊢ φ \to Z = G^{-1} [\{0_{E}\}]$
137	10	mpteq1i	$⊢ (p \in U ⟼ O (p) (A)) = (p \in {Base}_{P} ⟼ O (p) (A))$
138	11 137	eqtri	$⊢ G = (p \in {Base}_{P} ⟼ O (p) (A))$
139	8 32 20 36 18 38 35 130 138	ply1annidllem	$⊢ φ \to \{q \in dom O \| O (q) (A) = 0_{E}\} = G^{-1} [\{0_{E}\}]$
140	136 139	eqtr4d	$⊢ φ \to Z = \{q \in dom O \| O (q) (A) = 0_{E}\}$
141		eqid	$⊢ E minPoly F = E minPoly F$
142	8 32 20 5 6 38 35 130 131 132 141	minplyval	$⊢ φ \to (E minPoly F) (A) = {idlGen}_{1p} (K) (\{q \in dom O \| O (q) (A) = 0_{E}\})$
143	142	sneqd	$⊢ φ \to \{(E minPoly F) (A)\} = \{{idlGen}_{1p} (K) (\{q \in dom O \| O (q) (A) = 0_{E}\})\}$
144	143	fveq2d	$⊢ φ \to RSpan (P) (\{(E minPoly F) (A)\}) = RSpan (P) (\{{idlGen}_{1p} (K) (\{q \in dom O \| O (q) (A) = 0_{E}\})\})$
145	133 140 144	3eqtr4d	$⊢ φ \to Z = RSpan (P) (\{(E minPoly F) (A)\})$
146		eqid	$⊢ 0_{P} = 0_{P}$
147		eqid	$⊢ 0_{{Poly}_{1} (E)} = 0_{{Poly}_{1} (E)}$
148	147 5 6 141 7	irngnminplynz	$⊢ φ \to (E minPoly F) (A) \neq 0_{{Poly}_{1} (E)}$
149		eqid	$⊢ {Poly}_{1} (E) = {Poly}_{1} (E)$
150	149 1 9 10 18 147	ressply10g	$⊢ φ \to 0_{{Poly}_{1} (E)} = 0_{P}$
151	148 150	neeqtrd	$⊢ φ \to (E minPoly F) (A) \neq 0_{P}$
152	8 32 20 5 6 38 141 146 151	minplyirred	$⊢ φ \to (E minPoly F) (A) \in Irred (P)$
153		eqid	$⊢ RSpan (P) (\{(E minPoly F) (A)\}) = RSpan (P) (\{(E minPoly F) (A)\})$
154		fldsdrgfld	$⊢ (E \in Field \land F \in SubDRing (E)) \to E ↾_{𝑠} F \in Field$
155	5 6 154	syl2anc	$⊢ φ \to E ↾_{𝑠} F \in Field$
156	1 155	eqeltrid	$⊢ φ \to K \in Field$
157	9	ply1pid	$⊢ K \in Field \to P \in PID$
158	156 157	syl	$⊢ φ \to P \in PID$
159	8 32 20 5 6 38 35 130 131 132 141	minplycl	$⊢ φ \to (E minPoly F) (A) \in {Base}_{P}$
160	159 10	eleqtrrdi	$⊢ φ \to (E minPoly F) (A) \in U$
161	95	crngringd	$⊢ φ \to P \in Ring$
162	160	snssd	$⊢ φ \to \{(E minPoly F) (A)\} \subseteq U$
163		eqid	$⊢ LIdeal (P) = LIdeal (P)$
164	131 10 163	rspcl	$⊢ (P \in Ring \land \{(E minPoly F) (A)\} \subseteq U) \to RSpan (P) (\{(E minPoly F) (A)\}) \in LIdeal (P)$
165	161 162 164	syl2anc	$⊢ φ \to RSpan (P) (\{(E minPoly F) (A)\}) \in LIdeal (P)$
166	10 131 146 153 158 160 151 165	mxidlirred	$⊢ φ \to (RSpan (P) (\{(E minPoly F) (A)\}) \in MaxIdeal (P) \leftrightarrow (E minPoly F) (A) \in Irred (P))$
167	152 166	mpbird	$⊢ φ \to RSpan (P) (\{(E minPoly F) (A)\}) \in MaxIdeal (P)$
168	145 167	eqeltrd	$⊢ φ \to Z \in MaxIdeal (P)$
169		eqid	$⊢ MaxIdeal (P) = MaxIdeal (P)$
170	169 124	crngmxidl	$⊢ P \in CRing \to MaxIdeal (P) = MaxIdeal ({opp}_{r} (P))$
171	95 170	syl	$⊢ φ \to MaxIdeal (P) = MaxIdeal ({opp}_{r} (P))$
172	168 171	eleqtrd	$⊢ φ \to Z \in MaxIdeal ({opp}_{r} (P))$
173	124 14 129 168 172	qsdrngi	$⊢ φ \to Q \in DivRing$
174	91 54 96 123 173	rndrhmcl	$⊢ φ \to L ↾_{𝑠} ran J \in DivRing$
175	90 174	eqeltrd	$⊢ φ \to L ↾_{𝑠} ran G \in DivRing$
176	53 175	eqeltrrd	$⊢ φ \to E ↾_{𝑠} ran G \in DivRing$
177		issdrg	$⊢ ran G \in SubDRing (E) \leftrightarrow (E \in DivRing \land ran G \in SubRing (E) \land E ↾_{𝑠} ran G \in DivRing)$
178	45 48 176 177	syl3anbrc	$⊢ φ \to ran G \in SubDRing (E)$
179		fveq2	$⊢ p = {var}_{1} (K) \to O (p) = O ({var}_{1} (K))$
180	179	fveq1d	$⊢ p = {var}_{1} (K) \to O (p) (A) = O ({var}_{1} (K)) (A)$
181	180	eqeq2d	$⊢ p = {var}_{1} (K) \to (A = O (p) (A) \leftrightarrow A = O ({var}_{1} (K)) (A))$
182	1 71	eqeltrid	$⊢ φ \to K \in DivRing$
183	182	drngringd	$⊢ φ \to K \in Ring$
184		eqid	$⊢ {var}_{1} (K) = {var}_{1} (K)$
185	184 9 10	vr1cl	$⊢ K \in Ring \to {var}_{1} (K) \in U$
186	183 185	syl	$⊢ φ \to {var}_{1} (K) \in U$
187	8 184 1 20 36 18	evls1var	$⊢ φ \to O ({var}_{1} (K)) = {I ↾}_{{Base}_{E}}$
188	187	fveq1d	$⊢ φ \to O ({var}_{1} (K)) (A) = ({I ↾}_{{Base}_{E}}) (A)$
189		fvresi	$⊢ A \in {Base}_{E} \to ({I ↾}_{{Base}_{E}}) (A) = A$
190	38 189	syl	$⊢ φ \to ({I ↾}_{{Base}_{E}}) (A) = A$
191	188 190	eqtr2d	$⊢ φ \to A = O ({var}_{1} (K)) (A)$
192	181 186 191	rspcedvdw	$⊢ φ \to \exists p \in U A = O (p) (A)$
193	11 192 7	elrnmptd	$⊢ φ \to A \in ran G$
194	193	snssd	$⊢ φ \to \{A\} \subseteq ran G$
195	97 194	unssd	$⊢ φ \to F \cup \{A\} \subseteq ran G$
196	20 45 178 195	fldgenssp	$⊢ φ \to E fldGen (F \cup \{A\}) \subseteq ran G$
197	44 196	eqssd	$⊢ φ \to ran G = E fldGen (F \cup \{A\})$
198	2 20	ressbas2	$⊢ E fldGen (F \cup \{A\}) \subseteq {Base}_{E} \to E fldGen (F \cup \{A\}) = {Base}_{L}$
199	115 198	syl	$⊢ φ \to E fldGen (F \cup \{A\}) = {Base}_{L}$
200		eqidd	$⊢ φ \to subringAlg (L) (F) = subringAlg (L) (F)$
201	20 45 56	fldgenssid	$⊢ φ \to F \cup \{A\} \subseteq E fldGen (F \cup \{A\})$
202	201	unssad	$⊢ φ \to F \subseteq E fldGen (F \cup \{A\})$
203	202 199	sseqtrd	$⊢ φ \to F \subseteq {Base}_{L}$
204	200 203	srabase	$⊢ φ \to {Base}_{L} = {Base}_{subringAlg (L) (F)}$
205	197 199 204	3eqtrd	$⊢ φ \to ran G = {Base}_{subringAlg (L) (F)}$
206		imaeq2	$⊢ q = p \to G [q] = G [p]$
207	206	unieqd	$⊢ q = p \to ⋃ G [q] = ⋃ G [p]$
208	207	cbvmptv	$⊢ (q \in {Base}_{(P /_{𝑠} (P ~_{QG} G^{-1} [\{0_{subringAlg (L) (F)}\}]))} ⟼ ⋃ G [q]) = (p \in {Base}_{(P /_{𝑠} (P ~_{QG} G^{-1} [\{0_{subringAlg (L) (F)}\}]))} ⟼ ⋃ G [p])$
209	27 28 29 30 205 208	lmhmqusker	$⊢ φ \to (q \in {Base}_{(P /_{𝑠} (P ~_{QG} G^{-1} [\{0_{subringAlg (L) (F)}\}]))} ⟼ ⋃ G [q]) \in ((P /_{𝑠} (P ~_{QG} G^{-1} [\{0_{subringAlg (L) (F)}\}])) LMIso subringAlg (L) (F))$
210		eqidd	$⊢ φ \to 0_{L} = 0_{L}$
211	200 210 203	sralmod0	$⊢ φ \to 0_{L} = 0_{subringAlg (L) (F)}$
212	211	sneqd	$⊢ φ \to \{0_{L}\} = \{0_{subringAlg (L) (F)}\}$
213	212	imaeq2d	$⊢ φ \to G^{-1} [\{0_{L}\}] = G^{-1} [\{0_{subringAlg (L) (F)}\}]$
214	13 213	eqtrid	$⊢ φ \to Z = G^{-1} [\{0_{subringAlg (L) (F)}\}]$
215	214	oveq2d	$⊢ φ \to P ~_{QG} Z = P ~_{QG} G^{-1} [\{0_{subringAlg (L) (F)}\}]$
216	215	oveq2d	$⊢ φ \to P /_{𝑠} (P ~_{QG} Z) = P /_{𝑠} (P ~_{QG} G^{-1} [\{0_{subringAlg (L) (F)}\}])$
217	14 216	eqtrid	$⊢ φ \to Q = P /_{𝑠} (P ~_{QG} G^{-1} [\{0_{subringAlg (L) (F)}\}])$
218	217	fveq2d	$⊢ φ \to {Base}_{Q} = {Base}_{(P /_{𝑠} (P ~_{QG} G^{-1} [\{0_{subringAlg (L) (F)}\}]))}$
219	218	mpteq1d	$⊢ φ \to (p \in {Base}_{Q} ⟼ ⋃ G [p]) = (p \in {Base}_{(P /_{𝑠} (P ~_{QG} G^{-1} [\{0_{subringAlg (L) (F)}\}]))} ⟼ ⋃ G [p])$
220	219 15 208	3eqtr4g	$⊢ φ \to J = (q \in {Base}_{(P /_{𝑠} (P ~_{QG} G^{-1} [\{0_{subringAlg (L) (F)}\}]))} ⟼ ⋃ G [q])$
221	217	oveq1d	$⊢ φ \to Q LMIso subringAlg (L) (F) = (P /_{𝑠} (P ~_{QG} G^{-1} [\{0_{subringAlg (L) (F)}\}])) LMIso subringAlg (L) (F)$
222	209 220 221	3eltr4d	$⊢ φ \to J \in (Q LMIso subringAlg (L) (F))$
223	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	algextdeglem3	$⊢ φ \to Q \in LVec$
224	222 223	lmimdim	$⊢ φ \to \dim (Q) = \dim (subringAlg (L) (F))$
225	20 5 56	fldgenfld	$⊢ φ \to E ↾_{𝑠} (E fldGen (F \cup \{A\})) \in Field$
226	2 225	eqeltrid	$⊢ φ \to L \in Field$
227	1 2 3 4 5 6 7	algextdeglem1	$⊢ φ \to L ↾_{𝑠} F = K$
228	24	oveq2d	$⊢ φ \to L ↾_{𝑠} F = L ↾_{𝑠} {Base}_{K}$
229	227 228	eqtr3d	$⊢ φ \to K = L ↾_{𝑠} {Base}_{K}$
230	2	subsubrg	$⊢ E fldGen (F \cup \{A\}) \in SubRing (E) \to (F \in SubRing (L) \leftrightarrow (F \in SubRing (E) \land F \subseteq E fldGen (F \cup \{A\})))$
231	230	biimpar	$⊢ (E fldGen (F \cup \{A\}) \in SubRing (E) \land (F \in SubRing (E) \land F \subseteq E fldGen (F \cup \{A\}))) \to F \in SubRing (L)$
232	60 18 202 231	syl12anc	$⊢ φ \to F \in SubRing (L)$
233	24 232	eqeltrrd	$⊢ φ \to {Base}_{K} \in SubRing (L)$
234		brfldext	$⊢ (L \in Field \land K \in Field) \to (L /_{FldExt} K \leftrightarrow (K = L ↾_{𝑠} {Base}_{K} \land {Base}_{K} \in SubRing (L)))$
235	234	biimpar	$⊢ ((L \in Field \land K \in Field) \land (K = L ↾_{𝑠} {Base}_{K} \land {Base}_{K} \in SubRing (L))) \to L /_{FldExt} K$
236	226 156 229 233 235	syl22anc	$⊢ φ \to L /_{FldExt} K$
237		extdgval	$⊢ L /_{FldExt} K \to L [. : .] K = \dim (subringAlg (L) ({Base}_{K}))$
238	236 237	syl	$⊢ φ \to L [. : .] K = \dim (subringAlg (L) ({Base}_{K}))$
239	26 224 238	3eqtr4d	$⊢ φ \to \dim (Q) = L [. : .] K$

Metamath Proof Explorer

Theorem algextdeglem4

Proof