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 = ∅ Mat R
Assertion mat0dimscm ⊢ R ∈ Ring ∧ X ∈ Base R → X ⋅ A ∅ = ∅

Proof

Step Hyp Ref Expression
1 mat0dim.a ⊢ A = ∅ Mat R
2 simpl ⊢ R ∈ Ring ∧ X ∈ Base R → R ∈ Ring
3 0fi ⊢ ∅ ∈ Fin
4 1 matlmod ⊢ ∅ ∈ Fin ∧ R ∈ Ring → A ∈ LMod
5 3 2 4 sylancr ⊢ R ∈ Ring ∧ X ∈ Base R → 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 → Base R = Base Scalar ⁡ A
9 8 eleq2d ⊢ R ∈ Ring → X ∈ Base R ↔ X ∈ Base Scalar ⁡ A
10 9 biimpa ⊢ R ∈ Ring ∧ X ∈ Base R → X ∈ Base Scalar ⁡ A
11 0ex ⊢ ∅ ∈ V
12 11 snid ⊢ ∅ ∈ ∅
13 1 fveq2i ⊢ Base A = Base ∅ Mat R
14 mat0dimbas0 ⊢ R ∈ Ring → Base ∅ Mat R = ∅
15 13 14 eqtrid ⊢ R ∈ Ring → Base A = ∅
16 12 15 eleqtrrid ⊢ R ∈ Ring → ∅ ∈ Base A
17 16 adantr ⊢ R ∈ Ring ∧ X ∈ Base R → ∅ ∈ Base A
18 eqid ⊢ Base A = Base A
19 eqid ⊢ Scalar ⁡ A = Scalar ⁡ A
20 eqid ⊢ ⋅ A = ⋅ A
21 eqid ⊢ Base Scalar ⁡ A = Base Scalar ⁡ A
22 18 19 20 21 lmodvscl ⊢ A ∈ LMod ∧ X ∈ Base Scalar ⁡ A ∧ ∅ ∈ Base A → X ⋅ A ∅ ∈ Base A
23 5 10 17 22 syl3anc ⊢ R ∈ Ring ∧ X ∈ Base R → X ⋅ A ∅ ∈ Base A
24 15 eleq2d ⊢ R ∈ Ring → X ⋅ A ∅ ∈ Base A ↔ X ⋅ A ∅ ∈ ∅
25 elsni ⊢ X ⋅ A ∅ ∈ ∅ → X ⋅ A ∅ = ∅
26 24 25 biimtrdi ⊢ R ∈ Ring → X ⋅ A ∅ ∈ Base A → X ⋅ A ∅ = ∅
27 2 23 26 sylc ⊢ R ∈ Ring ∧ X ∈ Base R → X ⋅ A ∅ = ∅