Metamath Proof Explorer

Theorem mavmulass

Description: Associativity of the multiplication of two NxN matrices with an N-dimensional vector. (Contributed by AV, 9-Feb-2019) (Revised by AV, 25-Feb-2019) (Proof shortened by AV, 22-Jul-2019)

Ref Expression
Hypotheses 1mavmul.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
1mavmul.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
1mavmul.t ⊢ · = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
1mavmul.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
1mavmul.n ⊢ ( 𝜑 → 𝑁 ∈ Fin )
1mavmul.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ↑m 𝑁 ) )
mavmulass.m ⊢ × = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ )
mavmulass.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐴 ) )
mavmulass.z ⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ 𝐴 ) )
Assertion mavmulass ( 𝜑 → ( ( 𝑋 × 𝑍 ) · 𝑌 ) = ( 𝑋 · ( 𝑍 · 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 1mavmul.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 1mavmul.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 1mavmul.t ⊢ · = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
4 1mavmul.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
5 1mavmul.n ⊢ ( 𝜑 → 𝑁 ∈ Fin )
6 1mavmul.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ↑m 𝑁 ) )
7 mavmulass.m ⊢ × = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ )
8 mavmulass.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐴 ) )
9 mavmulass.z ⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ 𝐴 ) )
10 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
11 1 2 matbas2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐵 ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
12 5 4 11 syl2anc ⊢ ( 𝜑 → ( 𝐵 ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
13 8 12 eleqtrrd ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑁 ) ) )
14 9 12 eleqtrrd ⊢ ( 𝜑 → 𝑍 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑁 ) ) )
15 2 4 7 5 5 5 13 14 mamucl ⊢ ( 𝜑 → ( 𝑋 × 𝑍 ) ∈ ( 𝐵 ↑m ( 𝑁 × 𝑁 ) ) )
16 15 12 eleqtrd ⊢ ( 𝜑 → ( 𝑋 × 𝑍 ) ∈ ( Base ‘ 𝐴 ) )
17 1 3 2 10 4 5 16 6 mavmulcl ⊢ ( 𝜑 → ( ( 𝑋 × 𝑍 ) · 𝑌 ) ∈ ( 𝐵 ↑m 𝑁 ) )
18 elmapi ⊢ ( ( ( 𝑋 × 𝑍 ) · 𝑌 ) ∈ ( 𝐵 ↑m 𝑁 ) → ( ( 𝑋 × 𝑍 ) · 𝑌 ) : 𝑁 ⟶ 𝐵 )
19 ffn ⊢ ( ( ( 𝑋 × 𝑍 ) · 𝑌 ) : 𝑁 ⟶ 𝐵 → ( ( 𝑋 × 𝑍 ) · 𝑌 ) Fn 𝑁 )
20 17 18 19 3syl ⊢ ( 𝜑 → ( ( 𝑋 × 𝑍 ) · 𝑌 ) Fn 𝑁 )
21 1 3 2 10 4 5 9 6 mavmulcl ⊢ ( 𝜑 → ( 𝑍 · 𝑌 ) ∈ ( 𝐵 ↑m 𝑁 ) )
22 1 3 2 10 4 5 8 21 mavmulcl ⊢ ( 𝜑 → ( 𝑋 · ( 𝑍 · 𝑌 ) ) ∈ ( 𝐵 ↑m 𝑁 ) )
23 elmapi ⊢ ( ( 𝑋 · ( 𝑍 · 𝑌 ) ) ∈ ( 𝐵 ↑m 𝑁 ) → ( 𝑋 · ( 𝑍 · 𝑌 ) ) : 𝑁 ⟶ 𝐵 )
24 ffn ⊢ ( ( 𝑋 · ( 𝑍 · 𝑌 ) ) : 𝑁 ⟶ 𝐵 → ( 𝑋 · ( 𝑍 · 𝑌 ) ) Fn 𝑁 )
25 22 23 24 3syl ⊢ ( 𝜑 → ( 𝑋 · ( 𝑍 · 𝑌 ) ) Fn 𝑁 )
26 4 ringcmnd ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → 𝑅 ∈ CMnd )
28 5 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → 𝑁 ∈ Fin )
29 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ ( 𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁 ) ) → 𝑅 ∈ Ring )
30 elmapi ⊢ ( 𝑋 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑁 ) ) → 𝑋 : ( 𝑁 × 𝑁 ) ⟶ 𝐵 )
31 13 30 syl ⊢ ( 𝜑 → 𝑋 : ( 𝑁 × 𝑁 ) ⟶ 𝐵 )
32 31 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ ( 𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁 ) ) → 𝑋 : ( 𝑁 × 𝑁 ) ⟶ 𝐵 )
33 simplr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ ( 𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁 ) ) → 𝑖 ∈ 𝑁 )
34 simprr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ ( 𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁 ) ) → 𝑘 ∈ 𝑁 )
35 32 33 34 fovcdmd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ ( 𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁 ) ) → ( 𝑖 𝑋 𝑘 ) ∈ 𝐵 )
36 elmapi ⊢ ( 𝑍 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑁 ) ) → 𝑍 : ( 𝑁 × 𝑁 ) ⟶ 𝐵 )
37 14 36 syl ⊢ ( 𝜑 → 𝑍 : ( 𝑁 × 𝑁 ) ⟶ 𝐵 )
38 37 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ ( 𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁 ) ) → 𝑍 : ( 𝑁 × 𝑁 ) ⟶ 𝐵 )
39 simprl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ ( 𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁 ) ) → 𝑗 ∈ 𝑁 )
40 38 34 39 fovcdmd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ ( 𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁 ) ) → ( 𝑘 𝑍 𝑗 ) ∈ 𝐵 )
41 elmapi ⊢ ( 𝑌 ∈ ( 𝐵 ↑m 𝑁 ) → 𝑌 : 𝑁 ⟶ 𝐵 )
42 ffvelcdm ⊢ ( ( 𝑌 : 𝑁 ⟶ 𝐵 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑌 ‘ 𝑗 ) ∈ 𝐵 )
43 42 ex ⊢ ( 𝑌 : 𝑁 ⟶ 𝐵 → ( 𝑗 ∈ 𝑁 → ( 𝑌 ‘ 𝑗 ) ∈ 𝐵 ) )
44 6 41 43 3syl ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑁 → ( 𝑌 ‘ 𝑗 ) ∈ 𝐵 ) )
45 44 imp ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑌 ‘ 𝑗 ) ∈ 𝐵 )
46 45 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ ( 𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁 ) ) → ( 𝑌 ‘ 𝑗 ) ∈ 𝐵 )
47 2 10 29 40 46 ringcld ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ ( 𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁 ) ) → ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ∈ 𝐵 )
48 2 10 29 35 47 ringcld ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ ( 𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁 ) ) → ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ∈ 𝐵 )
49 2 27 28 28 48 gsumcom3fi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) ) ) ) )
50 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑅 ∈ Ring )
51 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑁 ∈ Fin )
52 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑋 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑁 ) ) )
53 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑍 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑁 ) ) )
54 simplr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
55 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
56 7 2 10 50 51 51 51 52 53 54 55 mamufv ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 ( 𝑋 × 𝑍 ) 𝑗 ) = ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 𝑗 ) ) ) ) )
57 56 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑖 ( 𝑋 × 𝑍 ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 𝑗 ) ) ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) )
58 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
59 45 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑌 ‘ 𝑗 ) ∈ 𝐵 )
60 4 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → 𝑅 ∈ Ring )
61 60 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → 𝑅 ∈ Ring )
62 31 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → 𝑋 : ( 𝑁 × 𝑁 ) ⟶ 𝐵 )
63 simplr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
64 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → 𝑘 ∈ 𝑁 )
65 62 63 64 fovcdmd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑖 𝑋 𝑘 ) ∈ 𝐵 )
66 65 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑖 𝑋 𝑘 ) ∈ 𝐵 )
67 37 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → 𝑍 : ( 𝑁 × 𝑁 ) ⟶ 𝐵 )
68 67 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → 𝑍 : ( 𝑁 × 𝑁 ) ⟶ 𝐵 )
69 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → 𝑘 ∈ 𝑁 )
70 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
71 68 69 70 fovcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑘 𝑍 𝑗 ) ∈ 𝐵 )
72 2 10 61 66 71 ringcld ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 𝑗 ) ) ∈ 𝐵 )
73 eqid ⊢ ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 𝑗 ) ) ) = ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 𝑗 ) ) )
74 ovexd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 𝑗 ) ) ∈ V )
75 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 0g ‘ 𝑅 ) ∈ V )
76 73 51 74 75 fsuppmptdm ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 𝑗 ) ) ) finSupp ( 0g ‘ 𝑅 ) )
77 2 58 10 50 51 59 72 76 gsummulc1 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 𝑗 ) ) ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) )
78 2 10 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝑖 𝑋 𝑘 ) ∈ 𝐵 ∧ ( 𝑘 𝑍 𝑗 ) ∈ 𝐵 ∧ ( 𝑌 ‘ 𝑗 ) ∈ 𝐵 ) ) → ( ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) = ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) )
79 29 35 40 46 78 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ ( 𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁 ) ) → ( ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) = ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) )
80 79 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → ( ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) = ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) )
81 80 mpteq2dva ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑘 ∈ 𝑁 ↦ ( ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) = ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) )
82 81 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) ) )
83 57 77 82 3eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑖 ( 𝑋 × 𝑍 ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) = ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) ) )
84 83 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑋 × 𝑍 ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) = ( 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) ) ) )
85 84 oveq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑋 × 𝑍 ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) ) ) ) )
86 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → 𝑅 ∈ Ring )
87 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → 𝑁 ∈ Fin )
88 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → 𝑍 ∈ ( Base ‘ 𝐴 ) )
89 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → 𝑌 ∈ ( 𝐵 ↑m 𝑁 ) )
90 1 3 2 10 86 87 88 89 64 mavmulfv ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → ( ( 𝑍 · 𝑌 ) ‘ 𝑘 ) = ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) )
91 90 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑍 · 𝑌 ) ‘ 𝑘 ) ) = ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) ) )
92 60 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑅 ∈ Ring )
93 67 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑍 : ( 𝑁 × 𝑁 ) ⟶ 𝐵 )
94 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑘 ∈ 𝑁 )
95 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
96 93 94 95 fovcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑘 𝑍 𝑗 ) ∈ 𝐵 )
97 44 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑗 ∈ 𝑁 → ( 𝑌 ‘ 𝑗 ) ∈ 𝐵 ) )
98 97 imp ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑌 ‘ 𝑗 ) ∈ 𝐵 )
99 2 10 92 96 98 ringcld ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ∈ 𝐵 )
100 eqid ⊢ ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) = ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) )
101 ovexd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ∈ V )
102 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → ( 0g ‘ 𝑅 ) ∈ V )
103 100 87 101 102 fsuppmptdm ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) finSupp ( 0g ‘ 𝑅 ) )
104 2 58 10 86 87 65 99 103 gsummulc2 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) ) = ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) ) )
105 91 104 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑍 · 𝑌 ) ‘ 𝑘 ) ) = ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) ) )
106 105 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑍 · 𝑌 ) ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) ) ) )
107 106 oveq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑍 · 𝑌 ) ‘ 𝑘 ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) ) ) ) )
108 49 85 107 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑋 × 𝑍 ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑍 · 𝑌 ) ‘ 𝑘 ) ) ) ) )
109 16 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑋 × 𝑍 ) ∈ ( Base ‘ 𝐴 ) )
110 6 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → 𝑌 ∈ ( 𝐵 ↑m 𝑁 ) )
111 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
112 1 3 2 10 60 28 109 110 111 mavmulfv ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( ( ( 𝑋 × 𝑍 ) · 𝑌 ) ‘ 𝑖 ) = ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑋 × 𝑍 ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) )
113 8 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → 𝑋 ∈ ( Base ‘ 𝐴 ) )
114 21 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑍 · 𝑌 ) ∈ ( 𝐵 ↑m 𝑁 ) )
115 1 3 2 10 60 28 113 114 111 mavmulfv ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( ( 𝑋 · ( 𝑍 · 𝑌 ) ) ‘ 𝑖 ) = ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑍 · 𝑌 ) ‘ 𝑘 ) ) ) ) )
116 108 112 115 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( ( ( 𝑋 × 𝑍 ) · 𝑌 ) ‘ 𝑖 ) = ( ( 𝑋 · ( 𝑍 · 𝑌 ) ) ‘ 𝑖 ) )
117 20 25 116 eqfnfvd ⊢ ( 𝜑 → ( ( 𝑋 × 𝑍 ) · 𝑌 ) = ( 𝑋 · ( 𝑍 · 𝑌 ) ) )