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

Metamath Proof Explorer

Theorem pwsvscaval

Description: Scalar multiplication of a single coordinate in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015)

Ref Expression
Hypotheses pwsvscaval.y 
|- Y = ( R ^s I )
pwsvscaval.b 
|- B = ( Base ` Y )
pwsvscaval.s 
|- .x. = ( .s ` R )
pwsvscaval.t 
|- .xb = ( .s ` Y )
pwsvscaval.f 
|- F = ( Scalar ` R )
pwsvscaval.k 
|- K = ( Base ` F )
pwsvscaval.r 
|- ( ph -> R e. V )
pwsvscaval.i 
|- ( ph -> I e. W )
pwsvscaval.a 
|- ( ph -> A e. K )
pwsvscaval.x 
|- ( ph -> X e. B )
pwsvscaval.j 
|- ( ph -> J e. I )
Assertion pwsvscaval 
|- ( ph -> ( ( A .xb X ) ` J ) = ( A .x. ( X ` J ) ) )

Proof

Step Hyp Ref Expression
1 pwsvscaval.y 
 |-  Y = ( R ^s I )
2 pwsvscaval.b 
 |-  B = ( Base ` Y )
3 pwsvscaval.s 
 |-  .x. = ( .s ` R )
4 pwsvscaval.t 
 |-  .xb = ( .s ` Y )
5 pwsvscaval.f 
 |-  F = ( Scalar ` R )
6 pwsvscaval.k 
 |-  K = ( Base ` F )
7 pwsvscaval.r 
 |-  ( ph -> R e. V )
8 pwsvscaval.i 
 |-  ( ph -> I e. W )
9 pwsvscaval.a 
 |-  ( ph -> A e. K )
10 pwsvscaval.x 
 |-  ( ph -> X e. B )
11 pwsvscaval.j 
 |-  ( ph -> J e. I )
12 1 2 3 4 5 6 7 8 9 10 pwsvscafval 
 |-  ( ph -> ( A .xb X ) = ( ( I X. { A } ) oF .x. X ) )
13 12 fveq1d 
 |-  ( ph -> ( ( A .xb X ) ` J ) = ( ( ( I X. { A } ) oF .x. X ) ` J ) )
14 eqid 
 |-  ( Base ` R ) = ( Base ` R )
15 1 14 2 7 8 10 pwselbas 
 |-  ( ph -> X : I --> ( Base ` R ) )
16 15 ffnd 
 |-  ( ph -> X Fn I )
17 eqidd 
 |-  ( ( ph /\ J e. I ) -> ( X ` J ) = ( X ` J ) )
18 8 9 16 17 ofc1 
 |-  ( ( ph /\ J e. I ) -> ( ( ( I X. { A } ) oF .x. X ) ` J ) = ( A .x. ( X ` J ) ) )
19 11 18 mpdan 
 |-  ( ph -> ( ( ( I X. { A } ) oF .x. X ) ` J ) = ( A .x. ( X ` J ) ) )
20 13 19 eqtrd 
 |-  ( ph -> ( ( A .xb X ) ` J ) = ( A .x. ( X ` J ) ) )