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