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. = ( 0g ` R )
scmatid.s 
|- S = ( N ScMat R )
Assertion scmatsubcl 
|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. S /\ Y e. S ) ) -> ( X ( -g ` A ) Y ) e. 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. = ( 0g ` R )
5 scmatid.s 
 |-  S = ( N ScMat R )
6 eqid 
 |-  ( 1r ` A ) = ( 1r ` A )
7 eqid 
 |-  ( .s ` A ) = ( .s ` A )
8 3 1 2 6 7 5 scmatscmid 
 |-  ( ( N e. Fin /\ R e. Ring /\ X e. S ) -> E. c e. E X = ( c ( .s ` A ) ( 1r ` A ) ) )
9 8 3expa 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ X e. S ) -> E. c e. E X = ( c ( .s ` A ) ( 1r ` A ) ) )
10 9 adantrr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. S /\ Y e. S ) ) -> E. c e. E X = ( c ( .s ` A ) ( 1r ` A ) ) )
11 3 1 2 6 7 5 scmatscmid 
 |-  ( ( N e. Fin /\ R e. Ring /\ Y e. S ) -> E. d e. E Y = ( d ( .s ` A ) ( 1r ` A ) ) )
12 11 3expia 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Y e. S -> E. d e. E Y = ( d ( .s ` A ) ( 1r ` A ) ) ) )
13 oveq12 
 |-  ( ( X = ( c ( .s ` A ) ( 1r ` A ) ) /\ Y = ( d ( .s ` A ) ( 1r ` A ) ) ) -> ( X ( -g ` A ) Y ) = ( ( c ( .s ` A ) ( 1r ` A ) ) ( -g ` A ) ( d ( .s ` A ) ( 1r ` A ) ) ) )
14 13 adantl 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) /\ ( X = ( c ( .s ` A ) ( 1r ` A ) ) /\ Y = ( d ( .s ` A ) ( 1r ` A ) ) ) ) -> ( X ( -g ` A ) Y ) = ( ( c ( .s ` A ) ( 1r ` A ) ) ( -g ` A ) ( d ( .s ` A ) ( 1r ` A ) ) ) )
15 eqid 
 |-  ( Scalar ` A ) = ( Scalar ` A )
16 eqid 
 |-  ( Base ` ( Scalar ` A ) ) = ( Base ` ( Scalar ` A ) )
17 eqid 
 |-  ( -g ` A ) = ( -g ` A )
18 eqid 
 |-  ( -g ` ( Scalar ` A ) ) = ( -g ` ( Scalar ` A ) )
19 1 matlmod 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. LMod )
20 19 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> A e. LMod )
21 1 matsca2 
 |-  ( ( N e. Fin /\ R e. Ring ) -> R = ( Scalar ` A ) )
22 21 fveq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Base ` R ) = ( Base ` ( Scalar ` A ) ) )
23 3 22 syl5eq 
 |-  ( ( N e. Fin /\ R e. Ring ) -> E = ( Base ` ( Scalar ` A ) ) )
24 23 eleq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( c e. E <-> c e. ( Base ` ( Scalar ` A ) ) ) )
25 24 biimpd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( c e. E -> c e. ( Base ` ( Scalar ` A ) ) ) )
26 25 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) -> ( c e. E -> c e. ( Base ` ( Scalar ` A ) ) ) )
27 26 imp 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> c e. ( Base ` ( Scalar ` A ) ) )
28 23 eleq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( d e. E <-> d e. ( Base ` ( Scalar ` A ) ) ) )
29 28 biimpa 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) -> d e. ( Base ` ( Scalar ` A ) ) )
30 29 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> d e. ( Base ` ( Scalar ` A ) ) )
31 1 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
32 2 6 ringidcl 
 |-  ( A e. Ring -> ( 1r ` A ) e. B )
33 31 32 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) e. B )
34 33 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( 1r ` A ) e. B )
35 2 7 15 16 17 18 20 27 30 34 lmodsubdir 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( ( c ( -g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) = ( ( c ( .s ` A ) ( 1r ` A ) ) ( -g ` A ) ( d ( .s ` A ) ( 1r ` A ) ) ) )
36 35 eqcomd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( ( c ( .s ` A ) ( 1r ` A ) ) ( -g ` A ) ( d ( .s ` A ) ( 1r ` A ) ) ) = ( ( c ( -g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) )
37 simpll 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( N e. Fin /\ R e. Ring ) )
38 21 eqcomd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Scalar ` A ) = R )
39 38 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( Scalar ` A ) = R )
40 39 fveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( -g ` ( Scalar ` A ) ) = ( -g ` R ) )
41 40 oveqd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( c ( -g ` ( Scalar ` A ) ) d ) = ( c ( -g ` R ) d ) )
42 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
43 42 adantl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> R e. Grp )
44 43 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> R e. Grp )
45 simpr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> c e. E )
46 simplr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> d e. E )
47 eqid 
 |-  ( -g ` R ) = ( -g ` R )
48 3 47 grpsubcl 
 |-  ( ( R e. Grp /\ c e. E /\ d e. E ) -> ( c ( -g ` R ) d ) e. E )
49 44 45 46 48 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( c ( -g ` R ) d ) e. E )
50 41 49 eqeltrd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( c ( -g ` ( Scalar ` A ) ) d ) e. E )
51 3 1 2 7 matvscl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( ( c ( -g ` ( Scalar ` A ) ) d ) e. E /\ ( 1r ` A ) e. B ) ) -> ( ( c ( -g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) e. B )
52 37 50 34 51 syl12anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( ( c ( -g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) e. B )
53 oveq1 
 |-  ( e = ( c ( -g ` ( Scalar ` A ) ) d ) -> ( e ( .s ` A ) ( 1r ` A ) ) = ( ( c ( -g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) )
54 53 eqeq2d 
 |-  ( e = ( c ( -g ` ( Scalar ` A ) ) d ) -> ( ( ( c ( -g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) = ( e ( .s ` A ) ( 1r ` A ) ) <-> ( ( c ( -g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) = ( ( c ( -g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) ) )
55 54 adantl 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) /\ e = ( c ( -g ` ( Scalar ` A ) ) d ) ) -> ( ( ( c ( -g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) = ( e ( .s ` A ) ( 1r ` A ) ) <-> ( ( c ( -g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) = ( ( c ( -g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) ) )
56 eqidd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( ( c ( -g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) = ( ( c ( -g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) )
57 50 55 56 rspcedvd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> E. e e. E ( ( c ( -g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) = ( e ( .s ` A ) ( 1r ` A ) ) )
58 3 1 2 6 7 5 scmatel 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( ( c ( -g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) e. S <-> ( ( ( c ( -g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) e. B /\ E. e e. E ( ( c ( -g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) = ( e ( .s ` A ) ( 1r ` A ) ) ) ) )
59 58 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( ( ( c ( -g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) e. S <-> ( ( ( c ( -g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) e. B /\ E. e e. E ( ( c ( -g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) = ( e ( .s ` A ) ( 1r ` A ) ) ) ) )
60 52 57 59 mpbir2and 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( ( c ( -g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) e. S )
61 36 60 eqeltrd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( ( c ( .s ` A ) ( 1r ` A ) ) ( -g ` A ) ( d ( .s ` A ) ( 1r ` A ) ) ) e. S )
62 61 adantr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) /\ ( X = ( c ( .s ` A ) ( 1r ` A ) ) /\ Y = ( d ( .s ` A ) ( 1r ` A ) ) ) ) -> ( ( c ( .s ` A ) ( 1r ` A ) ) ( -g ` A ) ( d ( .s ` A ) ( 1r ` A ) ) ) e. S )
63 14 62 eqeltrd 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) /\ ( X = ( c ( .s ` A ) ( 1r ` A ) ) /\ Y = ( d ( .s ` A ) ( 1r ` A ) ) ) ) -> ( X ( -g ` A ) Y ) e. S )
64 63 exp32 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( X = ( c ( .s ` A ) ( 1r ` A ) ) -> ( Y = ( d ( .s ` A ) ( 1r ` A ) ) -> ( X ( -g ` A ) Y ) e. S ) ) )
65 64 rexlimdva 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) -> ( E. c e. E X = ( c ( .s ` A ) ( 1r ` A ) ) -> ( Y = ( d ( .s ` A ) ( 1r ` A ) ) -> ( X ( -g ` A ) Y ) e. S ) ) )
66 65 com23 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) -> ( Y = ( d ( .s ` A ) ( 1r ` A ) ) -> ( E. c e. E X = ( c ( .s ` A ) ( 1r ` A ) ) -> ( X ( -g ` A ) Y ) e. S ) ) )
67 66 rexlimdva 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( E. d e. E Y = ( d ( .s ` A ) ( 1r ` A ) ) -> ( E. c e. E X = ( c ( .s ` A ) ( 1r ` A ) ) -> ( X ( -g ` A ) Y ) e. S ) ) )
68 12 67 syldc 
 |-  ( Y e. S -> ( ( N e. Fin /\ R e. Ring ) -> ( E. c e. E X = ( c ( .s ` A ) ( 1r ` A ) ) -> ( X ( -g ` A ) Y ) e. S ) ) )
69 68 adantl 
 |-  ( ( X e. S /\ Y e. S ) -> ( ( N e. Fin /\ R e. Ring ) -> ( E. c e. E X = ( c ( .s ` A ) ( 1r ` A ) ) -> ( X ( -g ` A ) Y ) e. S ) ) )
70 69 impcom 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. S /\ Y e. S ) ) -> ( E. c e. E X = ( c ( .s ` A ) ( 1r ` A ) ) -> ( X ( -g ` A ) Y ) e. S ) )
71 10 70 mpd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. S /\ Y e. S ) ) -> ( X ( -g ` A ) Y ) e. S )