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

Metamath Proof Explorer

Theorem fldgenval

Description: Value of the field generating function: ( F fldGen S ) is the smallest sub-division-ring of F containing S . (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 fldgenval 
|- ( ph -> ( F fldGen S ) = |^| { a e. ( SubDRing ` F ) | S C_ a } )

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 2 elexd 
 |-  ( ph -> F e. _V )
5 1 fvexi 
 |-  B e. _V
6 5 a1i 
 |-  ( ph -> B e. _V )
7 6 3 ssexd 
 |-  ( ph -> S e. _V )
8 1 sdrgid 
 |-  ( F e. DivRing -> B e. ( SubDRing ` F ) )
9 2 8 syl 
 |-  ( ph -> B e. ( SubDRing ` F ) )
10 sseq2 
 |-  ( a = B -> ( S C_ a <-> S C_ B ) )
11 10 adantl 
 |-  ( ( ph /\ a = B ) -> ( S C_ a <-> S C_ B ) )
12 9 11 3 rspcedvd 
 |-  ( ph -> E. a e. ( SubDRing ` F ) S C_ a )
13 intexrab 
 |-  ( E. a e. ( SubDRing ` F ) S C_ a <-> |^| { a e. ( SubDRing ` F ) | S C_ a } e. _V )
14 12 13 sylib 
 |-  ( ph -> |^| { a e. ( SubDRing ` F ) | S C_ a } e. _V )
15 simpl 
 |-  ( ( f = F /\ s = S ) -> f = F )
16 15 fveq2d 
 |-  ( ( f = F /\ s = S ) -> ( SubDRing ` f ) = ( SubDRing ` F ) )
17 simpr 
 |-  ( ( f = F /\ s = S ) -> s = S )
18 17 sseq1d 
 |-  ( ( f = F /\ s = S ) -> ( s C_ a <-> S C_ a ) )
19 16 18 rabeqbidv 
 |-  ( ( f = F /\ s = S ) -> { a e. ( SubDRing ` f ) | s C_ a } = { a e. ( SubDRing ` F ) | S C_ a } )
20 19 inteqd 
 |-  ( ( f = F /\ s = S ) -> |^| { a e. ( SubDRing ` f ) | s C_ a } = |^| { a e. ( SubDRing ` F ) | S C_ a } )
21 df-fldgen 
 |-  fldGen = ( f e. _V , s e. _V |-> |^| { a e. ( SubDRing ` f ) | s C_ a } )
22 20 21 ovmpoga 
 |-  ( ( F e. _V /\ S e. _V /\ |^| { a e. ( SubDRing ` F ) | S C_ a } e. _V ) -> ( F fldGen S ) = |^| { a e. ( SubDRing ` F ) | S C_ a } )
23 4 7 14 22 syl3anc 
 |-  ( ph -> ( F fldGen S ) = |^| { a e. ( SubDRing ` F ) | S C_ a } )