Step |
Hyp |
Ref |
Expression |
1 |
|
mat0dim.a |
⊢ 𝐴 = ( ∅ Mat 𝑅 ) |
2 |
|
0fin |
⊢ ∅ ∈ Fin |
3 |
1
|
matring |
⊢ ( ( ∅ ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring ) |
4 |
2 3
|
mpan |
⊢ ( 𝑅 ∈ Ring → 𝐴 ∈ Ring ) |
5 |
|
ringgrp |
⊢ ( 𝐴 ∈ Ring → 𝐴 ∈ Grp ) |
6 |
|
eqid |
⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 ) |
7 |
|
eqid |
⊢ ( 0g ‘ 𝐴 ) = ( 0g ‘ 𝐴 ) |
8 |
6 7
|
grpidcl |
⊢ ( 𝐴 ∈ Grp → ( 0g ‘ 𝐴 ) ∈ ( Base ‘ 𝐴 ) ) |
9 |
4 5 8
|
3syl |
⊢ ( 𝑅 ∈ Ring → ( 0g ‘ 𝐴 ) ∈ ( Base ‘ 𝐴 ) ) |
10 |
1
|
fveq2i |
⊢ ( Base ‘ 𝐴 ) = ( Base ‘ ( ∅ Mat 𝑅 ) ) |
11 |
|
mat0dimbas0 |
⊢ ( 𝑅 ∈ Ring → ( Base ‘ ( ∅ Mat 𝑅 ) ) = { ∅ } ) |
12 |
10 11
|
eqtrid |
⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝐴 ) = { ∅ } ) |
13 |
12
|
eleq2d |
⊢ ( 𝑅 ∈ Ring → ( ( 0g ‘ 𝐴 ) ∈ ( Base ‘ 𝐴 ) ↔ ( 0g ‘ 𝐴 ) ∈ { ∅ } ) ) |
14 |
|
elsni |
⊢ ( ( 0g ‘ 𝐴 ) ∈ { ∅ } → ( 0g ‘ 𝐴 ) = ∅ ) |
15 |
13 14
|
syl6bi |
⊢ ( 𝑅 ∈ Ring → ( ( 0g ‘ 𝐴 ) ∈ ( Base ‘ 𝐴 ) → ( 0g ‘ 𝐴 ) = ∅ ) ) |
16 |
9 15
|
mpd |
⊢ ( 𝑅 ∈ Ring → ( 0g ‘ 𝐴 ) = ∅ ) |