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

Metamath Proof Explorer

Theorem frlmvscaval

Description: Coordinates of a scalar multiple with respect to a basis in a free module. (Contributed by Stefan O'Rear, 3-Feb-2015)

Ref Expression
Hypotheses frlmvscaval.y 
|- Y = ( R freeLMod I )
frlmvscaval.b 
|- B = ( Base ` Y )
frlmvscaval.k 
|- K = ( Base ` R )
frlmvscaval.i 
|- ( ph -> I e. W )
frlmvscaval.a 
|- ( ph -> A e. K )
frlmvscaval.x 
|- ( ph -> X e. B )
frlmvscaval.j 
|- ( ph -> J e. I )
frlmvscaval.v 
|- .xb = ( .s ` Y )
frlmvscaval.t 
|- .x. = ( .r ` R )
Assertion frlmvscaval 
|- ( ph -> ( ( A .xb X ) ` J ) = ( A .x. ( X ` J ) ) )

Proof

Step Hyp Ref Expression
1 frlmvscaval.y 
 |-  Y = ( R freeLMod I )
2 frlmvscaval.b 
 |-  B = ( Base ` Y )
3 frlmvscaval.k 
 |-  K = ( Base ` R )
4 frlmvscaval.i 
 |-  ( ph -> I e. W )
5 frlmvscaval.a 
 |-  ( ph -> A e. K )
6 frlmvscaval.x 
 |-  ( ph -> X e. B )
7 frlmvscaval.j 
 |-  ( ph -> J e. I )
8 frlmvscaval.v 
 |-  .xb = ( .s ` Y )
9 frlmvscaval.t 
 |-  .x. = ( .r ` R )
10 1 2 3 4 5 6 8 9 frlmvscafval 
 |-  ( ph -> ( A .xb X ) = ( ( I X. { A } ) oF .x. X ) )
11 10 fveq1d 
 |-  ( ph -> ( ( A .xb X ) ` J ) = ( ( ( I X. { A } ) oF .x. X ) ` J ) )
12 fnconstg 
 |-  ( A e. K -> ( I X. { A } ) Fn I )
13 5 12 syl 
 |-  ( ph -> ( I X. { A } ) Fn I )
14 1 3 2 frlmbasf 
 |-  ( ( I e. W /\ X e. B ) -> X : I --> K )
15 4 6 14 syl2anc 
 |-  ( ph -> X : I --> K )
16 15 ffnd 
 |-  ( ph -> X Fn I )
17 fnfvof 
 |-  ( ( ( ( I X. { A } ) Fn I /\ X Fn I ) /\ ( I e. W /\ J e. I ) ) -> ( ( ( I X. { A } ) oF .x. X ) ` J ) = ( ( ( I X. { A } ) ` J ) .x. ( X ` J ) ) )
18 13 16 4 7 17 syl22anc 
 |-  ( ph -> ( ( ( I X. { A } ) oF .x. X ) ` J ) = ( ( ( I X. { A } ) ` J ) .x. ( X ` J ) ) )
19 fvconst2g 
 |-  ( ( A e. K /\ J e. I ) -> ( ( I X. { A } ) ` J ) = A )
20 5 7 19 syl2anc 
 |-  ( ph -> ( ( I X. { A } ) ` J ) = A )
21 20 oveq1d 
 |-  ( ph -> ( ( ( I X. { A } ) ` J ) .x. ( X ` J ) ) = ( A .x. ( X ` J ) ) )
22 11 18 21 3eqtrd 
 |-  ( ph -> ( ( A .xb X ) ` J ) = ( A .x. ( X ` J ) ) )