Metamath Proof Explorer

Theorem sravsca

Description: The scalar product operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Mario Carneiro, 4-Oct-2015) (Revised by Thierry Arnoux, 16-Jun-2019)

Ref Expression
Hypotheses srapart.a 
|- ( ph -> A = ( ( subringAlg ` W ) ` S ) )
srapart.s 
|- ( ph -> S C_ ( Base ` W ) )
Assertion sravsca 
|- ( ph -> ( .r ` W ) = ( .s ` A ) )

Proof

Step Hyp Ref Expression
1 srapart.a 
 |-  ( ph -> A = ( ( subringAlg ` W ) ` S ) )
2 srapart.s 
 |-  ( ph -> S C_ ( Base ` W ) )
3 ovex 
 |-  ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) e. _V
4 fvex 
 |-  ( .r ` W ) e. _V
5 vscaid 
 |-  .s = Slot ( .s ` ndx )
6 5 setsid 
 |-  ( ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) e. _V /\ ( .r ` W ) e. _V ) -> ( .r ` W ) = ( .s ` ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) ) )
7 3 4 6 mp2an 
 |-  ( .r ` W ) = ( .s ` ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) )
8 6re 
 |-  6 e. RR
9 6lt8 
 |-  6 < 8
10 8 9 ltneii 
 |-  6 =/= 8
11 vscandx 
 |-  ( .s ` ndx ) = 6
12 ipndx 
 |-  ( .i ` ndx ) = 8
13 11 12 neeq12i 
 |-  ( ( .s ` ndx ) =/= ( .i ` ndx ) <-> 6 =/= 8 )
14 10 13 mpbir 
 |-  ( .s ` ndx ) =/= ( .i ` ndx )
15 5 14 setsnid 
 |-  ( .s ` ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) ) = ( .s ` ( ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) sSet <. ( .i ` ndx ) , ( .r ` W ) >. ) )
16 7 15 eqtri 
 |-  ( .r ` W ) = ( .s ` ( ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) sSet <. ( .i ` ndx ) , ( .r ` W ) >. ) )
17 1 adantl 
 |-  ( ( W e. _V /\ ph ) -> A = ( ( subringAlg ` W ) ` S ) )
18 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 ) >. ) )
19 2 18 sylan2 
 |-  ( ( W e. _V /\ ph ) -> ( ( subringAlg ` W ) ` S ) = ( ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) sSet <. ( .i ` ndx ) , ( .r ` W ) >. ) )
20 17 19 eqtrd 
 |-  ( ( W e. _V /\ ph ) -> A = ( ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) sSet <. ( .i ` ndx ) , ( .r ` W ) >. ) )
21 20 fveq2d 
 |-  ( ( W e. _V /\ ph ) -> ( .s ` A ) = ( .s ` ( ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) sSet <. ( .i ` ndx ) , ( .r ` W ) >. ) ) )
22 16 21 eqtr4id 
 |-  ( ( W e. _V /\ ph ) -> ( .r ` W ) = ( .s ` A ) )
23 5 str0 
 |-  (/) = ( .s ` (/) )
24 fvprc 
 |-  ( -. W e. _V -> ( .r ` W ) = (/) )
25 24 adantr 
 |-  ( ( -. W e. _V /\ ph ) -> ( .r ` W ) = (/) )
26 fv2prc 
 |-  ( -. W e. _V -> ( ( subringAlg ` W ) ` S ) = (/) )
27 1 26 sylan9eqr 
 |-  ( ( -. W e. _V /\ ph ) -> A = (/) )
28 27 fveq2d 
 |-  ( ( -. W e. _V /\ ph ) -> ( .s ` A ) = ( .s ` (/) ) )
29 23 25 28 3eqtr4a 
 |-  ( ( -. W e. _V /\ ph ) -> ( .r ` W ) = ( .s ` A ) )
30 22 29 pm2.61ian 
 |-  ( ph -> ( .r ` W ) = ( .s ` A ) )