Metamath Proof Explorer

Theorem scmataddcl

Description: The sum of two scalar matrices is a scalar matrix. (Contributed by AV, 25-Dec-2019)

Ref Expression
Hypotheses scmatid.a ⊢ A = N Mat R
scmatid.b ⊢ B = Base A
scmatid.e ⊢ E = Base R
scmatid.0 ⊢ 0 ˙ = 0 R
scmatid.s ⊢ S = N ScMat R
Assertion scmataddcl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ X ∈ S ∧ Y ∈ S → X + A Y ∈ S

Proof

Step Hyp Ref Expression
1 scmatid.a ⊢ A = N Mat R
2 scmatid.b ⊢ B = Base A
3 scmatid.e ⊢ E = Base R
4 scmatid.0 ⊢ 0 ˙ = 0 R
5 scmatid.s ⊢ S = N ScMat R
6 eqid ⊢ 1 A = 1 A
7 eqid ⊢ ⋅ A = ⋅ A
8 3 1 2 6 7 5 scmatscmid ⊢ N ∈ Fin ∧ R ∈ Ring ∧ X ∈ S → ∃ c ∈ E X = c ⋅ A 1 A
9 8 3expa ⊢ N ∈ Fin ∧ R ∈ Ring ∧ X ∈ S → ∃ c ∈ E X = c ⋅ A 1 A
10 9 adantrr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ X ∈ S ∧ Y ∈ S → ∃ c ∈ E X = c ⋅ A 1 A
11 3 1 2 6 7 5 scmatscmid ⊢ N ∈ Fin ∧ R ∈ Ring ∧ Y ∈ S → ∃ d ∈ E Y = d ⋅ A 1 A
12 11 3expia ⊢ N ∈ Fin ∧ R ∈ Ring → Y ∈ S → ∃ d ∈ E Y = d ⋅ A 1 A
13 oveq12 ⊢ X = c ⋅ A 1 A ∧ Y = d ⋅ A 1 A → X + A Y = c ⋅ A 1 A + A d ⋅ A 1 A
14 13 adantl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E ∧ X = c ⋅ A 1 A ∧ Y = d ⋅ A 1 A → X + A Y = c ⋅ A 1 A + A d ⋅ A 1 A
15 1 matlmod ⊢ N ∈ Fin ∧ R ∈ Ring → A ∈ LMod
16 15 ad2antrr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → A ∈ LMod
17 1 matsca2 ⊢ N ∈ Fin ∧ R ∈ Ring → R = Scalar ⁡ A
18 17 fveq2d ⊢ N ∈ Fin ∧ R ∈ Ring → Base R = Base Scalar ⁡ A
19 3 18 eqtrid ⊢ N ∈ Fin ∧ R ∈ Ring → E = Base Scalar ⁡ A
20 19 eleq2d ⊢ N ∈ Fin ∧ R ∈ Ring → c ∈ E ↔ c ∈ Base Scalar ⁡ A
21 20 biimpd ⊢ N ∈ Fin ∧ R ∈ Ring → c ∈ E → c ∈ Base Scalar ⁡ A
22 21 adantr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E → c ∈ E → c ∈ Base Scalar ⁡ A
23 22 imp ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → c ∈ Base Scalar ⁡ A
24 19 eleq2d ⊢ N ∈ Fin ∧ R ∈ Ring → d ∈ E ↔ d ∈ Base Scalar ⁡ A
25 24 biimpa ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E → d ∈ Base Scalar ⁡ A
26 25 adantr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → d ∈ Base Scalar ⁡ A
27 1 matring ⊢ N ∈ Fin ∧ R ∈ Ring → A ∈ Ring
28 2 6 ringidcl ⊢ A ∈ Ring → 1 A ∈ B
29 27 28 syl ⊢ N ∈ Fin ∧ R ∈ Ring → 1 A ∈ B
30 29 ad2antrr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → 1 A ∈ B
31 eqid ⊢ + A = + A
32 eqid ⊢ Scalar ⁡ A = Scalar ⁡ A
33 eqid ⊢ Base Scalar ⁡ A = Base Scalar ⁡ A
34 eqid ⊢ + Scalar ⁡ A = + Scalar ⁡ A
35 2 31 32 7 33 34 lmodvsdir ⊢ A ∈ LMod ∧ c ∈ Base Scalar ⁡ A ∧ d ∈ Base Scalar ⁡ A ∧ 1 A ∈ B → c + Scalar ⁡ A d ⋅ A 1 A = c ⋅ A 1 A + A d ⋅ A 1 A
36 16 23 26 30 35 syl13anc ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → c + Scalar ⁡ A d ⋅ A 1 A = c ⋅ A 1 A + A d ⋅ A 1 A
37 36 eqcomd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → c ⋅ A 1 A + A d ⋅ A 1 A = c + Scalar ⁡ A d ⋅ A 1 A
38 simpll ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → N ∈ Fin ∧ R ∈ Ring
39 17 eqcomd ⊢ N ∈ Fin ∧ R ∈ Ring → Scalar ⁡ A = R
40 39 ad2antrr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → Scalar ⁡ A = R
41 40 fveq2d ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → + Scalar ⁡ A = + R
42 41 oveqd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → c + Scalar ⁡ A d = c + R d
43 ringgrp ⊢ R ∈ Ring → R ∈ Grp
44 43 adantl ⊢ N ∈ Fin ∧ R ∈ Ring → R ∈ Grp
45 44 ad2antrr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → R ∈ Grp
46 simpr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → c ∈ E
47 simplr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → d ∈ E
48 eqid ⊢ + R = + R
49 3 48 grpcl ⊢ R ∈ Grp ∧ c ∈ E ∧ d ∈ E → c + R d ∈ E
50 45 46 47 49 syl3anc ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → c + R d ∈ E
51 42 50 eqeltrd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → c + Scalar ⁡ A d ∈ E
52 3 1 2 7 matvscl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ c + Scalar ⁡ A d ∈ E ∧ 1 A ∈ B → c + Scalar ⁡ A d ⋅ A 1 A ∈ B
53 38 51 30 52 syl12anc ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → c + Scalar ⁡ A d ⋅ A 1 A ∈ B
54 oveq1 ⊢ e = c + Scalar ⁡ A d → e ⋅ A 1 A = c + Scalar ⁡ A d ⋅ A 1 A
55 54 eqeq2d ⊢ e = c + Scalar ⁡ A d → c + Scalar ⁡ A d ⋅ A 1 A = e ⋅ A 1 A ↔ c + Scalar ⁡ A d ⋅ A 1 A = c + Scalar ⁡ A d ⋅ A 1 A
56 55 adantl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E ∧ e = c + Scalar ⁡ A d → c + Scalar ⁡ A d ⋅ A 1 A = e ⋅ A 1 A ↔ c + Scalar ⁡ A d ⋅ A 1 A = c + Scalar ⁡ A d ⋅ A 1 A
57 eqidd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → c + Scalar ⁡ A d ⋅ A 1 A = c + Scalar ⁡ A d ⋅ A 1 A
58 51 56 57 rspcedvd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → ∃ e ∈ E c + Scalar ⁡ A d ⋅ A 1 A = e ⋅ A 1 A
59 3 1 2 6 7 5 scmatel ⊢ N ∈ Fin ∧ R ∈ Ring → c + Scalar ⁡ A d ⋅ A 1 A ∈ S ↔ c + Scalar ⁡ A d ⋅ A 1 A ∈ B ∧ ∃ e ∈ E c + Scalar ⁡ A d ⋅ A 1 A = e ⋅ A 1 A
60 59 ad2antrr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → c + Scalar ⁡ A d ⋅ A 1 A ∈ S ↔ c + Scalar ⁡ A d ⋅ A 1 A ∈ B ∧ ∃ e ∈ E c + Scalar ⁡ A d ⋅ A 1 A = e ⋅ A 1 A
61 53 58 60 mpbir2and ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → c + Scalar ⁡ A d ⋅ A 1 A ∈ S
62 37 61 eqeltrd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → c ⋅ A 1 A + A d ⋅ A 1 A ∈ S
63 62 adantr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E ∧ X = c ⋅ A 1 A ∧ Y = d ⋅ A 1 A → c ⋅ A 1 A + A d ⋅ A 1 A ∈ S
64 14 63 eqeltrd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E ∧ X = c ⋅ A 1 A ∧ Y = d ⋅ A 1 A → X + A Y ∈ S
65 64 exp32 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → X = c ⋅ A 1 A → Y = d ⋅ A 1 A → X + A Y ∈ S
66 65 rexlimdva ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E → ∃ c ∈ E X = c ⋅ A 1 A → Y = d ⋅ A 1 A → X + A Y ∈ S
67 66 com23 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E → Y = d ⋅ A 1 A → ∃ c ∈ E X = c ⋅ A 1 A → X + A Y ∈ S
68 67 rexlimdva ⊢ N ∈ Fin ∧ R ∈ Ring → ∃ d ∈ E Y = d ⋅ A 1 A → ∃ c ∈ E X = c ⋅ A 1 A → X + A Y ∈ S
69 12 68 syldc ⊢ Y ∈ S → N ∈ Fin ∧ R ∈ Ring → ∃ c ∈ E X = c ⋅ A 1 A → X + A Y ∈ S
70 69 adantl ⊢ X ∈ S ∧ Y ∈ S → N ∈ Fin ∧ R ∈ Ring → ∃ c ∈ E X = c ⋅ A 1 A → X + A Y ∈ S
71 70 impcom ⊢ N ∈ Fin ∧ R ∈ Ring ∧ X ∈ S ∧ Y ∈ S → ∃ c ∈ E X = c ⋅ A 1 A → X + A Y ∈ S
72 10 71 mpd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ X ∈ S ∧ Y ∈ S → X + A Y ∈ S