Step | Hyp | Ref
| Expression |
1 | | ghmgrp.f |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) |
2 | | ghmgrp.x |
. . 3
⊢ 𝑋 = (Base‘𝐺) |
3 | | ghmgrp.y |
. . 3
⊢ 𝑌 = (Base‘𝐻) |
4 | | ghmgrp.p |
. . 3
⊢ + =
(+g‘𝐺) |
5 | | ghmgrp.q |
. . 3
⊢ ⨣ =
(+g‘𝐻) |
6 | | ghmgrp.1 |
. . 3
⊢ (𝜑 → 𝐹:𝑋–onto→𝑌) |
7 | | ghmgrp.3 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ Grp) |
8 | | grpmnd 18102 |
. . . 4
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) |
9 | 7, 8 | syl 17 |
. . 3
⊢ (𝜑 → 𝐺 ∈ Mnd) |
10 | 1, 2, 3, 4, 5, 6, 9 | mhmmnd 18213 |
. 2
⊢ (𝜑 → 𝐻 ∈ Mnd) |
11 | | fof 6565 |
. . . . . . . 8
⊢ (𝐹:𝑋–onto→𝑌 → 𝐹:𝑋⟶𝑌) |
12 | 6, 11 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝑋⟶𝑌) |
13 | 12 | ad3antrrr 729 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) ∧ (𝐹‘𝑖) = 𝑎) → 𝐹:𝑋⟶𝑌) |
14 | 7 | ad3antrrr 729 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) ∧ (𝐹‘𝑖) = 𝑎) → 𝐺 ∈ Grp) |
15 | | simplr 768 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) ∧ (𝐹‘𝑖) = 𝑎) → 𝑖 ∈ 𝑋) |
16 | | eqid 2798 |
. . . . . . . 8
⊢
(invg‘𝐺) = (invg‘𝐺) |
17 | 2, 16 | grpinvcl 18143 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑖 ∈ 𝑋) → ((invg‘𝐺)‘𝑖) ∈ 𝑋) |
18 | 14, 15, 17 | syl2anc 587 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) ∧ (𝐹‘𝑖) = 𝑎) → ((invg‘𝐺)‘𝑖) ∈ 𝑋) |
19 | 13, 18 | ffvelrnd 6829 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) ∧ (𝐹‘𝑖) = 𝑎) → (𝐹‘((invg‘𝐺)‘𝑖)) ∈ 𝑌) |
20 | 1 | 3adant1r 1174 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) |
21 | 7, 17 | sylan 583 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((invg‘𝐺)‘𝑖) ∈ 𝑋) |
22 | | simpr 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋) |
23 | 20, 21, 22 | mhmlem 18211 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐹‘(((invg‘𝐺)‘𝑖) + 𝑖)) = ((𝐹‘((invg‘𝐺)‘𝑖)) ⨣ (𝐹‘𝑖))) |
24 | 23 | ad4ant13 750 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) ∧ (𝐹‘𝑖) = 𝑎) → (𝐹‘(((invg‘𝐺)‘𝑖) + 𝑖)) = ((𝐹‘((invg‘𝐺)‘𝑖)) ⨣ (𝐹‘𝑖))) |
25 | | eqid 2798 |
. . . . . . . . . 10
⊢
(0g‘𝐺) = (0g‘𝐺) |
26 | 2, 4, 25, 16 | grplinv 18144 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝑖 ∈ 𝑋) → (((invg‘𝐺)‘𝑖) + 𝑖) = (0g‘𝐺)) |
27 | 26 | fveq2d 6649 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑖 ∈ 𝑋) → (𝐹‘(((invg‘𝐺)‘𝑖) + 𝑖)) = (𝐹‘(0g‘𝐺))) |
28 | 14, 15, 27 | syl2anc 587 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) ∧ (𝐹‘𝑖) = 𝑎) → (𝐹‘(((invg‘𝐺)‘𝑖) + 𝑖)) = (𝐹‘(0g‘𝐺))) |
29 | 1, 2, 3, 4, 5, 6, 9, 25 | mhmid 18212 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘(0g‘𝐺)) = (0g‘𝐻)) |
30 | 29 | ad3antrrr 729 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) ∧ (𝐹‘𝑖) = 𝑎) → (𝐹‘(0g‘𝐺)) = (0g‘𝐻)) |
31 | 28, 30 | eqtrd 2833 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) ∧ (𝐹‘𝑖) = 𝑎) → (𝐹‘(((invg‘𝐺)‘𝑖) + 𝑖)) = (0g‘𝐻)) |
32 | | simpr 488 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) ∧ (𝐹‘𝑖) = 𝑎) → (𝐹‘𝑖) = 𝑎) |
33 | 32 | oveq2d 7151 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) ∧ (𝐹‘𝑖) = 𝑎) → ((𝐹‘((invg‘𝐺)‘𝑖)) ⨣ (𝐹‘𝑖)) = ((𝐹‘((invg‘𝐺)‘𝑖)) ⨣ 𝑎)) |
34 | 24, 31, 33 | 3eqtr3rd 2842 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) ∧ (𝐹‘𝑖) = 𝑎) → ((𝐹‘((invg‘𝐺)‘𝑖)) ⨣ 𝑎) = (0g‘𝐻)) |
35 | | oveq1 7142 |
. . . . . . 7
⊢ (𝑓 = (𝐹‘((invg‘𝐺)‘𝑖)) → (𝑓 ⨣ 𝑎) = ((𝐹‘((invg‘𝐺)‘𝑖)) ⨣ 𝑎)) |
36 | 35 | eqeq1d 2800 |
. . . . . 6
⊢ (𝑓 = (𝐹‘((invg‘𝐺)‘𝑖)) → ((𝑓 ⨣ 𝑎) = (0g‘𝐻) ↔ ((𝐹‘((invg‘𝐺)‘𝑖)) ⨣ 𝑎) = (0g‘𝐻))) |
37 | 36 | rspcev 3571 |
. . . . 5
⊢ (((𝐹‘((invg‘𝐺)‘𝑖)) ∈ 𝑌 ∧ ((𝐹‘((invg‘𝐺)‘𝑖)) ⨣ 𝑎) = (0g‘𝐻)) → ∃𝑓 ∈ 𝑌 (𝑓 ⨣ 𝑎) = (0g‘𝐻)) |
38 | 19, 34, 37 | syl2anc 587 |
. . . 4
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) ∧ (𝐹‘𝑖) = 𝑎) → ∃𝑓 ∈ 𝑌 (𝑓 ⨣ 𝑎) = (0g‘𝐻)) |
39 | | foelrni 6702 |
. . . . 5
⊢ ((𝐹:𝑋–onto→𝑌 ∧ 𝑎 ∈ 𝑌) → ∃𝑖 ∈ 𝑋 (𝐹‘𝑖) = 𝑎) |
40 | 6, 39 | sylan 583 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑌) → ∃𝑖 ∈ 𝑋 (𝐹‘𝑖) = 𝑎) |
41 | 38, 40 | r19.29a 3248 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑌) → ∃𝑓 ∈ 𝑌 (𝑓 ⨣ 𝑎) = (0g‘𝐻)) |
42 | 41 | ralrimiva 3149 |
. 2
⊢ (𝜑 → ∀𝑎 ∈ 𝑌 ∃𝑓 ∈ 𝑌 (𝑓 ⨣ 𝑎) = (0g‘𝐻)) |
43 | | eqid 2798 |
. . 3
⊢
(0g‘𝐻) = (0g‘𝐻) |
44 | 3, 5, 43 | isgrp 18101 |
. 2
⊢ (𝐻 ∈ Grp ↔ (𝐻 ∈ Mnd ∧ ∀𝑎 ∈ 𝑌 ∃𝑓 ∈ 𝑌 (𝑓 ⨣ 𝑎) = (0g‘𝐻))) |
45 | 10, 42, 44 | sylanbrc 586 |
1
⊢ (𝜑 → 𝐻 ∈ Grp) |