Metamath Proof Explorer

Theorem mat0scmat

Description: The empty matrix over a ring is a scalar matrix (and therefore, by scmatdmat , also a diagonal matrix). (Contributed by AV, 21-Dec-2019)

Ref Expression
Assertion mat0scmat ⊢ R ∈ Ring → ∅ ∈ ∅ ScMat R

Proof

Step Hyp Ref Expression
1 0ex ⊢ ∅ ∈ V
2 1 snid ⊢ ∅ ∈ ∅
3 mat0dimbas0 ⊢ R ∈ Ring → Base ∅ Mat R = ∅
4 2 3 eleqtrrid ⊢ R ∈ Ring → ∅ ∈ Base ∅ Mat R
5 eqid ⊢ Base R = Base R
6 eqid ⊢ 1 R = 1 R
7 5 6 ringidcl ⊢ R ∈ Ring → 1 R ∈ Base R
8 oveq1 ⊢ c = 1 R → c ⋅ ∅ Mat R ∅ = 1 R ⋅ ∅ Mat R ∅
9 8 eqeq2d ⊢ c = 1 R → ∅ = c ⋅ ∅ Mat R ∅ ↔ ∅ = 1 R ⋅ ∅ Mat R ∅
10 9 adantl ⊢ R ∈ Ring ∧ c = 1 R → ∅ = c ⋅ ∅ Mat R ∅ ↔ ∅ = 1 R ⋅ ∅ Mat R ∅
11 eqid ⊢ ∅ Mat R = ∅ Mat R
12 11 mat0dimscm ⊢ R ∈ Ring ∧ 1 R ∈ Base R → 1 R ⋅ ∅ Mat R ∅ = ∅
13 7 12 mpdan ⊢ R ∈ Ring → 1 R ⋅ ∅ Mat R ∅ = ∅
14 13 eqcomd ⊢ R ∈ Ring → ∅ = 1 R ⋅ ∅ Mat R ∅
15 7 10 14 rspcedvd ⊢ R ∈ Ring → ∃ c ∈ Base R ∅ = c ⋅ ∅ Mat R ∅
16 11 mat0dimid ⊢ R ∈ Ring → 1 ∅ Mat R = ∅
17 16 oveq2d ⊢ R ∈ Ring → c ⋅ ∅ Mat R 1 ∅ Mat R = c ⋅ ∅ Mat R ∅
18 17 eqeq2d ⊢ R ∈ Ring → ∅ = c ⋅ ∅ Mat R 1 ∅ Mat R ↔ ∅ = c ⋅ ∅ Mat R ∅
19 18 rexbidv ⊢ R ∈ Ring → ∃ c ∈ Base R ∅ = c ⋅ ∅ Mat R 1 ∅ Mat R ↔ ∃ c ∈ Base R ∅ = c ⋅ ∅ Mat R ∅
20 15 19 mpbird ⊢ R ∈ Ring → ∃ c ∈ Base R ∅ = c ⋅ ∅ Mat R 1 ∅ Mat R
21 0fi ⊢ ∅ ∈ Fin
22 eqid ⊢ Base ∅ Mat R = Base ∅ Mat R
23 eqid ⊢ 1 ∅ Mat R = 1 ∅ Mat R
24 eqid ⊢ ⋅ ∅ Mat R = ⋅ ∅ Mat R
25 eqid ⊢ ∅ ScMat R = ∅ ScMat R
26 5 11 22 23 24 25 scmatel ⊢ ∅ ∈ Fin ∧ R ∈ Ring → ∅ ∈ ∅ ScMat R ↔ ∅ ∈ Base ∅ Mat R ∧ ∃ c ∈ Base R ∅ = c ⋅ ∅ Mat R 1 ∅ Mat R
27 21 26 mpan ⊢ R ∈ Ring → ∅ ∈ ∅ ScMat R ↔ ∅ ∈ Base ∅ Mat R ∧ ∃ c ∈ Base R ∅ = c ⋅ ∅ Mat R 1 ∅ Mat R
28 4 20 27 mpbir2and ⊢ R ∈ Ring → ∅ ∈ ∅ ScMat R