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→∅∈∅ScMatR

Proof

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