Metamath Proof Explorer

Theorem rhmcomulpsr

Description: Show that the ring homomorphism in rhmpsr preserves multiplication. (Contributed by SN, 18-May-2025)

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

Proof

Step Hyp Ref Expression
1 rhmcomulpsr.p ⊢ 𝑃 = ( 𝐼 mPwSer 𝑅 )
2 rhmcomulpsr.q ⊢ 𝑄 = ( 𝐼 mPwSer 𝑆 )
3 rhmcomulpsr.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
4 rhmcomulpsr.c ⊢ 𝐶 = ( Base ‘ 𝑄 )
5 rhmcomulpsr.1 ⊢ · = ( .r ‘ 𝑃 )
6 rhmcomulpsr.2 ⊢ ∙ = ( .r ‘ 𝑄 )
7 rhmcomulpsr.h ⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) )
8 rhmcomulpsr.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
9 rhmcomulpsr.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 14 3 8 psrelbas ⊢ ( 𝜑 → 𝐹 : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
18 1 10 14 3 9 psrelbas ⊢ ( 𝜑 → 𝐺 : { 𝑓 ∈ ( ℕ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 45 adantll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑑 ) ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } )
47 elrabi ⊢ ( ( 𝑘 ∘f − 𝑑 ) ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } → ( 𝑘 ∘f − 𝑑 ) ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } )
48 46 47 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ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 psrmulfval ⊢ ( 𝜑 → ( 𝐹 · 𝐺 ) = ( 𝑘 ∈ { 𝑓 ∈ ( ℕ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 mhmcopsr ⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) ∈ 𝐶 )
71 1 2 3 4 35 9 mhmcopsr ⊢ ( 𝜑 → ( 𝐻 ∘ 𝐺 ) ∈ 𝐶 )
72 2 4 54 6 14 70 71 psrmulfval ⊢ ( 𝜑 → ( ( 𝐻 ∘ 𝐹 ) ∙ ( 𝐻 ∘ 𝐺 ) ) = ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝑆 Σg ( 𝑑 ∈ { 𝑒 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑒 ∘r ≤ 𝑘 } ↦ ( ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑑 ) ( .r ‘ 𝑆 ) ( ( 𝐻 ∘ 𝐺 ) ‘ ( 𝑘 ∘f − 𝑑 ) ) ) ) ) ) )
73 67 69 72 3eqtr4d ⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝐹 · 𝐺 ) ) = ( ( 𝐻 ∘ 𝐹 ) ∙ ( 𝐻 ∘ 𝐺 ) ) )