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 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 0fi 
 |-  (/) 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 ) ) = { (/) } )