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 ( ( ( 𝑋𝐵𝑌𝐵 ) ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( 𝐼 ( 𝑋 𝑌 ) 𝐽 ) = ( ( 𝐼 𝑋 𝐽 ) + ( 𝐼 𝑌 𝐽 ) ) )