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

Metamath Proof Explorer

Theorem mat0dimid

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

Ref Expression
Hypothesis mat0dim.a ⊢ 𝐴 = ( ∅ Mat 𝑅 )
Assertion mat0dimid ( 𝑅 ∈ Ring → ( 1r ‘ 𝐴 ) = ∅ )

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 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
6 eqid ⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
7 5 6 ringidcl ⊢ ( 𝐴 ∈ Ring → ( 1r ‘ 𝐴 ) ∈ ( Base ‘ 𝐴 ) )
8 4 7 syl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝐴 ) ∈ ( Base ‘ 𝐴 ) )
9 1 fveq2i ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ ( ∅ Mat 𝑅 ) )
10 mat0dimbas0 ⊢ ( 𝑅 ∈ Ring → ( Base ‘ ( ∅ Mat 𝑅 ) ) = { ∅ } )
11 9 10 eqtrid ⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝐴 ) = { ∅ } )
12 11 eleq2d ⊢ ( 𝑅 ∈ Ring → ( ( 1r ‘ 𝐴 ) ∈ ( Base ‘ 𝐴 ) ↔ ( 1r ‘ 𝐴 ) ∈ { ∅ } ) )
13 elsni ⊢ ( ( 1r ‘ 𝐴 ) ∈ { ∅ } → ( 1r ‘ 𝐴 ) = ∅ )
14 12 13 biimtrdi ⊢ ( 𝑅 ∈ Ring → ( ( 1r ‘ 𝐴 ) ∈ ( Base ‘ 𝐴 ) → ( 1r ‘ 𝐴 ) = ∅ ) )
15 8 14 mpd ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝐴 ) = ∅ )