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	⊢ ( 𝜑 → ( ( 𝑋 × 𝑍 ) · 𝑌 ) = ( 𝑋 · ( 𝑍 · 𝑌 ) ) )