Metamath Proof Explorer


Theorem rhmcomulmpl

Description: Show that the ring homomorphism in rhmmpl preserves multiplication. (Contributed by SN, 8-Feb-2025)

Ref Expression
Hypotheses rhmcomulmpl.p 𝑃 = ( 𝐼 mPoly 𝑅 )
rhmcomulmpl.q 𝑄 = ( 𝐼 mPoly 𝑆 )
rhmcomulmpl.b 𝐵 = ( Base ‘ 𝑃 )
rhmcomulmpl.c 𝐶 = ( Base ‘ 𝑄 )
rhmcomulmpl.1 · = ( .r𝑃 )
rhmcomulmpl.2 = ( .r𝑄 )
rhmcomulmpl.h ( 𝜑𝐻 ∈ ( 𝑅 RingHom 𝑆 ) )
rhmcomulmpl.f ( 𝜑𝐹𝐵 )
rhmcomulmpl.g ( 𝜑𝐺𝐵 )
Assertion rhmcomulmpl ( 𝜑 → ( 𝐻 ∘ ( 𝐹 · 𝐺 ) ) = ( ( 𝐻𝐹 ) ( 𝐻𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 rhmcomulmpl.p 𝑃 = ( 𝐼 mPoly 𝑅 )
2 rhmcomulmpl.q 𝑄 = ( 𝐼 mPoly 𝑆 )
3 rhmcomulmpl.b 𝐵 = ( Base ‘ 𝑃 )
4 rhmcomulmpl.c 𝐶 = ( Base ‘ 𝑄 )
5 rhmcomulmpl.1 · = ( .r𝑃 )
6 rhmcomulmpl.2 = ( .r𝑄 )
7 rhmcomulmpl.h ( 𝜑𝐻 ∈ ( 𝑅 RingHom 𝑆 ) )
8 rhmcomulmpl.f ( 𝜑𝐹𝐵 )
9 rhmcomulmpl.g ( 𝜑𝐺𝐵 )
10 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
11 eqid ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
12 10 11 rhmf ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐻 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
13 7 12 syl ( 𝜑𝐻 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
14 eqid { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
15 rhmrcl1 ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑅 ∈ Ring )
16 7 15 syl ( 𝜑𝑅 ∈ Ring )
17 1 10 3 14 8 mplelf ( 𝜑𝐹 : { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
18 1 10 3 14 9 mplelf ( 𝜑𝐺 : { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
19 14 16 17 18 rhmpsrlem2 ( ( 𝜑𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ↦ ( ( 𝐹𝑑 ) ( .r𝑅 ) ( 𝐺 ‘ ( 𝑘f𝑑 ) ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
20 13 19 cofmpt ( 𝜑 → ( 𝐻 ∘ ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ↦ ( ( 𝐹𝑑 ) ( .r𝑅 ) ( 𝐺 ‘ ( 𝑘f𝑑 ) ) ) ) ) ) ) = ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝐻 ‘ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ↦ ( ( 𝐹𝑑 ) ( .r𝑅 ) ( 𝐺 ‘ ( 𝑘f𝑑 ) ) ) ) ) ) ) )
21 eqid ( 0g𝑅 ) = ( 0g𝑅 )
22 16 ringcmnd ( 𝜑𝑅 ∈ CMnd )
23 22 adantr ( ( 𝜑𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) → 𝑅 ∈ CMnd )
24 rhmrcl2 ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑆 ∈ Ring )
25 7 24 syl ( 𝜑𝑆 ∈ Ring )
26 25 ringgrpd ( 𝜑𝑆 ∈ Grp )
27 26 grpmndd ( 𝜑𝑆 ∈ Mnd )
28 27 adantr ( ( 𝜑𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) → 𝑆 ∈ Mnd )
29 ovex ( ℕ0m 𝐼 ) ∈ V
30 29 rabex { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∈ V
31 30 rabex { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ∈ V
32 31 a1i ( ( 𝜑𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) → { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ∈ V )
33 rhmghm ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐻 ∈ ( 𝑅 GrpHom 𝑆 ) )
34 ghmmhm ( 𝐻 ∈ ( 𝑅 GrpHom 𝑆 ) → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
35 7 33 34 3syl ( 𝜑𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
36 35 adantr ( ( 𝜑𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
37 eqid ( .r𝑅 ) = ( .r𝑅 )
38 16 ad2antrr ( ( ( 𝜑𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ) → 𝑅 ∈ Ring )
39 elrabi ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } → 𝑑 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } )
40 17 ffvelcdmda ( ( 𝜑𝑑 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝐹𝑑 ) ∈ ( Base ‘ 𝑅 ) )
41 39 40 sylan2 ( ( 𝜑𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ) → ( 𝐹𝑑 ) ∈ ( Base ‘ 𝑅 ) )
42 41 adantlr ( ( ( 𝜑𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ) → ( 𝐹𝑑 ) ∈ ( Base ‘ 𝑅 ) )
43 18 ad2antrr ( ( ( 𝜑𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ) → 𝐺 : { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
44 eqid { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } = { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 }
45 14 44 psrbagconcl ( ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ) → ( 𝑘f𝑑 ) ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } )
46 elrabi ( ( 𝑘f𝑑 ) ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } → ( 𝑘f𝑑 ) ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } )
47 45 46 syl ( ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ) → ( 𝑘f𝑑 ) ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } )
48 47 adantll ( ( ( 𝜑𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ) → ( 𝑘f𝑑 ) ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } )
49 43 48 ffvelcdmd ( ( ( 𝜑𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ) → ( 𝐺 ‘ ( 𝑘f𝑑 ) ) ∈ ( Base ‘ 𝑅 ) )
50 10 37 38 42 49 ringcld ( ( ( 𝜑𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ) → ( ( 𝐹𝑑 ) ( .r𝑅 ) ( 𝐺 ‘ ( 𝑘f𝑑 ) ) ) ∈ ( Base ‘ 𝑅 ) )
51 14 16 17 18 rhmpsrlem1 ( ( 𝜑𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ↦ ( ( 𝐹𝑑 ) ( .r𝑅 ) ( 𝐺 ‘ ( 𝑘f𝑑 ) ) ) ) finSupp ( 0g𝑅 ) )
52 10 21 23 28 32 36 50 51 gsummptmhm ( ( 𝜑𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑆 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ↦ ( 𝐻 ‘ ( ( 𝐹𝑑 ) ( .r𝑅 ) ( 𝐺 ‘ ( 𝑘f𝑑 ) ) ) ) ) ) = ( 𝐻 ‘ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ↦ ( ( 𝐹𝑑 ) ( .r𝑅 ) ( 𝐺 ‘ ( 𝑘f𝑑 ) ) ) ) ) ) )
53 7 ad2antrr ( ( ( 𝜑𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ) → 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) )
54 eqid ( .r𝑆 ) = ( .r𝑆 )
55 10 37 54 rhmmul ( ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ( 𝐹𝑑 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐺 ‘ ( 𝑘f𝑑 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝐻 ‘ ( ( 𝐹𝑑 ) ( .r𝑅 ) ( 𝐺 ‘ ( 𝑘f𝑑 ) ) ) ) = ( ( 𝐻 ‘ ( 𝐹𝑑 ) ) ( .r𝑆 ) ( 𝐻 ‘ ( 𝐺 ‘ ( 𝑘f𝑑 ) ) ) ) )
56 53 42 49 55 syl3anc ( ( ( 𝜑𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ) → ( 𝐻 ‘ ( ( 𝐹𝑑 ) ( .r𝑅 ) ( 𝐺 ‘ ( 𝑘f𝑑 ) ) ) ) = ( ( 𝐻 ‘ ( 𝐹𝑑 ) ) ( .r𝑆 ) ( 𝐻 ‘ ( 𝐺 ‘ ( 𝑘f𝑑 ) ) ) ) )
57 17 ad2antrr ( ( ( 𝜑𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ) → 𝐹 : { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
58 39 adantl ( ( ( 𝜑𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ) → 𝑑 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } )
59 57 58 fvco3d ( ( ( 𝜑𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ) → ( ( 𝐻𝐹 ) ‘ 𝑑 ) = ( 𝐻 ‘ ( 𝐹𝑑 ) ) )
60 43 48 fvco3d ( ( ( 𝜑𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ) → ( ( 𝐻𝐺 ) ‘ ( 𝑘f𝑑 ) ) = ( 𝐻 ‘ ( 𝐺 ‘ ( 𝑘f𝑑 ) ) ) )
61 59 60 oveq12d ( ( ( 𝜑𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ) → ( ( ( 𝐻𝐹 ) ‘ 𝑑 ) ( .r𝑆 ) ( ( 𝐻𝐺 ) ‘ ( 𝑘f𝑑 ) ) ) = ( ( 𝐻 ‘ ( 𝐹𝑑 ) ) ( .r𝑆 ) ( 𝐻 ‘ ( 𝐺 ‘ ( 𝑘f𝑑 ) ) ) ) )
62 56 61 eqtr4d ( ( ( 𝜑𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ) → ( 𝐻 ‘ ( ( 𝐹𝑑 ) ( .r𝑅 ) ( 𝐺 ‘ ( 𝑘f𝑑 ) ) ) ) = ( ( ( 𝐻𝐹 ) ‘ 𝑑 ) ( .r𝑆 ) ( ( 𝐻𝐺 ) ‘ ( 𝑘f𝑑 ) ) ) )
63 62 mpteq2dva ( ( 𝜑𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ↦ ( 𝐻 ‘ ( ( 𝐹𝑑 ) ( .r𝑅 ) ( 𝐺 ‘ ( 𝑘f𝑑 ) ) ) ) ) = ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ↦ ( ( ( 𝐻𝐹 ) ‘ 𝑑 ) ( .r𝑆 ) ( ( 𝐻𝐺 ) ‘ ( 𝑘f𝑑 ) ) ) ) )
64 63 oveq2d ( ( 𝜑𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑆 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ↦ ( 𝐻 ‘ ( ( 𝐹𝑑 ) ( .r𝑅 ) ( 𝐺 ‘ ( 𝑘f𝑑 ) ) ) ) ) ) = ( 𝑆 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ↦ ( ( ( 𝐻𝐹 ) ‘ 𝑑 ) ( .r𝑆 ) ( ( 𝐻𝐺 ) ‘ ( 𝑘f𝑑 ) ) ) ) ) )
65 52 64 eqtr3d ( ( 𝜑𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝐻 ‘ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ↦ ( ( 𝐹𝑑 ) ( .r𝑅 ) ( 𝐺 ‘ ( 𝑘f𝑑 ) ) ) ) ) ) = ( 𝑆 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ↦ ( ( ( 𝐻𝐹 ) ‘ 𝑑 ) ( .r𝑆 ) ( ( 𝐻𝐺 ) ‘ ( 𝑘f𝑑 ) ) ) ) ) )
66 65 mpteq2dva ( 𝜑 → ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝐻 ‘ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ↦ ( ( 𝐹𝑑 ) ( .r𝑅 ) ( 𝐺 ‘ ( 𝑘f𝑑 ) ) ) ) ) ) ) = ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝑆 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ↦ ( ( ( 𝐻𝐹 ) ‘ 𝑑 ) ( .r𝑆 ) ( ( 𝐻𝐺 ) ‘ ( 𝑘f𝑑 ) ) ) ) ) ) )
67 20 66 eqtrd ( 𝜑 → ( 𝐻 ∘ ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ↦ ( ( 𝐹𝑑 ) ( .r𝑅 ) ( 𝐺 ‘ ( 𝑘f𝑑 ) ) ) ) ) ) ) = ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝑆 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ↦ ( ( ( 𝐻𝐹 ) ‘ 𝑑 ) ( .r𝑆 ) ( ( 𝐻𝐺 ) ‘ ( 𝑘f𝑑 ) ) ) ) ) ) )
68 1 3 37 5 14 8 9 mplmul ( 𝜑 → ( 𝐹 · 𝐺 ) = ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ↦ ( ( 𝐹𝑑 ) ( .r𝑅 ) ( 𝐺 ‘ ( 𝑘f𝑑 ) ) ) ) ) ) )
69 68 coeq2d ( 𝜑 → ( 𝐻 ∘ ( 𝐹 · 𝐺 ) ) = ( 𝐻 ∘ ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ↦ ( ( 𝐹𝑑 ) ( .r𝑅 ) ( 𝐺 ‘ ( 𝑘f𝑑 ) ) ) ) ) ) ) )
70 1 2 3 4 35 8 mhmcompl ( 𝜑 → ( 𝐻𝐹 ) ∈ 𝐶 )
71 1 2 3 4 35 9 mhmcompl ( 𝜑 → ( 𝐻𝐺 ) ∈ 𝐶 )
72 2 4 54 6 14 70 71 mplmul ( 𝜑 → ( ( 𝐻𝐹 ) ( 𝐻𝐺 ) ) = ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝑆 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒r𝑘 } ↦ ( ( ( 𝐻𝐹 ) ‘ 𝑑 ) ( .r𝑆 ) ( ( 𝐻𝐺 ) ‘ ( 𝑘f𝑑 ) ) ) ) ) ) )
73 67 69 72 3eqtr4d ( 𝜑 → ( 𝐻 ∘ ( 𝐹 · 𝐺 ) ) = ( ( 𝐻𝐹 ) ( 𝐻𝐺 ) ) )