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

Metamath Proof Explorer

Theorem fldgenssp

Description: The field generated by a set of elements in a division ring is contained in any sub-division-ring which contains those elements. (Contributed by Thierry Arnoux, 25-Feb-2025)

Ref Expression
Hypotheses fldgenval.1 
|- B = ( Base ` F )
fldgenval.2 
|- ( ph -> F e. DivRing )
fldgenidfld.s 
|- ( ph -> S e. ( SubDRing ` F ) )
fldgenssp.t 
|- ( ph -> T C_ S )
Assertion fldgenssp 
|- ( ph -> ( F fldGen T ) C_ 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 fldgenssp.t 
 |-  ( ph -> T C_ S )
5 issdrg 
 |-  ( S e. ( SubDRing ` F ) <-> ( F e. DivRing /\ S e. ( SubRing ` F ) /\ ( F |`s S ) e. DivRing ) )
6 3 5 sylib 
 |-  ( ph -> ( F e. DivRing /\ S e. ( SubRing ` F ) /\ ( F |`s S ) e. DivRing ) )
7 6 simp2d 
 |-  ( ph -> S e. ( SubRing ` F ) )
8 1 subrgss 
 |-  ( S e. ( SubRing ` F ) -> S C_ B )
9 7 8 syl 
 |-  ( ph -> S C_ B )
10 4 9 sstrd 
 |-  ( ph -> T C_ B )
11 1 2 10 fldgenval 
 |-  ( ph -> ( F fldGen T ) = |^| { a e. ( SubDRing ` F ) | T C_ a } )
12 sseq2 
 |-  ( a = S -> ( T C_ a <-> T C_ S ) )
13 12 3 4 elrabd 
 |-  ( ph -> S e. { a e. ( SubDRing ` F ) | T C_ a } )
14 intss1 
 |-  ( S e. { a e. ( SubDRing ` F ) | T C_ a } -> |^| { a e. ( SubDRing ` F ) | T C_ a } C_ S )
15 13 14 syl 
 |-  ( ph -> |^| { a e. ( SubDRing ` F ) | T C_ a } C_ S )
16 11 15 eqsstrd 
 |-  ( ph -> ( F fldGen T ) C_ S )