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 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 ( 0g𝑅 ) = ( 0g𝑅 )
53 1 18 19 26 32 ringcld ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑃 ) ) ∧ ( 𝑗𝑂𝑙𝑁 ) ) → ( ( 𝑖 𝑋 𝑙 ) ( .r𝑅 ) ( 𝑙 𝑌 𝑗 ) ) ∈ 𝐵 )
54 53 anassrs ( ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑃 ) ) ∧ 𝑗𝑂 ) ∧ 𝑙𝑁 ) → ( ( 𝑖 𝑋 𝑙 ) ( .r𝑅 ) ( 𝑙 𝑌 𝑗 ) ) ∈ 𝐵 )
55 eqid ( 𝑙𝑁 ↦ ( ( 𝑖 𝑋 𝑙 ) ( .r𝑅 ) ( 𝑙 𝑌 𝑗 ) ) ) = ( 𝑙𝑁 ↦ ( ( 𝑖 𝑋 𝑙 ) ( .r𝑅 ) ( 𝑙 𝑌 𝑗 ) ) )
56 ovexd ( ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑃 ) ) ∧ 𝑗𝑂 ) ∧ 𝑙𝑁 ) → ( ( 𝑖 𝑋 𝑙 ) ( .r𝑅 ) ( 𝑙 𝑌 𝑗 ) ) ∈ V )
57 fvexd ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑃 ) ) ∧ 𝑗𝑂 ) → ( 0g𝑅 ) ∈ V )
58 55 45 56 57 fsuppmptdm ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑃 ) ) ∧ 𝑗𝑂 ) → ( 𝑙𝑁 ↦ ( ( 𝑖 𝑋 𝑙 ) ( .r𝑅 ) ( 𝑙 𝑌 𝑗 ) ) ) finSupp ( 0g𝑅 ) )
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 ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑃 ) ) ∧ 𝑙𝑁 ) → ( 0g𝑅 ) ∈ V )
81 78 70 79 80 fsuppmptdm ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑃 ) ) ∧ 𝑙𝑁 ) → ( 𝑗𝑂 ↦ ( ( 𝑙 𝑌 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) finSupp ( 0g𝑅 ) )
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 ( 𝜑 → ( ( 𝑋 𝐹 𝑌 ) 𝐺 𝑍 ) = ( 𝑋 𝐻 ( 𝑌 𝐼 𝑍 ) ) )