Metamath Proof Explorer

Theorem scmatsubcl

Description: The difference of two scalar matrices is a scalar matrix. (Contributed by AV, 20-Aug-2019) (Revised by AV, 19-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 scmatsubcl ⊢ 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 eqid ⊢ Scalar ⁡ A = Scalar ⁡ A
16 eqid ⊢ Base Scalar ⁡ A = Base Scalar ⁡ A
17 eqid ⊢ - A = - A
18 eqid ⊢ - Scalar ⁡ A = - Scalar ⁡ A
19 1 matlmod ⊢ N ∈ Fin ∧ R ∈ Ring → A ∈ LMod
20 19 ad2antrr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → A ∈ LMod
21 1 matsca2 ⊢ N ∈ Fin ∧ R ∈ Ring → R = Scalar ⁡ A
22 21 fveq2d ⊢ N ∈ Fin ∧ R ∈ Ring → Base R = Base Scalar ⁡ A
23 3 22 syl5eq ⊢ N ∈ Fin ∧ R ∈ Ring → E = Base Scalar ⁡ A
24 23 eleq2d ⊢ N ∈ Fin ∧ R ∈ Ring → c ∈ E ↔ c ∈ Base Scalar ⁡ A
25 24 biimpd ⊢ N ∈ Fin ∧ R ∈ Ring → c ∈ E → c ∈ Base Scalar ⁡ A
26 25 adantr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E → c ∈ E → c ∈ Base Scalar ⁡ A
27 26 imp ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → c ∈ Base Scalar ⁡ A
28 23 eleq2d ⊢ N ∈ Fin ∧ R ∈ Ring → d ∈ E ↔ d ∈ Base Scalar ⁡ A
29 28 biimpa ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E → d ∈ Base Scalar ⁡ A
30 29 adantr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → d ∈ Base Scalar ⁡ A
31 1 matring ⊢ N ∈ Fin ∧ R ∈ Ring → A ∈ Ring
32 2 6 ringidcl ⊢ A ∈ Ring → 1 A ∈ B
33 31 32 syl ⊢ N ∈ Fin ∧ R ∈ Ring → 1 A ∈ B
34 33 ad2antrr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → 1 A ∈ B
35 2 7 15 16 17 18 20 27 30 34 lmodsubdir ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → c - Scalar ⁡ A d ⋅ A 1 A = c ⋅ A 1 A - A d ⋅ A 1 A
36 35 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
37 simpll ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → N ∈ Fin ∧ R ∈ Ring
38 21 eqcomd ⊢ N ∈ Fin ∧ R ∈ Ring → Scalar ⁡ A = R
39 38 ad2antrr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → Scalar ⁡ A = R
40 39 fveq2d ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → - Scalar ⁡ A = - R
41 40 oveqd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → c - Scalar ⁡ A d = c - R d
42 ringgrp ⊢ R ∈ Ring → R ∈ Grp
43 42 adantl ⊢ N ∈ Fin ∧ R ∈ Ring → R ∈ Grp
44 43 ad2antrr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → R ∈ Grp
45 simpr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → c ∈ E
46 simplr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → d ∈ E
47 eqid ⊢ - R = - R
48 3 47 grpsubcl ⊢ R ∈ Grp ∧ c ∈ E ∧ d ∈ E → c - R d ∈ E
49 44 45 46 48 syl3anc ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → c - R d ∈ E
50 41 49 eqeltrd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → c - Scalar ⁡ A d ∈ E
51 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
52 37 50 34 51 syl12anc ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → c - Scalar ⁡ A d ⋅ A 1 A ∈ B
53 oveq1 ⊢ e = c - Scalar ⁡ A d → e ⋅ A 1 A = c - Scalar ⁡ A d ⋅ A 1 A
54 53 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
55 54 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
56 eqidd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → c - Scalar ⁡ A d ⋅ A 1 A = c - Scalar ⁡ A d ⋅ A 1 A
57 50 55 56 rspcedvd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → ∃ e ∈ E c - Scalar ⁡ A d ⋅ A 1 A = e ⋅ A 1 A
58 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
59 58 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
60 52 57 59 mpbir2and ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → c - Scalar ⁡ A d ⋅ A 1 A ∈ S
61 36 60 eqeltrd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → c ⋅ A 1 A - A d ⋅ A 1 A ∈ S
62 61 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
63 14 62 eqeltrd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E ∧ X = c ⋅ A 1 A ∧ Y = d ⋅ A 1 A → X - A Y ∈ S
64 63 exp32 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E ∧ c ∈ E → X = c ⋅ A 1 A → Y = d ⋅ A 1 A → X - A Y ∈ S
65 64 rexlimdva ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E → ∃ c ∈ E X = c ⋅ A 1 A → Y = d ⋅ A 1 A → X - A Y ∈ S
66 65 com23 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ d ∈ E → Y = d ⋅ A 1 A → ∃ c ∈ E X = c ⋅ A 1 A → X - A Y ∈ S
67 66 rexlimdva ⊢ N ∈ Fin ∧ R ∈ Ring → ∃ d ∈ E Y = d ⋅ A 1 A → ∃ c ∈ E X = c ⋅ A 1 A → X - A Y ∈ S
68 12 67 syldc ⊢ Y ∈ S → N ∈ Fin ∧ R ∈ Ring → ∃ c ∈ E X = c ⋅ A 1 A → X - A Y ∈ S
69 68 adantl ⊢ X ∈ S ∧ Y ∈ S → N ∈ Fin ∧ R ∈ Ring → ∃ c ∈ E X = c ⋅ A 1 A → X - A Y ∈ S
70 69 impcom ⊢ N ∈ Fin ∧ R ∈ Ring ∧ X ∈ S ∧ Y ∈ S → ∃ c ∈ E X = c ⋅ A 1 A → X - A Y ∈ S
71 10 70 mpd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ X ∈ S ∧ Y ∈ S → X - A Y ∈ S