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 syl5eq ⊢ ( ( ( ( ( ( ( 𝑁 ∈ 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 ) ∧ 𝐶 ∈ 𝑆 ) → ∃ 𝑐 ∈ 𝐾 ∀ 𝑚 ∈ 𝐵 ( 𝐶 × 𝑚 ) = ( 𝑐 ∗ 𝑚 ) )