Metamath Proof Explorer

Theorem dmatscmcl

Description: The multiplication of a diagonal matrix with a scalar is a diagonal matrix. (Contributed by AV, 19-Dec-2019)

Ref Expression
Hypotheses dmatscmcl.k 
|- K = ( Base ` R )
dmatscmcl.a 
|- A = ( N Mat R )
dmatscmcl.b 
|- B = ( Base ` A )
dmatscmcl.s 
|- .* = ( .s ` A )
dmatscmcl.d 
|- D = ( N DMat R )
Assertion dmatscmcl 
|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( C e. K /\ M e. D ) ) -> ( C .* M ) e. D )

Proof

Step Hyp Ref Expression
1 dmatscmcl.k 
 |-  K = ( Base ` R )
2 dmatscmcl.a 
 |-  A = ( N Mat R )
3 dmatscmcl.b 
 |-  B = ( Base ` A )
4 dmatscmcl.s 
 |-  .* = ( .s ` A )
5 dmatscmcl.d 
 |-  D = ( N DMat R )
6 simprl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( C e. K /\ M e. D ) ) -> C e. K )
7 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
8 2 3 7 5 dmatmat 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( M e. D -> M e. B ) )
9 8 com12 
 |-  ( M e. D -> ( ( N e. Fin /\ R e. Ring ) -> M e. B ) )
10 9 adantl 
 |-  ( ( C e. K /\ M e. D ) -> ( ( N e. Fin /\ R e. Ring ) -> M e. B ) )
11 10 impcom 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( C e. K /\ M e. D ) ) -> M e. B )
12 6 11 jca 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( C e. K /\ M e. D ) ) -> ( C e. K /\ M e. B ) )
13 1 2 3 4 matvscl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( C e. K /\ M e. B ) ) -> ( C .* M ) e. B )
14 12 13 syldan 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( C e. K /\ M e. D ) ) -> ( C .* M ) e. B )
15 2 3 7 5 dmatel 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( M e. D <-> ( M e. B /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = ( 0g ` R ) ) ) ) )
16 15 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) -> ( M e. D <-> ( M e. B /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = ( 0g ` R ) ) ) ) )
17 simp-4r 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ M e. B ) /\ ( i e. N /\ j e. N ) ) -> R e. Ring )
18 simpr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) -> C e. K )
19 18 anim1i 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ M e. B ) -> ( C e. K /\ M e. B ) )
20 19 adantr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ M e. B ) /\ ( i e. N /\ j e. N ) ) -> ( C e. K /\ M e. B ) )
21 simpr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ M e. B ) /\ ( i e. N /\ j e. N ) ) -> ( i e. N /\ j e. N ) )
22 17 20 21 3jca 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ M e. B ) /\ ( i e. N /\ j e. N ) ) -> ( R e. Ring /\ ( C e. K /\ M e. B ) /\ ( i e. N /\ j e. N ) ) )
23 22 adantr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ M e. B ) /\ ( i e. N /\ j e. N ) ) /\ ( i M j ) = ( 0g ` R ) ) -> ( R e. Ring /\ ( C e. K /\ M e. B ) /\ ( i e. N /\ j e. N ) ) )
24 eqid 
 |-  ( .r ` R ) = ( .r ` R )
25 2 3 1 4 24 matvscacell 
 |-  ( ( R e. Ring /\ ( C e. K /\ M e. B ) /\ ( i e. N /\ j e. N ) ) -> ( i ( C .* M ) j ) = ( C ( .r ` R ) ( i M j ) ) )
26 23 25 syl 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ M e. B ) /\ ( i e. N /\ j e. N ) ) /\ ( i M j ) = ( 0g ` R ) ) -> ( i ( C .* M ) j ) = ( C ( .r ` R ) ( i M j ) ) )
27 oveq2 
 |-  ( ( i M j ) = ( 0g ` R ) -> ( C ( .r ` R ) ( i M j ) ) = ( C ( .r ` R ) ( 0g ` R ) ) )
28 27 adantl 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ M e. B ) /\ ( i e. N /\ j e. N ) ) /\ ( i M j ) = ( 0g ` R ) ) -> ( C ( .r ` R ) ( i M j ) ) = ( C ( .r ` R ) ( 0g ` R ) ) )
29 1 24 7 ringrz 
 |-  ( ( R e. Ring /\ C e. K ) -> ( C ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
30 29 ad5ant23 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ M e. B ) /\ ( i e. N /\ j e. N ) ) -> ( C ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
31 30 adantr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ M e. B ) /\ ( i e. N /\ j e. N ) ) /\ ( i M j ) = ( 0g ` R ) ) -> ( C ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
32 26 28 31 3eqtrd 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ M e. B ) /\ ( i e. N /\ j e. N ) ) /\ ( i M j ) = ( 0g ` R ) ) -> ( i ( C .* M ) j ) = ( 0g ` R ) )
33 32 ex 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ M e. B ) /\ ( i e. N /\ j e. N ) ) -> ( ( i M j ) = ( 0g ` R ) -> ( i ( C .* M ) j ) = ( 0g ` R ) ) )
34 33 imim2d 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ M e. B ) /\ ( i e. N /\ j e. N ) ) -> ( ( i =/= j -> ( i M j ) = ( 0g ` R ) ) -> ( i =/= j -> ( i ( C .* M ) j ) = ( 0g ` R ) ) ) )
35 34 ralimdvva 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ M e. B ) -> ( A. i e. N A. j e. N ( i =/= j -> ( i M j ) = ( 0g ` R ) ) -> A. i e. N A. j e. N ( i =/= j -> ( i ( C .* M ) j ) = ( 0g ` R ) ) ) )
36 35 expimpd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) -> ( ( M e. B /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = ( 0g ` R ) ) ) -> A. i e. N A. j e. N ( i =/= j -> ( i ( C .* M ) j ) = ( 0g ` R ) ) ) )
37 16 36 sylbid 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) -> ( M e. D -> A. i e. N A. j e. N ( i =/= j -> ( i ( C .* M ) j ) = ( 0g ` R ) ) ) )
38 37 impr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( C e. K /\ M e. D ) ) -> A. i e. N A. j e. N ( i =/= j -> ( i ( C .* M ) j ) = ( 0g ` R ) ) )
39 2 3 7 5 dmatel 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( C .* M ) e. D <-> ( ( C .* M ) e. B /\ A. i e. N A. j e. N ( i =/= j -> ( i ( C .* M ) j ) = ( 0g ` R ) ) ) ) )
40 39 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( C e. K /\ M e. D ) ) -> ( ( C .* M ) e. D <-> ( ( C .* M ) e. B /\ A. i e. N A. j e. N ( i =/= j -> ( i ( C .* M ) j ) = ( 0g ` R ) ) ) ) )
41 14 38 40 mpbir2and 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( C e. K /\ M e. D ) ) -> ( C .* M ) e. D )