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 0fi ⊢ ∅ ∈ 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 ⁡ ∅ = ∅