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 )