Metamath Proof Explorer

Theorem d0mat2pmat

Description: The transformed empty set as matrix of dimenson 0 is the empty set (i.e., the polynomial matrix of dimension 0). (Contributed by AV, 4-Aug-2019)

		Ref	Expression
	Assertion	d0mat2pmat	$⊢ R \in V \to (\emptyset matToPolyMat R) (\emptyset) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		0fin	$⊢ \emptyset \in Fin$
2		id	$⊢ R \in V \to R \in V$
3		0ex	$⊢ \emptyset \in V$
4	3	snid	$⊢ \emptyset \in \{\emptyset\}$
5		mat0dimbas0	$⊢ R \in V \to {Base}_{(\emptyset Mat R)} = \{\emptyset\}$
6	4 5	eleqtrrid	$⊢ R \in V \to \emptyset \in {Base}_{(\emptyset Mat R)}$
7		eqid	$⊢ \emptyset matToPolyMat R = \emptyset matToPolyMat R$
8		eqid	$⊢ \emptyset Mat R = \emptyset Mat R$
9		eqid	$⊢ {Base}_{(\emptyset Mat R)} = {Base}_{(\emptyset Mat R)}$
10		eqid	$⊢ {Poly}_{1} (R) = {Poly}_{1} (R)$
11		eqid	$⊢ algSc ({Poly}_{1} (R)) = algSc ({Poly}_{1} (R))$
12	7 8 9 10 11	mat2pmatval	$⊢ (\emptyset \in Fin \land R \in V \land \emptyset \in {Base}_{(\emptyset Mat R)}) \to (\emptyset matToPolyMat R) (\emptyset) = (x \in \emptyset, y \in \emptyset ⟼ algSc ({Poly}_{1} (R)) (x \emptyset y))$
13	1 2 6 12	mp3an2i	$⊢ R \in V \to (\emptyset matToPolyMat R) (\emptyset) = (x \in \emptyset, y \in \emptyset ⟼ algSc ({Poly}_{1} (R)) (x \emptyset y))$
14		mpo0	$⊢ (x \in \emptyset, y \in \emptyset ⟼ algSc ({Poly}_{1} (R)) (x \emptyset y)) = \emptyset$
15	13 14	eqtrdi	$⊢ R \in V \to (\emptyset matToPolyMat R) (\emptyset) = \emptyset$