Metamath Proof Explorer

Theorem matvsca2

Description: Scalar multiplication in the matrix ring is cell-wise. (Contributed by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypotheses matvsca2.a 
|- A = ( N Mat R )
matvsca2.b 
|- B = ( Base ` A )
matvsca2.k 
|- K = ( Base ` R )
matvsca2.v 
|- .x. = ( .s ` A )
matvsca2.t 
|- .X. = ( .r ` R )
matvsca2.c 
|- C = ( N X. N )
Assertion matvsca2 
|- ( ( X e. K /\ Y e. B ) -> ( X .x. Y ) = ( ( C X. { X } ) oF .X. Y ) )

Proof

Step Hyp Ref Expression
1 matvsca2.a 
 |-  A = ( N Mat R )
2 matvsca2.b 
 |-  B = ( Base ` A )
3 matvsca2.k 
 |-  K = ( Base ` R )
4 matvsca2.v 
 |-  .x. = ( .s ` A )
5 matvsca2.t 
 |-  .X. = ( .r ` R )
6 matvsca2.c 
 |-  C = ( N X. N )
7 1 2 matrcl 
 |-  ( Y e. B -> ( N e. Fin /\ R e. _V ) )
8 7 adantl 
 |-  ( ( X e. K /\ Y e. B ) -> ( N e. Fin /\ R e. _V ) )
9 eqid 
 |-  ( R freeLMod ( N X. N ) ) = ( R freeLMod ( N X. N ) )
10 1 9 matvsca 
 |-  ( ( N e. Fin /\ R e. _V ) -> ( .s ` ( R freeLMod ( N X. N ) ) ) = ( .s ` A ) )
11 8 10 syl 
 |-  ( ( X e. K /\ Y e. B ) -> ( .s ` ( R freeLMod ( N X. N ) ) ) = ( .s ` A ) )
12 11 4 eqtr4di 
 |-  ( ( X e. K /\ Y e. B ) -> ( .s ` ( R freeLMod ( N X. N ) ) ) = .x. )
13 12 oveqd 
 |-  ( ( X e. K /\ Y e. B ) -> ( X ( .s ` ( R freeLMod ( N X. N ) ) ) Y ) = ( X .x. Y ) )
14 eqid 
 |-  ( Base ` ( R freeLMod ( N X. N ) ) ) = ( Base ` ( R freeLMod ( N X. N ) ) )
15 8 simpld 
 |-  ( ( X e. K /\ Y e. B ) -> N e. Fin )
16 xpfi 
 |-  ( ( N e. Fin /\ N e. Fin ) -> ( N X. N ) e. Fin )
17 15 15 16 syl2anc 
 |-  ( ( X e. K /\ Y e. B ) -> ( N X. N ) e. Fin )
18 simpl 
 |-  ( ( X e. K /\ Y e. B ) -> X e. K )
19 simpr 
 |-  ( ( X e. K /\ Y e. B ) -> Y e. B )
20 1 9 matbas 
 |-  ( ( N e. Fin /\ R e. _V ) -> ( Base ` ( R freeLMod ( N X. N ) ) ) = ( Base ` A ) )
21 8 20 syl 
 |-  ( ( X e. K /\ Y e. B ) -> ( Base ` ( R freeLMod ( N X. N ) ) ) = ( Base ` A ) )
22 21 2 eqtr4di 
 |-  ( ( X e. K /\ Y e. B ) -> ( Base ` ( R freeLMod ( N X. N ) ) ) = B )
23 19 22 eleqtrrd 
 |-  ( ( X e. K /\ Y e. B ) -> Y e. ( Base ` ( R freeLMod ( N X. N ) ) ) )
24 eqid 
 |-  ( .s ` ( R freeLMod ( N X. N ) ) ) = ( .s ` ( R freeLMod ( N X. N ) ) )
25 9 14 3 17 18 23 24 5 frlmvscafval 
 |-  ( ( X e. K /\ Y e. B ) -> ( X ( .s ` ( R freeLMod ( N X. N ) ) ) Y ) = ( ( ( N X. N ) X. { X } ) oF .X. Y ) )
26 6 xpeq1i 
 |-  ( C X. { X } ) = ( ( N X. N ) X. { X } )
27 26 oveq1i 
 |-  ( ( C X. { X } ) oF .X. Y ) = ( ( ( N X. N ) X. { X } ) oF .X. Y )
28 25 27 eqtr4di 
 |-  ( ( X e. K /\ Y e. B ) -> ( X ( .s ` ( R freeLMod ( N X. N ) ) ) Y ) = ( ( C X. { X } ) oF .X. Y ) )
29 13 28 eqtr3d 
 |-  ( ( X e. K /\ Y e. B ) -> ( X .x. Y ) = ( ( C X. { X } ) oF .X. Y ) )