Metamath Proof Explorer

Theorem pmat0op

Description: The zero polynomial matrix over a ring represented as operation. (Contributed by AV, 16-Nov-2019)

	Ref	Expression
Hypotheses	pmatring.p	$⊢ P = {Poly}_{1} (R)$
	pmatring.c	$⊢ C = N Mat P$
	pmat0op.z	$⊢ \underset{˙}{0} = 0_{P}$
Assertion	pmat0op	$⊢ (N \in Fin \land R \in Ring) \to 0_{C} = (i \in N, j \in N ⟼ \underset{˙}{0})$

Step	Hyp	Ref	Expression
1		pmatring.p	$⊢ P = {Poly}_{1} (R)$
2		pmatring.c	$⊢ C = N Mat P$
3		pmat0op.z	$⊢ \underset{˙}{0} = 0_{P}$
4	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
5	2 3	mat0op	$⊢ (N \in Fin \land P \in Ring) \to 0_{C} = (i \in N, j \in N ⟼ \underset{˙}{0})$
6	4 5	sylan2	$⊢ (N \in Fin \land R \in Ring) \to 0_{C} = (i \in N, j \in N ⟼ \underset{˙}{0})$