This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 0fi ⊢ ∅ ∈ 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 biimtrdi ⊢ ( 𝑅 ∈ Ring → ( ( 0g ‘ 𝐴 ) ∈ ( Base ‘ 𝐴 ) → ( 0g ‘ 𝐴 ) = ∅ ) )
16 9 15 mpd ⊢ ( 𝑅 ∈ Ring → ( 0g ‘ 𝐴 ) = ∅ )