Theorem scmatscmiddistr

Description: Distributive law for scalar and ring multiplication for scalar matrices expressed as multiplications of a scalar with the identity matrix. (Contributed by AV, 19-Dec-2019)

	Ref	Expression
Hypotheses	scmatscmide.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	scmatscmide.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	scmatscmide.0	⊢ 0 = ( 0g ‘ 𝑅 )
	scmatscmide.1	⊢ 1 = ( 1r ‘ 𝐴 )
	scmatscmide.m	⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
	scmatscmiddistr.t	⊢ · = ( .r ‘ 𝑅 )
	scmatscmiddistr.m	⊢ × = ( .r ‘ 𝐴 )
Assertion	scmatscmiddistr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → ( ( 𝑆 ∗ 1 ) × ( 𝑇 ∗ 1 ) ) = ( ( 𝑆 · 𝑇 ) ∗ 1 ) )

Proof

Step	Hyp	Ref	Expression
1		scmatscmide.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		scmatscmide.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		scmatscmide.0	⊢ 0 = ( 0g ‘ 𝑅 )
4		scmatscmide.1	⊢ 1 = ( 1r ‘ 𝐴 )
5		scmatscmide.m	⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
6		scmatscmiddistr.t	⊢ · = ( .r ‘ 𝑅 )
7		scmatscmiddistr.m	⊢ × = ( .r ‘ 𝐴 )
8		simprl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → 𝑆 ∈ 𝐵 )
9		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
10		eqid	⊢ ( 𝑁 DMat 𝑅 ) = ( 𝑁 DMat 𝑅 )
11	1 9 3 10	dmatid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐴 ) ∈ ( 𝑁 DMat 𝑅 ) )
12	4 11	eqeltrid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 1 ∈ ( 𝑁 DMat 𝑅 ) )
13	12	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → 1 ∈ ( 𝑁 DMat 𝑅 ) )
14	8 13	jca	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → ( 𝑆 ∈ 𝐵 ∧ 1 ∈ ( 𝑁 DMat 𝑅 ) ) )
15	2 1 9 5 10	dmatscmcl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 1 ∈ ( 𝑁 DMat 𝑅 ) ) ) → ( 𝑆 ∗ 1 ) ∈ ( 𝑁 DMat 𝑅 ) )
16	14 15	syldan	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → ( 𝑆 ∗ 1 ) ∈ ( 𝑁 DMat 𝑅 ) )
17		simprr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → 𝑇 ∈ 𝐵 )
18	17 13	jca	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → ( 𝑇 ∈ 𝐵 ∧ 1 ∈ ( 𝑁 DMat 𝑅 ) ) )
19	2 1 9 5 10	dmatscmcl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑇 ∈ 𝐵 ∧ 1 ∈ ( 𝑁 DMat 𝑅 ) ) ) → ( 𝑇 ∗ 1 ) ∈ ( 𝑁 DMat 𝑅 ) )
20	18 19	syldan	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → ( 𝑇 ∗ 1 ) ∈ ( 𝑁 DMat 𝑅 ) )
21	16 20	jca	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → ( ( 𝑆 ∗ 1 ) ∈ ( 𝑁 DMat 𝑅 ) ∧ ( 𝑇 ∗ 1 ) ∈ ( 𝑁 DMat 𝑅 ) ) )
22	7	oveqi	⊢ ( ( 𝑆 ∗ 1 ) × ( 𝑇 ∗ 1 ) ) = ( ( 𝑆 ∗ 1 ) ( .r ‘ 𝐴 ) ( 𝑇 ∗ 1 ) )
23	1 9 3 10	dmatmul	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( ( 𝑆 ∗ 1 ) ∈ ( 𝑁 DMat 𝑅 ) ∧ ( 𝑇 ∗ 1 ) ∈ ( 𝑁 DMat 𝑅 ) ) ) → ( ( 𝑆 ∗ 1 ) ( .r ‘ 𝐴 ) ( 𝑇 ∗ 1 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( ( 𝑖 ( 𝑆 ∗ 1 ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑖 ( 𝑇 ∗ 1 ) 𝑗 ) ) , 0 ) ) )
24	22 23	eqtrid	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( ( 𝑆 ∗ 1 ) ∈ ( 𝑁 DMat 𝑅 ) ∧ ( 𝑇 ∗ 1 ) ∈ ( 𝑁 DMat 𝑅 ) ) ) → ( ( 𝑆 ∗ 1 ) × ( 𝑇 ∗ 1 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( ( 𝑖 ( 𝑆 ∗ 1 ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑖 ( 𝑇 ∗ 1 ) 𝑗 ) ) , 0 ) ) )
25	21 24	syldan	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → ( ( 𝑆 ∗ 1 ) × ( 𝑇 ∗ 1 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( ( 𝑖 ( 𝑆 ∗ 1 ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑖 ( 𝑇 ∗ 1 ) 𝑗 ) ) , 0 ) ) )
26		simpll	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → 𝑁 ∈ Fin )
27		simplr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → 𝑅 ∈ Ring )
28	26 27 8	3jca	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐵 ) )
29	28	3ad2ant1	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐵 ) )
30		3simpc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) )
31	1 2 3 4 5	scmatscmide	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑆 ∗ 1 ) 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑆 , 0 ) )
32	29 30 31	syl2anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 ( 𝑆 ∗ 1 ) 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑆 , 0 ) )
33	26 27 17	3jca	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑇 ∈ 𝐵 ) )
34	33	3ad2ant1	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑇 ∈ 𝐵 ) )
35	1 2 3 4 5	scmatscmide	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑇 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑇 ∗ 1 ) 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑇 , 0 ) )
36	34 30 35	syl2anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 ( 𝑇 ∗ 1 ) 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑇 , 0 ) )
37	32 36	oveq12d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑖 ( 𝑆 ∗ 1 ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑖 ( 𝑇 ∗ 1 ) 𝑗 ) ) = ( if ( 𝑖 = 𝑗 , 𝑆 , 0 ) ( .r ‘ 𝑅 ) if ( 𝑖 = 𝑗 , 𝑇 , 0 ) ) )
38	37	ifeq1d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → if ( 𝑖 = 𝑗 , ( ( 𝑖 ( 𝑆 ∗ 1 ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑖 ( 𝑇 ∗ 1 ) 𝑗 ) ) , 0 ) = if ( 𝑖 = 𝑗 , ( if ( 𝑖 = 𝑗 , 𝑆 , 0 ) ( .r ‘ 𝑅 ) if ( 𝑖 = 𝑗 , 𝑇 , 0 ) ) , 0 ) )
39	38	mpoeq3dva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( ( 𝑖 ( 𝑆 ∗ 1 ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑖 ( 𝑇 ∗ 1 ) 𝑗 ) ) , 0 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( if ( 𝑖 = 𝑗 , 𝑆 , 0 ) ( .r ‘ 𝑅 ) if ( 𝑖 = 𝑗 , 𝑇 , 0 ) ) , 0 ) ) )
40		iftrue	⊢ ( 𝑖 = 𝑗 → if ( 𝑖 = 𝑗 , 𝑆 , 0 ) = 𝑆 )
41		iftrue	⊢ ( 𝑖 = 𝑗 → if ( 𝑖 = 𝑗 , 𝑇 , 0 ) = 𝑇 )
42	40 41	oveq12d	⊢ ( 𝑖 = 𝑗 → ( if ( 𝑖 = 𝑗 , 𝑆 , 0 ) ( .r ‘ 𝑅 ) if ( 𝑖 = 𝑗 , 𝑇 , 0 ) ) = ( 𝑆 ( .r ‘ 𝑅 ) 𝑇 ) )
43	42	adantl	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑖 = 𝑗 ) → ( if ( 𝑖 = 𝑗 , 𝑆 , 0 ) ( .r ‘ 𝑅 ) if ( 𝑖 = 𝑗 , 𝑇 , 0 ) ) = ( 𝑆 ( .r ‘ 𝑅 ) 𝑇 ) )
44	43	ifeq1da	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → if ( 𝑖 = 𝑗 , ( if ( 𝑖 = 𝑗 , 𝑆 , 0 ) ( .r ‘ 𝑅 ) if ( 𝑖 = 𝑗 , 𝑇 , 0 ) ) , 0 ) = if ( 𝑖 = 𝑗 , ( 𝑆 ( .r ‘ 𝑅 ) 𝑇 ) , 0 ) )
45	44	mpoeq3dva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( if ( 𝑖 = 𝑗 , 𝑆 , 0 ) ( .r ‘ 𝑅 ) if ( 𝑖 = 𝑗 , 𝑇 , 0 ) ) , 0 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( 𝑆 ( .r ‘ 𝑅 ) 𝑇 ) , 0 ) ) )
46		eqidd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( 𝑆 ( .r ‘ 𝑅 ) 𝑇 ) , 0 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( 𝑆 ( .r ‘ 𝑅 ) 𝑇 ) , 0 ) ) )
47		eqeq12	⊢ ( ( 𝑖 = 𝑥 ∧ 𝑗 = 𝑦 ) → ( 𝑖 = 𝑗 ↔ 𝑥 = 𝑦 ) )
48	6	eqcomi	⊢ ( .r ‘ 𝑅 ) = ·
49	48	oveqi	⊢ ( 𝑆 ( .r ‘ 𝑅 ) 𝑇 ) = ( 𝑆 · 𝑇 )
50	49	a1i	⊢ ( ( 𝑖 = 𝑥 ∧ 𝑗 = 𝑦 ) → ( 𝑆 ( .r ‘ 𝑅 ) 𝑇 ) = ( 𝑆 · 𝑇 ) )
51	47 50	ifbieq1d	⊢ ( ( 𝑖 = 𝑥 ∧ 𝑗 = 𝑦 ) → if ( 𝑖 = 𝑗 , ( 𝑆 ( .r ‘ 𝑅 ) 𝑇 ) , 0 ) = if ( 𝑥 = 𝑦 , ( 𝑆 · 𝑇 ) , 0 ) )
52	51	adantl	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ ( 𝑖 = 𝑥 ∧ 𝑗 = 𝑦 ) ) → if ( 𝑖 = 𝑗 , ( 𝑆 ( .r ‘ 𝑅 ) 𝑇 ) , 0 ) = if ( 𝑥 = 𝑦 , ( 𝑆 · 𝑇 ) , 0 ) )
53		simprl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → 𝑥 ∈ 𝑁 )
54		simprr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → 𝑦 ∈ 𝑁 )
55		ovex	⊢ ( 𝑆 · 𝑇 ) ∈ V
56	3	fvexi	⊢ 0 ∈ V
57	55 56	ifex	⊢ if ( 𝑥 = 𝑦 , ( 𝑆 · 𝑇 ) , 0 ) ∈ V
58	57	a1i	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → if ( 𝑥 = 𝑦 , ( 𝑆 · 𝑇 ) , 0 ) ∈ V )
59	46 52 53 54 58	ovmpod	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( 𝑆 ( .r ‘ 𝑅 ) 𝑇 ) , 0 ) ) 𝑦 ) = if ( 𝑥 = 𝑦 , ( 𝑆 · 𝑇 ) , 0 ) )
60	27 8 17	3jca	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) )
61	2 6	ringcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) → ( 𝑆 · 𝑇 ) ∈ 𝐵 )
62	60 61	syl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → ( 𝑆 · 𝑇 ) ∈ 𝐵 )
63	26 27 62	3jca	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑆 · 𝑇 ) ∈ 𝐵 ) )
64	1 2 3 4 5	scmatscmide	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑆 · 𝑇 ) ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 𝑥 ( ( 𝑆 · 𝑇 ) ∗ 1 ) 𝑦 ) = if ( 𝑥 = 𝑦 , ( 𝑆 · 𝑇 ) , 0 ) )
65	63 64	sylan	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 𝑥 ( ( 𝑆 · 𝑇 ) ∗ 1 ) 𝑦 ) = if ( 𝑥 = 𝑦 , ( 𝑆 · 𝑇 ) , 0 ) )
66	59 65	eqtr4d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( 𝑆 ( .r ‘ 𝑅 ) 𝑇 ) , 0 ) ) 𝑦 ) = ( 𝑥 ( ( 𝑆 · 𝑇 ) ∗ 1 ) 𝑦 ) )
67	66	ralrimivva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( 𝑆 ( .r ‘ 𝑅 ) 𝑇 ) , 0 ) ) 𝑦 ) = ( 𝑥 ( ( 𝑆 · 𝑇 ) ∗ 1 ) 𝑦 ) )
68		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
69	2 68	ringcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) → ( 𝑆 ( .r ‘ 𝑅 ) 𝑇 ) ∈ 𝐵 )
70	60 69	syl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → ( 𝑆 ( .r ‘ 𝑅 ) 𝑇 ) ∈ 𝐵 )
71	2 3	ring0cl	⊢ ( 𝑅 ∈ Ring → 0 ∈ 𝐵 )
72	71	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 0 ∈ 𝐵 )
73	72	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → 0 ∈ 𝐵 )
74	70 73	ifcld	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → if ( 𝑖 = 𝑗 , ( 𝑆 ( .r ‘ 𝑅 ) 𝑇 ) , 0 ) ∈ 𝐵 )
75	74	3ad2ant1	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → if ( 𝑖 = 𝑗 , ( 𝑆 ( .r ‘ 𝑅 ) 𝑇 ) , 0 ) ∈ 𝐵 )
76	1 2 9 26 27 75	matbas2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( 𝑆 ( .r ‘ 𝑅 ) 𝑇 ) , 0 ) ) ∈ ( Base ‘ 𝐴 ) )
77	1	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
78	9 4	ringidcl	⊢ ( 𝐴 ∈ Ring → 1 ∈ ( Base ‘ 𝐴 ) )
79	77 78	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 1 ∈ ( Base ‘ 𝐴 ) )
80	79	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → 1 ∈ ( Base ‘ 𝐴 ) )
81	62 80	jca	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → ( ( 𝑆 · 𝑇 ) ∈ 𝐵 ∧ 1 ∈ ( Base ‘ 𝐴 ) ) )
82	2 1 9 5	matvscl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( ( 𝑆 · 𝑇 ) ∈ 𝐵 ∧ 1 ∈ ( Base ‘ 𝐴 ) ) ) → ( ( 𝑆 · 𝑇 ) ∗ 1 ) ∈ ( Base ‘ 𝐴 ) )
83	81 82	syldan	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → ( ( 𝑆 · 𝑇 ) ∗ 1 ) ∈ ( Base ‘ 𝐴 ) )
84	1 9	eqmat	⊢ ( ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( 𝑆 ( .r ‘ 𝑅 ) 𝑇 ) , 0 ) ) ∈ ( Base ‘ 𝐴 ) ∧ ( ( 𝑆 · 𝑇 ) ∗ 1 ) ∈ ( Base ‘ 𝐴 ) ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( 𝑆 ( .r ‘ 𝑅 ) 𝑇 ) , 0 ) ) = ( ( 𝑆 · 𝑇 ) ∗ 1 ) ↔ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( 𝑆 ( .r ‘ 𝑅 ) 𝑇 ) , 0 ) ) 𝑦 ) = ( 𝑥 ( ( 𝑆 · 𝑇 ) ∗ 1 ) 𝑦 ) ) )
85	76 83 84	syl2anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( 𝑆 ( .r ‘ 𝑅 ) 𝑇 ) , 0 ) ) = ( ( 𝑆 · 𝑇 ) ∗ 1 ) ↔ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( 𝑆 ( .r ‘ 𝑅 ) 𝑇 ) , 0 ) ) 𝑦 ) = ( 𝑥 ( ( 𝑆 · 𝑇 ) ∗ 1 ) 𝑦 ) ) )
86	67 85	mpbird	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( 𝑆 ( .r ‘ 𝑅 ) 𝑇 ) , 0 ) ) = ( ( 𝑆 · 𝑇 ) ∗ 1 ) )
87	45 86	eqtrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( if ( 𝑖 = 𝑗 , 𝑆 , 0 ) ( .r ‘ 𝑅 ) if ( 𝑖 = 𝑗 , 𝑇 , 0 ) ) , 0 ) ) = ( ( 𝑆 · 𝑇 ) ∗ 1 ) )
88	39 87	eqtrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( ( 𝑖 ( 𝑆 ∗ 1 ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑖 ( 𝑇 ∗ 1 ) 𝑗 ) ) , 0 ) ) = ( ( 𝑆 · 𝑇 ) ∗ 1 ) )
89	25 88	eqtrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) ) → ( ( 𝑆 ∗ 1 ) × ( 𝑇 ∗ 1 ) ) = ( ( 𝑆 · 𝑇 ) ∗ 1 ) )