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