Metamath Proof Explorer

Theorem fldgensdrg

Description: A generated subfield is a sub-division-ring. (Contributed by Thierry Arnoux, 11-Jan-2025)

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

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 2 drngringd 
 |-  ( ph -> F e. Ring )
6 eqid 
 |-  ( F |`s |^| { a e. ( SubDRing ` F ) | S C_ a } ) = ( F |`s |^| { a e. ( SubDRing ` F ) | S C_ a } )
7 sseq2 
 |-  ( a = x -> ( S C_ a <-> S C_ x ) )
8 7 elrab 
 |-  ( x e. { a e. ( SubDRing ` F ) | S C_ a } <-> ( x e. ( SubDRing ` F ) /\ S C_ x ) )
9 8 biimpi 
 |-  ( x e. { a e. ( SubDRing ` F ) | S C_ a } -> ( x e. ( SubDRing ` F ) /\ S C_ x ) )
10 9 adantl 
 |-  ( ( ph /\ x e. { a e. ( SubDRing ` F ) | S C_ a } ) -> ( x e. ( SubDRing ` F ) /\ S C_ x ) )
11 10 simpld 
 |-  ( ( ph /\ x e. { a e. ( SubDRing ` F ) | S C_ a } ) -> x e. ( SubDRing ` F ) )
12 issdrg 
 |-  ( x e. ( SubDRing ` F ) <-> ( F e. DivRing /\ x e. ( SubRing ` F ) /\ ( F |`s x ) e. DivRing ) )
13 12 simp2bi 
 |-  ( x e. ( SubDRing ` F ) -> x e. ( SubRing ` F ) )
14 11 13 syl 
 |-  ( ( ph /\ x e. { a e. ( SubDRing ` F ) | S C_ a } ) -> x e. ( SubRing ` F ) )
15 14 ex 
 |-  ( ph -> ( x e. { a e. ( SubDRing ` F ) | S C_ a } -> x e. ( SubRing ` F ) ) )
16 15 ssrdv 
 |-  ( ph -> { a e. ( SubDRing ` F ) | S C_ a } C_ ( SubRing ` F ) )
17 sseq2 
 |-  ( a = B -> ( S C_ a <-> S C_ B ) )
18 1 sdrgid 
 |-  ( F e. DivRing -> B e. ( SubDRing ` F ) )
19 2 18 syl 
 |-  ( ph -> B e. ( SubDRing ` F ) )
20 17 19 3 elrabd 
 |-  ( ph -> B e. { a e. ( SubDRing ` F ) | S C_ a } )
21 20 ne0d 
 |-  ( ph -> { a e. ( SubDRing ` F ) | S C_ a } =/= (/) )
22 12 simp3bi 
 |-  ( x e. ( SubDRing ` F ) -> ( F |`s x ) e. DivRing )
23 11 22 syl 
 |-  ( ( ph /\ x e. { a e. ( SubDRing ` F ) | S C_ a } ) -> ( F |`s x ) e. DivRing )
24 6 2 16 21 23 subdrgint 
 |-  ( ph -> ( F |`s |^| { a e. ( SubDRing ` F ) | S C_ a } ) e. DivRing )
25 24 drngringd 
 |-  ( ph -> ( F |`s |^| { a e. ( SubDRing ` F ) | S C_ a } ) e. Ring )
26 intss1 
 |-  ( B e. { a e. ( SubDRing ` F ) | S C_ a } -> |^| { a e. ( SubDRing ` F ) | S C_ a } C_ B )
27 20 26 syl 
 |-  ( ph -> |^| { a e. ( SubDRing ` F ) | S C_ a } C_ B )
28 issdrg 
 |-  ( a e. ( SubDRing ` F ) <-> ( F e. DivRing /\ a e. ( SubRing ` F ) /\ ( F |`s a ) e. DivRing ) )
29 28 simp2bi 
 |-  ( a e. ( SubDRing ` F ) -> a e. ( SubRing ` F ) )
30 eqid 
 |-  ( 1r ` F ) = ( 1r ` F )
31 30 subrg1cl 
 |-  ( a e. ( SubRing ` F ) -> ( 1r ` F ) e. a )
32 29 31 syl 
 |-  ( a e. ( SubDRing ` F ) -> ( 1r ` F ) e. a )
33 32 ad2antlr 
 |-  ( ( ( ph /\ a e. ( SubDRing ` F ) ) /\ S C_ a ) -> ( 1r ` F ) e. a )
34 33 ex 
 |-  ( ( ph /\ a e. ( SubDRing ` F ) ) -> ( S C_ a -> ( 1r ` F ) e. a ) )
35 34 ralrimiva 
 |-  ( ph -> A. a e. ( SubDRing ` F ) ( S C_ a -> ( 1r ` F ) e. a ) )
36 fvex 
 |-  ( 1r ` F ) e. _V
37 36 elintrab 
 |-  ( ( 1r ` F ) e. |^| { a e. ( SubDRing ` F ) | S C_ a } <-> A. a e. ( SubDRing ` F ) ( S C_ a -> ( 1r ` F ) e. a ) )
38 35 37 sylibr 
 |-  ( ph -> ( 1r ` F ) e. |^| { a e. ( SubDRing ` F ) | S C_ a } )
39 1 30 issubrg 
 |-  ( |^| { a e. ( SubDRing ` F ) | S C_ a } e. ( SubRing ` F ) <-> ( ( F e. Ring /\ ( F |`s |^| { a e. ( SubDRing ` F ) | S C_ a } ) e. Ring ) /\ ( |^| { a e. ( SubDRing ` F ) | S C_ a } C_ B /\ ( 1r ` F ) e. |^| { a e. ( SubDRing ` F ) | S C_ a } ) ) )
40 39 biimpri 
 |-  ( ( ( F e. Ring /\ ( F |`s |^| { a e. ( SubDRing ` F ) | S C_ a } ) e. Ring ) /\ ( |^| { a e. ( SubDRing ` F ) | S C_ a } C_ B /\ ( 1r ` F ) e. |^| { a e. ( SubDRing ` F ) | S C_ a } ) ) -> |^| { a e. ( SubDRing ` F ) | S C_ a } e. ( SubRing ` F ) )
41 5 25 27 38 40 syl22anc 
 |-  ( ph -> |^| { a e. ( SubDRing ` F ) | S C_ a } e. ( SubRing ` F ) )
42 issdrg 
 |-  ( |^| { a e. ( SubDRing ` F ) | S C_ a } e. ( SubDRing ` F ) <-> ( F e. DivRing /\ |^| { a e. ( SubDRing ` F ) | S C_ a } e. ( SubRing ` F ) /\ ( F |`s |^| { a e. ( SubDRing ` F ) | S C_ a } ) e. DivRing ) )
43 2 41 24 42 syl3anbrc 
 |-  ( ph -> |^| { a e. ( SubDRing ` F ) | S C_ a } e. ( SubDRing ` F ) )
44 4 43 eqeltrd 
 |-  ( ph -> ( F fldGen S ) e. ( SubDRing ` F ) )