Theorem algextdeglem1

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