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