Metamath Proof Explorer

Theorem mat0dimscm

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

Ref Expression
Hypothesis mat0dim.a ⊢A=∅MatR
Assertion mat0dimscm ⊢R∈Ring∧X∈BaseR→X⋅A∅=∅

Proof

Step Hyp Ref Expression
1 mat0dim.a ⊢A=∅MatR
2 simpl ⊢R∈Ring∧X∈BaseR→R∈Ring
3 0fin ⊢∅∈Fin
4 1 matlmod ⊢∅∈Fin∧R∈Ring→A∈LMod
5 3 2 4 sylancr ⊢R∈Ring∧X∈BaseR→A∈LMod
6 1 matsca2 ⊢∅∈Fin∧R∈Ring→R=Scalar⁡A
7 3 6 mpan ⊢R∈Ring→R=Scalar⁡A
8 7 fveq2d ⊢R∈Ring→BaseR=BaseScalar⁡A
9 8 eleq2d ⊢R∈Ring→X∈BaseR↔X∈BaseScalar⁡A
10 9 biimpa ⊢R∈Ring∧X∈BaseR→X∈BaseScalar⁡A
11 0ex ⊢∅∈V
12 11 snid ⊢∅∈∅
13 1 fveq2i ⊢BaseA=Base∅MatR
14 mat0dimbas0 ⊢R∈Ring→Base∅MatR=∅
15 13 14 eqtrid ⊢R∈Ring→BaseA=∅
16 12 15 eleqtrrid ⊢R∈Ring→∅∈BaseA
17 16 adantr ⊢R∈Ring∧X∈BaseR→∅∈BaseA
18 eqid ⊢BaseA=BaseA
19 eqid ⊢Scalar⁡A=Scalar⁡A
20 eqid ⊢⋅A=⋅A
21 eqid ⊢BaseScalar⁡A=BaseScalar⁡A
22 18 19 20 21 lmodvscl ⊢A∈LMod∧X∈BaseScalar⁡A∧∅∈BaseA→X⋅A∅∈BaseA
23 5 10 17 22 syl3anc ⊢R∈Ring∧X∈BaseR→X⋅A∅∈BaseA
24 15 eleq2d ⊢R∈Ring→X⋅A∅∈BaseA↔X⋅A∅∈∅
25 elsni ⊢X⋅A∅∈∅→X⋅A∅=∅
26 24 25 syl6bi ⊢R∈Ring→X⋅A∅∈BaseA→X⋅A∅=∅
27 2 23 26 sylc ⊢R∈Ring∧X∈BaseR→X⋅A∅=∅