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

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 ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
Assertion matlmod ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ LMod )

Proof

Step Hyp Ref Expression
1 matlmod.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 sqxpexg ⊢ ( 𝑁 ∈ Fin → ( 𝑁 × 𝑁 ) ∈ V )
3 eqid ⊢ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) = ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) )
4 3 frlmlmod ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 × 𝑁 ) ∈ V ) → ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ∈ LMod )
5 4 ancoms ⊢ ( ( ( 𝑁 × 𝑁 ) ∈ V ∧ 𝑅 ∈ Ring ) → ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ∈ LMod )
6 2 5 sylan ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ∈ LMod )
7 eqidd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) )
8 1 3 matbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( Base ‘ 𝐴 ) )
9 1 3 matplusg ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( +g ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( +g ‘ 𝐴 ) )
10 9 oveqdr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) ) ) → ( 𝑥 ( +g ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) )
11 eqidd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Scalar ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( Scalar ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) )
12 1 3 matsca ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Scalar ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( Scalar ‘ 𝐴 ) )
13 eqid ⊢ ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) ) = ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) )
14 1 3 matvsca ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ·𝑠 ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( ·𝑠 ‘ 𝐴 ) )
15 14 oveqdr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) ) ) → ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐴 ) 𝑦 ) )
16 7 8 10 11 12 13 15 lmodpropd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ∈ LMod ↔ 𝐴 ∈ LMod ) )
17 6 16 mpbid ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ LMod )