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	⊢ ( 𝑅 ∈ 𝑉 → ( ( ∅ matToPolyMat 𝑅 ) ‘ ∅ ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		0fin	⊢ ∅ ∈ Fin
2		id	⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ 𝑉 )
3		0ex	⊢ ∅ ∈ V
4	3	snid	⊢ ∅ ∈ { ∅ }
5		mat0dimbas0	⊢ ( 𝑅 ∈ 𝑉 → ( Base ‘ ( ∅ Mat 𝑅 ) ) = { ∅ } )
6	4 5	eleqtrrid	⊢ ( 𝑅 ∈ 𝑉 → ∅ ∈ ( Base ‘ ( ∅ Mat 𝑅 ) ) )
7		eqid	⊢ ( ∅ matToPolyMat 𝑅 ) = ( ∅ matToPolyMat 𝑅 )
8		eqid	⊢ ( ∅ Mat 𝑅 ) = ( ∅ Mat 𝑅 )
9		eqid	⊢ ( Base ‘ ( ∅ Mat 𝑅 ) ) = ( Base ‘ ( ∅ Mat 𝑅 ) )
10		eqid	⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
11		eqid	⊢ ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) = ( algSc ‘ ( Poly1 ‘ 𝑅 ) )
12	7 8 9 10 11	mat2pmatval	⊢ ( ( ∅ ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ ∅ ∈ ( Base ‘ ( ∅ Mat 𝑅 ) ) ) → ( ( ∅ matToPolyMat 𝑅 ) ‘ ∅ ) = ( 𝑥 ∈ ∅ , 𝑦 ∈ ∅ ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( 𝑥 ∅ 𝑦 ) ) ) )
13	1 2 6 12	mp3an2i	⊢ ( 𝑅 ∈ 𝑉 → ( ( ∅ matToPolyMat 𝑅 ) ‘ ∅ ) = ( 𝑥 ∈ ∅ , 𝑦 ∈ ∅ ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( 𝑥 ∅ 𝑦 ) ) ) )
14		mpo0	⊢ ( 𝑥 ∈ ∅ , 𝑦 ∈ ∅ ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( 𝑥 ∅ 𝑦 ) ) ) = ∅
15	13 14	eqtrdi	⊢ ( 𝑅 ∈ 𝑉 → ( ( ∅ matToPolyMat 𝑅 ) ‘ ∅ ) = ∅ )