matplusg2

Description: Addition in the matrix ring is cell-wise. (Contributed by Stefan O'Rear, 5-Sep-2015)

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

Proof

Step	Hyp	Ref	Expression
1		matplusg2.a	$⊢ A = N Mat R$
2		matplusg2.b	$⊢ B = {Base}_{A}$
3		matplusg2.p	$⊢ \underset{˙}{✚} = +_{A}$
4		matplusg2.q	$⊢ \underset{˙}{+} = +_{R}$
5	1 2	matrcl	$⊢ X \in B \to (N \in Fin \land R \in V)$
6	5	adantr	$⊢ (X \in B \land Y \in B) \to (N \in Fin \land R \in V)$
7		eqid	$⊢ R freeLMod (N \times N) = R freeLMod (N \times N)$
8	1 7	matplusg	$⊢ (N \in Fin \land R \in V) \to +_{(R freeLMod (N \times N))} = +_{A}$
9	8 3	eqtr4di	$⊢ (N \in Fin \land R \in V) \to +_{(R freeLMod (N \times N))} = \underset{˙}{✚}$
10	6 9	syl	$⊢ (X \in B \land Y \in B) \to +_{(R freeLMod (N \times N))} = \underset{˙}{✚}$
11	10	oveqd	$⊢ (X \in B \land Y \in B) \to X +_{(R freeLMod (N \times N))} Y = X \underset{˙}{✚} Y$
12		eqid	$⊢ {Base}_{(R freeLMod (N \times N))} = {Base}_{(R freeLMod (N \times N))}$
13	6	simprd	$⊢ (X \in B \land Y \in B) \to R \in V$
14	6	simpld	$⊢ (X \in B \land Y \in B) \to N \in Fin$
15		xpfi	$⊢ (N \in Fin \land N \in Fin) \to N \times N \in Fin$
16	14 14 15	syl2anc	$⊢ (X \in B \land Y \in B) \to N \times N \in Fin$
17		simpl	$⊢ (X \in B \land Y \in B) \to X \in B$
18	1 7	matbas	$⊢ (N \in Fin \land R \in V) \to {Base}_{(R freeLMod (N \times N))} = {Base}_{A}$
19	6 18	syl	$⊢ (X \in B \land Y \in B) \to {Base}_{(R freeLMod (N \times N))} = {Base}_{A}$
20	19 2	eqtr4di	$⊢ (X \in B \land Y \in B) \to {Base}_{(R freeLMod (N \times N))} = B$
21	17 20	eleqtrrd	$⊢ (X \in B \land Y \in B) \to X \in {Base}_{(R freeLMod (N \times N))}$
22		simpr	$⊢ (X \in B \land Y \in B) \to Y \in B$
23	22 20	eleqtrrd	$⊢ (X \in B \land Y \in B) \to Y \in {Base}_{(R freeLMod (N \times N))}$
24		eqid	$⊢ +_{(R freeLMod (N \times N))} = +_{(R freeLMod (N \times N))}$
25	7 12 13 16 21 23 4 24	frlmplusgval	$⊢ (X \in B \land Y \in B) \to X +_{(R freeLMod (N \times N))} Y = X {\underset{˙}{+}}_{f} Y$
26	11 25	eqtr3d	$⊢ (X \in B \land Y \in B) \to X \underset{˙}{✚} Y = X {\underset{˙}{+}}_{f} Y$

Metamath Proof Explorer

Theorem matplusg2

Proof