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 ⊢ A = ∅ Mat R
Assertion mat0dimid ⊢ R ∈ Ring → 1 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 eqid ⊢ Base A = Base A
6 eqid ⊢ 1 A = 1 A
7 5 6 ringidcl ⊢ A ∈ Ring → 1 A ∈ Base A
8 4 7 syl ⊢ R ∈ Ring → 1 A ∈ Base A
9 1 fveq2i ⊢ Base A = Base ∅ Mat R
10 mat0dimbas0 ⊢ R ∈ Ring → Base ∅ Mat R = ∅
11 9 10 eqtrid ⊢ R ∈ Ring → Base A = ∅
12 11 eleq2d ⊢ R ∈ Ring → 1 A ∈ Base A ↔ 1 A ∈ ∅
13 elsni ⊢ 1 A ∈ ∅ → 1 A = ∅
14 12 13 biimtrdi ⊢ R ∈ Ring → 1 A ∈ Base A → 1 A = ∅
15 8 14 mpd ⊢ R ∈ Ring → 1 A = ∅