mat0op

Description: Value of a zero matrix as operation. (Contributed by AV, 2-Dec-2018)

	Ref	Expression
Hypotheses	mat0op.a	$⊢ A = N Mat R$
	mat0op.z	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	mat0op	$⊢ (N \in Fin \land R \in Ring) \to 0_{A} = (i \in N, j \in N ⟼ \underset{˙}{0})$

Step	Hyp	Ref	Expression
1		mat0op.a	$⊢ A = N Mat R$
2		mat0op.z	$⊢ \underset{˙}{0} = 0_{R}$
3		eqid	$⊢ R freeLMod (N \times N) = R freeLMod (N \times N)$
4	1 3	mat0	$⊢ (N \in Fin \land R \in Ring) \to 0_{(R freeLMod (N \times N))} = 0_{A}$
5		fconstmpo	$⊢ (N \times N) \times \{0_{R}\} = (i \in N, j \in N ⟼ 0_{R})$
6		simpr	$⊢ (N \in Fin \land R \in Ring) \to R \in Ring$
7		sqxpexg	$⊢ N \in Fin \to N \times N \in V$
8	7	adantr	$⊢ (N \in Fin \land R \in Ring) \to N \times N \in V$
9		eqid	$⊢ 0_{R} = 0_{R}$
10	3 9	frlm0	$⊢ (R \in Ring \land N \times N \in V) \to (N \times N) \times \{0_{R}\} = 0_{(R freeLMod (N \times N))}$
11	6 8 10	syl2anc	$⊢ (N \in Fin \land R \in Ring) \to (N \times N) \times \{0_{R}\} = 0_{(R freeLMod (N \times N))}$
12	2	eqcomi	$⊢ 0_{R} = \underset{˙}{0}$
13	12	a1i	$⊢ (i \in N \land j \in N) \to 0_{R} = \underset{˙}{0}$
14	13	mpoeq3ia	$⊢ (i \in N, j \in N ⟼ 0_{R}) = (i \in N, j \in N ⟼ \underset{˙}{0})$
15	14	a1i	$⊢ (N \in Fin \land R \in Ring) \to (i \in N, j \in N ⟼ 0_{R}) = (i \in N, j \in N ⟼ \underset{˙}{0})$
16	5 11 15	3eqtr3a	$⊢ (N \in Fin \land R \in Ring) \to 0_{(R freeLMod (N \times N))} = (i \in N, j \in N ⟼ \underset{˙}{0})$
17	4 16	eqtr3d	$⊢ (N \in Fin \land R \in Ring) \to 0_{A} = (i \in N, j \in N ⟼ \underset{˙}{0})$

Metamath Proof Explorer