mamuass

Description: Matrix multiplication is associative, see also statement in Lang p. 505. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Hypotheses	mamucl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	mamucl.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	mamuass.m	⊢ ( 𝜑 → 𝑀 ∈ Fin )
	mamuass.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
	mamuass.o	⊢ ( 𝜑 → 𝑂 ∈ Fin )
	mamuass.p	⊢ ( 𝜑 → 𝑃 ∈ Fin )
	mamuass.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ↑_m ( 𝑀 × 𝑁 ) ) )
	mamuass.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ↑_m ( 𝑁 × 𝑂 ) ) )
	mamuass.z	⊢ ( 𝜑 → 𝑍 ∈ ( 𝐵 ↑_m ( 𝑂 × 𝑃 ) ) )
	mamuass.f	⊢ 𝐹 = ( 𝑅 maMul ⟨ 𝑀 , 𝑁 , 𝑂 ⟩ )
	mamuass.g	⊢ 𝐺 = ( 𝑅 maMul ⟨ 𝑀 , 𝑂 , 𝑃 ⟩ )
	mamuass.h	⊢ 𝐻 = ( 𝑅 maMul ⟨ 𝑀 , 𝑁 , 𝑃 ⟩ )
	mamuass.i	⊢ 𝐼 = ( 𝑅 maMul ⟨ 𝑁 , 𝑂 , 𝑃 ⟩ )
Assertion	mamuass	⊢ ( 𝜑 → ( ( 𝑋 𝐹 𝑌 ) 𝐺 𝑍 ) = ( 𝑋 𝐻 ( 𝑌 𝐼 𝑍 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mamucl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		mamucl.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
3		mamuass.m	⊢ ( 𝜑 → 𝑀 ∈ Fin )
4		mamuass.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
5		mamuass.o	⊢ ( 𝜑 → 𝑂 ∈ Fin )
6		mamuass.p	⊢ ( 𝜑 → 𝑃 ∈ Fin )
7		mamuass.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ↑_m ( 𝑀 × 𝑁 ) ) )
8		mamuass.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ↑_m ( 𝑁 × 𝑂 ) ) )
9		mamuass.z	⊢ ( 𝜑 → 𝑍 ∈ ( 𝐵 ↑_m ( 𝑂 × 𝑃 ) ) )
10		mamuass.f	⊢ 𝐹 = ( 𝑅 maMul ⟨ 𝑀 , 𝑁 , 𝑂 ⟩ )
11		mamuass.g	⊢ 𝐺 = ( 𝑅 maMul ⟨ 𝑀 , 𝑂 , 𝑃 ⟩ )
12		mamuass.h	⊢ 𝐻 = ( 𝑅 maMul ⟨ 𝑀 , 𝑁 , 𝑃 ⟩ )
13		mamuass.i	⊢ 𝐼 = ( 𝑅 maMul ⟨ 𝑁 , 𝑂 , 𝑃 ⟩ )
14	2	ringcmnd	⊢ ( 𝜑 → 𝑅 ∈ CMnd )
15	14	adantr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) → 𝑅 ∈ CMnd )
16	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) → 𝑂 ∈ Fin )
17	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) → 𝑁 ∈ Fin )
18		eqid	⊢ ( ._r ‘ 𝑅 ) = ( ._r ‘ 𝑅 )
19	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ ( 𝑗 ∈ 𝑂 ∧ 𝑙 ∈ 𝑁 ) ) → 𝑅 ∈ Ring )
20		elmapi	⊢ ( 𝑋 ∈ ( 𝐵 ↑_m ( 𝑀 × 𝑁 ) ) → 𝑋 : ( 𝑀 × 𝑁 ) ⟶ 𝐵 )
21	7 20	syl	⊢ ( 𝜑 → 𝑋 : ( 𝑀 × 𝑁 ) ⟶ 𝐵 )
22	21	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑙 ∈ 𝑁 ) → 𝑋 : ( 𝑀 × 𝑁 ) ⟶ 𝐵 )
23		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑙 ∈ 𝑁 ) → 𝑖 ∈ 𝑀 )
24		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑙 ∈ 𝑁 ) → 𝑙 ∈ 𝑁 )
25	22 23 24	fovcdmd	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑙 ∈ 𝑁 ) → ( 𝑖 𝑋 𝑙 ) ∈ 𝐵 )
26	25	adantrl	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ ( 𝑗 ∈ 𝑂 ∧ 𝑙 ∈ 𝑁 ) ) → ( 𝑖 𝑋 𝑙 ) ∈ 𝐵 )
27		elmapi	⊢ ( 𝑌 ∈ ( 𝐵 ↑_m ( 𝑁 × 𝑂 ) ) → 𝑌 : ( 𝑁 × 𝑂 ) ⟶ 𝐵 )
28	8 27	syl	⊢ ( 𝜑 → 𝑌 : ( 𝑁 × 𝑂 ) ⟶ 𝐵 )
29	28	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ ( 𝑗 ∈ 𝑂 ∧ 𝑙 ∈ 𝑁 ) ) → 𝑌 : ( 𝑁 × 𝑂 ) ⟶ 𝐵 )
30		simprr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ ( 𝑗 ∈ 𝑂 ∧ 𝑙 ∈ 𝑁 ) ) → 𝑙 ∈ 𝑁 )
31		simprl	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ ( 𝑗 ∈ 𝑂 ∧ 𝑙 ∈ 𝑁 ) ) → 𝑗 ∈ 𝑂 )
32	29 30 31	fovcdmd	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ ( 𝑗 ∈ 𝑂 ∧ 𝑙 ∈ 𝑁 ) ) → ( 𝑙 𝑌 𝑗 ) ∈ 𝐵 )
33		elmapi	⊢ ( 𝑍 ∈ ( 𝐵 ↑_m ( 𝑂 × 𝑃 ) ) → 𝑍 : ( 𝑂 × 𝑃 ) ⟶ 𝐵 )
34	9 33	syl	⊢ ( 𝜑 → 𝑍 : ( 𝑂 × 𝑃 ) ⟶ 𝐵 )
35	34	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑗 ∈ 𝑂 ) → 𝑍 : ( 𝑂 × 𝑃 ) ⟶ 𝐵 )
36		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑗 ∈ 𝑂 ) → 𝑗 ∈ 𝑂 )
37		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑗 ∈ 𝑂 ) → 𝑘 ∈ 𝑃 )
38	35 36 37	fovcdmd	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑗 ∈ 𝑂 ) → ( 𝑗 𝑍 𝑘 ) ∈ 𝐵 )
39	38	adantrr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ ( 𝑗 ∈ 𝑂 ∧ 𝑙 ∈ 𝑁 ) ) → ( 𝑗 𝑍 𝑘 ) ∈ 𝐵 )
40	1 18 19 32 39	ringcld	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ ( 𝑗 ∈ 𝑂 ∧ 𝑙 ∈ 𝑁 ) ) → ( ( 𝑙 𝑌 𝑗 ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ∈ 𝐵 )
41	1 18 19 26 40	ringcld	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ ( 𝑗 ∈ 𝑂 ∧ 𝑙 ∈ 𝑁 ) ) → ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( ( 𝑙 𝑌 𝑗 ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ∈ 𝐵 )
42	1 15 16 17 41	gsumcom3fi	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) → ( 𝑅 Σ_g ( 𝑗 ∈ 𝑂 ↦ ( 𝑅 Σ_g ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( ( 𝑙 𝑌 𝑗 ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) ) ) ) = ( 𝑅 Σ_g ( 𝑙 ∈ 𝑁 ↦ ( 𝑅 Σ_g ( 𝑗 ∈ 𝑂 ↦ ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( ( 𝑙 𝑌 𝑗 ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) ) ) ) )
43	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑗 ∈ 𝑂 ) → 𝑅 ∈ Ring )
44	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑗 ∈ 𝑂 ) → 𝑀 ∈ Fin )
45	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑗 ∈ 𝑂 ) → 𝑁 ∈ Fin )
46	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑗 ∈ 𝑂 ) → 𝑂 ∈ Fin )
47	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑗 ∈ 𝑂 ) → 𝑋 ∈ ( 𝐵 ↑_m ( 𝑀 × 𝑁 ) ) )
48	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑗 ∈ 𝑂 ) → 𝑌 ∈ ( 𝐵 ↑_m ( 𝑁 × 𝑂 ) ) )
49		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑗 ∈ 𝑂 ) → 𝑖 ∈ 𝑀 )
50	10 1 18 43 44 45 46 47 48 49 36	mamufv	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑗 ∈ 𝑂 ) → ( 𝑖 ( 𝑋 𝐹 𝑌 ) 𝑗 ) = ( 𝑅 Σ_g ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( 𝑙 𝑌 𝑗 ) ) ) ) )
51	50	oveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑗 ∈ 𝑂 ) → ( ( 𝑖 ( 𝑋 𝐹 𝑌 ) 𝑗 ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) = ( ( 𝑅 Σ_g ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( 𝑙 𝑌 𝑗 ) ) ) ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) )
52		eqid	⊢ ( 0_g ‘ 𝑅 ) = ( 0_g ‘ 𝑅 )
53	1 18 19 26 32	ringcld	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ ( 𝑗 ∈ 𝑂 ∧ 𝑙 ∈ 𝑁 ) ) → ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( 𝑙 𝑌 𝑗 ) ) ∈ 𝐵 )
54	53	anassrs	⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑗 ∈ 𝑂 ) ∧ 𝑙 ∈ 𝑁 ) → ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( 𝑙 𝑌 𝑗 ) ) ∈ 𝐵 )
55		eqid	⊢ ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( 𝑙 𝑌 𝑗 ) ) ) = ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( 𝑙 𝑌 𝑗 ) ) )
56		ovexd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑗 ∈ 𝑂 ) ∧ 𝑙 ∈ 𝑁 ) → ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( 𝑙 𝑌 𝑗 ) ) ∈ V )
57		fvexd	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑗 ∈ 𝑂 ) → ( 0_g ‘ 𝑅 ) ∈ V )
58	55 45 56 57	fsuppmptdm	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑗 ∈ 𝑂 ) → ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( 𝑙 𝑌 𝑗 ) ) ) finSupp ( 0_g ‘ 𝑅 ) )
59	1 52 18 43 45 38 54 58	gsummulc1	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑗 ∈ 𝑂 ) → ( 𝑅 Σ_g ( 𝑙 ∈ 𝑁 ↦ ( ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( 𝑙 𝑌 𝑗 ) ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) = ( ( 𝑅 Σ_g ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( 𝑙 𝑌 𝑗 ) ) ) ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) )
60	1 18	ringass	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝑖 𝑋 𝑙 ) ∈ 𝐵 ∧ ( 𝑙 𝑌 𝑗 ) ∈ 𝐵 ∧ ( 𝑗 𝑍 𝑘 ) ∈ 𝐵 ) ) → ( ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( 𝑙 𝑌 𝑗 ) ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) = ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( ( 𝑙 𝑌 𝑗 ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) )
61	19 26 32 39 60	syl13anc	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ ( 𝑗 ∈ 𝑂 ∧ 𝑙 ∈ 𝑁 ) ) → ( ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( 𝑙 𝑌 𝑗 ) ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) = ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( ( 𝑙 𝑌 𝑗 ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) )
62	61	anassrs	⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑗 ∈ 𝑂 ) ∧ 𝑙 ∈ 𝑁 ) → ( ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( 𝑙 𝑌 𝑗 ) ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) = ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( ( 𝑙 𝑌 𝑗 ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) )
63	62	mpteq2dva	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑗 ∈ 𝑂 ) → ( 𝑙 ∈ 𝑁 ↦ ( ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( 𝑙 𝑌 𝑗 ) ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) = ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( ( 𝑙 𝑌 𝑗 ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) )
64	63	oveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑗 ∈ 𝑂 ) → ( 𝑅 Σ_g ( 𝑙 ∈ 𝑁 ↦ ( ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( 𝑙 𝑌 𝑗 ) ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) = ( 𝑅 Σ_g ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( ( 𝑙 𝑌 𝑗 ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) ) )
65	51 59 64	3eqtr2d	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑗 ∈ 𝑂 ) → ( ( 𝑖 ( 𝑋 𝐹 𝑌 ) 𝑗 ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) = ( 𝑅 Σ_g ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( ( 𝑙 𝑌 𝑗 ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) ) )
66	65	mpteq2dva	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) → ( 𝑗 ∈ 𝑂 ↦ ( ( 𝑖 ( 𝑋 𝐹 𝑌 ) 𝑗 ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) = ( 𝑗 ∈ 𝑂 ↦ ( 𝑅 Σ_g ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( ( 𝑙 𝑌 𝑗 ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) ) ) )
67	66	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) → ( 𝑅 Σ_g ( 𝑗 ∈ 𝑂 ↦ ( ( 𝑖 ( 𝑋 𝐹 𝑌 ) 𝑗 ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) = ( 𝑅 Σ_g ( 𝑗 ∈ 𝑂 ↦ ( 𝑅 Σ_g ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( ( 𝑙 𝑌 𝑗 ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) ) ) ) )
68	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑙 ∈ 𝑁 ) → 𝑅 ∈ Ring )
69	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑙 ∈ 𝑁 ) → 𝑁 ∈ Fin )
70	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑙 ∈ 𝑁 ) → 𝑂 ∈ Fin )
71	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑙 ∈ 𝑁 ) → 𝑃 ∈ Fin )
72	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑙 ∈ 𝑁 ) → 𝑌 ∈ ( 𝐵 ↑_m ( 𝑁 × 𝑂 ) ) )
73	9	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑙 ∈ 𝑁 ) → 𝑍 ∈ ( 𝐵 ↑_m ( 𝑂 × 𝑃 ) ) )
74		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑙 ∈ 𝑁 ) → 𝑘 ∈ 𝑃 )
75	13 1 18 68 69 70 71 72 73 24 74	mamufv	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑙 ∈ 𝑁 ) → ( 𝑙 ( 𝑌 𝐼 𝑍 ) 𝑘 ) = ( 𝑅 Σ_g ( 𝑗 ∈ 𝑂 ↦ ( ( 𝑙 𝑌 𝑗 ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) )
76	75	oveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑙 ∈ 𝑁 ) → ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( 𝑙 ( 𝑌 𝐼 𝑍 ) 𝑘 ) ) = ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( 𝑅 Σ_g ( 𝑗 ∈ 𝑂 ↦ ( ( 𝑙 𝑌 𝑗 ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) ) )
77	40	anass1rs	⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑂 ) → ( ( 𝑙 𝑌 𝑗 ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ∈ 𝐵 )
78		eqid	⊢ ( 𝑗 ∈ 𝑂 ↦ ( ( 𝑙 𝑌 𝑗 ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) = ( 𝑗 ∈ 𝑂 ↦ ( ( 𝑙 𝑌 𝑗 ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) )
79		ovexd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑂 ) → ( ( 𝑙 𝑌 𝑗 ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ∈ V )
80		fvexd	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑙 ∈ 𝑁 ) → ( 0_g ‘ 𝑅 ) ∈ V )
81	78 70 79 80	fsuppmptdm	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑙 ∈ 𝑁 ) → ( 𝑗 ∈ 𝑂 ↦ ( ( 𝑙 𝑌 𝑗 ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) finSupp ( 0_g ‘ 𝑅 ) )
82	1 52 18 68 70 25 77 81	gsummulc2	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑙 ∈ 𝑁 ) → ( 𝑅 Σ_g ( 𝑗 ∈ 𝑂 ↦ ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( ( 𝑙 𝑌 𝑗 ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) ) = ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( 𝑅 Σ_g ( 𝑗 ∈ 𝑂 ↦ ( ( 𝑙 𝑌 𝑗 ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) ) )
83	76 82	eqtr4d	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑙 ∈ 𝑁 ) → ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( 𝑙 ( 𝑌 𝐼 𝑍 ) 𝑘 ) ) = ( 𝑅 Σ_g ( 𝑗 ∈ 𝑂 ↦ ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( ( 𝑙 𝑌 𝑗 ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) ) )
84	83	mpteq2dva	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) → ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( 𝑙 ( 𝑌 𝐼 𝑍 ) 𝑘 ) ) ) = ( 𝑙 ∈ 𝑁 ↦ ( 𝑅 Σ_g ( 𝑗 ∈ 𝑂 ↦ ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( ( 𝑙 𝑌 𝑗 ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) ) ) )
85	84	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) → ( 𝑅 Σ_g ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( 𝑙 ( 𝑌 𝐼 𝑍 ) 𝑘 ) ) ) ) = ( 𝑅 Σ_g ( 𝑙 ∈ 𝑁 ↦ ( 𝑅 Σ_g ( 𝑗 ∈ 𝑂 ↦ ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( ( 𝑙 𝑌 𝑗 ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) ) ) ) )
86	42 67 85	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) → ( 𝑅 Σ_g ( 𝑗 ∈ 𝑂 ↦ ( ( 𝑖 ( 𝑋 𝐹 𝑌 ) 𝑗 ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) = ( 𝑅 Σ_g ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( 𝑙 ( 𝑌 𝐼 𝑍 ) 𝑘 ) ) ) ) )
87	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) → 𝑅 ∈ Ring )
88	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) → 𝑀 ∈ Fin )
89	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) → 𝑃 ∈ Fin )
90	1 2 10 3 4 5 7 8	mamucl	⊢ ( 𝜑 → ( 𝑋 𝐹 𝑌 ) ∈ ( 𝐵 ↑_m ( 𝑀 × 𝑂 ) ) )
91	90	adantr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) → ( 𝑋 𝐹 𝑌 ) ∈ ( 𝐵 ↑_m ( 𝑀 × 𝑂 ) ) )
92	9	adantr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) → 𝑍 ∈ ( 𝐵 ↑_m ( 𝑂 × 𝑃 ) ) )
93		simprl	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) → 𝑖 ∈ 𝑀 )
94		simprr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) → 𝑘 ∈ 𝑃 )
95	11 1 18 87 88 16 89 91 92 93 94	mamufv	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) → ( 𝑖 ( ( 𝑋 𝐹 𝑌 ) 𝐺 𝑍 ) 𝑘 ) = ( 𝑅 Σ_g ( 𝑗 ∈ 𝑂 ↦ ( ( 𝑖 ( 𝑋 𝐹 𝑌 ) 𝑗 ) ( ._r ‘ 𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) )
96	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) → 𝑋 ∈ ( 𝐵 ↑_m ( 𝑀 × 𝑁 ) ) )
97	1 2 13 4 5 6 8 9	mamucl	⊢ ( 𝜑 → ( 𝑌 𝐼 𝑍 ) ∈ ( 𝐵 ↑_m ( 𝑁 × 𝑃 ) ) )
98	97	adantr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) → ( 𝑌 𝐼 𝑍 ) ∈ ( 𝐵 ↑_m ( 𝑁 × 𝑃 ) ) )
99	12 1 18 87 88 17 89 96 98 93 94	mamufv	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) → ( 𝑖 ( 𝑋 𝐻 ( 𝑌 𝐼 𝑍 ) ) 𝑘 ) = ( 𝑅 Σ_g ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑙 ) ( ._r ‘ 𝑅 ) ( 𝑙 ( 𝑌 𝐼 𝑍 ) 𝑘 ) ) ) ) )
100	86 95 99	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) → ( 𝑖 ( ( 𝑋 𝐹 𝑌 ) 𝐺 𝑍 ) 𝑘 ) = ( 𝑖 ( 𝑋 𝐻 ( 𝑌 𝐼 𝑍 ) ) 𝑘 ) )
101	100	ralrimivva	⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝑀 ∀ 𝑘 ∈ 𝑃 ( 𝑖 ( ( 𝑋 𝐹 𝑌 ) 𝐺 𝑍 ) 𝑘 ) = ( 𝑖 ( 𝑋 𝐻 ( 𝑌 𝐼 𝑍 ) ) 𝑘 ) )
102	1 2 11 3 5 6 90 9	mamucl	⊢ ( 𝜑 → ( ( 𝑋 𝐹 𝑌 ) 𝐺 𝑍 ) ∈ ( 𝐵 ↑_m ( 𝑀 × 𝑃 ) ) )
103		elmapi	⊢ ( ( ( 𝑋 𝐹 𝑌 ) 𝐺 𝑍 ) ∈ ( 𝐵 ↑_m ( 𝑀 × 𝑃 ) ) → ( ( 𝑋 𝐹 𝑌 ) 𝐺 𝑍 ) : ( 𝑀 × 𝑃 ) ⟶ 𝐵 )
104		ffn	⊢ ( ( ( 𝑋 𝐹 𝑌 ) 𝐺 𝑍 ) : ( 𝑀 × 𝑃 ) ⟶ 𝐵 → ( ( 𝑋 𝐹 𝑌 ) 𝐺 𝑍 ) Fn ( 𝑀 × 𝑃 ) )
105	102 103 104	3syl	⊢ ( 𝜑 → ( ( 𝑋 𝐹 𝑌 ) 𝐺 𝑍 ) Fn ( 𝑀 × 𝑃 ) )
106	1 2 12 3 4 6 7 97	mamucl	⊢ ( 𝜑 → ( 𝑋 𝐻 ( 𝑌 𝐼 𝑍 ) ) ∈ ( 𝐵 ↑_m ( 𝑀 × 𝑃 ) ) )
107		elmapi	⊢ ( ( 𝑋 𝐻 ( 𝑌 𝐼 𝑍 ) ) ∈ ( 𝐵 ↑_m ( 𝑀 × 𝑃 ) ) → ( 𝑋 𝐻 ( 𝑌 𝐼 𝑍 ) ) : ( 𝑀 × 𝑃 ) ⟶ 𝐵 )
108		ffn	⊢ ( ( 𝑋 𝐻 ( 𝑌 𝐼 𝑍 ) ) : ( 𝑀 × 𝑃 ) ⟶ 𝐵 → ( 𝑋 𝐻 ( 𝑌 𝐼 𝑍 ) ) Fn ( 𝑀 × 𝑃 ) )
109	106 107 108	3syl	⊢ ( 𝜑 → ( 𝑋 𝐻 ( 𝑌 𝐼 𝑍 ) ) Fn ( 𝑀 × 𝑃 ) )
110		eqfnov2	⊢ ( ( ( ( 𝑋 𝐹 𝑌 ) 𝐺 𝑍 ) Fn ( 𝑀 × 𝑃 ) ∧ ( 𝑋 𝐻 ( 𝑌 𝐼 𝑍 ) ) Fn ( 𝑀 × 𝑃 ) ) → ( ( ( 𝑋 𝐹 𝑌 ) 𝐺 𝑍 ) = ( 𝑋 𝐻 ( 𝑌 𝐼 𝑍 ) ) ↔ ∀ 𝑖 ∈ 𝑀 ∀ 𝑘 ∈ 𝑃 ( 𝑖 ( ( 𝑋 𝐹 𝑌 ) 𝐺 𝑍 ) 𝑘 ) = ( 𝑖 ( 𝑋 𝐻 ( 𝑌 𝐼 𝑍 ) ) 𝑘 ) ) )
111	105 109 110	syl2anc	⊢ ( 𝜑 → ( ( ( 𝑋 𝐹 𝑌 ) 𝐺 𝑍 ) = ( 𝑋 𝐻 ( 𝑌 𝐼 𝑍 ) ) ↔ ∀ 𝑖 ∈ 𝑀 ∀ 𝑘 ∈ 𝑃 ( 𝑖 ( ( 𝑋 𝐹 𝑌 ) 𝐺 𝑍 ) 𝑘 ) = ( 𝑖 ( 𝑋 𝐻 ( 𝑌 𝐼 𝑍 ) ) 𝑘 ) ) )
112	101 111	mpbird	⊢ ( 𝜑 → ( ( 𝑋 𝐹 𝑌 ) 𝐺 𝑍 ) = ( 𝑋 𝐻 ( 𝑌 𝐼 𝑍 ) ) )

Metamath Proof Explorer

Theorem mamuass

Proof