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 V matToPolyMat R =

Proof

Step Hyp Ref Expression
1 0fin Fin
2 id R V R V
3 0ex V
4 3 snid
5 mat0dimbas0 R V Base Mat R =
6 4 5 eleqtrrid R V 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 Poly 1 R = Poly 1 R
11 eqid algSc Poly 1 R = algSc Poly 1 R
12 7 8 9 10 11 mat2pmatval Fin R V Base Mat R matToPolyMat R = x , y algSc Poly 1 R x y
13 1 2 6 12 mp3an2i R V matToPolyMat R = x , y algSc Poly 1 R x y
14 mpo0 x , y algSc Poly 1 R x y =
15 13 14 eqtrdi R V matToPolyMat R =