This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )