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 ( 𝑅 ∈ 𝑉 → ( Base ‘ ( ∅ Mat 𝑅 ) ) = { ∅ } )

Proof

Step Hyp Ref Expression
1 0xp ⊢ ( ∅ × ∅ ) = ∅
2 1 a1i ⊢ ( 𝑅 ∈ 𝑉 → ( ∅ × ∅ ) = ∅ )
3 2 oveq2d ⊢ ( 𝑅 ∈ 𝑉 → ( ( Base ‘ 𝑅 ) ↑m ( ∅ × ∅ ) ) = ( ( Base ‘ 𝑅 ) ↑m ∅ ) )
4 fvex ⊢ ( Base ‘ 𝑅 ) ∈ V
5 map0e ⊢ ( ( Base ‘ 𝑅 ) ∈ V → ( ( Base ‘ 𝑅 ) ↑m ∅ ) = 1o )
6 4 5 mp1i ⊢ ( 𝑅 ∈ 𝑉 → ( ( Base ‘ 𝑅 ) ↑m ∅ ) = 1o )
7 3 6 eqtrd ⊢ ( 𝑅 ∈ 𝑉 → ( ( Base ‘ 𝑅 ) ↑m ( ∅ × ∅ ) ) = 1o )
8 0fi ⊢ ∅ ∈ Fin
9 eqid ⊢ ( ∅ Mat 𝑅 ) = ( ∅ Mat 𝑅 )
10 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
11 9 10 matbas2 ⊢ ( ( ∅ ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( ( Base ‘ 𝑅 ) ↑m ( ∅ × ∅ ) ) = ( Base ‘ ( ∅ Mat 𝑅 ) ) )
12 8 11 mpan ⊢ ( 𝑅 ∈ 𝑉 → ( ( Base ‘ 𝑅 ) ↑m ( ∅ × ∅ ) ) = ( Base ‘ ( ∅ Mat 𝑅 ) ) )
13 df1o2 ⊢ 1o = { ∅ }
14 13 a1i ⊢ ( 𝑅 ∈ 𝑉 → 1o = { ∅ } )
15 7 12 14 3eqtr3d ⊢ ( 𝑅 ∈ 𝑉 → ( Base ‘ ( ∅ Mat 𝑅 ) ) = { ∅ } )