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 ∈ Fin ∧ R ∈ Ring → A ∈ LMod

Proof

Step Hyp Ref Expression
1 matlmod.a ⊢ A = N Mat R
2 sqxpexg ⊢ N ∈ Fin → N × N ∈ V
3 eqid ⊢ R freeLMod N × N = R freeLMod N × N
4 3 frlmlmod ⊢ R ∈ Ring ∧ N × N ∈ V → R freeLMod N × N ∈ LMod
5 4 ancoms ⊢ N × N ∈ V ∧ R ∈ Ring → R freeLMod N × N ∈ LMod
6 2 5 sylan ⊢ N ∈ Fin ∧ R ∈ Ring → R freeLMod N × N ∈ LMod
7 eqidd ⊢ N ∈ Fin ∧ R ∈ Ring → Base R freeLMod N × N = Base R freeLMod N × N
8 1 3 matbas ⊢ N ∈ Fin ∧ R ∈ Ring → Base R freeLMod N × N = Base A
9 1 3 matplusg ⊢ N ∈ Fin ∧ R ∈ Ring → + R freeLMod N × N = + A
10 9 oveqdr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ x ∈ Base R freeLMod N × N ∧ y ∈ Base R freeLMod N × N → x + R freeLMod N × N y = x + A y
11 eqidd ⊢ N ∈ Fin ∧ R ∈ Ring → Scalar ⁡ R freeLMod N × N = Scalar ⁡ R freeLMod N × N
12 1 3 matsca ⊢ N ∈ Fin ∧ R ∈ Ring → Scalar ⁡ R freeLMod N × N = Scalar ⁡ A
13 eqid ⊢ Base Scalar ⁡ R freeLMod N × N = Base Scalar ⁡ R freeLMod N × N
14 1 3 matvsca ⊢ N ∈ Fin ∧ R ∈ Ring → ⋅ R freeLMod N × N = ⋅ A
15 14 oveqdr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ x ∈ Base Scalar ⁡ R freeLMod N × N ∧ y ∈ Base R freeLMod N × N → x ⋅ R freeLMod N × N y = x ⋅ A y
16 7 8 10 11 12 13 15 lmodpropd ⊢ N ∈ Fin ∧ R ∈ Ring → R freeLMod N × N ∈ LMod ↔ A ∈ LMod
17 6 16 mpbid ⊢ N ∈ Fin ∧ R ∈ Ring → A ∈ LMod