Metamath Proof Explorer

Theorem rgspnval

Description: Value of the ring-span of a set of elements in a ring. (Contributed by Stefan O'Rear, 7-Dec-2014)

Ref Expression
Hypotheses rgspnval.r 
|- ( ph -> R e. Ring )
rgspnval.b 
|- ( ph -> B = ( Base ` R ) )
rgspnval.ss 
|- ( ph -> A C_ B )
rgspnval.n 
|- ( ph -> N = ( RingSpan ` R ) )
rgspnval.sp 
|- ( ph -> U = ( N ` A ) )
Assertion rgspnval 
|- ( ph -> U = |^| { t e. ( SubRing ` R ) | A C_ t } )

Proof

Step Hyp Ref Expression
1 rgspnval.r 
 |-  ( ph -> R e. Ring )
2 rgspnval.b 
 |-  ( ph -> B = ( Base ` R ) )
3 rgspnval.ss 
 |-  ( ph -> A C_ B )
4 rgspnval.n 
 |-  ( ph -> N = ( RingSpan ` R ) )
5 rgspnval.sp 
 |-  ( ph -> U = ( N ` A ) )
6 4 fveq1d 
 |-  ( ph -> ( N ` A ) = ( ( RingSpan ` R ) ` A ) )
7 elex 
 |-  ( R e. Ring -> R e. _V )
8 fveq2 
 |-  ( a = R -> ( Base ` a ) = ( Base ` R ) )
9 8 pweqd 
 |-  ( a = R -> ~P ( Base ` a ) = ~P ( Base ` R ) )
10 fveq2 
 |-  ( a = R -> ( SubRing ` a ) = ( SubRing ` R ) )
11 rabeq 
 |-  ( ( SubRing ` a ) = ( SubRing ` R ) -> { t e. ( SubRing ` a ) | b C_ t } = { t e. ( SubRing ` R ) | b C_ t } )
12 10 11 syl 
 |-  ( a = R -> { t e. ( SubRing ` a ) | b C_ t } = { t e. ( SubRing ` R ) | b C_ t } )
13 12 inteqd 
 |-  ( a = R -> |^| { t e. ( SubRing ` a ) | b C_ t } = |^| { t e. ( SubRing ` R ) | b C_ t } )
14 9 13 mpteq12dv 
 |-  ( a = R -> ( b e. ~P ( Base ` a ) |-> |^| { t e. ( SubRing ` a ) | b C_ t } ) = ( b e. ~P ( Base ` R ) |-> |^| { t e. ( SubRing ` R ) | b C_ t } ) )
15 df-rgspn 
 |-  RingSpan = ( a e. _V |-> ( b e. ~P ( Base ` a ) |-> |^| { t e. ( SubRing ` a ) | b C_ t } ) )
16 fvex 
 |-  ( Base ` R ) e. _V
17 16 pwex 
 |-  ~P ( Base ` R ) e. _V
18 17 mptex 
 |-  ( b e. ~P ( Base ` R ) |-> |^| { t e. ( SubRing ` R ) | b C_ t } ) e. _V
19 14 15 18 fvmpt 
 |-  ( R e. _V -> ( RingSpan ` R ) = ( b e. ~P ( Base ` R ) |-> |^| { t e. ( SubRing ` R ) | b C_ t } ) )
20 1 7 19 3syl 
 |-  ( ph -> ( RingSpan ` R ) = ( b e. ~P ( Base ` R ) |-> |^| { t e. ( SubRing ` R ) | b C_ t } ) )
21 20 fveq1d 
 |-  ( ph -> ( ( RingSpan ` R ) ` A ) = ( ( b e. ~P ( Base ` R ) |-> |^| { t e. ( SubRing ` R ) | b C_ t } ) ` A ) )
22 eqid 
 |-  ( b e. ~P ( Base ` R ) |-> |^| { t e. ( SubRing ` R ) | b C_ t } ) = ( b e. ~P ( Base ` R ) |-> |^| { t e. ( SubRing ` R ) | b C_ t } )
23 sseq1 
 |-  ( b = A -> ( b C_ t <-> A C_ t ) )
24 23 rabbidv 
 |-  ( b = A -> { t e. ( SubRing ` R ) | b C_ t } = { t e. ( SubRing ` R ) | A C_ t } )
25 24 inteqd 
 |-  ( b = A -> |^| { t e. ( SubRing ` R ) | b C_ t } = |^| { t e. ( SubRing ` R ) | A C_ t } )
26 3 2 sseqtrd 
 |-  ( ph -> A C_ ( Base ` R ) )
27 16 elpw2 
 |-  ( A e. ~P ( Base ` R ) <-> A C_ ( Base ` R ) )
28 26 27 sylibr 
 |-  ( ph -> A e. ~P ( Base ` R ) )
29 eqid 
 |-  ( Base ` R ) = ( Base ` R )
30 29 subrgid 
 |-  ( R e. Ring -> ( Base ` R ) e. ( SubRing ` R ) )
31 1 30 syl 
 |-  ( ph -> ( Base ` R ) e. ( SubRing ` R ) )
32 2 31 eqeltrd 
 |-  ( ph -> B e. ( SubRing ` R ) )
33 sseq2 
 |-  ( t = B -> ( A C_ t <-> A C_ B ) )
34 33 rspcev 
 |-  ( ( B e. ( SubRing ` R ) /\ A C_ B ) -> E. t e. ( SubRing ` R ) A C_ t )
35 32 3 34 syl2anc 
 |-  ( ph -> E. t e. ( SubRing ` R ) A C_ t )
36 intexrab 
 |-  ( E. t e. ( SubRing ` R ) A C_ t <-> |^| { t e. ( SubRing ` R ) | A C_ t } e. _V )
37 35 36 sylib 
 |-  ( ph -> |^| { t e. ( SubRing ` R ) | A C_ t } e. _V )
38 22 25 28 37 fvmptd3 
 |-  ( ph -> ( ( b e. ~P ( Base ` R ) |-> |^| { t e. ( SubRing ` R ) | b C_ t } ) ` A ) = |^| { t e. ( SubRing ` R ) | A C_ t } )
39 21 38 eqtrd 
 |-  ( ph -> ( ( RingSpan ` R ) ` A ) = |^| { t e. ( SubRing ` R ) | A C_ t } )
40 5 6 39 3eqtrd 
 |-  ( ph -> U = |^| { t e. ( SubRing ` R ) | A C_ t } )