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.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	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.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
8		rhmcomulmpl.h	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) )
9		rhmcomulmpl.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
10		rhmcomulmpl.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
11		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
12		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
13	11 12	rhmf	⊢ ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐻 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
14	8 13	syl	⊢ ( 𝜑 → 𝐻 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
15		eqid	⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
16		rhmrcl1	⊢ ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑅 ∈ Ring )
17	8 16	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
18	1 11 3 15 9	mplelf	⊢ ( 𝜑 → 𝐹 : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
19	1 11 3 15 10	mplelf	⊢ ( 𝜑 → 𝐺 : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
20	15 17 18 19	rhmmpllem2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
21	14 20	cofmpt	⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) ) ) = ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝐻 ‘ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) ) ) )
22		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
23	17	ringcmnd	⊢ ( 𝜑 → 𝑅 ∈ CMnd )
24	23	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → 𝑅 ∈ CMnd )
25		rhmrcl2	⊢ ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑆 ∈ Ring )
26	8 25	syl	⊢ ( 𝜑 → 𝑆 ∈ Ring )
27	26	ringgrpd	⊢ ( 𝜑 → 𝑆 ∈ Grp )
28	27	grpmndd	⊢ ( 𝜑 → 𝑆 ∈ Mnd )
29	28	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → 𝑆 ∈ Mnd )
30		ovex	⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
31	30	rabex	⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∈ V
32	31	rabex	⊢ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ∈ V
33	32	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ∈ V )
34		rhmghm	⊢ ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐻 ∈ ( 𝑅 GrpHom 𝑆 ) )
35		ghmmhm	⊢ ( 𝐻 ∈ ( 𝑅 GrpHom 𝑆 ) → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
36	8 34 35	3syl	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
37	36	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
38		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
39	17	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → 𝑅 ∈ Ring )
40	18	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → 𝐹 : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
41		breq1	⊢ ( 𝑒 = 𝑑 → ( 𝑒 ∘r ≤ 𝑘 ↔ 𝑑 ∘r ≤ 𝑘 ) )
42	41	elrab	⊢ ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↔ ( 𝑑 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∧ 𝑑 ∘r ≤ 𝑘 ) )
43	42	biimpi	⊢ ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } → ( 𝑑 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∧ 𝑑 ∘r ≤ 𝑘 ) )
44	43	adantl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → ( 𝑑 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∧ 𝑑 ∘r ≤ 𝑘 ) )
45	44	simpld	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → 𝑑 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } )
46	40 45	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → ( 𝐹 ‘ 𝑑 ) ∈ ( Base ‘ 𝑅 ) )
47	19	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → 𝐺 : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
48		simplr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } )
49	15	psrbagf	⊢ ( 𝑑 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } → 𝑑 : 𝐼 ⟶ ℕ0 )
50	45 49	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → 𝑑 : 𝐼 ⟶ ℕ0 )
51	44	simprd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → 𝑑 ∘r ≤ 𝑘 )
52	15	psrbagcon	⊢ ( ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∧ 𝑑 : 𝐼 ⟶ ℕ0 ∧ 𝑑 ∘r ≤ 𝑘 ) → ( ( 𝑘 ∘f − 𝑑 ) ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∧ ( 𝑘 ∘f − 𝑑 ) ∘r ≤ 𝑘 ) )
53	48 50 51 52	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → ( ( 𝑘 ∘f − 𝑑 ) ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∧ ( 𝑘 ∘f − 𝑑 ) ∘r ≤ 𝑘 ) )
54	53	simpld	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑑 ) ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } )
55	47 54	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ∈ ( Base ‘ 𝑅 ) )
56	11 38 39 46 55	ringcld	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ∈ ( Base ‘ 𝑅 ) )
57	15 17 18 19	rhmmpllem1	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) finSupp ( 0g ‘ 𝑅 ) )
58	11 22 24 29 33 37 56 57	gsummptmhm	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑆 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( 𝐻 ‘ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) ) = ( 𝐻 ‘ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) ) )
59	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) )
60		eqid	⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
61	11 38 60	rhmmul	⊢ ( ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ( 𝐹 ‘ 𝑑 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝐻 ‘ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) = ( ( 𝐻 ‘ ( 𝐹 ‘ 𝑑 ) ) ( .r ‘ 𝑆 ) ( 𝐻 ‘ ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) )
62	59 46 55 61	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → ( 𝐻 ‘ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) = ( ( 𝐻 ‘ ( 𝐹 ‘ 𝑑 ) ) ( .r ‘ 𝑆 ) ( 𝐻 ‘ ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) )
63	40 45	fvco3d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑑 ) = ( 𝐻 ‘ ( 𝐹 ‘ 𝑑 ) ) )
64	47 54	fvco3d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → ( ( 𝐻 ∘ 𝐺 ) ‘ ( 𝑘 ∘f − 𝑑 ) ) = ( 𝐻 ‘ ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) )
65	63 64	oveq12d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → ( ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑑 ) ( .r ‘ 𝑆 ) ( ( 𝐻 ∘ 𝐺 ) ‘ ( 𝑘 ∘f − 𝑑 ) ) ) = ( ( 𝐻 ‘ ( 𝐹 ‘ 𝑑 ) ) ( .r ‘ 𝑆 ) ( 𝐻 ‘ ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) )
66	62 65	eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → ( 𝐻 ‘ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) = ( ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑑 ) ( .r ‘ 𝑆 ) ( ( 𝐻 ∘ 𝐺 ) ‘ ( 𝑘 ∘f − 𝑑 ) ) ) )
67	66	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( 𝐻 ‘ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) = ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑑 ) ( .r ‘ 𝑆 ) ( ( 𝐻 ∘ 𝐺 ) ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) )
68	67	oveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑆 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( 𝐻 ‘ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) ) = ( 𝑆 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑑 ) ( .r ‘ 𝑆 ) ( ( 𝐻 ∘ 𝐺 ) ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) )
69	58 68	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝐻 ‘ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) ) = ( 𝑆 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑑 ) ( .r ‘ 𝑆 ) ( ( 𝐻 ∘ 𝐺 ) ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) )
70	69	mpteq2dva	⊢ ( 𝜑 → ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝐻 ‘ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) ) ) = ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝑆 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑑 ) ( .r ‘ 𝑆 ) ( ( 𝐻 ∘ 𝐺 ) ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) ) )
71	21 70	eqtrd	⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) ) ) = ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝑆 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑑 ) ( .r ‘ 𝑆 ) ( ( 𝐻 ∘ 𝐺 ) ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) ) )
72	1 3 38 5 15 9 10	mplmul	⊢ ( 𝜑 → ( 𝐹 · 𝐺 ) = ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) ) )
73	72	coeq2d	⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝐹 · 𝐺 ) ) = ( 𝐻 ∘ ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( 𝐹 ‘ 𝑑 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) ) ) )
74	1 2 3 4 7 36 9	mhmcompl	⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) ∈ 𝐶 )
75	1 2 3 4 7 36 10	mhmcompl	⊢ ( 𝜑 → ( 𝐻 ∘ 𝐺 ) ∈ 𝐶 )
76	2 4 60 6 15 74 75	mplmul	⊢ ( 𝜑 → ( ( 𝐻 ∘ 𝐹 ) ∙ ( 𝐻 ∘ 𝐺 ) ) = ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝑆 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑑 ) ( .r ‘ 𝑆 ) ( ( 𝐻 ∘ 𝐺 ) ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) ) )
77	71 73 76	3eqtr4d	⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝐹 · 𝐺 ) ) = ( ( 𝐻 ∘ 𝐹 ) ∙ ( 𝐻 ∘ 𝐺 ) ) )