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

Metamath Proof Explorer

Theorem matplusgcell

Description: Addition in the matrix ring is cell-wise. (Contributed by AV, 2-Aug-2019)

Ref Expression
Hypotheses matplusgcell.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
matplusgcell.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
matplusgcell.p ⊢ ✚ = ( +g ‘ 𝐴 )
matplusgcell.q ⊢ + = ( +g ‘ 𝑅 )
Assertion matplusgcell ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( 𝑋 ✚ 𝑌 ) 𝐽 ) = ( ( 𝐼 𝑋 𝐽 ) + ( 𝐼 𝑌 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 matplusgcell.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 matplusgcell.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 matplusgcell.p ⊢ ✚ = ( +g ‘ 𝐴 )
4 matplusgcell.q ⊢ + = ( +g ‘ 𝑅 )
5 1 2 3 4 matplusg2 ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ✚ 𝑌 ) = ( 𝑋 ∘f + 𝑌 ) )
6 5 oveqd ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐼 ( 𝑋 ✚ 𝑌 ) 𝐽 ) = ( 𝐼 ( 𝑋 ∘f + 𝑌 ) 𝐽 ) )
7 6 adantr ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( 𝑋 ✚ 𝑌 ) 𝐽 ) = ( 𝐼 ( 𝑋 ∘f + 𝑌 ) 𝐽 ) )
8 df-ov ⊢ ( 𝐼 ( 𝑋 ∘f + 𝑌 ) 𝐽 ) = ( ( 𝑋 ∘f + 𝑌 ) ‘ ⟨ 𝐼 , 𝐽 ⟩ )
9 8 a1i ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( 𝑋 ∘f + 𝑌 ) 𝐽 ) = ( ( 𝑋 ∘f + 𝑌 ) ‘ ⟨ 𝐼 , 𝐽 ⟩ ) )
10 opelxp ⊢ ( ⟨ 𝐼 , 𝐽 ⟩ ∈ ( 𝑁 × 𝑁 ) ↔ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) )
11 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
12 1 11 2 matbas2i ⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
13 elmapfn ⊢ ( 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) → 𝑋 Fn ( 𝑁 × 𝑁 ) )
14 12 13 syl ⊢ ( 𝑋 ∈ 𝐵 → 𝑋 Fn ( 𝑁 × 𝑁 ) )
15 14 adantr ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 Fn ( 𝑁 × 𝑁 ) )
16 1 11 2 matbas2i ⊢ ( 𝑌 ∈ 𝐵 → 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
17 elmapfn ⊢ ( 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) → 𝑌 Fn ( 𝑁 × 𝑁 ) )
18 16 17 syl ⊢ ( 𝑌 ∈ 𝐵 → 𝑌 Fn ( 𝑁 × 𝑁 ) )
19 18 adantl ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 Fn ( 𝑁 × 𝑁 ) )
20 1 2 matrcl ⊢ ( 𝑋 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
21 xpfi ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 𝑁 × 𝑁 ) ∈ Fin )
22 21 anidms ⊢ ( 𝑁 ∈ Fin → ( 𝑁 × 𝑁 ) ∈ Fin )
23 22 adantr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( 𝑁 × 𝑁 ) ∈ Fin )
24 20 23 syl ⊢ ( 𝑋 ∈ 𝐵 → ( 𝑁 × 𝑁 ) ∈ Fin )
25 24 adantr ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑁 × 𝑁 ) ∈ Fin )
26 inidm ⊢ ( ( 𝑁 × 𝑁 ) ∩ ( 𝑁 × 𝑁 ) ) = ( 𝑁 × 𝑁 )
27 df-ov ⊢ ( 𝐼 𝑋 𝐽 ) = ( 𝑋 ‘ ⟨ 𝐼 , 𝐽 ⟩ )
28 27 eqcomi ⊢ ( 𝑋 ‘ ⟨ 𝐼 , 𝐽 ⟩ ) = ( 𝐼 𝑋 𝐽 )
29 28 a1i ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ⟨ 𝐼 , 𝐽 ⟩ ∈ ( 𝑁 × 𝑁 ) ) → ( 𝑋 ‘ ⟨ 𝐼 , 𝐽 ⟩ ) = ( 𝐼 𝑋 𝐽 ) )
30 df-ov ⊢ ( 𝐼 𝑌 𝐽 ) = ( 𝑌 ‘ ⟨ 𝐼 , 𝐽 ⟩ )
31 30 eqcomi ⊢ ( 𝑌 ‘ ⟨ 𝐼 , 𝐽 ⟩ ) = ( 𝐼 𝑌 𝐽 )
32 31 a1i ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ⟨ 𝐼 , 𝐽 ⟩ ∈ ( 𝑁 × 𝑁 ) ) → ( 𝑌 ‘ ⟨ 𝐼 , 𝐽 ⟩ ) = ( 𝐼 𝑌 𝐽 ) )
33 15 19 25 25 26 29 32 ofval ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ⟨ 𝐼 , 𝐽 ⟩ ∈ ( 𝑁 × 𝑁 ) ) → ( ( 𝑋 ∘f + 𝑌 ) ‘ ⟨ 𝐼 , 𝐽 ⟩ ) = ( ( 𝐼 𝑋 𝐽 ) + ( 𝐼 𝑌 𝐽 ) ) )
34 10 33 sylan2br ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( ( 𝑋 ∘f + 𝑌 ) ‘ ⟨ 𝐼 , 𝐽 ⟩ ) = ( ( 𝐼 𝑋 𝐽 ) + ( 𝐼 𝑌 𝐽 ) ) )
35 7 9 34 3eqtrd ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( 𝑋 ✚ 𝑌 ) 𝐽 ) = ( ( 𝐼 𝑋 𝐽 ) + ( 𝐼 𝑌 𝐽 ) ) )