Metamath Proof Explorer

Theorem matplusg2

Description: Addition in the matrix ring is cell-wise. (Contributed by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypotheses matplusg2.a ⊢ A = N Mat R
matplusg2.b ⊢ B = Base A
matplusg2.p ⊢ ✚ ˙ = + A
matplusg2.q ⊢ + ˙ = + R
Assertion matplusg2 ⊢ X ∈ B ∧ Y ∈ B → X ✚ ˙ Y = X + ˙ f Y

Proof

Step Hyp Ref Expression
1 matplusg2.a ⊢ A = N Mat R
2 matplusg2.b ⊢ B = Base A
3 matplusg2.p ⊢ ✚ ˙ = + A
4 matplusg2.q ⊢ + ˙ = + R
5 1 2 matrcl ⊢ X ∈ B → N ∈ Fin ∧ R ∈ V
6 5 adantr ⊢ X ∈ B ∧ Y ∈ B → N ∈ Fin ∧ R ∈ V
7 eqid ⊢ R freeLMod N × N = R freeLMod N × N
8 1 7 matplusg ⊢ N ∈ Fin ∧ R ∈ V → + R freeLMod N × N = + A
9 8 3 eqtr4di ⊢ N ∈ Fin ∧ R ∈ V → + R freeLMod N × N = ✚ ˙
10 6 9 syl ⊢ X ∈ B ∧ Y ∈ B → + R freeLMod N × N = ✚ ˙
11 10 oveqd ⊢ X ∈ B ∧ Y ∈ B → X + R freeLMod N × N Y = X ✚ ˙ Y
12 eqid ⊢ Base R freeLMod N × N = Base R freeLMod N × N
13 6 simprd ⊢ X ∈ B ∧ Y ∈ B → R ∈ V
14 6 simpld ⊢ X ∈ B ∧ Y ∈ B → N ∈ Fin
15 xpfi ⊢ N ∈ Fin ∧ N ∈ Fin → N × N ∈ Fin
16 14 14 15 syl2anc ⊢ X ∈ B ∧ Y ∈ B → N × N ∈ Fin
17 simpl ⊢ X ∈ B ∧ Y ∈ B → X ∈ B
18 1 7 matbas ⊢ N ∈ Fin ∧ R ∈ V → Base R freeLMod N × N = Base A
19 6 18 syl ⊢ X ∈ B ∧ Y ∈ B → Base R freeLMod N × N = Base A
20 19 2 eqtr4di ⊢ X ∈ B ∧ Y ∈ B → Base R freeLMod N × N = B
21 17 20 eleqtrrd ⊢ X ∈ B ∧ Y ∈ B → X ∈ Base R freeLMod N × N
22 simpr ⊢ X ∈ B ∧ Y ∈ B → Y ∈ B
23 22 20 eleqtrrd ⊢ X ∈ B ∧ Y ∈ B → Y ∈ Base R freeLMod N × N
24 eqid ⊢ + R freeLMod N × N = + R freeLMod N × N
25 7 12 13 16 21 23 4 24 frlmplusgval ⊢ X ∈ B ∧ Y ∈ B → X + R freeLMod N × N Y = X + ˙ f Y
26 11 25 eqtr3d ⊢ X ∈ B ∧ Y ∈ B → X ✚ ˙ Y = X + ˙ f Y