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 = ( Base ` F )
	fldgenval.2	|- ( ph -> F e. DivRing )
	fldgenidfld.s	|- ( ph -> S e. ( SubDRing ` F ) )
Assertion	fldgenidfld	|- ( ph -> ( F fldGen S ) = S )

Proof

Step	Hyp	Ref	Expression
1		fldgenval.1	|- B = ( Base ` F )
2		fldgenval.2	|- ( ph -> F e. DivRing )
3		fldgenidfld.s	|- ( ph -> S e. ( SubDRing ` F ) )
4	1	sdrgss	|- ( S e. ( SubDRing ` F ) -> S C_ B )
5	3 4	syl	|- ( ph -> S C_ B )
6	1 2 5	fldgenval	|- ( ph -> ( F fldGen S ) = |^| { a e. ( SubDRing ` F ) | S C_ a } )
7		intmin	|- ( S e. ( SubDRing ` F ) -> |^| { a e. ( SubDRing ` F ) | S C_ a } = S )
8	3 7	syl	|- ( ph -> |^| { a e. ( SubDRing ` F ) | S C_ a } = S )
9	6 8	eqtrd	|- ( ph -> ( F fldGen S ) = S )