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 ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
matplusg2.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
matplusg2.p ⊢ ✚ = ( +g ‘ 𝐴 )
matplusg2.q ⊢ + = ( +g ‘ 𝑅 )
Assertion matplusg2 ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ✚ 𝑌 ) = ( 𝑋 ∘f + 𝑌 ) )

Proof

Step Hyp Ref Expression
1 matplusg2.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 matplusg2.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 matplusg2.p ⊢ ✚ = ( +g ‘ 𝐴 )
4 matplusg2.q ⊢ + = ( +g ‘ 𝑅 )
5 1 2 matrcl ⊢ ( 𝑋 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
6 5 adantr ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
7 eqid ⊢ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) = ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) )
8 1 7 matplusg ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( +g ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( +g ‘ 𝐴 ) )
9 8 3 eqtr4di ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( +g ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ✚ )
10 6 9 syl ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( +g ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ✚ )
11 10 oveqd ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( +g ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) 𝑌 ) = ( 𝑋 ✚ 𝑌 ) )
12 eqid ⊢ ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) )
13 6 simprd ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑅 ∈ V )
14 6 simpld ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑁 ∈ Fin )
15 xpfi ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 𝑁 × 𝑁 ) ∈ Fin )
16 14 14 15 syl2anc ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑁 × 𝑁 ) ∈ Fin )
17 simpl ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
18 1 7 matbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( Base ‘ 𝐴 ) )
19 6 18 syl ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( Base ‘ 𝐴 ) )
20 19 2 eqtr4di ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = 𝐵 )
21 17 20 eleqtrrd ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) )
22 simpr ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
23 22 20 eleqtrrd ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) )
24 eqid ⊢ ( +g ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( +g ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) )
25 7 12 13 16 21 23 4 24 frlmplusgval ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( +g ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) 𝑌 ) = ( 𝑋 ∘f + 𝑌 ) )
26 11 25 eqtr3d ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ✚ 𝑌 ) = ( 𝑋 ∘f + 𝑌 ) )