Metamath Proof Explorer

Theorem matvscl

Description: Closure of the scalar multiplication in the matrix ring. ( lmodvscl analog.) (Contributed by AV, 27-Nov-2019)

Ref Expression
Hypotheses matvscl.k ⊢ K = Base R
matvscl.a ⊢ A = N Mat R
matvscl.b ⊢ B = Base A
matvscl.s ⊢ · ˙ = ⋅ A
Assertion matvscl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ B → C · ˙ X ∈ B

Proof

Step Hyp Ref Expression
1 matvscl.k ⊢ K = Base R
2 matvscl.a ⊢ A = N Mat R
3 matvscl.b ⊢ B = Base A
4 matvscl.s ⊢ · ˙ = ⋅ A
5 2 matlmod ⊢ N ∈ Fin ∧ R ∈ Ring → A ∈ LMod
6 5 adantr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ B → A ∈ LMod
7 2 matsca2 ⊢ N ∈ Fin ∧ R ∈ Ring → R = Scalar ⁡ A
8 7 fveq2d ⊢ N ∈ Fin ∧ R ∈ Ring → Base R = Base Scalar ⁡ A
9 1 8 syl5eq ⊢ N ∈ Fin ∧ R ∈ Ring → K = Base Scalar ⁡ A
10 9 eleq2d ⊢ N ∈ Fin ∧ R ∈ Ring → C ∈ K ↔ C ∈ Base Scalar ⁡ A
11 10 biimpd ⊢ N ∈ Fin ∧ R ∈ Ring → C ∈ K → C ∈ Base Scalar ⁡ A
12 11 adantrd ⊢ N ∈ Fin ∧ R ∈ Ring → C ∈ K ∧ X ∈ B → C ∈ Base Scalar ⁡ A
13 12 imp ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ B → C ∈ Base Scalar ⁡ A
14 simprr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ B → X ∈ B
15 eqid ⊢ Scalar ⁡ A = Scalar ⁡ A
16 eqid ⊢ Base Scalar ⁡ A = Base Scalar ⁡ A
17 3 15 4 16 lmodvscl ⊢ A ∈ LMod ∧ C ∈ Base Scalar ⁡ A ∧ X ∈ B → C · ˙ X ∈ B
18 6 13 14 17 syl3anc ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ B → C · ˙ X ∈ B