# 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 ) )`
` |-  ( ( 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 ) )`