Metamath Proof Explorer

Theorem smatvscl

Description: Closure of the scalar multiplication in the ring of scalar matrices. ( matvscl analog.) (Contributed by AV, 24-Dec-2019)

Ref Expression
Hypotheses smatvscl.k ⊢ K = Base R
smatvscl.a ⊢ A = N Mat R
smatvscl.s ⊢ S = N ScMat R
smatvscl.t ⊢ ∗ ˙ = ⋅ A
Assertion smatvscl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ S → C ∗ ˙ X ∈ S

Proof

Step Hyp Ref Expression
1 smatvscl.k ⊢ K = Base R
2 smatvscl.a ⊢ A = N Mat R
3 smatvscl.s ⊢ S = N ScMat R
4 smatvscl.t ⊢ ∗ ˙ = ⋅ A
5 eqid ⊢ Base R = Base R
6 eqid ⊢ Base A = Base A
7 eqid ⊢ 1 A = 1 A
8 5 2 6 7 4 3 scmatel ⊢ N ∈ Fin ∧ R ∈ Ring → X ∈ S ↔ X ∈ Base A ∧ ∃ c ∈ Base R X = c ∗ ˙ 1 A
9 oveq2 ⊢ X = c ∗ ˙ 1 A → C ∗ ˙ X = C ∗ ˙ c ∗ ˙ 1 A
10 9 adantl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ Base A ∧ c ∈ Base R ∧ X = c ∗ ˙ 1 A → C ∗ ˙ X = C ∗ ˙ c ∗ ˙ 1 A
11 2 matlmod ⊢ N ∈ Fin ∧ R ∈ Ring → A ∈ LMod
12 11 ad3antrrr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ Base A ∧ c ∈ Base R → A ∈ LMod
13 2 matsca2 ⊢ N ∈ Fin ∧ R ∈ Ring → R = Scalar ⁡ A
14 13 fveq2d ⊢ N ∈ Fin ∧ R ∈ Ring → Base R = Base Scalar ⁡ A
15 1 14 eqtrid ⊢ N ∈ Fin ∧ R ∈ Ring → K = Base Scalar ⁡ A
16 15 eleq2d ⊢ N ∈ Fin ∧ R ∈ Ring → C ∈ K ↔ C ∈ Base Scalar ⁡ A
17 16 biimpa ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K → C ∈ Base Scalar ⁡ A
18 17 ad2antrr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ Base A ∧ c ∈ Base R → C ∈ Base Scalar ⁡ A
19 13 ad2antrr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ Base A → R = Scalar ⁡ A
20 19 fveq2d ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ Base A → Base R = Base Scalar ⁡ A
21 20 eleq2d ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ Base A → c ∈ Base R ↔ c ∈ Base Scalar ⁡ A
22 21 biimpa ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ Base A ∧ c ∈ Base R → c ∈ Base Scalar ⁡ A
23 2 matring ⊢ N ∈ Fin ∧ R ∈ Ring → A ∈ Ring
24 6 7 ringidcl ⊢ A ∈ Ring → 1 A ∈ Base A
25 23 24 syl ⊢ N ∈ Fin ∧ R ∈ Ring → 1 A ∈ Base A
26 25 ad3antrrr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ Base A ∧ c ∈ Base R → 1 A ∈ Base A
27 eqid ⊢ Scalar ⁡ A = Scalar ⁡ A
28 eqid ⊢ Base Scalar ⁡ A = Base Scalar ⁡ A
29 eqid ⊢ ⋅ Scalar ⁡ A = ⋅ Scalar ⁡ A
30 6 27 4 28 29 lmodvsass ⊢ A ∈ LMod ∧ C ∈ Base Scalar ⁡ A ∧ c ∈ Base Scalar ⁡ A ∧ 1 A ∈ Base A → C ⋅ Scalar ⁡ A c ∗ ˙ 1 A = C ∗ ˙ c ∗ ˙ 1 A
31 12 18 22 26 30 syl13anc ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ Base A ∧ c ∈ Base R → C ⋅ Scalar ⁡ A c ∗ ˙ 1 A = C ∗ ˙ c ∗ ˙ 1 A
32 31 eqcomd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ Base A ∧ c ∈ Base R → C ∗ ˙ c ∗ ˙ 1 A = C ⋅ Scalar ⁡ A c ∗ ˙ 1 A
33 simplll ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ Base A ∧ c ∈ Base R → N ∈ Fin ∧ R ∈ Ring
34 13 adantr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K → R = Scalar ⁡ A
35 34 eqcomd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K → Scalar ⁡ A = R
36 35 ad2antrr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ Base A ∧ c ∈ Base R → Scalar ⁡ A = R
37 36 fveq2d ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ Base A ∧ c ∈ Base R → ⋅ Scalar ⁡ A = ⋅ R
38 37 oveqd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ Base A ∧ c ∈ Base R → C ⋅ Scalar ⁡ A c = C ⋅ R c
39 simp-4r ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ Base A ∧ c ∈ Base R → R ∈ Ring
40 simpllr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ Base A ∧ c ∈ Base R → C ∈ K
41 1 eqcomi ⊢ Base R = K
42 41 eleq2i ⊢ c ∈ Base R ↔ c ∈ K
43 42 bilani ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ Base A ∧ c ∈ Base R → c ∈ K
44 eqid ⊢ ⋅ R = ⋅ R
45 1 44 ringcl ⊢ R ∈ Ring ∧ C ∈ K ∧ c ∈ K → C ⋅ R c ∈ K
46 39 40 43 45 syl3anc ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ Base A ∧ c ∈ Base R → C ⋅ R c ∈ K
47 38 46 eqeltrd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ Base A ∧ c ∈ Base R → C ⋅ Scalar ⁡ A c ∈ K
48 1 2 6 4 matvscl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ⋅ Scalar ⁡ A c ∈ K ∧ 1 A ∈ Base A → C ⋅ Scalar ⁡ A c ∗ ˙ 1 A ∈ Base A
49 33 47 26 48 syl12anc ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ Base A ∧ c ∈ Base R → C ⋅ Scalar ⁡ A c ∗ ˙ 1 A ∈ Base A
50 oveq1 ⊢ C ⋅ Scalar ⁡ A c = e → C ⋅ Scalar ⁡ A c ∗ ˙ 1 A = e ∗ ˙ 1 A
51 50 eqcoms ⊢ e = C ⋅ Scalar ⁡ A c → C ⋅ Scalar ⁡ A c ∗ ˙ 1 A = e ∗ ˙ 1 A
52 51 adantl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ Base A ∧ c ∈ Base R ∧ e = C ⋅ Scalar ⁡ A c → C ⋅ Scalar ⁡ A c ∗ ˙ 1 A = e ∗ ˙ 1 A
53 47 52 rspcedeqvd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ Base A ∧ c ∈ Base R → ∃ e ∈ K C ⋅ Scalar ⁡ A c ∗ ˙ 1 A = e ∗ ˙ 1 A
54 1 2 6 7 4 3 scmatel ⊢ N ∈ Fin ∧ R ∈ Ring → C ⋅ Scalar ⁡ A c ∗ ˙ 1 A ∈ S ↔ C ⋅ Scalar ⁡ A c ∗ ˙ 1 A ∈ Base A ∧ ∃ e ∈ K C ⋅ Scalar ⁡ A c ∗ ˙ 1 A = e ∗ ˙ 1 A
55 54 ad3antrrr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ Base A ∧ c ∈ Base R → C ⋅ Scalar ⁡ A c ∗ ˙ 1 A ∈ S ↔ C ⋅ Scalar ⁡ A c ∗ ˙ 1 A ∈ Base A ∧ ∃ e ∈ K C ⋅ Scalar ⁡ A c ∗ ˙ 1 A = e ∗ ˙ 1 A
56 49 53 55 mpbir2and ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ Base A ∧ c ∈ Base R → C ⋅ Scalar ⁡ A c ∗ ˙ 1 A ∈ S
57 32 56 eqeltrd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ Base A ∧ c ∈ Base R → C ∗ ˙ c ∗ ˙ 1 A ∈ S
58 57 adantr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ Base A ∧ c ∈ Base R ∧ X = c ∗ ˙ 1 A → C ∗ ˙ c ∗ ˙ 1 A ∈ S
59 10 58 eqeltrd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ Base A ∧ c ∈ Base R ∧ X = c ∗ ˙ 1 A → C ∗ ˙ X ∈ S
60 59 rexlimdva2 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ Base A → ∃ c ∈ Base R X = c ∗ ˙ 1 A → C ∗ ˙ X ∈ S
61 60 expimpd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K → X ∈ Base A ∧ ∃ c ∈ Base R X = c ∗ ˙ 1 A → C ∗ ˙ X ∈ S
62 61 ex ⊢ N ∈ Fin ∧ R ∈ Ring → C ∈ K → X ∈ Base A ∧ ∃ c ∈ Base R X = c ∗ ˙ 1 A → C ∗ ˙ X ∈ S
63 62 com23 ⊢ N ∈ Fin ∧ R ∈ Ring → X ∈ Base A ∧ ∃ c ∈ Base R X = c ∗ ˙ 1 A → C ∈ K → C ∗ ˙ X ∈ S
64 8 63 sylbid ⊢ N ∈ Fin ∧ R ∈ Ring → X ∈ S → C ∈ K → C ∗ ˙ X ∈ S
65 64 com23 ⊢ N ∈ Fin ∧ R ∈ Ring → C ∈ K → X ∈ S → C ∗ ˙ X ∈ S
66 65 imp32 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ K ∧ X ∈ S → C ∗ ˙ X ∈ S