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 e. V -> ( Base ` ( (/) Mat R ) ) = { (/) } )

Proof

Step	Hyp	Ref	Expression
1		0xp	|- ( (/) X. (/) ) = (/)
2	1	a1i	|- ( R e. V -> ( (/) X. (/) ) = (/) )
3	2	oveq2d	|- ( R e. V -> ( ( Base ` R ) ^m ( (/) X. (/) ) ) = ( ( Base ` R ) ^m (/) ) )
4		fvex	|- ( Base ` R ) e. _V
5		map0e	|- ( ( Base ` R ) e. _V -> ( ( Base ` R ) ^m (/) ) = 1o )
6	4 5	mp1i	|- ( R e. V -> ( ( Base ` R ) ^m (/) ) = 1o )
7	3 6	eqtrd	|- ( R e. V -> ( ( Base ` R ) ^m ( (/) X. (/) ) ) = 1o )
8		0fin	|- (/) e. Fin
9		eqid	|- ( (/) Mat R ) = ( (/) Mat R )
10		eqid	|- ( Base ` R ) = ( Base ` R )
11	9 10	matbas2	|- ( ( (/) e. Fin /\ R e. V ) -> ( ( Base ` R ) ^m ( (/) X. (/) ) ) = ( Base ` ( (/) Mat R ) ) )
12	8 11	mpan	|- ( R e. V -> ( ( Base ` R ) ^m ( (/) X. (/) ) ) = ( Base ` ( (/) Mat R ) ) )
13		df1o2	|- 1o = { (/) }
14	13	a1i	|- ( R e. V -> 1o = { (/) } )
15	7 12 14	3eqtr3d	|- ( R e. V -> ( Base ` ( (/) Mat R ) ) = { (/) } )