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