Theorem fldgenidfld

Description: The subfield generated by a subfield is the subfield itself. (Contributed by Thierry Arnoux, 15-Jan-2025)

	Ref	Expression
Hypotheses	fldgenval.1	$$⊢B={\mathrm{Base}}_F$$
	fldgenval.2	$$⊢\phi \to F\in \mathrm{DivRing}$$
	fldgenidfld.s	$$⊢\phi \to S\in \mathrm{SubDRing}\left(F\right)$$
Assertion	fldgenidfld	Could not format assertion : No typesetting found for |- ( ph -> ( F fldGen S ) = S ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		fldgenval.1	$$⊢B={\mathrm{Base}}_F$$
2		fldgenval.2	$$⊢\phi \to F\in \mathrm{DivRing}$$
3		fldgenidfld.s	$$⊢\phi \to S\in \mathrm{SubDRing}\left(F\right)$$
4	1	sdrgss	$$⊢S\in \mathrm{SubDRing}\left(F\right)\to S\subseteq B$$
5	3 4	syl	$$⊢\phi \to S\subseteq B$$
6	1 2 5	fldgenval	Could not format ( ph -> ( F fldGen S ) = |^| { a e. ( SubDRing ` F ) | S C_ a } ) : No typesetting found for |- ( ph -> ( F fldGen S ) = |^| { a e. ( SubDRing ` F ) | S C_ a } ) with typecode |-
7		intmin	$$⊢S\in \mathrm{SubDRing}\left(F\right)\to \bigcap \left\{a\in \mathrm{SubDRing}\left(F\right)|S\subseteq a\right\}=S$$
8	3 7	syl	$$⊢\phi \to \bigcap \left\{a\in \mathrm{SubDRing}\left(F\right)|S\subseteq a\right\}=S$$
9	6 8	eqtrd	Could not format ( ph -> ( F fldGen S ) = S ) : No typesetting found for |- ( ph -> ( F fldGen S ) = S ) with typecode |-