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 ⊢ A = ∅ Mat R
Assertion mat0dim0 ⊢ R ∈ Ring → 0 A = ∅

Proof

Step Hyp Ref Expression
1 mat0dim.a ⊢ A = ∅ Mat R
2 0fi ⊢ ∅ ∈ Fin
3 1 matring ⊢ ∅ ∈ Fin ∧ R ∈ Ring → A ∈ Ring
4 2 3 mpan ⊢ R ∈ Ring → A ∈ Ring
5 ringgrp ⊢ A ∈ Ring → A ∈ Grp
6 eqid ⊢ Base A = Base A
7 eqid ⊢ 0 A = 0 A
8 6 7 grpidcl ⊢ A ∈ Grp → 0 A ∈ Base A
9 4 5 8 3syl ⊢ R ∈ Ring → 0 A ∈ Base A
10 1 fveq2i ⊢ Base A = Base ∅ Mat R
11 mat0dimbas0 ⊢ R ∈ Ring → Base ∅ Mat R = ∅
12 10 11 eqtrid ⊢ R ∈ Ring → Base A = ∅
13 12 eleq2d ⊢ R ∈ Ring → 0 A ∈ Base A ↔ 0 A ∈ ∅
14 elsni ⊢ 0 A ∈ ∅ → 0 A = ∅
15 13 14 biimtrdi ⊢ R ∈ Ring → 0 A ∈ Base A → 0 A = ∅
16 9 15 mpd ⊢ R ∈ Ring → 0 A = ∅