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 ringcmn ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
27 4 26 syl ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
28 27 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → 𝑅 ∈ CMnd )
29 5 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → 𝑁 ∈ Fin )
30 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ ( 𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁 ) ) → 𝑅 ∈ Ring )
31 elmapi ⊢ ( 𝑋 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑁 ) ) → 𝑋 : ( 𝑁 × 𝑁 ) ⟶ 𝐵 )
32 13 31 syl ⊢ ( 𝜑 → 𝑋 : ( 𝑁 × 𝑁 ) ⟶ 𝐵 )
33 32 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ ( 𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁 ) ) → 𝑋 : ( 𝑁 × 𝑁 ) ⟶ 𝐵 )
34 simplr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ ( 𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁 ) ) → 𝑖 ∈ 𝑁 )
35 simprr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ ( 𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁 ) ) → 𝑘 ∈ 𝑁 )
36 33 34 35 fovrnd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ ( 𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁 ) ) → ( 𝑖 𝑋 𝑘 ) ∈ 𝐵 )
37 elmapi ⊢ ( 𝑍 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑁 ) ) → 𝑍 : ( 𝑁 × 𝑁 ) ⟶ 𝐵 )
38 14 37 syl ⊢ ( 𝜑 → 𝑍 : ( 𝑁 × 𝑁 ) ⟶ 𝐵 )
39 38 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ ( 𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁 ) ) → 𝑍 : ( 𝑁 × 𝑁 ) ⟶ 𝐵 )
40 simprl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ ( 𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁 ) ) → 𝑗 ∈ 𝑁 )
41 39 35 40 fovrnd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ ( 𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁 ) ) → ( 𝑘 𝑍 𝑗 ) ∈ 𝐵 )
42 elmapi ⊢ ( 𝑌 ∈ ( 𝐵 ↑m 𝑁 ) → 𝑌 : 𝑁 ⟶ 𝐵 )
43 ffvelrn ⊢ ( ( 𝑌 : 𝑁 ⟶ 𝐵 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑌 ‘ 𝑗 ) ∈ 𝐵 )
44 43 ex ⊢ ( 𝑌 : 𝑁 ⟶ 𝐵 → ( 𝑗 ∈ 𝑁 → ( 𝑌 ‘ 𝑗 ) ∈ 𝐵 ) )
45 6 42 44 3syl ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑁 → ( 𝑌 ‘ 𝑗 ) ∈ 𝐵 ) )
46 45 imp ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑌 ‘ 𝑗 ) ∈ 𝐵 )
47 46 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ ( 𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁 ) ) → ( 𝑌 ‘ 𝑗 ) ∈ 𝐵 )
48 2 10 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑘 𝑍 𝑗 ) ∈ 𝐵 ∧ ( 𝑌 ‘ 𝑗 ) ∈ 𝐵 ) → ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ∈ 𝐵 )
49 30 41 47 48 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ ( 𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁 ) ) → ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ∈ 𝐵 )
50 2 10 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑖 𝑋 𝑘 ) ∈ 𝐵 ∧ ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ∈ 𝐵 ) → ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ∈ 𝐵 )
51 30 36 49 50 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ ( 𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁 ) ) → ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ∈ 𝐵 )
52 2 28 29 29 51 gsumcom3fi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) ) ) ) )
53 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑅 ∈ Ring )
54 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑁 ∈ Fin )
55 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑋 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑁 ) ) )
56 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑍 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑁 ) ) )
57 simplr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
58 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
59 7 2 10 53 54 54 54 55 56 57 58 mamufv ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 ( 𝑋 × 𝑍 ) 𝑗 ) = ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 𝑗 ) ) ) ) )
60 59 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑖 ( 𝑋 × 𝑍 ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 𝑗 ) ) ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) )
61 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
62 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
63 46 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑌 ‘ 𝑗 ) ∈ 𝐵 )
64 4 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → 𝑅 ∈ Ring )
65 64 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → 𝑅 ∈ Ring )
66 32 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → 𝑋 : ( 𝑁 × 𝑁 ) ⟶ 𝐵 )
67 simplr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
68 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → 𝑘 ∈ 𝑁 )
69 66 67 68 fovrnd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑖 𝑋 𝑘 ) ∈ 𝐵 )
70 69 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑖 𝑋 𝑘 ) ∈ 𝐵 )
71 38 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → 𝑍 : ( 𝑁 × 𝑁 ) ⟶ 𝐵 )
72 71 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → 𝑍 : ( 𝑁 × 𝑁 ) ⟶ 𝐵 )
73 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → 𝑘 ∈ 𝑁 )
74 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
75 72 73 74 fovrnd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑘 𝑍 𝑗 ) ∈ 𝐵 )
76 2 10 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑖 𝑋 𝑘 ) ∈ 𝐵 ∧ ( 𝑘 𝑍 𝑗 ) ∈ 𝐵 ) → ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 𝑗 ) ) ∈ 𝐵 )
77 65 70 75 76 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 𝑗 ) ) ∈ 𝐵 )
78 eqid ⊢ ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 𝑗 ) ) ) = ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 𝑗 ) ) )
79 ovexd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 𝑗 ) ) ∈ V )
80 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 0g ‘ 𝑅 ) ∈ V )
81 78 54 79 80 fsuppmptdm ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 𝑗 ) ) ) finSupp ( 0g ‘ 𝑅 ) )
82 2 61 62 10 53 54 63 77 81 gsummulc1 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 𝑗 ) ) ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) )
83 2 10 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝑖 𝑋 𝑘 ) ∈ 𝐵 ∧ ( 𝑘 𝑍 𝑗 ) ∈ 𝐵 ∧ ( 𝑌 ‘ 𝑗 ) ∈ 𝐵 ) ) → ( ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) = ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) )
84 30 36 41 47 83 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ ( 𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁 ) ) → ( ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) = ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) )
85 84 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → ( ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) = ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) )
86 85 mpteq2dva ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑘 ∈ 𝑁 ↦ ( ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) = ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) )
87 86 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) ) )
88 60 82 87 3eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑖 ( 𝑋 × 𝑍 ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) = ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) ) )
89 88 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑋 × 𝑍 ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) = ( 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) ) ) )
90 89 oveq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑋 × 𝑍 ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) ) ) ) )
91 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → 𝑅 ∈ Ring )
92 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → 𝑁 ∈ Fin )
93 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → 𝑍 ∈ ( Base ‘ 𝐴 ) )
94 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → 𝑌 ∈ ( 𝐵 ↑m 𝑁 ) )
95 1 3 2 10 91 92 93 94 68 mavmulfv ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → ( ( 𝑍 · 𝑌 ) ‘ 𝑘 ) = ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) )
96 95 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑍 · 𝑌 ) ‘ 𝑘 ) ) = ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) ) )
97 64 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑅 ∈ Ring )
98 71 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑍 : ( 𝑁 × 𝑁 ) ⟶ 𝐵 )
99 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑘 ∈ 𝑁 )
100 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
101 98 99 100 fovrnd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑘 𝑍 𝑗 ) ∈ 𝐵 )
102 45 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑗 ∈ 𝑁 → ( 𝑌 ‘ 𝑗 ) ∈ 𝐵 ) )
103 102 imp ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑌 ‘ 𝑗 ) ∈ 𝐵 )
104 97 101 103 48 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ∈ 𝐵 )
105 eqid ⊢ ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) = ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) )
106 ovexd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ∈ V )
107 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → ( 0g ‘ 𝑅 ) ∈ V )
108 105 92 106 107 fsuppmptdm ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) finSupp ( 0g ‘ 𝑅 ) )
109 2 61 62 10 91 92 69 104 108 gsummulc2 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) ) = ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) ) )
110 96 109 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑍 · 𝑌 ) ‘ 𝑘 ) ) = ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) ) )
111 110 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑍 · 𝑌 ) ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) ) ) )
112 111 oveq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑍 · 𝑌 ) ‘ 𝑘 ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑘 𝑍 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) ) ) ) )
113 52 90 112 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑋 × 𝑍 ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑍 · 𝑌 ) ‘ 𝑘 ) ) ) ) )
114 16 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑋 × 𝑍 ) ∈ ( Base ‘ 𝐴 ) )
115 6 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → 𝑌 ∈ ( 𝐵 ↑m 𝑁 ) )
116 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
117 1 3 2 10 64 29 114 115 116 mavmulfv ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( ( ( 𝑋 × 𝑍 ) · 𝑌 ) ‘ 𝑖 ) = ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑋 × 𝑍 ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) )
118 8 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → 𝑋 ∈ ( Base ‘ 𝐴 ) )
119 21 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑍 · 𝑌 ) ∈ ( 𝐵 ↑m 𝑁 ) )
120 1 3 2 10 64 29 118 119 116 mavmulfv ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( ( 𝑋 · ( 𝑍 · 𝑌 ) ) ‘ 𝑖 ) = ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( ( 𝑍 · 𝑌 ) ‘ 𝑘 ) ) ) ) )
121 113 117 120 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( ( ( 𝑋 × 𝑍 ) · 𝑌 ) ‘ 𝑖 ) = ( ( 𝑋 · ( 𝑍 · 𝑌 ) ) ‘ 𝑖 ) )
122 20 25 121 eqfnfvd ⊢ ( 𝜑 → ( ( 𝑋 × 𝑍 ) · 𝑌 ) = ( 𝑋 · ( 𝑍 · 𝑌 ) ) )