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 𝐾 = ( Base ‘ 𝑅 )
scmatscm.a 𝐴 = ( 𝑁 Mat 𝑅 )
scmatscm.b 𝐵 = ( Base ‘ 𝐴 )
scmatscm.t = ( ·𝑠𝐴 )
scmatscm.m × = ( .r𝐴 )
scmatscm.c 𝑆 = ( 𝑁 ScMat 𝑅 )
Assertion scmatscm ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) → ∃ 𝑐𝐾𝑚𝐵 ( 𝐶 × 𝑚 ) = ( 𝑐 𝑚 ) )

Proof

Step Hyp Ref Expression
1 scmatscm.k 𝐾 = ( Base ‘ 𝑅 )
2 scmatscm.a 𝐴 = ( 𝑁 Mat 𝑅 )
3 scmatscm.b 𝐵 = ( Base ‘ 𝐴 )
4 scmatscm.t = ( ·𝑠𝐴 )
5 scmatscm.m × = ( .r𝐴 )
6 scmatscm.c 𝑆 = ( 𝑁 ScMat 𝑅 )
7 eqid ( 1r𝐴 ) = ( 1r𝐴 )
8 1 2 3 7 4 6 scmatscmid ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐶𝑆 ) → ∃ 𝑐𝐾 𝐶 = ( 𝑐 ( 1r𝐴 ) ) )
9 8 3expa ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) → ∃ 𝑐𝐾 𝐶 = ( 𝑐 ( 1r𝐴 ) ) )
10 oveq1 ( 𝐶 = ( 𝑐 ( 1r𝐴 ) ) → ( 𝐶 × 𝑚 ) = ( ( 𝑐 ( 1r𝐴 ) ) × 𝑚 ) )
11 simpr ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 ∈ Ring )
12 11 ad4antr ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → 𝑅 ∈ Ring )
13 simpl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
14 13 adantr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
15 2 matring ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
16 3 7 ringidcl ( 𝐴 ∈ Ring → ( 1r𝐴 ) ∈ 𝐵 )
17 15 16 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r𝐴 ) ∈ 𝐵 )
18 17 adantr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) → ( 1r𝐴 ) ∈ 𝐵 )
19 18 anim1ci ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) → ( 𝑐𝐾 ∧ ( 1r𝐴 ) ∈ 𝐵 ) )
20 1 2 3 4 matvscl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑐𝐾 ∧ ( 1r𝐴 ) ∈ 𝐵 ) ) → ( 𝑐 ( 1r𝐴 ) ) ∈ 𝐵 )
21 14 19 20 syl2anc ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) → ( 𝑐 ( 1r𝐴 ) ) ∈ 𝐵 )
22 21 anim1i ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) → ( ( 𝑐 ( 1r𝐴 ) ) ∈ 𝐵𝑚𝐵 ) )
23 22 adantr ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( ( 𝑐 ( 1r𝐴 ) ) ∈ 𝐵𝑚𝐵 ) )
24 simpr ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖𝑁𝑗𝑁 ) )
25 2 3 5 matmulcell ( ( 𝑅 ∈ Ring ∧ ( ( 𝑐 ( 1r𝐴 ) ) ∈ 𝐵𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖 ( ( 𝑐 ( 1r𝐴 ) ) × 𝑚 ) 𝑗 ) = ( 𝑅 Σg ( 𝑘𝑁 ↦ ( ( 𝑖 ( 𝑐 ( 1r𝐴 ) ) 𝑘 ) ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) ) ) )
26 12 23 24 25 syl3anc ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖 ( ( 𝑐 ( 1r𝐴 ) ) × 𝑚 ) 𝑗 ) = ( 𝑅 Σg ( 𝑘𝑁 ↦ ( ( 𝑖 ( 𝑐 ( 1r𝐴 ) ) 𝑘 ) ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) ) ) )
27 13 anim1i ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑐𝐾 ) )
28 df-3an ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑐𝐾 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑐𝐾 ) )
29 27 28 sylibr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑐𝐾 ) )
30 29 ad3antrrr ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑘𝑁 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑐𝐾 ) )
31 eqid ( 0g𝑅 ) = ( 0g𝑅 )
32 2 1 4 31 matsc ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑐𝐾 ) → ( 𝑐 ( 1r𝐴 ) ) = ( 𝑥𝑁 , 𝑦𝑁 ↦ if ( 𝑥 = 𝑦 , 𝑐 , ( 0g𝑅 ) ) ) )
33 30 32 syl ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑘𝑁 ) → ( 𝑐 ( 1r𝐴 ) ) = ( 𝑥𝑁 , 𝑦𝑁 ↦ if ( 𝑥 = 𝑦 , 𝑐 , ( 0g𝑅 ) ) ) )
34 eqeq12 ( ( 𝑥 = 𝑖𝑦 = 𝑘 ) → ( 𝑥 = 𝑦𝑖 = 𝑘 ) )
35 34 ifbid ( ( 𝑥 = 𝑖𝑦 = 𝑘 ) → if ( 𝑥 = 𝑦 , 𝑐 , ( 0g𝑅 ) ) = if ( 𝑖 = 𝑘 , 𝑐 , ( 0g𝑅 ) ) )
36 35 adantl ( ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑘𝑁 ) ∧ ( 𝑥 = 𝑖𝑦 = 𝑘 ) ) → if ( 𝑥 = 𝑦 , 𝑐 , ( 0g𝑅 ) ) = if ( 𝑖 = 𝑘 , 𝑐 , ( 0g𝑅 ) ) )
37 simpl ( ( 𝑖𝑁𝑗𝑁 ) → 𝑖𝑁 )
38 37 adantl ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → 𝑖𝑁 )
39 38 adantr ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑘𝑁 ) → 𝑖𝑁 )
40 simpr ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑘𝑁 ) → 𝑘𝑁 )
41 vex 𝑐 ∈ V
42 fvex ( 0g𝑅 ) ∈ V
43 41 42 ifex if ( 𝑖 = 𝑘 , 𝑐 , ( 0g𝑅 ) ) ∈ V
44 43 a1i ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑘𝑁 ) → if ( 𝑖 = 𝑘 , 𝑐 , ( 0g𝑅 ) ) ∈ V )
45 33 36 39 40 44 ovmpod ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑘𝑁 ) → ( 𝑖 ( 𝑐 ( 1r𝐴 ) ) 𝑘 ) = if ( 𝑖 = 𝑘 , 𝑐 , ( 0g𝑅 ) ) )
46 45 oveq1d ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑘𝑁 ) → ( ( 𝑖 ( 𝑐 ( 1r𝐴 ) ) 𝑘 ) ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) = ( if ( 𝑖 = 𝑘 , 𝑐 , ( 0g𝑅 ) ) ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) )
47 46 mpteq2dva ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑘𝑁 ↦ ( ( 𝑖 ( 𝑐 ( 1r𝐴 ) ) 𝑘 ) ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) ) = ( 𝑘𝑁 ↦ ( if ( 𝑖 = 𝑘 , 𝑐 , ( 0g𝑅 ) ) ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) ) )
48 47 oveq2d ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑅 Σg ( 𝑘𝑁 ↦ ( ( 𝑖 ( 𝑐 ( 1r𝐴 ) ) 𝑘 ) ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) ) ) = ( 𝑅 Σg ( 𝑘𝑁 ↦ ( if ( 𝑖 = 𝑘 , 𝑐 , ( 0g𝑅 ) ) ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) ) ) )
49 ovif ( if ( 𝑖 = 𝑘 , 𝑐 , ( 0g𝑅 ) ) ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) = if ( 𝑖 = 𝑘 , ( 𝑐 ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) , ( ( 0g𝑅 ) ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) )
50 simp-6r ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑘𝑁 ) → 𝑅 ∈ Ring )
51 simplrr ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑘𝑁 ) → 𝑗𝑁 )
52 simpr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) → 𝑚𝐵 )
53 52 ad2antrr ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑘𝑁 ) → 𝑚𝐵 )
54 2 1 3 40 51 53 matecld ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑘𝑁 ) → ( 𝑘 𝑚 𝑗 ) ∈ 𝐾 )
55 eqid ( .r𝑅 ) = ( .r𝑅 )
56 1 55 31 ringlz ( ( 𝑅 ∈ Ring ∧ ( 𝑘 𝑚 𝑗 ) ∈ 𝐾 ) → ( ( 0g𝑅 ) ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) = ( 0g𝑅 ) )
57 50 54 56 syl2anc ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑘𝑁 ) → ( ( 0g𝑅 ) ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) = ( 0g𝑅 ) )
58 57 ifeq2d ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑘𝑁 ) → if ( 𝑖 = 𝑘 , ( 𝑐 ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) , ( ( 0g𝑅 ) ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) ) = if ( 𝑖 = 𝑘 , ( 𝑐 ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) , ( 0g𝑅 ) ) )
59 49 58 eqtrid ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑘𝑁 ) → ( if ( 𝑖 = 𝑘 , 𝑐 , ( 0g𝑅 ) ) ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) = if ( 𝑖 = 𝑘 , ( 𝑐 ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) , ( 0g𝑅 ) ) )
60 59 mpteq2dva ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑘𝑁 ↦ ( if ( 𝑖 = 𝑘 , 𝑐 , ( 0g𝑅 ) ) ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) ) = ( 𝑘𝑁 ↦ if ( 𝑖 = 𝑘 , ( 𝑐 ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) , ( 0g𝑅 ) ) ) )
61 60 oveq2d ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑅 Σg ( 𝑘𝑁 ↦ ( if ( 𝑖 = 𝑘 , 𝑐 , ( 0g𝑅 ) ) ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) ) ) = ( 𝑅 Σg ( 𝑘𝑁 ↦ if ( 𝑖 = 𝑘 , ( 𝑐 ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) , ( 0g𝑅 ) ) ) ) )
62 ringmnd ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
63 62 adantl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 ∈ Mnd )
64 63 ad4antr ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → 𝑅 ∈ Mnd )
65 simpl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑁 ∈ Fin )
66 65 ad4antr ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → 𝑁 ∈ Fin )
67 equcom ( 𝑖 = 𝑘𝑘 = 𝑖 )
68 ifbi ( ( 𝑖 = 𝑘𝑘 = 𝑖 ) → if ( 𝑖 = 𝑘 , ( 𝑐 ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) , ( 0g𝑅 ) ) = if ( 𝑘 = 𝑖 , ( 𝑐 ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) , ( 0g𝑅 ) ) )
69 67 68 ax-mp if ( 𝑖 = 𝑘 , ( 𝑐 ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) , ( 0g𝑅 ) ) = if ( 𝑘 = 𝑖 , ( 𝑐 ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) , ( 0g𝑅 ) )
70 69 mpteq2i ( 𝑘𝑁 ↦ if ( 𝑖 = 𝑘 , ( 𝑐 ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) , ( 0g𝑅 ) ) ) = ( 𝑘𝑁 ↦ if ( 𝑘 = 𝑖 , ( 𝑐 ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) , ( 0g𝑅 ) ) )
71 1 eleq2i ( 𝑐𝐾𝑐 ∈ ( Base ‘ 𝑅 ) )
72 71 biimpi ( 𝑐𝐾𝑐 ∈ ( Base ‘ 𝑅 ) )
73 72 adantl ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) → 𝑐 ∈ ( Base ‘ 𝑅 ) )
74 73 ad3antrrr ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑘𝑁 ) → 𝑐 ∈ ( Base ‘ 𝑅 ) )
75 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
76 2 75 3 40 51 53 matecld ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑘𝑁 ) → ( 𝑘 𝑚 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
77 75 55 ringcl ( ( 𝑅 ∈ Ring ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 𝑚 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝑐 ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) ∈ ( Base ‘ 𝑅 ) )
78 50 74 76 77 syl3anc ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑘𝑁 ) → ( 𝑐 ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) ∈ ( Base ‘ 𝑅 ) )
79 78 ralrimiva ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ∀ 𝑘𝑁 ( 𝑐 ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) ∈ ( Base ‘ 𝑅 ) )
80 31 64 66 38 70 79 gsummpt1n0 ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑅 Σg ( 𝑘𝑁 ↦ if ( 𝑖 = 𝑘 , ( 𝑐 ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) , ( 0g𝑅 ) ) ) ) = 𝑖 / 𝑘 ( 𝑐 ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) )
81 48 61 80 3eqtrd ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑅 Σg ( 𝑘𝑁 ↦ ( ( 𝑖 ( 𝑐 ( 1r𝐴 ) ) 𝑘 ) ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) ) ) = 𝑖 / 𝑘 ( 𝑐 ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) )
82 csbov2g ( 𝑖𝑁 𝑖 / 𝑘 ( 𝑐 ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) = ( 𝑐 ( .r𝑅 ) 𝑖 / 𝑘 ( 𝑘 𝑚 𝑗 ) ) )
83 csbov1g ( 𝑖𝑁 𝑖 / 𝑘 ( 𝑘 𝑚 𝑗 ) = ( 𝑖 / 𝑘 𝑘 𝑚 𝑗 ) )
84 csbvarg ( 𝑖𝑁 𝑖 / 𝑘 𝑘 = 𝑖 )
85 84 oveq1d ( 𝑖𝑁 → ( 𝑖 / 𝑘 𝑘 𝑚 𝑗 ) = ( 𝑖 𝑚 𝑗 ) )
86 83 85 eqtrd ( 𝑖𝑁 𝑖 / 𝑘 ( 𝑘 𝑚 𝑗 ) = ( 𝑖 𝑚 𝑗 ) )
87 86 oveq2d ( 𝑖𝑁 → ( 𝑐 ( .r𝑅 ) 𝑖 / 𝑘 ( 𝑘 𝑚 𝑗 ) ) = ( 𝑐 ( .r𝑅 ) ( 𝑖 𝑚 𝑗 ) ) )
88 82 87 eqtrd ( 𝑖𝑁 𝑖 / 𝑘 ( 𝑐 ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) = ( 𝑐 ( .r𝑅 ) ( 𝑖 𝑚 𝑗 ) ) )
89 88 adantr ( ( 𝑖𝑁𝑗𝑁 ) → 𝑖 / 𝑘 ( 𝑐 ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) = ( 𝑐 ( .r𝑅 ) ( 𝑖 𝑚 𝑗 ) ) )
90 89 adantl ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → 𝑖 / 𝑘 ( 𝑐 ( .r𝑅 ) ( 𝑘 𝑚 𝑗 ) ) = ( 𝑐 ( .r𝑅 ) ( 𝑖 𝑚 𝑗 ) ) )
91 26 81 90 3eqtrd ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖 ( ( 𝑐 ( 1r𝐴 ) ) × 𝑚 ) 𝑗 ) = ( 𝑐 ( .r𝑅 ) ( 𝑖 𝑚 𝑗 ) ) )
92 simpr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) → 𝑐𝐾 )
93 92 anim1i ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) → ( 𝑐𝐾𝑚𝐵 ) )
94 93 adantr ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑐𝐾𝑚𝐵 ) )
95 2 3 1 4 55 matvscacell ( ( 𝑅 ∈ Ring ∧ ( 𝑐𝐾𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖 ( 𝑐 𝑚 ) 𝑗 ) = ( 𝑐 ( .r𝑅 ) ( 𝑖 𝑚 𝑗 ) ) )
96 12 94 24 95 syl3anc ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖 ( 𝑐 𝑚 ) 𝑗 ) = ( 𝑐 ( .r𝑅 ) ( 𝑖 𝑚 𝑗 ) ) )
97 91 96 eqtr4d ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖 ( ( 𝑐 ( 1r𝐴 ) ) × 𝑚 ) 𝑗 ) = ( 𝑖 ( 𝑐 𝑚 ) 𝑗 ) )
98 97 ralrimivva ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) → ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 ( ( 𝑐 ( 1r𝐴 ) ) × 𝑚 ) 𝑗 ) = ( 𝑖 ( 𝑐 𝑚 ) 𝑗 ) )
99 15 ad3antrrr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) → 𝐴 ∈ Ring )
100 21 adantr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) → ( 𝑐 ( 1r𝐴 ) ) ∈ 𝐵 )
101 3 5 ringcl ( ( 𝐴 ∈ Ring ∧ ( 𝑐 ( 1r𝐴 ) ) ∈ 𝐵𝑚𝐵 ) → ( ( 𝑐 ( 1r𝐴 ) ) × 𝑚 ) ∈ 𝐵 )
102 99 100 52 101 syl3anc ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) → ( ( 𝑐 ( 1r𝐴 ) ) × 𝑚 ) ∈ 𝐵 )
103 13 ad2antrr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
104 1 2 3 4 matvscl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑐𝐾𝑚𝐵 ) ) → ( 𝑐 𝑚 ) ∈ 𝐵 )
105 103 93 104 syl2anc ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) → ( 𝑐 𝑚 ) ∈ 𝐵 )
106 2 3 eqmat ( ( ( ( 𝑐 ( 1r𝐴 ) ) × 𝑚 ) ∈ 𝐵 ∧ ( 𝑐 𝑚 ) ∈ 𝐵 ) → ( ( ( 𝑐 ( 1r𝐴 ) ) × 𝑚 ) = ( 𝑐 𝑚 ) ↔ ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 ( ( 𝑐 ( 1r𝐴 ) ) × 𝑚 ) 𝑗 ) = ( 𝑖 ( 𝑐 𝑚 ) 𝑗 ) ) )
107 102 105 106 syl2anc ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) → ( ( ( 𝑐 ( 1r𝐴 ) ) × 𝑚 ) = ( 𝑐 𝑚 ) ↔ ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 ( ( 𝑐 ( 1r𝐴 ) ) × 𝑚 ) 𝑗 ) = ( 𝑖 ( 𝑐 𝑚 ) 𝑗 ) ) )
108 98 107 mpbird ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) → ( ( 𝑐 ( 1r𝐴 ) ) × 𝑚 ) = ( 𝑐 𝑚 ) )
109 10 108 sylan9eqr ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) ∧ 𝐶 = ( 𝑐 ( 1r𝐴 ) ) ) → ( 𝐶 × 𝑚 ) = ( 𝑐 𝑚 ) )
110 109 ex ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) ∧ 𝑚𝐵 ) → ( 𝐶 = ( 𝑐 ( 1r𝐴 ) ) → ( 𝐶 × 𝑚 ) = ( 𝑐 𝑚 ) ) )
111 110 ralrimdva ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) ∧ 𝑐𝐾 ) → ( 𝐶 = ( 𝑐 ( 1r𝐴 ) ) → ∀ 𝑚𝐵 ( 𝐶 × 𝑚 ) = ( 𝑐 𝑚 ) ) )
112 111 reximdva ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) → ( ∃ 𝑐𝐾 𝐶 = ( 𝑐 ( 1r𝐴 ) ) → ∃ 𝑐𝐾𝑚𝐵 ( 𝐶 × 𝑚 ) = ( 𝑐 𝑚 ) ) )
113 9 112 mpd ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶𝑆 ) → ∃ 𝑐𝐾𝑚𝐵 ( 𝐶 × 𝑚 ) = ( 𝑐 𝑚 ) )