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 ⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
15 rhmrcl1 ⊢ ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑅 ∈ Ring )
16 7 15 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
17 1 10 3 14 8 mplelf ⊢ ( 𝜑 → 𝐹 : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
18 1 10 3 14 9 mplelf ⊢ ( 𝜑 → 𝐺 : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
19 14 16 17 18 rhmpsrlem2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
20 13 19 cofmpt ⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) ) ) = ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝐻 ‘ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) ) ) )
21 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
22 16 ringcmnd ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → 𝑅 ∈ CMnd )
24 rhmrcl2 ⊢ ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑆 ∈ Ring )
25 7 24 syl ⊢ ( 𝜑 → 𝑆 ∈ Ring )
26 25 ringgrpd ⊢ ( 𝜑 → 𝑆 ∈ Grp )
27 26 grpmndd ⊢ ( 𝜑 → 𝑆 ∈ Mnd )
28 27 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → 𝑆 ∈ Mnd )
29 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
30 29 rabex ⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∈ V
31 30 rabex ⊢ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ∈ V
32 31 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ∈ V )
33 rhmghm ⊢ ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐻 ∈ ( 𝑅 GrpHom 𝑆 ) )
34 ghmmhm ⊢ ( 𝐻 ∈ ( 𝑅 GrpHom 𝑆 ) → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
35 7 33 34 3syl ⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
36 35 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
37 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
38 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → 𝑅 ∈ Ring )
39 elrabi ⊢ ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } → 𝑑 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } )
40 17 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝐹 ‘ 𝑑 ) ∈ ( Base ‘ 𝑅 ) )
41 39 40 sylan2 ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → ( 𝐹 ‘ 𝑑 ) ∈ ( Base ‘ 𝑅 ) )
42 41 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → ( 𝐹 ‘ 𝑑 ) ∈ ( Base ‘ 𝑅 ) )
43 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → 𝐺 : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
44 eqid ⊢ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } = { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 }
45 14 44 psrbagconcl ⊢ ( ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑑 ) ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } )
46 elrabi ⊢ ( ( 𝑘 ∘f − 𝑑 ) ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } → ( 𝑘 ∘f − 𝑑 ) ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } )
47 45 46 syl ⊢ ( ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑑 ) ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } )
48 47 adantll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑑 ) ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } )
49 43 48 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ∈ ( Base ‘ 𝑅 ) )
50 10 37 38 42 49 ringcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ∈ ( Base ‘ 𝑅 ) )
51 14 16 17 18 rhmpsrlem1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) finSupp ( 0g ‘ 𝑅 ) )
52 10 21 23 28 32 36 50 51 gsummptmhm ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑆 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( 𝐻 ‘ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) ) = ( 𝐻 ‘ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) ) )
53 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ 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 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → ( 𝐻 ‘ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) = ( ( 𝐻 ‘ ( 𝐹 ‘ 𝑑 ) ) ( .r ‘ 𝑆 ) ( 𝐻 ‘ ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) )
57 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → 𝐹 : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
58 39 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → 𝑑 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } )
59 57 58 fvco3d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑑 ) = ( 𝐻 ‘ ( 𝐹 ‘ 𝑑 ) ) )
60 43 48 fvco3d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → ( ( 𝐻 ∘ 𝐺 ) ‘ ( 𝑘 ∘f − 𝑑 ) ) = ( 𝐻 ‘ ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) )
61 59 60 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → ( ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑑 ) ( .r ‘ 𝑆 ) ( ( 𝐻 ∘ 𝐺 ) ‘ ( 𝑘 ∘f − 𝑑 ) ) ) = ( ( 𝐻 ‘ ( 𝐹 ‘ 𝑑 ) ) ( .r ‘ 𝑆 ) ( 𝐻 ‘ ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) )
62 56 61 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → ( 𝐻 ‘ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) = ( ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑑 ) ( .r ‘ 𝑆 ) ( ( 𝐻 ∘ 𝐺 ) ‘ ( 𝑘 ∘f − 𝑑 ) ) ) )
63 62 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( 𝐻 ‘ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) = ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑑 ) ( .r ‘ 𝑆 ) ( ( 𝐻 ∘ 𝐺 ) ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) )
64 63 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑆 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( 𝐻 ‘ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) ) = ( 𝑆 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑑 ) ( .r ‘ 𝑆 ) ( ( 𝐻 ∘ 𝐺 ) ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) )
65 52 64 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝐻 ‘ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) ) = ( 𝑆 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑑 ) ( .r ‘ 𝑆 ) ( ( 𝐻 ∘ 𝐺 ) ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) )
66 65 mpteq2dva ⊢ ( 𝜑 → ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝐻 ‘ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) ) ) = ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝑆 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑑 ) ( .r ‘ 𝑆 ) ( ( 𝐻 ∘ 𝐺 ) ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) ) )
67 20 66 eqtrd ⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) ) ) = ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝑆 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑑 ) ( .r ‘ 𝑆 ) ( ( 𝐻 ∘ 𝐺 ) ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) ) )
68 1 3 37 5 14 8 9 mplmul ⊢ ( 𝜑 → ( 𝐹 · 𝐺 ) = ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) ) )
69 68 coeq2d ⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝐹 · 𝐺 ) ) = ( 𝐻 ∘ ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ 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 ⊢ ( 𝜑 → ( ( 𝐻 ∘ 𝐹 ) ∙ ( 𝐻 ∘ 𝐺 ) ) = ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝑆 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑑 ) ( .r ‘ 𝑆 ) ( ( 𝐻 ∘ 𝐺 ) ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) ) )
73 67 69 72 3eqtr4d ⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝐹 · 𝐺 ) ) = ( ( 𝐻 ∘ 𝐹 ) ∙ ( 𝐻 ∘ 𝐺 ) ) )