| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . 4
⊢
(Base‘𝑆) =
(Base‘𝑆) |
| 2 | | eqid 2737 |
. . . 4
⊢
(Base‘𝑇) =
(Base‘𝑇) |
| 3 | 1, 2 | ghmf 19238 |
. . 3
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
| 4 | 3 | frnd 6744 |
. 2
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → ran 𝐹 ⊆ (Base‘𝑇)) |
| 5 | 3 | fdmd 6746 |
. . . 4
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → dom 𝐹 = (Base‘𝑆)) |
| 6 | | ghmgrp1 19236 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑆 ∈ Grp) |
| 7 | 1 | grpbn0 18984 |
. . . . 5
⊢ (𝑆 ∈ Grp →
(Base‘𝑆) ≠
∅) |
| 8 | 6, 7 | syl 17 |
. . . 4
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (Base‘𝑆) ≠ ∅) |
| 9 | 5, 8 | eqnetrd 3008 |
. . 3
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → dom 𝐹 ≠ ∅) |
| 10 | | dm0rn0 5935 |
. . . 4
⊢ (dom
𝐹 = ∅ ↔ ran
𝐹 =
∅) |
| 11 | 10 | necon3bii 2993 |
. . 3
⊢ (dom
𝐹 ≠ ∅ ↔ ran
𝐹 ≠
∅) |
| 12 | 9, 11 | sylib 218 |
. 2
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → ran 𝐹 ≠ ∅) |
| 13 | | eqid 2737 |
. . . . . . . . . 10
⊢
(+g‘𝑆) = (+g‘𝑆) |
| 14 | | eqid 2737 |
. . . . . . . . . 10
⊢
(+g‘𝑇) = (+g‘𝑇) |
| 15 | 1, 13, 14 | ghmlin 19239 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆) ∧ 𝑎 ∈ (Base‘𝑆)) → (𝐹‘(𝑐(+g‘𝑆)𝑎)) = ((𝐹‘𝑐)(+g‘𝑇)(𝐹‘𝑎))) |
| 16 | 3 | ffnd 6737 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹 Fn (Base‘𝑆)) |
| 17 | 16 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆) ∧ 𝑎 ∈ (Base‘𝑆)) → 𝐹 Fn (Base‘𝑆)) |
| 18 | 1, 13 | grpcl 18959 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Grp ∧ 𝑐 ∈ (Base‘𝑆) ∧ 𝑎 ∈ (Base‘𝑆)) → (𝑐(+g‘𝑆)𝑎) ∈ (Base‘𝑆)) |
| 19 | 6, 18 | syl3an1 1164 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆) ∧ 𝑎 ∈ (Base‘𝑆)) → (𝑐(+g‘𝑆)𝑎) ∈ (Base‘𝑆)) |
| 20 | | fnfvelrn 7100 |
. . . . . . . . . 10
⊢ ((𝐹 Fn (Base‘𝑆) ∧ (𝑐(+g‘𝑆)𝑎) ∈ (Base‘𝑆)) → (𝐹‘(𝑐(+g‘𝑆)𝑎)) ∈ ran 𝐹) |
| 21 | 17, 19, 20 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆) ∧ 𝑎 ∈ (Base‘𝑆)) → (𝐹‘(𝑐(+g‘𝑆)𝑎)) ∈ ran 𝐹) |
| 22 | 15, 21 | eqeltrrd 2842 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆) ∧ 𝑎 ∈ (Base‘𝑆)) → ((𝐹‘𝑐)(+g‘𝑇)(𝐹‘𝑎)) ∈ ran 𝐹) |
| 23 | 22 | 3expia 1122 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆)) → (𝑎 ∈ (Base‘𝑆) → ((𝐹‘𝑐)(+g‘𝑇)(𝐹‘𝑎)) ∈ ran 𝐹)) |
| 24 | 23 | ralrimiv 3145 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆)) → ∀𝑎 ∈ (Base‘𝑆)((𝐹‘𝑐)(+g‘𝑇)(𝐹‘𝑎)) ∈ ran 𝐹) |
| 25 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑏 = (𝐹‘𝑎) → ((𝐹‘𝑐)(+g‘𝑇)𝑏) = ((𝐹‘𝑐)(+g‘𝑇)(𝐹‘𝑎))) |
| 26 | 25 | eleq1d 2826 |
. . . . . . . . 9
⊢ (𝑏 = (𝐹‘𝑎) → (((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹 ↔ ((𝐹‘𝑐)(+g‘𝑇)(𝐹‘𝑎)) ∈ ran 𝐹)) |
| 27 | 26 | ralrn 7108 |
. . . . . . . 8
⊢ (𝐹 Fn (Base‘𝑆) → (∀𝑏 ∈ ran 𝐹((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹 ↔ ∀𝑎 ∈ (Base‘𝑆)((𝐹‘𝑐)(+g‘𝑇)(𝐹‘𝑎)) ∈ ran 𝐹)) |
| 28 | 16, 27 | syl 17 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (∀𝑏 ∈ ran 𝐹((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹 ↔ ∀𝑎 ∈ (Base‘𝑆)((𝐹‘𝑐)(+g‘𝑇)(𝐹‘𝑎)) ∈ ran 𝐹)) |
| 29 | 28 | adantr 480 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆)) → (∀𝑏 ∈ ran 𝐹((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹 ↔ ∀𝑎 ∈ (Base‘𝑆)((𝐹‘𝑐)(+g‘𝑇)(𝐹‘𝑎)) ∈ ran 𝐹)) |
| 30 | 24, 29 | mpbird 257 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆)) → ∀𝑏 ∈ ran 𝐹((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹) |
| 31 | | eqid 2737 |
. . . . . . 7
⊢
(invg‘𝑆) = (invg‘𝑆) |
| 32 | | eqid 2737 |
. . . . . . 7
⊢
(invg‘𝑇) = (invg‘𝑇) |
| 33 | 1, 31, 32 | ghminv 19241 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆)) → (𝐹‘((invg‘𝑆)‘𝑐)) = ((invg‘𝑇)‘(𝐹‘𝑐))) |
| 34 | 16 | adantr 480 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆)) → 𝐹 Fn (Base‘𝑆)) |
| 35 | 1, 31 | grpinvcl 19005 |
. . . . . . . 8
⊢ ((𝑆 ∈ Grp ∧ 𝑐 ∈ (Base‘𝑆)) →
((invg‘𝑆)‘𝑐) ∈ (Base‘𝑆)) |
| 36 | 6, 35 | sylan 580 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆)) → ((invg‘𝑆)‘𝑐) ∈ (Base‘𝑆)) |
| 37 | | fnfvelrn 7100 |
. . . . . . 7
⊢ ((𝐹 Fn (Base‘𝑆) ∧
((invg‘𝑆)‘𝑐) ∈ (Base‘𝑆)) → (𝐹‘((invg‘𝑆)‘𝑐)) ∈ ran 𝐹) |
| 38 | 34, 36, 37 | syl2anc 584 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆)) → (𝐹‘((invg‘𝑆)‘𝑐)) ∈ ran 𝐹) |
| 39 | 33, 38 | eqeltrrd 2842 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆)) → ((invg‘𝑇)‘(𝐹‘𝑐)) ∈ ran 𝐹) |
| 40 | 30, 39 | jca 511 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆)) → (∀𝑏 ∈ ran 𝐹((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹 ∧ ((invg‘𝑇)‘(𝐹‘𝑐)) ∈ ran 𝐹)) |
| 41 | 40 | ralrimiva 3146 |
. . 3
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → ∀𝑐 ∈ (Base‘𝑆)(∀𝑏 ∈ ran 𝐹((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹 ∧ ((invg‘𝑇)‘(𝐹‘𝑐)) ∈ ran 𝐹)) |
| 42 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑎 = (𝐹‘𝑐) → (𝑎(+g‘𝑇)𝑏) = ((𝐹‘𝑐)(+g‘𝑇)𝑏)) |
| 43 | 42 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑎 = (𝐹‘𝑐) → ((𝑎(+g‘𝑇)𝑏) ∈ ran 𝐹 ↔ ((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹)) |
| 44 | 43 | ralbidv 3178 |
. . . . . 6
⊢ (𝑎 = (𝐹‘𝑐) → (∀𝑏 ∈ ran 𝐹(𝑎(+g‘𝑇)𝑏) ∈ ran 𝐹 ↔ ∀𝑏 ∈ ran 𝐹((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹)) |
| 45 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑎 = (𝐹‘𝑐) → ((invg‘𝑇)‘𝑎) = ((invg‘𝑇)‘(𝐹‘𝑐))) |
| 46 | 45 | eleq1d 2826 |
. . . . . 6
⊢ (𝑎 = (𝐹‘𝑐) → (((invg‘𝑇)‘𝑎) ∈ ran 𝐹 ↔ ((invg‘𝑇)‘(𝐹‘𝑐)) ∈ ran 𝐹)) |
| 47 | 44, 46 | anbi12d 632 |
. . . . 5
⊢ (𝑎 = (𝐹‘𝑐) → ((∀𝑏 ∈ ran 𝐹(𝑎(+g‘𝑇)𝑏) ∈ ran 𝐹 ∧ ((invg‘𝑇)‘𝑎) ∈ ran 𝐹) ↔ (∀𝑏 ∈ ran 𝐹((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹 ∧ ((invg‘𝑇)‘(𝐹‘𝑐)) ∈ ran 𝐹))) |
| 48 | 47 | ralrn 7108 |
. . . 4
⊢ (𝐹 Fn (Base‘𝑆) → (∀𝑎 ∈ ran 𝐹(∀𝑏 ∈ ran 𝐹(𝑎(+g‘𝑇)𝑏) ∈ ran 𝐹 ∧ ((invg‘𝑇)‘𝑎) ∈ ran 𝐹) ↔ ∀𝑐 ∈ (Base‘𝑆)(∀𝑏 ∈ ran 𝐹((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹 ∧ ((invg‘𝑇)‘(𝐹‘𝑐)) ∈ ran 𝐹))) |
| 49 | 16, 48 | syl 17 |
. . 3
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (∀𝑎 ∈ ran 𝐹(∀𝑏 ∈ ran 𝐹(𝑎(+g‘𝑇)𝑏) ∈ ran 𝐹 ∧ ((invg‘𝑇)‘𝑎) ∈ ran 𝐹) ↔ ∀𝑐 ∈ (Base‘𝑆)(∀𝑏 ∈ ran 𝐹((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹 ∧ ((invg‘𝑇)‘(𝐹‘𝑐)) ∈ ran 𝐹))) |
| 50 | 41, 49 | mpbird 257 |
. 2
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → ∀𝑎 ∈ ran 𝐹(∀𝑏 ∈ ran 𝐹(𝑎(+g‘𝑇)𝑏) ∈ ran 𝐹 ∧ ((invg‘𝑇)‘𝑎) ∈ ran 𝐹)) |
| 51 | | ghmgrp2 19237 |
. . 3
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑇 ∈ Grp) |
| 52 | 2, 14, 32 | issubg2 19159 |
. . 3
⊢ (𝑇 ∈ Grp → (ran 𝐹 ∈ (SubGrp‘𝑇) ↔ (ran 𝐹 ⊆ (Base‘𝑇) ∧ ran 𝐹 ≠ ∅ ∧ ∀𝑎 ∈ ran 𝐹(∀𝑏 ∈ ran 𝐹(𝑎(+g‘𝑇)𝑏) ∈ ran 𝐹 ∧ ((invg‘𝑇)‘𝑎) ∈ ran 𝐹)))) |
| 53 | 51, 52 | syl 17 |
. 2
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (ran 𝐹 ∈ (SubGrp‘𝑇) ↔ (ran 𝐹 ⊆ (Base‘𝑇) ∧ ran 𝐹 ≠ ∅ ∧ ∀𝑎 ∈ ran 𝐹(∀𝑏 ∈ ran 𝐹(𝑎(+g‘𝑇)𝑏) ∈ ran 𝐹 ∧ ((invg‘𝑇)‘𝑎) ∈ ran 𝐹)))) |
| 54 | 4, 12, 50, 53 | mpbir3and 1343 |
1
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → ran 𝐹 ∈ (SubGrp‘𝑇)) |