| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | rhmcomulmpl.h | . . . . 5
⊢ (𝜑 → 𝐻 ∈ (𝑅 RingHom 𝑆)) | 
| 2 |  | eqid 2736 | . . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 3 |  | eqid 2736 | . . . . . 6
⊢
(Base‘𝑆) =
(Base‘𝑆) | 
| 4 | 2, 3 | rhmf 20486 | . . . . 5
⊢ (𝐻 ∈ (𝑅 RingHom 𝑆) → 𝐻:(Base‘𝑅)⟶(Base‘𝑆)) | 
| 5 | 1, 4 | syl 17 | . . . 4
⊢ (𝜑 → 𝐻:(Base‘𝑅)⟶(Base‘𝑆)) | 
| 6 |  | eqid 2736 | . . . . 5
⊢ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin} | 
| 7 |  | rhmrcl1 20477 | . . . . . 6
⊢ (𝐻 ∈ (𝑅 RingHom 𝑆) → 𝑅 ∈ Ring) | 
| 8 | 1, 7 | syl 17 | . . . . 5
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 9 |  | rhmcomulmpl.p | . . . . . 6
⊢ 𝑃 = (𝐼 mPoly 𝑅) | 
| 10 |  | rhmcomulmpl.b | . . . . . 6
⊢ 𝐵 = (Base‘𝑃) | 
| 11 |  | rhmcomulmpl.f | . . . . . 6
⊢ (𝜑 → 𝐹 ∈ 𝐵) | 
| 12 | 9, 2, 10, 6, 11 | mplelf 22019 | . . . . 5
⊢ (𝜑 → 𝐹:{𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) | 
| 13 |  | rhmcomulmpl.g | . . . . . 6
⊢ (𝜑 → 𝐺 ∈ 𝐵) | 
| 14 | 9, 2, 10, 6, 13 | mplelf 22019 | . . . . 5
⊢ (𝜑 → 𝐺:{𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) | 
| 15 | 6, 8, 12, 14 | rhmpsrlem2 21962 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑅 Σg
(𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑘 ∘f − 𝑑))))) ∈ (Base‘𝑅)) | 
| 16 | 5, 15 | cofmpt 7151 | . . 3
⊢ (𝜑 → (𝐻 ∘ (𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ (𝑅 Σg
(𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑘 ∘f − 𝑑))))))) = (𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ (𝐻‘(𝑅 Σg (𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑘 ∘f − 𝑑)))))))) | 
| 17 |  | eqid 2736 | . . . . . 6
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 18 | 8 | ringcmnd 20282 | . . . . . . 7
⊢ (𝜑 → 𝑅 ∈ CMnd) | 
| 19 | 18 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑅 ∈ CMnd) | 
| 20 |  | rhmrcl2 20478 | . . . . . . . . . 10
⊢ (𝐻 ∈ (𝑅 RingHom 𝑆) → 𝑆 ∈ Ring) | 
| 21 | 1, 20 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ Ring) | 
| 22 | 21 | ringgrpd 20240 | . . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ Grp) | 
| 23 | 22 | grpmndd 18965 | . . . . . . 7
⊢ (𝜑 → 𝑆 ∈ Mnd) | 
| 24 | 23 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑆 ∈ Mnd) | 
| 25 |  | ovex 7465 | . . . . . . . . 9
⊢
(ℕ0 ↑m 𝐼) ∈ V | 
| 26 | 25 | rabex 5338 | . . . . . . . 8
⊢ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∈
V | 
| 27 | 26 | rabex 5338 | . . . . . . 7
⊢ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘} ∈ V | 
| 28 | 27 | a1i 11 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘} ∈ V) | 
| 29 |  | rhmghm 20485 | . . . . . . . 8
⊢ (𝐻 ∈ (𝑅 RingHom 𝑆) → 𝐻 ∈ (𝑅 GrpHom 𝑆)) | 
| 30 |  | ghmmhm 19245 | . . . . . . . 8
⊢ (𝐻 ∈ (𝑅 GrpHom 𝑆) → 𝐻 ∈ (𝑅 MndHom 𝑆)) | 
| 31 | 1, 29, 30 | 3syl 18 | . . . . . . 7
⊢ (𝜑 → 𝐻 ∈ (𝑅 MndHom 𝑆)) | 
| 32 | 31 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝐻 ∈ (𝑅 MndHom 𝑆)) | 
| 33 |  | eqid 2736 | . . . . . . 7
⊢
(.r‘𝑅) = (.r‘𝑅) | 
| 34 | 8 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘}) → 𝑅 ∈ Ring) | 
| 35 |  | elrabi 3686 | . . . . . . . . 9
⊢ (𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘} → 𝑑 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}) | 
| 36 | 12 | ffvelcdmda 7103 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑑 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝐹‘𝑑) ∈ (Base‘𝑅)) | 
| 37 | 35, 36 | sylan2 593 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘}) → (𝐹‘𝑑) ∈ (Base‘𝑅)) | 
| 38 | 37 | adantlr 715 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘}) → (𝐹‘𝑑) ∈ (Base‘𝑅)) | 
| 39 | 14 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘}) → 𝐺:{𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) | 
| 40 |  | eqid 2736 | . . . . . . . . . . 11
⊢ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘} = {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘} | 
| 41 | 6, 40 | psrbagconcl 21948 | . . . . . . . . . 10
⊢ ((𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∧ 𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘}) → (𝑘 ∘f − 𝑑) ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘}) | 
| 42 |  | elrabi 3686 | . . . . . . . . . 10
⊢ ((𝑘 ∘f −
𝑑) ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘} → (𝑘 ∘f − 𝑑) ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}) | 
| 43 | 41, 42 | syl 17 | . . . . . . . . 9
⊢ ((𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∧ 𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘}) → (𝑘 ∘f − 𝑑) ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}) | 
| 44 | 43 | adantll 714 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘}) → (𝑘 ∘f − 𝑑) ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}) | 
| 45 | 39, 44 | ffvelcdmd 7104 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘}) → (𝐺‘(𝑘 ∘f − 𝑑)) ∈ (Base‘𝑅)) | 
| 46 | 2, 33, 34, 38, 45 | ringcld 20258 | . . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘}) → ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑘 ∘f − 𝑑))) ∈ (Base‘𝑅)) | 
| 47 | 6, 8, 12, 14 | rhmpsrlem1 21961 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑘 ∘f − 𝑑)))) finSupp
(0g‘𝑅)) | 
| 48 | 2, 17, 19, 24, 28, 32, 46, 47 | gsummptmhm 19959 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑆 Σg
(𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘} ↦ (𝐻‘((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑘 ∘f − 𝑑)))))) = (𝐻‘(𝑅 Σg (𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑘 ∘f − 𝑑))))))) | 
| 49 | 1 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘}) → 𝐻 ∈ (𝑅 RingHom 𝑆)) | 
| 50 |  | eqid 2736 | . . . . . . . . . 10
⊢
(.r‘𝑆) = (.r‘𝑆) | 
| 51 | 2, 33, 50 | rhmmul 20487 | . . . . . . . . 9
⊢ ((𝐻 ∈ (𝑅 RingHom 𝑆) ∧ (𝐹‘𝑑) ∈ (Base‘𝑅) ∧ (𝐺‘(𝑘 ∘f − 𝑑)) ∈ (Base‘𝑅)) → (𝐻‘((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑘 ∘f − 𝑑)))) = ((𝐻‘(𝐹‘𝑑))(.r‘𝑆)(𝐻‘(𝐺‘(𝑘 ∘f − 𝑑))))) | 
| 52 | 49, 38, 45, 51 | syl3anc 1372 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘}) → (𝐻‘((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑘 ∘f − 𝑑)))) = ((𝐻‘(𝐹‘𝑑))(.r‘𝑆)(𝐻‘(𝐺‘(𝑘 ∘f − 𝑑))))) | 
| 53 | 12 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘}) → 𝐹:{𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) | 
| 54 | 35 | adantl 481 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘}) → 𝑑 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}) | 
| 55 | 53, 54 | fvco3d 7008 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘}) → ((𝐻 ∘ 𝐹)‘𝑑) = (𝐻‘(𝐹‘𝑑))) | 
| 56 | 39, 44 | fvco3d 7008 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘}) → ((𝐻 ∘ 𝐺)‘(𝑘 ∘f − 𝑑)) = (𝐻‘(𝐺‘(𝑘 ∘f − 𝑑)))) | 
| 57 | 55, 56 | oveq12d 7450 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘}) → (((𝐻 ∘ 𝐹)‘𝑑)(.r‘𝑆)((𝐻 ∘ 𝐺)‘(𝑘 ∘f − 𝑑))) = ((𝐻‘(𝐹‘𝑑))(.r‘𝑆)(𝐻‘(𝐺‘(𝑘 ∘f − 𝑑))))) | 
| 58 | 52, 57 | eqtr4d 2779 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘}) → (𝐻‘((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑘 ∘f − 𝑑)))) = (((𝐻 ∘ 𝐹)‘𝑑)(.r‘𝑆)((𝐻 ∘ 𝐺)‘(𝑘 ∘f − 𝑑)))) | 
| 59 | 58 | mpteq2dva 5241 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘} ↦ (𝐻‘((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑘 ∘f − 𝑑))))) = (𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘} ↦ (((𝐻 ∘ 𝐹)‘𝑑)(.r‘𝑆)((𝐻 ∘ 𝐺)‘(𝑘 ∘f − 𝑑))))) | 
| 60 | 59 | oveq2d 7448 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑆 Σg
(𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘} ↦ (𝐻‘((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑘 ∘f − 𝑑)))))) = (𝑆 Σg (𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘} ↦ (((𝐻 ∘ 𝐹)‘𝑑)(.r‘𝑆)((𝐻 ∘ 𝐺)‘(𝑘 ∘f − 𝑑)))))) | 
| 61 | 48, 60 | eqtr3d 2778 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝐻‘(𝑅 Σg (𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑘 ∘f − 𝑑)))))) = (𝑆 Σg (𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘} ↦ (((𝐻 ∘ 𝐹)‘𝑑)(.r‘𝑆)((𝐻 ∘ 𝐺)‘(𝑘 ∘f − 𝑑)))))) | 
| 62 | 61 | mpteq2dva 5241 | . . 3
⊢ (𝜑 → (𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ (𝐻‘(𝑅 Σg (𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑘 ∘f − 𝑑))))))) = (𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ (𝑆 Σg
(𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘} ↦ (((𝐻 ∘ 𝐹)‘𝑑)(.r‘𝑆)((𝐻 ∘ 𝐺)‘(𝑘 ∘f − 𝑑))))))) | 
| 63 | 16, 62 | eqtrd 2776 | . 2
⊢ (𝜑 → (𝐻 ∘ (𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ (𝑅 Σg
(𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑘 ∘f − 𝑑))))))) = (𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ (𝑆 Σg
(𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘} ↦ (((𝐻 ∘ 𝐹)‘𝑑)(.r‘𝑆)((𝐻 ∘ 𝐺)‘(𝑘 ∘f − 𝑑))))))) | 
| 64 |  | rhmcomulmpl.1 | . . . 4
⊢  · =
(.r‘𝑃) | 
| 65 | 9, 10, 33, 64, 6, 11, 13 | mplmul 22032 | . . 3
⊢ (𝜑 → (𝐹 · 𝐺) = (𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ (𝑅 Σg
(𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑘 ∘f − 𝑑))))))) | 
| 66 | 65 | coeq2d 5872 | . 2
⊢ (𝜑 → (𝐻 ∘ (𝐹 · 𝐺)) = (𝐻 ∘ (𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ (𝑅 Σg
(𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑘 ∘f − 𝑑)))))))) | 
| 67 |  | rhmcomulmpl.q | . . 3
⊢ 𝑄 = (𝐼 mPoly 𝑆) | 
| 68 |  | rhmcomulmpl.c | . . 3
⊢ 𝐶 = (Base‘𝑄) | 
| 69 |  | rhmcomulmpl.2 | . . 3
⊢  ∙ =
(.r‘𝑄) | 
| 70 | 9, 67, 10, 68, 31, 11 | mhmcompl 22385 | . . 3
⊢ (𝜑 → (𝐻 ∘ 𝐹) ∈ 𝐶) | 
| 71 | 9, 67, 10, 68, 31, 13 | mhmcompl 22385 | . . 3
⊢ (𝜑 → (𝐻 ∘ 𝐺) ∈ 𝐶) | 
| 72 | 67, 68, 50, 69, 6, 70, 71 | mplmul 22032 | . 2
⊢ (𝜑 → ((𝐻 ∘ 𝐹) ∙ (𝐻 ∘ 𝐺)) = (𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ (𝑆 Σg
(𝑑 ∈ {𝑒 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑒 ∘r ≤ 𝑘} ↦ (((𝐻 ∘ 𝐹)‘𝑑)(.r‘𝑆)((𝐻 ∘ 𝐺)‘(𝑘 ∘f − 𝑑))))))) | 
| 73 | 63, 66, 72 | 3eqtr4d 2786 | 1
⊢ (𝜑 → (𝐻 ∘ (𝐹 · 𝐺)) = ((𝐻 ∘ 𝐹) ∙ (𝐻 ∘ 𝐺))) |