matplusgcell

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

	Ref	Expression
Hypotheses	matplusgcell.a	$⊢ A = N Mat R$
	matplusgcell.b	$⊢ B = {Base}_{A}$
	matplusgcell.p	$⊢ \underset{˙}{✚} = +_{A}$
	matplusgcell.q	$⊢ \underset{˙}{+} = +_{R}$
Assertion	matplusgcell	$⊢ ((X \in B \land Y \in B) \land (I \in N \land J \in N)) \to I (X \underset{˙}{✚} Y) J = (I X J) \underset{˙}{+} (I Y J)$

Proof

Step	Hyp	Ref	Expression
1		matplusgcell.a	$⊢ A = N Mat R$
2		matplusgcell.b	$⊢ B = {Base}_{A}$
3		matplusgcell.p	$⊢ \underset{˙}{✚} = +_{A}$
4		matplusgcell.q	$⊢ \underset{˙}{+} = +_{R}$
5	1 2 3 4	matplusg2	$⊢ (X \in B \land Y \in B) \to X \underset{˙}{✚} Y = X {\underset{˙}{+}}_{f} Y$
6	5	oveqd	$⊢ (X \in B \land Y \in B) \to I (X \underset{˙}{✚} Y) J = I (X {\underset{˙}{+}}_{f} Y) J$
7	6	adantr	$⊢ ((X \in B \land Y \in B) \land (I \in N \land J \in N)) \to I (X \underset{˙}{✚} Y) J = I (X {\underset{˙}{+}}_{f} Y) J$
8		df-ov	$⊢ I (X {\underset{˙}{+}}_{f} Y) J = (X {\underset{˙}{+}}_{f} Y) (⟨I, J⟩)$
9	8	a1i	$⊢ ((X \in B \land Y \in B) \land (I \in N \land J \in N)) \to I (X {\underset{˙}{+}}_{f} Y) J = (X {\underset{˙}{+}}_{f} Y) (⟨I, J⟩)$
10		opelxp	$⊢ ⟨I, J⟩ \in (N \times N) \leftrightarrow (I \in N \land J \in N)$
11		eqid	$⊢ {Base}_{R} = {Base}_{R}$
12	1 11 2	matbas2i	$⊢ X \in B \to X \in ({Base}_{R}^{(N \times N)})$
13		elmapfn	$⊢ X \in ({Base}_{R}^{(N \times N)}) \to X Fn (N \times N)$
14	12 13	syl	$⊢ X \in B \to X Fn (N \times N)$
15	14	adantr	$⊢ (X \in B \land Y \in B) \to X Fn (N \times N)$
16	1 11 2	matbas2i	$⊢ Y \in B \to Y \in ({Base}_{R}^{(N \times N)})$
17		elmapfn	$⊢ Y \in ({Base}_{R}^{(N \times N)}) \to Y Fn (N \times N)$
18	16 17	syl	$⊢ Y \in B \to Y Fn (N \times N)$
19	18	adantl	$⊢ (X \in B \land Y \in B) \to Y Fn (N \times N)$
20	1 2	matrcl	$⊢ X \in B \to (N \in Fin \land R \in V)$
21		xpfi	$⊢ (N \in Fin \land N \in Fin) \to N \times N \in Fin$
22	21	anidms	$⊢ N \in Fin \to N \times N \in Fin$
23	22	adantr	$⊢ (N \in Fin \land R \in V) \to N \times N \in Fin$
24	20 23	syl	$⊢ X \in B \to N \times N \in Fin$
25	24	adantr	$⊢ (X \in B \land Y \in B) \to N \times N \in Fin$
26		inidm	$⊢ (N \times N) \cap (N \times N) = N \times N$
27		df-ov	$⊢ I X J = X (⟨I, J⟩)$
28	27	eqcomi	$⊢ X (⟨I, J⟩) = I X J$
29	28	a1i	$⊢ ((X \in B \land Y \in B) \land ⟨I, J⟩ \in (N \times N)) \to X (⟨I, J⟩) = I X J$
30		df-ov	$⊢ I Y J = Y (⟨I, J⟩)$
31	30	eqcomi	$⊢ Y (⟨I, J⟩) = I Y J$
32	31	a1i	$⊢ ((X \in B \land Y \in B) \land ⟨I, J⟩ \in (N \times N)) \to Y (⟨I, J⟩) = I Y J$
33	15 19 25 25 26 29 32	ofval	$⊢ ((X \in B \land Y \in B) \land ⟨I, J⟩ \in (N \times N)) \to (X {\underset{˙}{+}}_{f} Y) (⟨I, J⟩) = (I X J) \underset{˙}{+} (I Y J)$
34	10 33	sylan2br	$⊢ ((X \in B \land Y \in B) \land (I \in N \land J \in N)) \to (X {\underset{˙}{+}}_{f} Y) (⟨I, J⟩) = (I X J) \underset{˙}{+} (I Y J)$
35	7 9 34	3eqtrd	$⊢ ((X \in B \land Y \in B) \land (I \in N \land J \in N)) \to I (X \underset{˙}{✚} Y) J = (I X J) \underset{˙}{+} (I Y J)$

Metamath Proof Explorer

Theorem matplusgcell

Proof