Metamath Proof Explorer

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