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 𝑅 ) ) = { ∅ } )