Metamath Proof Explorer


Theorem mat0dim0

Description: The zero of the algebra of matrices with dimension 0. (Contributed by AV, 6-Aug-2019)

Ref Expression
Hypothesis mat0dim.a 𝐴 = ( ∅ Mat 𝑅 )
Assertion mat0dim0 ( 𝑅 ∈ Ring → ( 0g𝐴 ) = ∅ )

Proof

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𝐴 ) = ∅ )