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=NMatR
scmatid.b ⊢B=BaseA
scmatid.e ⊢E=BaseR
scmatid.0 ⊢0˙=0R
scmatid.s ⊢S=NScMatR
Assertion scmataddcl ⊢N∈Fin∧R∈Ring∧X∈S∧Y∈S→X+AY∈S

Proof

Step Hyp Ref Expression
1 scmatid.a ⊢A=NMatR
2 scmatid.b ⊢B=BaseA
3 scmatid.e ⊢E=BaseR
4 scmatid.0 ⊢0˙=0R
5 scmatid.s ⊢S=NScMatR
6 eqid ⊢1A=1A
7 eqid ⊢⋅A=⋅A
8 3 1 2 6 7 5 scmatscmid ⊢N∈Fin∧R∈Ring∧X∈S→∃c∈EX=c⋅A1A
9 8 3expa ⊢N∈Fin∧R∈Ring∧X∈S→∃c∈EX=c⋅A1A
10 9 adantrr ⊢N∈Fin∧R∈Ring∧X∈S∧Y∈S→∃c∈EX=c⋅A1A
11 3 1 2 6 7 5 scmatscmid ⊢N∈Fin∧R∈Ring∧Y∈S→∃d∈EY=d⋅A1A
12 11 3expia ⊢N∈Fin∧R∈Ring→Y∈S→∃d∈EY=d⋅A1A
13 oveq12 ⊢X=c⋅A1A∧Y=d⋅A1A→X+AY=c⋅A1A+Ad⋅A1A
14 13 adantl ⊢N∈Fin∧R∈Ring∧d∈E∧c∈E∧X=c⋅A1A∧Y=d⋅A1A→X+AY=c⋅A1A+Ad⋅A1A
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→BaseR=BaseScalar⁡A
19 3 18 eqtrid ⊢N∈Fin∧R∈Ring→E=BaseScalar⁡A
20 19 eleq2d ⊢N∈Fin∧R∈Ring→c∈E↔c∈BaseScalar⁡A
21 20 biimpd ⊢N∈Fin∧R∈Ring→c∈E→c∈BaseScalar⁡A
22 21 adantr ⊢N∈Fin∧R∈Ring∧d∈E→c∈E→c∈BaseScalar⁡A
23 22 imp ⊢N∈Fin∧R∈Ring∧d∈E∧c∈E→c∈BaseScalar⁡A
24 19 eleq2d ⊢N∈Fin∧R∈Ring→d∈E↔d∈BaseScalar⁡A
25 24 biimpa ⊢N∈Fin∧R∈Ring∧d∈E→d∈BaseScalar⁡A
26 25 adantr ⊢N∈Fin∧R∈Ring∧d∈E∧c∈E→d∈BaseScalar⁡A
27 1 matring ⊢N∈Fin∧R∈Ring→A∈Ring
28 2 6 ringidcl ⊢A∈Ring→1A∈B
29 27 28 syl ⊢N∈Fin∧R∈Ring→1A∈B
30 29 ad2antrr ⊢N∈Fin∧R∈Ring∧d∈E∧c∈E→1A∈B
31 eqid ⊢+A=+A
32 eqid ⊢Scalar⁡A=Scalar⁡A
33 eqid ⊢BaseScalar⁡A=BaseScalar⁡A
34 eqid ⊢+Scalar⁡A=+Scalar⁡A
35 2 31 32 7 33 34 lmodvsdir ⊢A∈LMod∧c∈BaseScalar⁡A∧d∈BaseScalar⁡A∧1A∈B→c+Scalar⁡Ad⋅A1A=c⋅A1A+Ad⋅A1A
36 16 23 26 30 35 syl13anc ⊢N∈Fin∧R∈Ring∧d∈E∧c∈E→c+Scalar⁡Ad⋅A1A=c⋅A1A+Ad⋅A1A
37 36 eqcomd ⊢N∈Fin∧R∈Ring∧d∈E∧c∈E→c⋅A1A+Ad⋅A1A=c+Scalar⁡Ad⋅A1A
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⁡Ad=c+Rd
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+Rd∈E
50 45 46 47 49 syl3anc ⊢N∈Fin∧R∈Ring∧d∈E∧c∈E→c+Rd∈E
51 42 50 eqeltrd ⊢N∈Fin∧R∈Ring∧d∈E∧c∈E→c+Scalar⁡Ad∈E
52 3 1 2 7 matvscl ⊢N∈Fin∧R∈Ring∧c+Scalar⁡Ad∈E∧1A∈B→c+Scalar⁡Ad⋅A1A∈B
53 38 51 30 52 syl12anc ⊢N∈Fin∧R∈Ring∧d∈E∧c∈E→c+Scalar⁡Ad⋅A1A∈B
54 oveq1 ⊢e=c+Scalar⁡Ad→e⋅A1A=c+Scalar⁡Ad⋅A1A
55 54 eqeq2d ⊢e=c+Scalar⁡Ad→c+Scalar⁡Ad⋅A1A=e⋅A1A↔c+Scalar⁡Ad⋅A1A=c+Scalar⁡Ad⋅A1A
56 55 adantl ⊢N∈Fin∧R∈Ring∧d∈E∧c∈E∧e=c+Scalar⁡Ad→c+Scalar⁡Ad⋅A1A=e⋅A1A↔c+Scalar⁡Ad⋅A1A=c+Scalar⁡Ad⋅A1A
57 eqidd ⊢N∈Fin∧R∈Ring∧d∈E∧c∈E→c+Scalar⁡Ad⋅A1A=c+Scalar⁡Ad⋅A1A
58 51 56 57 rspcedvd ⊢N∈Fin∧R∈Ring∧d∈E∧c∈E→∃e∈Ec+Scalar⁡Ad⋅A1A=e⋅A1A
59 3 1 2 6 7 5 scmatel ⊢N∈Fin∧R∈Ring→c+Scalar⁡Ad⋅A1A∈S↔c+Scalar⁡Ad⋅A1A∈B∧∃e∈Ec+Scalar⁡Ad⋅A1A=e⋅A1A
60 59 ad2antrr ⊢N∈Fin∧R∈Ring∧d∈E∧c∈E→c+Scalar⁡Ad⋅A1A∈S↔c+Scalar⁡Ad⋅A1A∈B∧∃e∈Ec+Scalar⁡Ad⋅A1A=e⋅A1A
61 53 58 60 mpbir2and ⊢N∈Fin∧R∈Ring∧d∈E∧c∈E→c+Scalar⁡Ad⋅A1A∈S
62 37 61 eqeltrd ⊢N∈Fin∧R∈Ring∧d∈E∧c∈E→c⋅A1A+Ad⋅A1A∈S
63 62 adantr ⊢N∈Fin∧R∈Ring∧d∈E∧c∈E∧X=c⋅A1A∧Y=d⋅A1A→c⋅A1A+Ad⋅A1A∈S
64 14 63 eqeltrd ⊢N∈Fin∧R∈Ring∧d∈E∧c∈E∧X=c⋅A1A∧Y=d⋅A1A→X+AY∈S
65 64 exp32 ⊢N∈Fin∧R∈Ring∧d∈E∧c∈E→X=c⋅A1A→Y=d⋅A1A→X+AY∈S
66 65 rexlimdva ⊢N∈Fin∧R∈Ring∧d∈E→∃c∈EX=c⋅A1A→Y=d⋅A1A→X+AY∈S
67 66 com23 ⊢N∈Fin∧R∈Ring∧d∈E→Y=d⋅A1A→∃c∈EX=c⋅A1A→X+AY∈S
68 67 rexlimdva ⊢N∈Fin∧R∈Ring→∃d∈EY=d⋅A1A→∃c∈EX=c⋅A1A→X+AY∈S
69 12 68 syldc ⊢Y∈S→N∈Fin∧R∈Ring→∃c∈EX=c⋅A1A→X+AY∈S
70 69 adantl ⊢X∈S∧Y∈S→N∈Fin∧R∈Ring→∃c∈EX=c⋅A1A→X+AY∈S
71 70 impcom ⊢N∈Fin∧R∈Ring∧X∈S∧Y∈S→∃c∈EX=c⋅A1A→X+AY∈S
72 10 71 mpd ⊢N∈Fin∧R∈Ring∧X∈S∧Y∈S→X+AY∈S