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 = ( 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 scmataddcl 
|- ( ( ( 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 1 matlmod 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. LMod )
16 15 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> A e. LMod )
17 1 matsca2 
 |-  ( ( N e. Fin /\ R e. Ring ) -> R = ( Scalar ` A ) )
18 17 fveq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Base ` R ) = ( Base ` ( Scalar ` A ) ) )
19 3 18 eqtrid 
 |-  ( ( N e. Fin /\ R e. Ring ) -> E = ( Base ` ( Scalar ` A ) ) )
20 19 eleq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( c e. E <-> c e. ( Base ` ( Scalar ` A ) ) ) )
21 20 biimpd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( c e. E -> c e. ( Base ` ( Scalar ` A ) ) ) )
22 21 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) -> ( c e. E -> c e. ( Base ` ( Scalar ` A ) ) ) )
23 22 imp 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> c e. ( Base ` ( Scalar ` A ) ) )
24 19 eleq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( d e. E <-> d e. ( Base ` ( Scalar ` A ) ) ) )
25 24 biimpa 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) -> d e. ( Base ` ( Scalar ` A ) ) )
26 25 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> d e. ( Base ` ( Scalar ` A ) ) )
27 1 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
28 2 6 ringidcl 
 |-  ( A e. Ring -> ( 1r ` A ) e. B )
29 27 28 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) e. B )
30 29 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( 1r ` A ) e. B )
31 eqid 
 |-  ( +g ` A ) = ( +g ` A )
32 eqid 
 |-  ( Scalar ` A ) = ( Scalar ` A )
33 eqid 
 |-  ( Base ` ( Scalar ` A ) ) = ( Base ` ( Scalar ` A ) )
34 eqid 
 |-  ( +g ` ( Scalar ` A ) ) = ( +g ` ( Scalar ` A ) )
35 2 31 32 7 33 34 lmodvsdir 
 |-  ( ( A e. LMod /\ ( c e. ( Base ` ( Scalar ` A ) ) /\ d e. ( Base ` ( Scalar ` A ) ) /\ ( 1r ` A ) e. B ) ) -> ( ( c ( +g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) = ( ( c ( .s ` A ) ( 1r ` A ) ) ( +g ` A ) ( d ( .s ` A ) ( 1r ` A ) ) ) )
36 16 23 26 30 35 syl13anc 
 |-  ( ( ( ( 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 ) ) ) )
37 36 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 ) ) )
38 simpll 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( N e. Fin /\ R e. Ring ) )
39 17 eqcomd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Scalar ` A ) = R )
40 39 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( Scalar ` A ) = R )
41 40 fveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( +g ` ( Scalar ` A ) ) = ( +g ` R ) )
42 41 oveqd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( c ( +g ` ( Scalar ` A ) ) d ) = ( c ( +g ` R ) d ) )
43 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
44 43 adantl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> R e. Grp )
45 44 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> R e. Grp )
46 simpr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> c e. E )
47 simplr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> d e. E )
48 eqid 
 |-  ( +g ` R ) = ( +g ` R )
49 3 48 grpcl 
 |-  ( ( R e. Grp /\ c e. E /\ d e. E ) -> ( c ( +g ` R ) d ) e. E )
50 45 46 47 49 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( c ( +g ` R ) d ) e. E )
51 42 50 eqeltrd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( c ( +g ` ( Scalar ` A ) ) d ) e. E )
52 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 )
53 38 51 30 52 syl12anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( ( c ( +g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) e. B )
54 oveq1 
 |-  ( e = ( c ( +g ` ( Scalar ` A ) ) d ) -> ( e ( .s ` A ) ( 1r ` A ) ) = ( ( c ( +g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) )
55 54 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 ) ) ) )
56 55 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 ) ) ) )
57 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 ) ) )
58 51 56 57 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 ) ) )
59 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 ) ) ) ) )
60 59 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 ) ) ) ) )
61 53 58 60 mpbir2and 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( ( c ( +g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) e. S )
62 37 61 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 )
63 62 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 )
64 14 63 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 )
65 64 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 ) ) )
66 65 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 ) ) )
67 66 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 ) ) )
68 67 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 ) ) )
69 12 68 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 ) ) )
70 69 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 ) ) )
71 70 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 ) )
72 10 71 mpd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. S /\ Y e. S ) ) -> ( X ( +g ` A ) Y ) e. S )