Metamath Proof Explorer

Theorem matlmod

Description: The matrix ring is a linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015)

Ref Expression
Hypothesis matlmod.a 
|- A = ( N Mat R )
Assertion matlmod 
|- ( ( N e. Fin /\ R e. Ring ) -> A e. LMod )

Proof

Step Hyp Ref Expression
1 matlmod.a 
 |-  A = ( N Mat R )
2 sqxpexg 
 |-  ( N e. Fin -> ( N X. N ) e. _V )
3 eqid 
 |-  ( R freeLMod ( N X. N ) ) = ( R freeLMod ( N X. N ) )
4 3 frlmlmod 
 |-  ( ( R e. Ring /\ ( N X. N ) e. _V ) -> ( R freeLMod ( N X. N ) ) e. LMod )
5 4 ancoms 
 |-  ( ( ( N X. N ) e. _V /\ R e. Ring ) -> ( R freeLMod ( N X. N ) ) e. LMod )
6 2 5 sylan 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( R freeLMod ( N X. N ) ) e. LMod )
7 eqidd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Base ` ( R freeLMod ( N X. N ) ) ) = ( Base ` ( R freeLMod ( N X. N ) ) ) )
8 1 3 matbas 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Base ` ( R freeLMod ( N X. N ) ) ) = ( Base ` A ) )
9 1 3 matplusg 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( +g ` ( R freeLMod ( N X. N ) ) ) = ( +g ` A ) )
10 9 oveqdr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( Base ` ( R freeLMod ( N X. N ) ) ) /\ y e. ( Base ` ( R freeLMod ( N X. N ) ) ) ) ) -> ( x ( +g ` ( R freeLMod ( N X. N ) ) ) y ) = ( x ( +g ` A ) y ) )
11 eqidd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Scalar ` ( R freeLMod ( N X. N ) ) ) = ( Scalar ` ( R freeLMod ( N X. N ) ) ) )
12 1 3 matsca 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Scalar ` ( R freeLMod ( N X. N ) ) ) = ( Scalar ` A ) )
13 eqid 
 |-  ( Base ` ( Scalar ` ( R freeLMod ( N X. N ) ) ) ) = ( Base ` ( Scalar ` ( R freeLMod ( N X. N ) ) ) )
14 1 3 matvsca 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( .s ` ( R freeLMod ( N X. N ) ) ) = ( .s ` A ) )
15 14 oveqdr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( Base ` ( Scalar ` ( R freeLMod ( N X. N ) ) ) ) /\ y e. ( Base ` ( R freeLMod ( N X. N ) ) ) ) ) -> ( x ( .s ` ( R freeLMod ( N X. N ) ) ) y ) = ( x ( .s ` A ) y ) )
16 7 8 10 11 12 13 15 lmodpropd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( R freeLMod ( N X. N ) ) e. LMod <-> A e. LMod ) )
17 6 16 mpbid 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. LMod )