Metamath Proof Explorer

Theorem scmatmulcl

Description: The product of two scalar matrices is a scalar matrix. (Contributed by AV, 21-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 scmatmulcl 
|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. S /\ Y e. S ) ) -> ( X ( .r ` 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 scmatel 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( X e. S <-> ( X e. B /\ E. c e. E X = ( c ( .s ` A ) ( 1r ` A ) ) ) ) )
9 3 1 2 6 7 5 scmatel 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Y e. S <-> ( Y e. B /\ E. d e. E Y = ( d ( .s ` A ) ( 1r ` A ) ) ) ) )
10 oveq12 
 |-  ( ( X = ( c ( .s ` A ) ( 1r ` A ) ) /\ Y = ( d ( .s ` A ) ( 1r ` A ) ) ) -> ( X ( .r ` A ) Y ) = ( ( c ( .s ` A ) ( 1r ` A ) ) ( .r ` A ) ( d ( .s ` A ) ( 1r ` A ) ) ) )
11 10 adantll 
 |-  ( ( ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ Y e. B ) /\ d e. E ) /\ X e. B ) /\ c e. E ) /\ X = ( c ( .s ` A ) ( 1r ` A ) ) ) /\ Y = ( d ( .s ` A ) ( 1r ` A ) ) ) -> ( X ( .r ` A ) Y ) = ( ( c ( .s ` A ) ( 1r ` A ) ) ( .r ` A ) ( d ( .s ` A ) ( 1r ` A ) ) ) )
12 simp-4l 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ Y e. B ) /\ d e. E ) /\ X e. B ) /\ c e. E ) -> ( N e. Fin /\ R e. Ring ) )
13 simplr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ Y e. B ) /\ d e. E ) /\ X e. B ) -> d e. E )
14 13 anim1ci 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ Y e. B ) /\ d e. E ) /\ X e. B ) /\ c e. E ) -> ( c e. E /\ d e. E ) )
15 eqid 
 |-  ( .r ` R ) = ( .r ` R )
16 eqid 
 |-  ( .r ` A ) = ( .r ` A )
17 1 3 4 6 7 15 16 scmatscmiddistr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( c e. E /\ d e. E ) ) -> ( ( c ( .s ` A ) ( 1r ` A ) ) ( .r ` A ) ( d ( .s ` A ) ( 1r ` A ) ) ) = ( ( c ( .r ` R ) d ) ( .s ` A ) ( 1r ` A ) ) )
18 12 14 17 syl2anc 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ Y e. B ) /\ d e. E ) /\ X e. B ) /\ c e. E ) -> ( ( c ( .s ` A ) ( 1r ` A ) ) ( .r ` A ) ( d ( .s ` A ) ( 1r ` A ) ) ) = ( ( c ( .r ` R ) d ) ( .s ` A ) ( 1r ` A ) ) )
19 simpl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( d e. E /\ c e. E ) ) -> ( N e. Fin /\ R e. Ring ) )
20 simplr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( d e. E /\ c e. E ) ) -> R e. Ring )
21 simprr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( d e. E /\ c e. E ) ) -> c e. E )
22 simpl 
 |-  ( ( d e. E /\ c e. E ) -> d e. E )
23 22 adantl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( d e. E /\ c e. E ) ) -> d e. E )
24 3 15 ringcl 
 |-  ( ( R e. Ring /\ c e. E /\ d e. E ) -> ( c ( .r ` R ) d ) e. E )
25 20 21 23 24 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( d e. E /\ c e. E ) ) -> ( c ( .r ` R ) d ) e. E )
26 1 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
27 2 6 ringidcl 
 |-  ( A e. Ring -> ( 1r ` A ) e. B )
28 26 27 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) e. B )
29 28 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( d e. E /\ c e. E ) ) -> ( 1r ` A ) e. B )
30 3 1 2 7 matvscl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( ( c ( .r ` R ) d ) e. E /\ ( 1r ` A ) e. B ) ) -> ( ( c ( .r ` R ) d ) ( .s ` A ) ( 1r ` A ) ) e. B )
31 19 25 29 30 syl12anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( d e. E /\ c e. E ) ) -> ( ( c ( .r ` R ) d ) ( .s ` A ) ( 1r ` A ) ) e. B )
32 oveq1 
 |-  ( e = ( c ( .r ` R ) d ) -> ( e ( .s ` A ) ( 1r ` A ) ) = ( ( c ( .r ` R ) d ) ( .s ` A ) ( 1r ` A ) ) )
33 32 eqeq2d 
 |-  ( e = ( c ( .r ` R ) d ) -> ( ( ( c ( .r ` R ) d ) ( .s ` A ) ( 1r ` A ) ) = ( e ( .s ` A ) ( 1r ` A ) ) <-> ( ( c ( .r ` R ) d ) ( .s ` A ) ( 1r ` A ) ) = ( ( c ( .r ` R ) d ) ( .s ` A ) ( 1r ` A ) ) ) )
34 33 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( d e. E /\ c e. E ) ) /\ e = ( c ( .r ` R ) d ) ) -> ( ( ( c ( .r ` R ) d ) ( .s ` A ) ( 1r ` A ) ) = ( e ( .s ` A ) ( 1r ` A ) ) <-> ( ( c ( .r ` R ) d ) ( .s ` A ) ( 1r ` A ) ) = ( ( c ( .r ` R ) d ) ( .s ` A ) ( 1r ` A ) ) ) )
35 eqidd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( d e. E /\ c e. E ) ) -> ( ( c ( .r ` R ) d ) ( .s ` A ) ( 1r ` A ) ) = ( ( c ( .r ` R ) d ) ( .s ` A ) ( 1r ` A ) ) )
36 25 34 35 rspcedvd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( d e. E /\ c e. E ) ) -> E. e e. E ( ( c ( .r ` R ) d ) ( .s ` A ) ( 1r ` A ) ) = ( e ( .s ` A ) ( 1r ` A ) ) )
37 3 1 2 6 7 5 scmatel 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( ( c ( .r ` R ) d ) ( .s ` A ) ( 1r ` A ) ) e. S <-> ( ( ( c ( .r ` R ) d ) ( .s ` A ) ( 1r ` A ) ) e. B /\ E. e e. E ( ( c ( .r ` R ) d ) ( .s ` A ) ( 1r ` A ) ) = ( e ( .s ` A ) ( 1r ` A ) ) ) ) )
38 37 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( d e. E /\ c e. E ) ) -> ( ( ( c ( .r ` R ) d ) ( .s ` A ) ( 1r ` A ) ) e. S <-> ( ( ( c ( .r ` R ) d ) ( .s ` A ) ( 1r ` A ) ) e. B /\ E. e e. E ( ( c ( .r ` R ) d ) ( .s ` A ) ( 1r ` A ) ) = ( e ( .s ` A ) ( 1r ` A ) ) ) ) )
39 31 36 38 mpbir2and 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( d e. E /\ c e. E ) ) -> ( ( c ( .r ` R ) d ) ( .s ` A ) ( 1r ` A ) ) e. S )
40 39 exp32 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( d e. E -> ( c e. E -> ( ( c ( .r ` R ) d ) ( .s ` A ) ( 1r ` A ) ) e. S ) ) )
41 40 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ Y e. B ) -> ( d e. E -> ( c e. E -> ( ( c ( .r ` R ) d ) ( .s ` A ) ( 1r ` A ) ) e. S ) ) )
42 41 imp 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ Y e. B ) /\ d e. E ) -> ( c e. E -> ( ( c ( .r ` R ) d ) ( .s ` A ) ( 1r ` A ) ) e. S ) )
43 42 adantr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ Y e. B ) /\ d e. E ) /\ X e. B ) -> ( c e. E -> ( ( c ( .r ` R ) d ) ( .s ` A ) ( 1r ` A ) ) e. S ) )
44 43 imp 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ Y e. B ) /\ d e. E ) /\ X e. B ) /\ c e. E ) -> ( ( c ( .r ` R ) d ) ( .s ` A ) ( 1r ` A ) ) e. S )
45 18 44 eqeltrd 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ Y e. B ) /\ d e. E ) /\ X e. B ) /\ c e. E ) -> ( ( c ( .s ` A ) ( 1r ` A ) ) ( .r ` A ) ( d ( .s ` A ) ( 1r ` A ) ) ) e. S )
46 45 adantr 
 |-  ( ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ Y e. B ) /\ d e. E ) /\ X e. B ) /\ c e. E ) /\ X = ( c ( .s ` A ) ( 1r ` A ) ) ) -> ( ( c ( .s ` A ) ( 1r ` A ) ) ( .r ` A ) ( d ( .s ` A ) ( 1r ` A ) ) ) e. S )
47 46 adantr 
 |-  ( ( ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ Y e. B ) /\ d e. E ) /\ X e. B ) /\ c e. E ) /\ X = ( c ( .s ` A ) ( 1r ` A ) ) ) /\ Y = ( d ( .s ` A ) ( 1r ` A ) ) ) -> ( ( c ( .s ` A ) ( 1r ` A ) ) ( .r ` A ) ( d ( .s ` A ) ( 1r ` A ) ) ) e. S )
48 11 47 eqeltrd 
 |-  ( ( ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ Y e. B ) /\ d e. E ) /\ X e. B ) /\ c e. E ) /\ X = ( c ( .s ` A ) ( 1r ` A ) ) ) /\ Y = ( d ( .s ` A ) ( 1r ` A ) ) ) -> ( X ( .r ` A ) Y ) e. S )
49 48 exp31 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ Y e. B ) /\ d e. E ) /\ X e. B ) /\ c e. E ) -> ( X = ( c ( .s ` A ) ( 1r ` A ) ) -> ( Y = ( d ( .s ` A ) ( 1r ` A ) ) -> ( X ( .r ` A ) Y ) e. S ) ) )
50 49 rexlimdva 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ Y e. B ) /\ d e. E ) /\ X e. B ) -> ( E. c e. E X = ( c ( .s ` A ) ( 1r ` A ) ) -> ( Y = ( d ( .s ` A ) ( 1r ` A ) ) -> ( X ( .r ` A ) Y ) e. S ) ) )
51 50 expimpd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ Y e. B ) /\ d e. E ) -> ( ( X e. B /\ E. c e. E X = ( c ( .s ` A ) ( 1r ` A ) ) ) -> ( Y = ( d ( .s ` A ) ( 1r ` A ) ) -> ( X ( .r ` A ) Y ) e. S ) ) )
52 51 com23 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ Y e. B ) /\ d e. E ) -> ( Y = ( d ( .s ` A ) ( 1r ` A ) ) -> ( ( X e. B /\ E. c e. E X = ( c ( .s ` A ) ( 1r ` A ) ) ) -> ( X ( .r ` A ) Y ) e. S ) ) )
53 52 rexlimdva 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ Y e. B ) -> ( E. d e. E Y = ( d ( .s ` A ) ( 1r ` A ) ) -> ( ( X e. B /\ E. c e. E X = ( c ( .s ` A ) ( 1r ` A ) ) ) -> ( X ( .r ` A ) Y ) e. S ) ) )
54 53 expimpd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( Y e. B /\ E. d e. E Y = ( d ( .s ` A ) ( 1r ` A ) ) ) -> ( ( X e. B /\ E. c e. E X = ( c ( .s ` A ) ( 1r ` A ) ) ) -> ( X ( .r ` A ) Y ) e. S ) ) )
55 9 54 sylbid 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Y e. S -> ( ( X e. B /\ E. c e. E X = ( c ( .s ` A ) ( 1r ` A ) ) ) -> ( X ( .r ` A ) Y ) e. S ) ) )
56 55 com23 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( X e. B /\ E. c e. E X = ( c ( .s ` A ) ( 1r ` A ) ) ) -> ( Y e. S -> ( X ( .r ` A ) Y ) e. S ) ) )
57 8 56 sylbid 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( X e. S -> ( Y e. S -> ( X ( .r ` A ) Y ) e. S ) ) )
58 57 imp32 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. S /\ Y e. S ) ) -> ( X ( .r ` A ) Y ) e. S )