Theorem algextdeglem4

Description: Lemma for algextdeg . (Contributed by Thierry Arnoux, 2-Apr-2025)

	Ref	Expression
Hypotheses	algextdeg.k	$$⊢K=E{\upharpoonright }_{𝑠}F$$
	algextdeg.l	No typesetting found for |- L = ( E |`s ( E fldGen ( F u. { A } ) ) ) with typecode |-
	algextdeg.d	$$⊢D={\mathrm{deg}}_1\left(E\right)$$
	algextdeg.m	No typesetting found for |- M = ( E minPoly F ) with typecode |-
	algextdeg.f	$$⊢\phi \to E\in \mathrm{Field}$$
	algextdeg.e	$$⊢\phi \to F\in \mathrm{SubDRing}\left(E\right)$$
	algextdeg.a	$$⊢\phi \to A\in \left(E\mathrm{IntgRing}F\right)$$
	algextdeglem.o	$$⊢O=E{\mathrm{evalSub}}_{1}F$$
	algextdeglem.y	$$⊢P={\mathrm{Poly}}_1\left(K\right)$$
	algextdeglem.u	$$⊢U={\mathrm{Base}}_P$$
	algextdeglem.g	$$⊢G=\left(p\in U⟼O\left(p\right)\left(A\right)\right)$$
	algextdeglem.n	$$⊢N=\left(x\in U⟼\left[x\right]\left(P{~}_{\mathit{QG}}Z\right)\right)$$
	algextdeglem.z	$$⊢Z=G^{-1}\left[\left\{0_L\right\}\right]$$
	algextdeglem.q	$$⊢Q=P{/}_{𝑠}\left(P{~}_{\mathit{QG}}Z\right)$$
	algextdeglem.j	$$⊢J=\left(p\in {\mathrm{Base}}_Q⟼\bigcup G\left[p\right]\right)$$
Assertion	algextdeglem4	$$⊢\phi \to \dim \left(Q\right)=L\left[.:.\right]K$$

Proof

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