This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mat0dimbas0

Description: The empty set is the one and only matrix of dimension 0, called "the empty matrix". (Contributed by AV, 27-Feb-2019)

Ref Expression
Assertion mat0dimbas0 ⊢ R ∈ V → Base ∅ Mat R = ∅

Proof

Step Hyp Ref Expression
1 0xp ⊢ ∅ × ∅ = ∅
2 1 a1i ⊢ R ∈ V → ∅ × ∅ = ∅
3 2 oveq2d ⊢ R ∈ V → Base R ∅ × ∅ = Base R ∅
4 fvex ⊢ Base R ∈ V
5 map0e ⊢ Base R ∈ V → Base R ∅ = 1 𝑜
6 4 5 mp1i ⊢ R ∈ V → Base R ∅ = 1 𝑜
7 3 6 eqtrd ⊢ R ∈ V → Base R ∅ × ∅ = 1 𝑜
8 0fi ⊢ ∅ ∈ Fin
9 eqid ⊢ ∅ Mat R = ∅ Mat R
10 eqid ⊢ Base R = Base R
11 9 10 matbas2 ⊢ ∅ ∈ Fin ∧ R ∈ V → Base R ∅ × ∅ = Base ∅ Mat R
12 8 11 mpan ⊢ R ∈ V → Base R ∅ × ∅ = Base ∅ Mat R
13 df1o2 ⊢ 1 𝑜 = ∅
14 13 a1i ⊢ R ∈ V → 1 𝑜 = ∅
15 7 12 14 3eqtr3d ⊢ R ∈ V → Base ∅ Mat R = ∅