Step |
Hyp |
Ref |
Expression |
1 |
|
mat0dim.a |
|- A = ( (/) Mat R ) |
2 |
|
0fin |
|- (/) e. Fin |
3 |
1
|
matring |
|- ( ( (/) e. Fin /\ R e. Ring ) -> A e. Ring ) |
4 |
2 3
|
mpan |
|- ( R e. Ring -> A e. Ring ) |
5 |
|
eqid |
|- ( Base ` A ) = ( Base ` A ) |
6 |
|
eqid |
|- ( 1r ` A ) = ( 1r ` A ) |
7 |
5 6
|
ringidcl |
|- ( A e. Ring -> ( 1r ` A ) e. ( Base ` A ) ) |
8 |
4 7
|
syl |
|- ( R e. Ring -> ( 1r ` A ) e. ( Base ` A ) ) |
9 |
1
|
fveq2i |
|- ( Base ` A ) = ( Base ` ( (/) Mat R ) ) |
10 |
|
mat0dimbas0 |
|- ( R e. Ring -> ( Base ` ( (/) Mat R ) ) = { (/) } ) |
11 |
9 10
|
syl5eq |
|- ( R e. Ring -> ( Base ` A ) = { (/) } ) |
12 |
11
|
eleq2d |
|- ( R e. Ring -> ( ( 1r ` A ) e. ( Base ` A ) <-> ( 1r ` A ) e. { (/) } ) ) |
13 |
|
elsni |
|- ( ( 1r ` A ) e. { (/) } -> ( 1r ` A ) = (/) ) |
14 |
12 13
|
syl6bi |
|- ( R e. Ring -> ( ( 1r ` A ) e. ( Base ` A ) -> ( 1r ` A ) = (/) ) ) |
15 |
8 14
|
mpd |
|- ( R e. Ring -> ( 1r ` A ) = (/) ) |