| Step |
Hyp |
Ref |
Expression |
| 1 |
|
mhpsubg.h |
⊢ 𝐻 = ( 𝐼 mHomP 𝑅 ) |
| 2 |
|
mhpsubg.p |
⊢ 𝑃 = ( 𝐼 mPoly 𝑅 ) |
| 3 |
|
mhpsubg.i |
⊢ ( 𝜑 → 𝐼 ∈ 𝑉 ) |
| 4 |
|
mhpsubg.r |
⊢ ( 𝜑 → 𝑅 ∈ Grp ) |
| 5 |
|
mhpsubg.n |
⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) |
| 6 |
|
eqid |
⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 ) |
| 7 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) |
| 8 |
1 2 6 7
|
mhpmpl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑥 ∈ ( Base ‘ 𝑃 ) ) |
| 9 |
8
|
ex |
⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) → 𝑥 ∈ ( Base ‘ 𝑃 ) ) ) |
| 10 |
9
|
ssrdv |
⊢ ( 𝜑 → ( 𝐻 ‘ 𝑁 ) ⊆ ( Base ‘ 𝑃 ) ) |
| 11 |
|
eqid |
⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) |
| 12 |
|
eqid |
⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } |
| 13 |
1 11 12 3 4 5
|
mhp0cl |
⊢ ( 𝜑 → ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( 0g ‘ 𝑅 ) } ) ∈ ( 𝐻 ‘ 𝑁 ) ) |
| 14 |
13
|
ne0d |
⊢ ( 𝜑 → ( 𝐻 ‘ 𝑁 ) ≠ ∅ ) |
| 15 |
|
eqid |
⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 ) |
| 16 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑅 ∈ Grp ) |
| 17 |
16
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑅 ∈ Grp ) |
| 18 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) |
| 19 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ) |
| 20 |
1 2 15 17 18 19
|
mhpaddcl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ) → ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ∈ ( 𝐻 ‘ 𝑁 ) ) |
| 21 |
20
|
ralrimiva |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) → ∀ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ∈ ( 𝐻 ‘ 𝑁 ) ) |
| 22 |
|
eqid |
⊢ ( invg ‘ 𝑃 ) = ( invg ‘ 𝑃 ) |
| 23 |
1 2 22 16 7
|
mhpinvcl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) → ( ( invg ‘ 𝑃 ) ‘ 𝑥 ) ∈ ( 𝐻 ‘ 𝑁 ) ) |
| 24 |
21 23
|
jca |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) → ( ∀ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( invg ‘ 𝑃 ) ‘ 𝑥 ) ∈ ( 𝐻 ‘ 𝑁 ) ) ) |
| 25 |
24
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ( ∀ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( invg ‘ 𝑃 ) ‘ 𝑥 ) ∈ ( 𝐻 ‘ 𝑁 ) ) ) |
| 26 |
2
|
mplgrp |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Grp ) → 𝑃 ∈ Grp ) |
| 27 |
3 4 26
|
syl2anc |
⊢ ( 𝜑 → 𝑃 ∈ Grp ) |
| 28 |
6 15 22
|
issubg2 |
⊢ ( 𝑃 ∈ Grp → ( ( 𝐻 ‘ 𝑁 ) ∈ ( SubGrp ‘ 𝑃 ) ↔ ( ( 𝐻 ‘ 𝑁 ) ⊆ ( Base ‘ 𝑃 ) ∧ ( 𝐻 ‘ 𝑁 ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ( ∀ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( invg ‘ 𝑃 ) ‘ 𝑥 ) ∈ ( 𝐻 ‘ 𝑁 ) ) ) ) ) |
| 29 |
27 28
|
syl |
⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝑁 ) ∈ ( SubGrp ‘ 𝑃 ) ↔ ( ( 𝐻 ‘ 𝑁 ) ⊆ ( Base ‘ 𝑃 ) ∧ ( 𝐻 ‘ 𝑁 ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ( ∀ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( invg ‘ 𝑃 ) ‘ 𝑥 ) ∈ ( 𝐻 ‘ 𝑁 ) ) ) ) ) |
| 30 |
10 14 25 29
|
mpbir3and |
⊢ ( 𝜑 → ( 𝐻 ‘ 𝑁 ) ∈ ( SubGrp ‘ 𝑃 ) ) |