Metamath Proof Explorer

Theorem scmatscm

Description: The multiplication of a matrix with a scalar matrix corresponds to a scalar multiplication. (Contributed by AV, 28-Dec-2019)

Ref Expression
Hypotheses scmatscm.k 
|- K = ( Base ` R )
scmatscm.a 
|- A = ( N Mat R )
scmatscm.b 
|- B = ( Base ` A )
scmatscm.t 
|- .* = ( .s ` A )
scmatscm.m 
|- .X. = ( .r ` A )
scmatscm.c 
|- S = ( N ScMat R )
Assertion scmatscm 
|- ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) -> E. c e. K A. m e. B ( C .X. m ) = ( c .* m ) )

Proof

Step Hyp Ref Expression
1 scmatscm.k 
 |-  K = ( Base ` R )
2 scmatscm.a 
 |-  A = ( N Mat R )
3 scmatscm.b 
 |-  B = ( Base ` A )
4 scmatscm.t 
 |-  .* = ( .s ` A )
5 scmatscm.m 
 |-  .X. = ( .r ` A )
6 scmatscm.c 
 |-  S = ( N ScMat R )
7 eqid 
 |-  ( 1r ` A ) = ( 1r ` A )
8 1 2 3 7 4 6 scmatscmid 
 |-  ( ( N e. Fin /\ R e. Ring /\ C e. S ) -> E. c e. K C = ( c .* ( 1r ` A ) ) )
9 8 3expa 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) -> E. c e. K C = ( c .* ( 1r ` A ) ) )
10 oveq1 
 |-  ( C = ( c .* ( 1r ` A ) ) -> ( C .X. m ) = ( ( c .* ( 1r ` A ) ) .X. m ) )
11 simpr 
 |-  ( ( N e. Fin /\ R e. Ring ) -> R e. Ring )
12 11 ad4antr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) -> R e. Ring )
13 simpl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) -> ( N e. Fin /\ R e. Ring ) )
14 13 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) -> ( N e. Fin /\ R e. Ring ) )
15 2 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
16 3 7 ringidcl 
 |-  ( A e. Ring -> ( 1r ` A ) e. B )
17 15 16 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) e. B )
18 17 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) -> ( 1r ` A ) e. B )
19 18 anim1ci 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) -> ( c e. K /\ ( 1r ` A ) e. B ) )
20 1 2 3 4 matvscl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( c e. K /\ ( 1r ` A ) e. B ) ) -> ( c .* ( 1r ` A ) ) e. B )
21 14 19 20 syl2anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) -> ( c .* ( 1r ` A ) ) e. B )
22 21 anim1i 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) -> ( ( c .* ( 1r ` A ) ) e. B /\ m e. B ) )
23 22 adantr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) -> ( ( c .* ( 1r ` A ) ) e. B /\ m e. B ) )
24 simpr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) -> ( i e. N /\ j e. N ) )
25 2 3 5 matmulcell 
 |-  ( ( R e. Ring /\ ( ( c .* ( 1r ` A ) ) e. B /\ m e. B ) /\ ( i e. N /\ j e. N ) ) -> ( i ( ( c .* ( 1r ` A ) ) .X. m ) j ) = ( R gsum ( k e. N |-> ( ( i ( c .* ( 1r ` A ) ) k ) ( .r ` R ) ( k m j ) ) ) ) )
26 12 23 24 25 syl3anc 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) -> ( i ( ( c .* ( 1r ` A ) ) .X. m ) j ) = ( R gsum ( k e. N |-> ( ( i ( c .* ( 1r ` A ) ) k ) ( .r ` R ) ( k m j ) ) ) ) )
27 13 anim1i 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) -> ( ( N e. Fin /\ R e. Ring ) /\ c e. K ) )
28 df-3an 
 |-  ( ( N e. Fin /\ R e. Ring /\ c e. K ) <-> ( ( N e. Fin /\ R e. Ring ) /\ c e. K ) )
29 27 28 sylibr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) -> ( N e. Fin /\ R e. Ring /\ c e. K ) )
30 29 ad3antrrr 
 |-  ( ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) /\ k e. N ) -> ( N e. Fin /\ R e. Ring /\ c e. K ) )
31 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
32 2 1 4 31 matsc 
 |-  ( ( N e. Fin /\ R e. Ring /\ c e. K ) -> ( c .* ( 1r ` A ) ) = ( x e. N , y e. N |-> if ( x = y , c , ( 0g ` R ) ) ) )
33 30 32 syl 
 |-  ( ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) /\ k e. N ) -> ( c .* ( 1r ` A ) ) = ( x e. N , y e. N |-> if ( x = y , c , ( 0g ` R ) ) ) )
34 eqeq12 
 |-  ( ( x = i /\ y = k ) -> ( x = y <-> i = k ) )
35 34 ifbid 
 |-  ( ( x = i /\ y = k ) -> if ( x = y , c , ( 0g ` R ) ) = if ( i = k , c , ( 0g ` R ) ) )
36 35 adantl 
 |-  ( ( ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) /\ k e. N ) /\ ( x = i /\ y = k ) ) -> if ( x = y , c , ( 0g ` R ) ) = if ( i = k , c , ( 0g ` R ) ) )
37 simpl 
 |-  ( ( i e. N /\ j e. N ) -> i e. N )
38 37 adantl 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) -> i e. N )
39 38 adantr 
 |-  ( ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) /\ k e. N ) -> i e. N )
40 simpr 
 |-  ( ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) /\ k e. N ) -> k e. N )
41 vex 
 |-  c e. _V
42 fvex 
 |-  ( 0g ` R ) e. _V
43 41 42 ifex 
 |-  if ( i = k , c , ( 0g ` R ) ) e. _V
44 43 a1i 
 |-  ( ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) /\ k e. N ) -> if ( i = k , c , ( 0g ` R ) ) e. _V )
45 33 36 39 40 44 ovmpod 
 |-  ( ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) /\ k e. N ) -> ( i ( c .* ( 1r ` A ) ) k ) = if ( i = k , c , ( 0g ` R ) ) )
46 45 oveq1d 
 |-  ( ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) /\ k e. N ) -> ( ( i ( c .* ( 1r ` A ) ) k ) ( .r ` R ) ( k m j ) ) = ( if ( i = k , c , ( 0g ` R ) ) ( .r ` R ) ( k m j ) ) )
47 46 mpteq2dva 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) -> ( k e. N |-> ( ( i ( c .* ( 1r ` A ) ) k ) ( .r ` R ) ( k m j ) ) ) = ( k e. N |-> ( if ( i = k , c , ( 0g ` R ) ) ( .r ` R ) ( k m j ) ) ) )
48 47 oveq2d 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) -> ( R gsum ( k e. N |-> ( ( i ( c .* ( 1r ` A ) ) k ) ( .r ` R ) ( k m j ) ) ) ) = ( R gsum ( k e. N |-> ( if ( i = k , c , ( 0g ` R ) ) ( .r ` R ) ( k m j ) ) ) ) )
49 ovif 
 |-  ( if ( i = k , c , ( 0g ` R ) ) ( .r ` R ) ( k m j ) ) = if ( i = k , ( c ( .r ` R ) ( k m j ) ) , ( ( 0g ` R ) ( .r ` R ) ( k m j ) ) )
50 simp-6r 
 |-  ( ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) /\ k e. N ) -> R e. Ring )
51 simplrr 
 |-  ( ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) /\ k e. N ) -> j e. N )
52 simpr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) -> m e. B )
53 52 ad2antrr 
 |-  ( ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) /\ k e. N ) -> m e. B )
54 2 1 3 40 51 53 matecld 
 |-  ( ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) /\ k e. N ) -> ( k m j ) e. K )
55 eqid 
 |-  ( .r ` R ) = ( .r ` R )
56 1 55 31 ringlz 
 |-  ( ( R e. Ring /\ ( k m j ) e. K ) -> ( ( 0g ` R ) ( .r ` R ) ( k m j ) ) = ( 0g ` R ) )
57 50 54 56 syl2anc 
 |-  ( ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) /\ k e. N ) -> ( ( 0g ` R ) ( .r ` R ) ( k m j ) ) = ( 0g ` R ) )
58 57 ifeq2d 
 |-  ( ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) /\ k e. N ) -> if ( i = k , ( c ( .r ` R ) ( k m j ) ) , ( ( 0g ` R ) ( .r ` R ) ( k m j ) ) ) = if ( i = k , ( c ( .r ` R ) ( k m j ) ) , ( 0g ` R ) ) )
59 49 58 eqtrid 
 |-  ( ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) /\ k e. N ) -> ( if ( i = k , c , ( 0g ` R ) ) ( .r ` R ) ( k m j ) ) = if ( i = k , ( c ( .r ` R ) ( k m j ) ) , ( 0g ` R ) ) )
60 59 mpteq2dva 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) -> ( k e. N |-> ( if ( i = k , c , ( 0g ` R ) ) ( .r ` R ) ( k m j ) ) ) = ( k e. N |-> if ( i = k , ( c ( .r ` R ) ( k m j ) ) , ( 0g ` R ) ) ) )
61 60 oveq2d 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) -> ( R gsum ( k e. N |-> ( if ( i = k , c , ( 0g ` R ) ) ( .r ` R ) ( k m j ) ) ) ) = ( R gsum ( k e. N |-> if ( i = k , ( c ( .r ` R ) ( k m j ) ) , ( 0g ` R ) ) ) ) )
62 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
63 62 adantl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> R e. Mnd )
64 63 ad4antr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) -> R e. Mnd )
65 simpl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> N e. Fin )
66 65 ad4antr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) -> N e. Fin )
67 equcom 
 |-  ( i = k <-> k = i )
68 ifbi 
 |-  ( ( i = k <-> k = i ) -> if ( i = k , ( c ( .r ` R ) ( k m j ) ) , ( 0g ` R ) ) = if ( k = i , ( c ( .r ` R ) ( k m j ) ) , ( 0g ` R ) ) )
69 67 68 ax-mp 
 |-  if ( i = k , ( c ( .r ` R ) ( k m j ) ) , ( 0g ` R ) ) = if ( k = i , ( c ( .r ` R ) ( k m j ) ) , ( 0g ` R ) )
70 69 mpteq2i 
 |-  ( k e. N |-> if ( i = k , ( c ( .r ` R ) ( k m j ) ) , ( 0g ` R ) ) ) = ( k e. N |-> if ( k = i , ( c ( .r ` R ) ( k m j ) ) , ( 0g ` R ) ) )
71 1 eleq2i 
 |-  ( c e. K <-> c e. ( Base ` R ) )
72 71 biimpi 
 |-  ( c e. K -> c e. ( Base ` R ) )
73 72 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) -> c e. ( Base ` R ) )
74 73 ad3antrrr 
 |-  ( ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) /\ k e. N ) -> c e. ( Base ` R ) )
75 eqid 
 |-  ( Base ` R ) = ( Base ` R )
76 2 75 3 40 51 53 matecld 
 |-  ( ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) /\ k e. N ) -> ( k m j ) e. ( Base ` R ) )
77 75 55 ringcl 
 |-  ( ( R e. Ring /\ c e. ( Base ` R ) /\ ( k m j ) e. ( Base ` R ) ) -> ( c ( .r ` R ) ( k m j ) ) e. ( Base ` R ) )
78 50 74 76 77 syl3anc 
 |-  ( ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) /\ k e. N ) -> ( c ( .r ` R ) ( k m j ) ) e. ( Base ` R ) )
79 78 ralrimiva 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) -> A. k e. N ( c ( .r ` R ) ( k m j ) ) e. ( Base ` R ) )
80 31 64 66 38 70 79 gsummpt1n0 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) -> ( R gsum ( k e. N |-> if ( i = k , ( c ( .r ` R ) ( k m j ) ) , ( 0g ` R ) ) ) ) = [_ i / k ]_ ( c ( .r ` R ) ( k m j ) ) )
81 48 61 80 3eqtrd 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) -> ( R gsum ( k e. N |-> ( ( i ( c .* ( 1r ` A ) ) k ) ( .r ` R ) ( k m j ) ) ) ) = [_ i / k ]_ ( c ( .r ` R ) ( k m j ) ) )
82 csbov2g 
 |-  ( i e. N -> [_ i / k ]_ ( c ( .r ` R ) ( k m j ) ) = ( c ( .r ` R ) [_ i / k ]_ ( k m j ) ) )
83 csbov1g 
 |-  ( i e. N -> [_ i / k ]_ ( k m j ) = ( [_ i / k ]_ k m j ) )
84 csbvarg 
 |-  ( i e. N -> [_ i / k ]_ k = i )
85 84 oveq1d 
 |-  ( i e. N -> ( [_ i / k ]_ k m j ) = ( i m j ) )
86 83 85 eqtrd 
 |-  ( i e. N -> [_ i / k ]_ ( k m j ) = ( i m j ) )
87 86 oveq2d 
 |-  ( i e. N -> ( c ( .r ` R ) [_ i / k ]_ ( k m j ) ) = ( c ( .r ` R ) ( i m j ) ) )
88 82 87 eqtrd 
 |-  ( i e. N -> [_ i / k ]_ ( c ( .r ` R ) ( k m j ) ) = ( c ( .r ` R ) ( i m j ) ) )
89 88 adantr 
 |-  ( ( i e. N /\ j e. N ) -> [_ i / k ]_ ( c ( .r ` R ) ( k m j ) ) = ( c ( .r ` R ) ( i m j ) ) )
90 89 adantl 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) -> [_ i / k ]_ ( c ( .r ` R ) ( k m j ) ) = ( c ( .r ` R ) ( i m j ) ) )
91 26 81 90 3eqtrd 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) -> ( i ( ( c .* ( 1r ` A ) ) .X. m ) j ) = ( c ( .r ` R ) ( i m j ) ) )
92 simpr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) -> c e. K )
93 92 anim1i 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) -> ( c e. K /\ m e. B ) )
94 93 adantr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) -> ( c e. K /\ m e. B ) )
95 2 3 1 4 55 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 ) ) )
96 12 94 24 95 syl3anc 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) -> ( i ( c .* m ) j ) = ( c ( .r ` R ) ( i m j ) ) )
97 91 96 eqtr4d 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ ( i e. N /\ j e. N ) ) -> ( i ( ( c .* ( 1r ` A ) ) .X. m ) j ) = ( i ( c .* m ) j ) )
98 97 ralrimivva 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) -> A. i e. N A. j e. N ( i ( ( c .* ( 1r ` A ) ) .X. m ) j ) = ( i ( c .* m ) j ) )
99 15 ad3antrrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) -> A e. Ring )
100 21 adantr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) -> ( c .* ( 1r ` A ) ) e. B )
101 3 5 ringcl 
 |-  ( ( A e. Ring /\ ( c .* ( 1r ` A ) ) e. B /\ m e. B ) -> ( ( c .* ( 1r ` A ) ) .X. m ) e. B )
102 99 100 52 101 syl3anc 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) -> ( ( c .* ( 1r ` A ) ) .X. m ) e. B )
103 13 ad2antrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) -> ( N e. Fin /\ R e. Ring ) )
104 1 2 3 4 matvscl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( c e. K /\ m e. B ) ) -> ( c .* m ) e. B )
105 103 93 104 syl2anc 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) -> ( c .* m ) e. B )
106 2 3 eqmat 
 |-  ( ( ( ( c .* ( 1r ` A ) ) .X. m ) e. B /\ ( c .* m ) e. B ) -> ( ( ( c .* ( 1r ` A ) ) .X. m ) = ( c .* m ) <-> A. i e. N A. j e. N ( i ( ( c .* ( 1r ` A ) ) .X. m ) j ) = ( i ( c .* m ) j ) ) )
107 102 105 106 syl2anc 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) -> ( ( ( c .* ( 1r ` A ) ) .X. m ) = ( c .* m ) <-> A. i e. N A. j e. N ( i ( ( c .* ( 1r ` A ) ) .X. m ) j ) = ( i ( c .* m ) j ) ) )
108 98 107 mpbird 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) -> ( ( c .* ( 1r ` A ) ) .X. m ) = ( c .* m ) )
109 10 108 sylan9eqr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) /\ C = ( c .* ( 1r ` A ) ) ) -> ( C .X. m ) = ( c .* m ) )
110 109 ex 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) /\ m e. B ) -> ( C = ( c .* ( 1r ` A ) ) -> ( C .X. m ) = ( c .* m ) ) )
111 110 ralrimdva 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) /\ c e. K ) -> ( C = ( c .* ( 1r ` A ) ) -> A. m e. B ( C .X. m ) = ( c .* m ) ) )
112 111 reximdva 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) -> ( E. c e. K C = ( c .* ( 1r ` A ) ) -> E. c e. K A. m e. B ( C .X. m ) = ( c .* m ) ) )
113 9 112 mpd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) -> E. c e. K A. m e. B ( C .X. m ) = ( c .* m ) )