Metamath Proof Explorer

Theorem sraval

Description: Lemma for srabase through sravsca . (Contributed by Mario Carneiro, 27-Nov-2014) (Revised by Thierry Arnoux, 16-Jun-2019)

Ref Expression
Assertion sraval 
|- ( ( W e. V /\ S C_ ( Base ` W ) ) -> ( ( subringAlg ` W ) ` S ) = ( ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) sSet <. ( .i ` ndx ) , ( .r ` W ) >. ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( W e. V -> W e. _V )
2 1 adantr 
 |-  ( ( W e. V /\ S C_ ( Base ` W ) ) -> W e. _V )
3 fveq2 
 |-  ( w = W -> ( Base ` w ) = ( Base ` W ) )
4 3 pweqd 
 |-  ( w = W -> ~P ( Base ` w ) = ~P ( Base ` W ) )
5 id 
 |-  ( w = W -> w = W )
6 oveq1 
 |-  ( w = W -> ( w |`s s ) = ( W |`s s ) )
7 6 opeq2d 
 |-  ( w = W -> <. ( Scalar ` ndx ) , ( w |`s s ) >. = <. ( Scalar ` ndx ) , ( W |`s s ) >. )
8 5 7 oveq12d 
 |-  ( w = W -> ( w sSet <. ( Scalar ` ndx ) , ( w |`s s ) >. ) = ( W sSet <. ( Scalar ` ndx ) , ( W |`s s ) >. ) )
9 fveq2 
 |-  ( w = W -> ( .r ` w ) = ( .r ` W ) )
10 9 opeq2d 
 |-  ( w = W -> <. ( .s ` ndx ) , ( .r ` w ) >. = <. ( .s ` ndx ) , ( .r ` W ) >. )
11 8 10 oveq12d 
 |-  ( w = W -> ( ( w sSet <. ( Scalar ` ndx ) , ( w |`s s ) >. ) sSet <. ( .s ` ndx ) , ( .r ` w ) >. ) = ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s s ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) )
12 9 opeq2d 
 |-  ( w = W -> <. ( .i ` ndx ) , ( .r ` w ) >. = <. ( .i ` ndx ) , ( .r ` W ) >. )
13 11 12 oveq12d 
 |-  ( w = W -> ( ( ( w sSet <. ( Scalar ` ndx ) , ( w |`s s ) >. ) sSet <. ( .s ` ndx ) , ( .r ` w ) >. ) sSet <. ( .i ` ndx ) , ( .r ` w ) >. ) = ( ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s s ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) sSet <. ( .i ` ndx ) , ( .r ` W ) >. ) )
14 4 13 mpteq12dv 
 |-  ( w = W -> ( s e. ~P ( Base ` w ) |-> ( ( ( w sSet <. ( Scalar ` ndx ) , ( w |`s s ) >. ) sSet <. ( .s ` ndx ) , ( .r ` w ) >. ) sSet <. ( .i ` ndx ) , ( .r ` w ) >. ) ) = ( s e. ~P ( Base ` W ) |-> ( ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s s ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) sSet <. ( .i ` ndx ) , ( .r ` W ) >. ) ) )
15 df-sra 
 |-  subringAlg = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> ( ( ( w sSet <. ( Scalar ` ndx ) , ( w |`s s ) >. ) sSet <. ( .s ` ndx ) , ( .r ` w ) >. ) sSet <. ( .i ` ndx ) , ( .r ` w ) >. ) ) )
16 fvex 
 |-  ( Base ` W ) e. _V
17 16 pwex 
 |-  ~P ( Base ` W ) e. _V
18 17 mptex 
 |-  ( s e. ~P ( Base ` W ) |-> ( ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s s ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) sSet <. ( .i ` ndx ) , ( .r ` W ) >. ) ) e. _V
19 14 15 18 fvmpt 
 |-  ( W e. _V -> ( subringAlg ` W ) = ( s e. ~P ( Base ` W ) |-> ( ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s s ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) sSet <. ( .i ` ndx ) , ( .r ` W ) >. ) ) )
20 2 19 syl 
 |-  ( ( W e. V /\ S C_ ( Base ` W ) ) -> ( subringAlg ` W ) = ( s e. ~P ( Base ` W ) |-> ( ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s s ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) sSet <. ( .i ` ndx ) , ( .r ` W ) >. ) ) )
21 simpr 
 |-  ( ( ( W e. V /\ S C_ ( Base ` W ) ) /\ s = S ) -> s = S )
22 21 oveq2d 
 |-  ( ( ( W e. V /\ S C_ ( Base ` W ) ) /\ s = S ) -> ( W |`s s ) = ( W |`s S ) )
23 22 opeq2d 
 |-  ( ( ( W e. V /\ S C_ ( Base ` W ) ) /\ s = S ) -> <. ( Scalar ` ndx ) , ( W |`s s ) >. = <. ( Scalar ` ndx ) , ( W |`s S ) >. )
24 23 oveq2d 
 |-  ( ( ( W e. V /\ S C_ ( Base ` W ) ) /\ s = S ) -> ( W sSet <. ( Scalar ` ndx ) , ( W |`s s ) >. ) = ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) )
25 24 oveq1d 
 |-  ( ( ( W e. V /\ S C_ ( Base ` W ) ) /\ s = S ) -> ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s s ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) = ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) )
26 25 oveq1d 
 |-  ( ( ( W e. V /\ S C_ ( Base ` W ) ) /\ s = S ) -> ( ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s s ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) sSet <. ( .i ` ndx ) , ( .r ` W ) >. ) = ( ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) sSet <. ( .i ` ndx ) , ( .r ` W ) >. ) )
27 simpr 
 |-  ( ( W e. V /\ S C_ ( Base ` W ) ) -> S C_ ( Base ` W ) )
28 16 elpw2 
 |-  ( S e. ~P ( Base ` W ) <-> S C_ ( Base ` W ) )
29 27 28 sylibr 
 |-  ( ( W e. V /\ S C_ ( Base ` W ) ) -> S e. ~P ( Base ` W ) )
30 ovexd 
 |-  ( ( W e. V /\ S C_ ( Base ` W ) ) -> ( ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) sSet <. ( .i ` ndx ) , ( .r ` W ) >. ) e. _V )
31 20 26 29 30 fvmptd 
 |-  ( ( W e. V /\ S C_ ( Base ` W ) ) -> ( ( subringAlg ` W ) ` S ) = ( ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) sSet <. ( .i ` ndx ) , ( .r ` W ) >. ) )