Metamath Proof Explorer

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 syl5eq ⊢ ( ( ( 𝑁 ∈ 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 ) )