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 e. V -> ( ( (/) matToPolyMat R ) ` (/) ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		0fin	|- (/) e. Fin
2		id	|- ( R e. V -> R e. V )
3		0ex	|- (/) e. _V
4	3	snid	|- (/) e. { (/) }
5		mat0dimbas0	|- ( R e. V -> ( Base ` ( (/) Mat R ) ) = { (/) } )
6	4 5	eleqtrrid	|- ( R e. V -> (/) e. ( Base ` ( (/) Mat R ) ) )
7		eqid	|- ( (/) matToPolyMat R ) = ( (/) matToPolyMat R )
8		eqid	|- ( (/) Mat R ) = ( (/) Mat R )
9		eqid	|- ( Base ` ( (/) Mat R ) ) = ( Base ` ( (/) Mat R ) )
10		eqid	|- ( Poly1 ` R ) = ( Poly1 ` R )
11		eqid	|- ( algSc ` ( Poly1 ` R ) ) = ( algSc ` ( Poly1 ` R ) )
12	7 8 9 10 11	mat2pmatval	|- ( ( (/) e. Fin /\ R e. V /\ (/) e. ( Base ` ( (/) Mat R ) ) ) -> ( ( (/) matToPolyMat R ) ` (/) ) = ( x e. (/) , y e. (/) |-> ( ( algSc ` ( Poly1 ` R ) ) ` ( x (/) y ) ) ) )
13	1 2 6 12	mp3an2i	|- ( R e. V -> ( ( (/) matToPolyMat R ) ` (/) ) = ( x e. (/) , y e. (/) |-> ( ( algSc ` ( Poly1 ` R ) ) ` ( x (/) y ) ) ) )
14		mpo0	|- ( x e. (/) , y e. (/) |-> ( ( algSc ` ( Poly1 ` R ) ) ` ( x (/) y ) ) ) = (/)
15	13 14	eqtrdi	|- ( R e. V -> ( ( (/) matToPolyMat R ) ` (/) ) = (/) )