Step |
Hyp |
Ref |
Expression |
1 |
|
mhpaddcl.h |
⊢ 𝐻 = ( 𝐼 mHomP 𝑅 ) |
2 |
|
mhpaddcl.p |
⊢ 𝑃 = ( 𝐼 mPoly 𝑅 ) |
3 |
|
mhpaddcl.a |
⊢ + = ( +g ‘ 𝑃 ) |
4 |
|
mhpaddcl.r |
⊢ ( 𝜑 → 𝑅 ∈ Grp ) |
5 |
|
mhpaddcl.n |
⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) |
6 |
|
mhpaddcl.x |
⊢ ( 𝜑 → 𝑋 ∈ ( 𝐻 ‘ 𝑁 ) ) |
7 |
|
mhpaddcl.y |
⊢ ( 𝜑 → 𝑌 ∈ ( 𝐻 ‘ 𝑁 ) ) |
8 |
|
eqid |
⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 ) |
9 |
|
eqid |
⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) |
10 |
|
eqid |
⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } |
11 |
|
reldmmhp |
⊢ Rel dom mHomP |
12 |
11 1 6
|
elfvov1 |
⊢ ( 𝜑 → 𝐼 ∈ V ) |
13 |
2
|
mplgrp |
⊢ ( ( 𝐼 ∈ V ∧ 𝑅 ∈ Grp ) → 𝑃 ∈ Grp ) |
14 |
12 4 13
|
syl2anc |
⊢ ( 𝜑 → 𝑃 ∈ Grp ) |
15 |
1 2 8 12 4 5 6
|
mhpmpl |
⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑃 ) ) |
16 |
1 2 8 12 4 5 7
|
mhpmpl |
⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝑃 ) ) |
17 |
8 3
|
grpcl |
⊢ ( ( 𝑃 ∈ Grp ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ∧ 𝑌 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑋 + 𝑌 ) ∈ ( Base ‘ 𝑃 ) ) |
18 |
14 15 16 17
|
syl3anc |
⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ ( Base ‘ 𝑃 ) ) |
19 |
|
eqid |
⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 ) |
20 |
2 8 19 3 15 16
|
mpladd |
⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) = ( 𝑋 ∘f ( +g ‘ 𝑅 ) 𝑌 ) ) |
21 |
20
|
oveq1d |
⊢ ( 𝜑 → ( ( 𝑋 + 𝑌 ) supp ( 0g ‘ 𝑅 ) ) = ( ( 𝑋 ∘f ( +g ‘ 𝑅 ) 𝑌 ) supp ( 0g ‘ 𝑅 ) ) ) |
22 |
|
ovexd |
⊢ ( 𝜑 → ( ℕ0 ↑m 𝐼 ) ∈ V ) |
23 |
10 22
|
rabexd |
⊢ ( 𝜑 → { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∈ V ) |
24 |
|
eqid |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) |
25 |
24 9
|
grpidcl |
⊢ ( 𝑅 ∈ Grp → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) |
26 |
4 25
|
syl |
⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) |
27 |
2 24 8 10 15
|
mplelf |
⊢ ( 𝜑 → 𝑋 : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) ) |
28 |
2 24 8 10 16
|
mplelf |
⊢ ( 𝜑 → 𝑌 : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) ) |
29 |
24 19 9
|
grplid |
⊢ ( ( 𝑅 ∈ Grp ∧ ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) ) |
30 |
4 26 29
|
syl2anc |
⊢ ( 𝜑 → ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) ) |
31 |
23 26 27 28 30
|
suppofssd |
⊢ ( 𝜑 → ( ( 𝑋 ∘f ( +g ‘ 𝑅 ) 𝑌 ) supp ( 0g ‘ 𝑅 ) ) ⊆ ( ( 𝑋 supp ( 0g ‘ 𝑅 ) ) ∪ ( 𝑌 supp ( 0g ‘ 𝑅 ) ) ) ) |
32 |
21 31
|
eqsstrd |
⊢ ( 𝜑 → ( ( 𝑋 + 𝑌 ) supp ( 0g ‘ 𝑅 ) ) ⊆ ( ( 𝑋 supp ( 0g ‘ 𝑅 ) ) ∪ ( 𝑌 supp ( 0g ‘ 𝑅 ) ) ) ) |
33 |
1 9 10 12 4 5 6
|
mhpdeg |
⊢ ( 𝜑 → ( 𝑋 supp ( 0g ‘ 𝑅 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) |
34 |
1 9 10 12 4 5 7
|
mhpdeg |
⊢ ( 𝜑 → ( 𝑌 supp ( 0g ‘ 𝑅 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) |
35 |
33 34
|
unssd |
⊢ ( 𝜑 → ( ( 𝑋 supp ( 0g ‘ 𝑅 ) ) ∪ ( 𝑌 supp ( 0g ‘ 𝑅 ) ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) |
36 |
32 35
|
sstrd |
⊢ ( 𝜑 → ( ( 𝑋 + 𝑌 ) supp ( 0g ‘ 𝑅 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) |
37 |
1 2 8 9 10 12 4 5 18 36
|
ismhp2 |
⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ ( 𝐻 ‘ 𝑁 ) ) |