Metamath Proof Explorer

Theorem matmulr

Description: Multiplication in the matrix algebra. (Contributed by Stefan O'Rear, 4-Sep-2015)

Ref Expression
Hypotheses matmulr.a 
|- A = ( N Mat R )
matmulr.t 
|- .x. = ( R maMul <. N , N , N >. )
Assertion matmulr 
|- ( ( N e. Fin /\ R e. V ) -> .x. = ( .r ` A ) )

Proof

Step Hyp Ref Expression
1 matmulr.a 
 |-  A = ( N Mat R )
2 matmulr.t 
 |-  .x. = ( R maMul <. N , N , N >. )
3 ovex 
 |-  ( R freeLMod ( N X. N ) ) e. _V
4 2 ovexi 
 |-  .x. e. _V
5 3 4 pm3.2i 
 |-  ( ( R freeLMod ( N X. N ) ) e. _V /\ .x. e. _V )
6 mulrid 
 |-  .r = Slot ( .r ` ndx )
7 6 setsid 
 |-  ( ( ( R freeLMod ( N X. N ) ) e. _V /\ .x. e. _V ) -> .x. = ( .r ` ( ( R freeLMod ( N X. N ) ) sSet <. ( .r ` ndx ) , .x. >. ) ) )
8 5 7 mp1i 
 |-  ( ( N e. Fin /\ R e. V ) -> .x. = ( .r ` ( ( R freeLMod ( N X. N ) ) sSet <. ( .r ` ndx ) , .x. >. ) ) )
9 eqid 
 |-  ( R freeLMod ( N X. N ) ) = ( R freeLMod ( N X. N ) )
10 1 9 2 matval 
 |-  ( ( N e. Fin /\ R e. V ) -> A = ( ( R freeLMod ( N X. N ) ) sSet <. ( .r ` ndx ) , .x. >. ) )
11 10 fveq2d 
 |-  ( ( N e. Fin /\ R e. V ) -> ( .r ` A ) = ( .r ` ( ( R freeLMod ( N X. N ) ) sSet <. ( .r ` ndx ) , .x. >. ) ) )
12 8 11 eqtr4d 
 |-  ( ( N e. Fin /\ R e. V ) -> .x. = ( .r ` A ) )