Theorem algextdeglem1

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)$$
Assertion	algextdeglem1	$$⊢\phi \to L{\upharpoonright }_{𝑠}F=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	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 |-
9		ovex	Could not format ( E fldGen ( F u. { A } ) ) e. _V : No typesetting found for |- ( E fldGen ( F u. { A } ) ) e. _V with typecode |-
10		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
11		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)$$
12	6 11	sylib	$$⊢\phi \to \left(E\in \mathrm{DivRing}\wedge F\in \mathrm{SubRing}\left(E\right)\wedge E{\upharpoonright }_{𝑠}F\in \mathrm{DivRing}\right)$$
13	12	simp1d	$$⊢\phi \to E\in \mathrm{DivRing}$$
14	12	simp2d	$$⊢\phi \to F\in \mathrm{SubRing}\left(E\right)$$
15		subrgsubg	$$⊢F\in \mathrm{SubRing}\left(E\right)\to F\in \mathrm{SubGrp}\left(E\right)$$
16	10	subgss	$$⊢F\in \mathrm{SubGrp}\left(E\right)\to F\subseteq {\mathrm{Base}}_E$$
17	14 15 16	3syl	$$⊢\phi \to F\subseteq {\mathrm{Base}}_E$$
18		eqid	$$⊢E{\mathrm{evalSub}}_{1}F=E{\mathrm{evalSub}}_{1}F$$
19		eqid	$$⊢0_E=0_E$$
20	5	fldcrngd	$$⊢\phi \to E\in \mathrm{CRing}$$
21	18 1 10 19 20 14	irngssv	$$⊢\phi \to E\mathrm{IntgRing}F\subseteq {\mathrm{Base}}_E$$
22	21 7	sseldd	$$⊢\phi \to A\in {\mathrm{Base}}_E$$
23	22	snssd	$$⊢\phi \to \left\{A\right\}\subseteq {\mathrm{Base}}_E$$
24	17 23	unssd	$$⊢\phi \to F\cup \left\{A\right\}\subseteq {\mathrm{Base}}_E$$
25	10 13 24	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 |-
26	25	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 |-
27		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 |-
28	9 26 27	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 |-
29	8 28	eqtrid	$$⊢\phi \to L{\upharpoonright }_{𝑠}F=E{\upharpoonright }_{𝑠}F$$
30	29 1	eqtr4di	$$⊢\phi \to L{\upharpoonright }_{𝑠}F=K$$