Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  scmatsubcl Structured version   Unicode version

Theorem scmatsubcl 18783
 Description: The difference of two scalar matrices is a scalar matrix. (Contributed by AV, 20-Aug-2019.) (Revised by AV, 19-Dec-2019.)
Hypotheses
Ref Expression
scmatid.a Mat
scmatid.b
scmatid.e
scmatid.0
scmatid.s ScMat
Assertion
Ref Expression
scmatsubcl

Proof of Theorem scmatsubcl
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 scmatid.e . . . . 5
2 scmatid.a . . . . 5 Mat
3 scmatid.b . . . . 5
4 eqid 2467 . . . . 5
5 eqid 2467 . . . . 5
6 scmatid.s . . . . 5 ScMat
71, 2, 3, 4, 5, 6scmatscmid 18772 . . . 4
873expa 1196 . . 3
101, 2, 3, 4, 5, 6scmatscmid 18772 . . . . . . 7
11103expia 1198 . . . . . 6
12 oveq12 6291 . . . . . . . . . . . 12
1312adantl 466 . . . . . . . . . . 11
14 eqid 2467 . . . . . . . . . . . . . . 15 Scalar Scalar
15 eqid 2467 . . . . . . . . . . . . . . 15 Scalar Scalar
16 eqid 2467 . . . . . . . . . . . . . . 15
17 eqid 2467 . . . . . . . . . . . . . . 15 Scalar Scalar
182matlmod 18695 . . . . . . . . . . . . . . . 16
1918ad2antrr 725 . . . . . . . . . . . . . . 15
202matsca2 18686 . . . . . . . . . . . . . . . . . . . . 21 Scalar
2120fveq2d 5868 . . . . . . . . . . . . . . . . . . . 20 Scalar
221, 21syl5eq 2520 . . . . . . . . . . . . . . . . . . 19 Scalar
2322eleq2d 2537 . . . . . . . . . . . . . . . . . 18 Scalar
2423biimpd 207 . . . . . . . . . . . . . . . . 17 Scalar
2524adantr 465 . . . . . . . . . . . . . . . 16 Scalar
2625imp 429 . . . . . . . . . . . . . . 15 Scalar
2722eleq2d 2537 . . . . . . . . . . . . . . . . 17 Scalar
2827biimpa 484 . . . . . . . . . . . . . . . 16 Scalar
2928adantr 465 . . . . . . . . . . . . . . 15 Scalar
302matrng 18709 . . . . . . . . . . . . . . . . 17
313, 4rngidcl 17003 . . . . . . . . . . . . . . . . 17
3230, 31syl 16 . . . . . . . . . . . . . . . 16
3332ad2antrr 725 . . . . . . . . . . . . . . 15
343, 5, 14, 15, 16, 17, 19, 26, 29, 33lmodsubdir 17348 . . . . . . . . . . . . . 14 Scalar
3534eqcomd 2475 . . . . . . . . . . . . 13 Scalar
36 simpll 753 . . . . . . . . . . . . . . 15
3720eqcomd 2475 . . . . . . . . . . . . . . . . . . 19 Scalar
3837ad2antrr 725 . . . . . . . . . . . . . . . . . 18 Scalar
3938fveq2d 5868 . . . . . . . . . . . . . . . . 17 Scalar
4039oveqd 6299 . . . . . . . . . . . . . . . 16 Scalar
41 rnggrp 16988 . . . . . . . . . . . . . . . . . . 19
4241adantl 466 . . . . . . . . . . . . . . . . . 18
4342ad2antrr 725 . . . . . . . . . . . . . . . . 17
44 simpr 461 . . . . . . . . . . . . . . . . 17
45 simplr 754 . . . . . . . . . . . . . . . . 17
46 eqid 2467 . . . . . . . . . . . . . . . . . 18
471, 46grpsubcl 15916 . . . . . . . . . . . . . . . . 17
4843, 44, 45, 47syl3anc 1228 . . . . . . . . . . . . . . . 16
4940, 48eqeltrd 2555 . . . . . . . . . . . . . . 15 Scalar
501, 2, 3, 5matvscl 18697 . . . . . . . . . . . . . . 15 Scalar Scalar
5136, 49, 33, 50syl12anc 1226 . . . . . . . . . . . . . 14 Scalar
52 oveq1 6289 . . . . . . . . . . . . . . . . 17 Scalar Scalar
5352eqeq2d 2481 . . . . . . . . . . . . . . . 16 Scalar Scalar Scalar Scalar
5453adantl 466 . . . . . . . . . . . . . . 15 Scalar Scalar Scalar Scalar
55 eqidd 2468 . . . . . . . . . . . . . . 15 Scalar Scalar
5649, 54, 55rspcedvd 3219 . . . . . . . . . . . . . 14 Scalar
571, 2, 3, 4, 5, 6scmatel 18771 . . . . . . . . . . . . . . 15 Scalar Scalar Scalar
5857ad2antrr 725 . . . . . . . . . . . . . 14 Scalar Scalar Scalar
5951, 56, 58mpbir2and 920 . . . . . . . . . . . . 13 Scalar
6035, 59eqeltrd 2555 . . . . . . . . . . . 12
6160adantr 465 . . . . . . . . . . 11
6213, 61eqeltrd 2555 . . . . . . . . . 10
6362exp32 605 . . . . . . . . 9
6463rexlimdva 2955 . . . . . . . 8
6564com23 78 . . . . . . 7
6665rexlimdva 2955 . . . . . 6
6711, 66syld 44 . . . . 5
6867com12 31 . . . 4