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

Metamath Proof Explorer

Theorem fldgenssv

Description: A generated subfield is a subset of the field's base. (Contributed by Thierry Arnoux, 25-Feb-2025)

Ref Expression
Hypotheses fldgenval.1 
|- B = ( Base ` F )
fldgenval.2 
|- ( ph -> F e. DivRing )
fldgenval.3 
|- ( ph -> S C_ B )
Assertion fldgenssv 
|- ( ph -> ( F fldGen S ) C_ B )

Proof

Step Hyp Ref Expression
1 fldgenval.1 
 |-  B = ( Base ` F )
2 fldgenval.2 
 |-  ( ph -> F e. DivRing )
3 fldgenval.3 
 |-  ( ph -> S C_ B )
4 1 2 3 fldgenval 
 |-  ( ph -> ( F fldGen S ) = |^| { a e. ( SubDRing ` F ) | S C_ a } )
5 sseq2 
 |-  ( a = B -> ( S C_ a <-> S C_ B ) )
6 1 sdrgid 
 |-  ( F e. DivRing -> B e. ( SubDRing ` F ) )
7 2 6 syl 
 |-  ( ph -> B e. ( SubDRing ` F ) )
8 5 7 3 elrabd 
 |-  ( ph -> B e. { a e. ( SubDRing ` F ) | S C_ a } )
9 intss1 
 |-  ( B e. { a e. ( SubDRing ` F ) | S C_ a } -> |^| { a e. ( SubDRing ` F ) | S C_ a } C_ B )
10 8 9 syl 
 |-  ( ph -> |^| { a e. ( SubDRing ` F ) | S C_ a } C_ B )
11 4 10 eqsstrd 
 |-  ( ph -> ( F fldGen S ) C_ B )