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 |
⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝐹 · 𝐺 ) ) = ( ( 𝐻 ∘ 𝐹 ) ∙ ( 𝐻 ∘ 𝐺 ) ) ) |