| 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 | 7 | grpmndd 18965 | . . 3
⊢ (𝜑 → 𝐺 ∈ Mnd) | 
| 9 | 1, 2, 3, 4, 5, 6, 8 | mhmmnd 19083 | . 2
⊢ (𝜑 → 𝐻 ∈ Mnd) | 
| 10 |  | fof 6819 | . . . . . . . 8
⊢ (𝐹:𝑋–onto→𝑌 → 𝐹:𝑋⟶𝑌) | 
| 11 | 6, 10 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝐹:𝑋⟶𝑌) | 
| 12 | 11 | ad3antrrr 730 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) ∧ (𝐹‘𝑖) = 𝑎) → 𝐹:𝑋⟶𝑌) | 
| 13 | 7 | ad3antrrr 730 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) ∧ (𝐹‘𝑖) = 𝑎) → 𝐺 ∈ Grp) | 
| 14 |  | simplr 768 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) ∧ (𝐹‘𝑖) = 𝑎) → 𝑖 ∈ 𝑋) | 
| 15 |  | eqid 2736 | . . . . . . . 8
⊢
(invg‘𝐺) = (invg‘𝐺) | 
| 16 | 2, 15 | grpinvcl 19006 | . . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑖 ∈ 𝑋) → ((invg‘𝐺)‘𝑖) ∈ 𝑋) | 
| 17 | 13, 14, 16 | syl2anc 584 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) ∧ (𝐹‘𝑖) = 𝑎) → ((invg‘𝐺)‘𝑖) ∈ 𝑋) | 
| 18 | 12, 17 | ffvelcdmd 7104 | . . . . 5
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) ∧ (𝐹‘𝑖) = 𝑎) → (𝐹‘((invg‘𝐺)‘𝑖)) ∈ 𝑌) | 
| 19 | 1 | 3adant1r 1177 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) | 
| 20 | 7, 16 | sylan 580 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((invg‘𝐺)‘𝑖) ∈ 𝑋) | 
| 21 |  | simpr 484 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋) | 
| 22 | 19, 20, 21 | mhmlem 19081 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐹‘(((invg‘𝐺)‘𝑖) + 𝑖)) = ((𝐹‘((invg‘𝐺)‘𝑖)) ⨣ (𝐹‘𝑖))) | 
| 23 | 22 | ad4ant13 751 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) ∧ (𝐹‘𝑖) = 𝑎) → (𝐹‘(((invg‘𝐺)‘𝑖) + 𝑖)) = ((𝐹‘((invg‘𝐺)‘𝑖)) ⨣ (𝐹‘𝑖))) | 
| 24 |  | eqid 2736 | . . . . . . . . . 10
⊢
(0g‘𝐺) = (0g‘𝐺) | 
| 25 | 2, 4, 24, 15 | grplinv 19008 | . . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝑖 ∈ 𝑋) → (((invg‘𝐺)‘𝑖) + 𝑖) = (0g‘𝐺)) | 
| 26 | 25 | fveq2d 6909 | . . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑖 ∈ 𝑋) → (𝐹‘(((invg‘𝐺)‘𝑖) + 𝑖)) = (𝐹‘(0g‘𝐺))) | 
| 27 | 13, 14, 26 | syl2anc 584 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) ∧ (𝐹‘𝑖) = 𝑎) → (𝐹‘(((invg‘𝐺)‘𝑖) + 𝑖)) = (𝐹‘(0g‘𝐺))) | 
| 28 | 1, 2, 3, 4, 5, 6, 8, 24 | mhmid 19082 | . . . . . . . 8
⊢ (𝜑 → (𝐹‘(0g‘𝐺)) = (0g‘𝐻)) | 
| 29 | 28 | ad3antrrr 730 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) ∧ (𝐹‘𝑖) = 𝑎) → (𝐹‘(0g‘𝐺)) = (0g‘𝐻)) | 
| 30 | 27, 29 | eqtrd 2776 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) ∧ (𝐹‘𝑖) = 𝑎) → (𝐹‘(((invg‘𝐺)‘𝑖) + 𝑖)) = (0g‘𝐻)) | 
| 31 |  | simpr 484 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) ∧ (𝐹‘𝑖) = 𝑎) → (𝐹‘𝑖) = 𝑎) | 
| 32 | 31 | oveq2d 7448 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) ∧ (𝐹‘𝑖) = 𝑎) → ((𝐹‘((invg‘𝐺)‘𝑖)) ⨣ (𝐹‘𝑖)) = ((𝐹‘((invg‘𝐺)‘𝑖)) ⨣ 𝑎)) | 
| 33 | 23, 30, 32 | 3eqtr3rd 2785 | . . . . 5
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) ∧ (𝐹‘𝑖) = 𝑎) → ((𝐹‘((invg‘𝐺)‘𝑖)) ⨣ 𝑎) = (0g‘𝐻)) | 
| 34 |  | oveq1 7439 | . . . . . . 7
⊢ (𝑓 = (𝐹‘((invg‘𝐺)‘𝑖)) → (𝑓 ⨣ 𝑎) = ((𝐹‘((invg‘𝐺)‘𝑖)) ⨣ 𝑎)) | 
| 35 | 34 | eqeq1d 2738 | . . . . . 6
⊢ (𝑓 = (𝐹‘((invg‘𝐺)‘𝑖)) → ((𝑓 ⨣ 𝑎) = (0g‘𝐻) ↔ ((𝐹‘((invg‘𝐺)‘𝑖)) ⨣ 𝑎) = (0g‘𝐻))) | 
| 36 | 35 | rspcev 3621 | . . . . 5
⊢ (((𝐹‘((invg‘𝐺)‘𝑖)) ∈ 𝑌 ∧ ((𝐹‘((invg‘𝐺)‘𝑖)) ⨣ 𝑎) = (0g‘𝐻)) → ∃𝑓 ∈ 𝑌 (𝑓 ⨣ 𝑎) = (0g‘𝐻)) | 
| 37 | 18, 33, 36 | syl2anc 584 | . . . 4
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) ∧ (𝐹‘𝑖) = 𝑎) → ∃𝑓 ∈ 𝑌 (𝑓 ⨣ 𝑎) = (0g‘𝐻)) | 
| 38 |  | foelcdmi 6969 | . . . . 5
⊢ ((𝐹:𝑋–onto→𝑌 ∧ 𝑎 ∈ 𝑌) → ∃𝑖 ∈ 𝑋 (𝐹‘𝑖) = 𝑎) | 
| 39 | 6, 38 | sylan 580 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑌) → ∃𝑖 ∈ 𝑋 (𝐹‘𝑖) = 𝑎) | 
| 40 | 37, 39 | r19.29a 3161 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑌) → ∃𝑓 ∈ 𝑌 (𝑓 ⨣ 𝑎) = (0g‘𝐻)) | 
| 41 | 40 | ralrimiva 3145 | . 2
⊢ (𝜑 → ∀𝑎 ∈ 𝑌 ∃𝑓 ∈ 𝑌 (𝑓 ⨣ 𝑎) = (0g‘𝐻)) | 
| 42 |  | eqid 2736 | . . 3
⊢
(0g‘𝐻) = (0g‘𝐻) | 
| 43 | 3, 5, 42 | isgrp 18958 | . 2
⊢ (𝐻 ∈ Grp ↔ (𝐻 ∈ Mnd ∧ ∀𝑎 ∈ 𝑌 ∃𝑓 ∈ 𝑌 (𝑓 ⨣ 𝑎) = (0g‘𝐻))) | 
| 44 | 9, 41, 43 | sylanbrc 583 | 1
⊢ (𝜑 → 𝐻 ∈ Grp) |