Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . 4
⊢
(Base‘𝑆) =
(Base‘𝑆) |
2 | | eqid 2737 |
. . . 4
⊢
(Base‘𝑇) =
(Base‘𝑇) |
3 | 1, 2 | ghmf 18626 |
. . 3
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
4 | 3 | frnd 6553 |
. 2
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → ran 𝐹 ⊆ (Base‘𝑇)) |
5 | 3 | fdmd 6556 |
. . . 4
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → dom 𝐹 = (Base‘𝑆)) |
6 | | ghmgrp1 18624 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑆 ∈ Grp) |
7 | 1 | grpbn0 18396 |
. . . . 5
⊢ (𝑆 ∈ Grp →
(Base‘𝑆) ≠
∅) |
8 | 6, 7 | syl 17 |
. . . 4
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (Base‘𝑆) ≠ ∅) |
9 | 5, 8 | eqnetrd 3008 |
. . 3
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → dom 𝐹 ≠ ∅) |
10 | | dm0rn0 5794 |
. . . 4
⊢ (dom
𝐹 = ∅ ↔ ran
𝐹 =
∅) |
11 | 10 | necon3bii 2993 |
. . 3
⊢ (dom
𝐹 ≠ ∅ ↔ ran
𝐹 ≠
∅) |
12 | 9, 11 | sylib 221 |
. 2
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → ran 𝐹 ≠ ∅) |
13 | | eqid 2737 |
. . . . . . . . . 10
⊢
(+g‘𝑆) = (+g‘𝑆) |
14 | | eqid 2737 |
. . . . . . . . . 10
⊢
(+g‘𝑇) = (+g‘𝑇) |
15 | 1, 13, 14 | ghmlin 18627 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆) ∧ 𝑎 ∈ (Base‘𝑆)) → (𝐹‘(𝑐(+g‘𝑆)𝑎)) = ((𝐹‘𝑐)(+g‘𝑇)(𝐹‘𝑎))) |
16 | 3 | ffnd 6546 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹 Fn (Base‘𝑆)) |
17 | 16 | 3ad2ant1 1135 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆) ∧ 𝑎 ∈ (Base‘𝑆)) → 𝐹 Fn (Base‘𝑆)) |
18 | 1, 13 | grpcl 18373 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Grp ∧ 𝑐 ∈ (Base‘𝑆) ∧ 𝑎 ∈ (Base‘𝑆)) → (𝑐(+g‘𝑆)𝑎) ∈ (Base‘𝑆)) |
19 | 6, 18 | syl3an1 1165 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆) ∧ 𝑎 ∈ (Base‘𝑆)) → (𝑐(+g‘𝑆)𝑎) ∈ (Base‘𝑆)) |
20 | | fnfvelrn 6901 |
. . . . . . . . . 10
⊢ ((𝐹 Fn (Base‘𝑆) ∧ (𝑐(+g‘𝑆)𝑎) ∈ (Base‘𝑆)) → (𝐹‘(𝑐(+g‘𝑆)𝑎)) ∈ ran 𝐹) |
21 | 17, 19, 20 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆) ∧ 𝑎 ∈ (Base‘𝑆)) → (𝐹‘(𝑐(+g‘𝑆)𝑎)) ∈ ran 𝐹) |
22 | 15, 21 | eqeltrrd 2839 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆) ∧ 𝑎 ∈ (Base‘𝑆)) → ((𝐹‘𝑐)(+g‘𝑇)(𝐹‘𝑎)) ∈ ran 𝐹) |
23 | 22 | 3expia 1123 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆)) → (𝑎 ∈ (Base‘𝑆) → ((𝐹‘𝑐)(+g‘𝑇)(𝐹‘𝑎)) ∈ ran 𝐹)) |
24 | 23 | ralrimiv 3104 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆)) → ∀𝑎 ∈ (Base‘𝑆)((𝐹‘𝑐)(+g‘𝑇)(𝐹‘𝑎)) ∈ ran 𝐹) |
25 | | oveq2 7221 |
. . . . . . . . . 10
⊢ (𝑏 = (𝐹‘𝑎) → ((𝐹‘𝑐)(+g‘𝑇)𝑏) = ((𝐹‘𝑐)(+g‘𝑇)(𝐹‘𝑎))) |
26 | 25 | eleq1d 2822 |
. . . . . . . . 9
⊢ (𝑏 = (𝐹‘𝑎) → (((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹 ↔ ((𝐹‘𝑐)(+g‘𝑇)(𝐹‘𝑎)) ∈ ran 𝐹)) |
27 | 26 | ralrn 6907 |
. . . . . . . 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 484 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆)) → (∀𝑏 ∈ ran 𝐹((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹 ↔ ∀𝑎 ∈ (Base‘𝑆)((𝐹‘𝑐)(+g‘𝑇)(𝐹‘𝑎)) ∈ ran 𝐹)) |
30 | 24, 29 | mpbird 260 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆)) → ∀𝑏 ∈ ran 𝐹((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹) |
31 | | eqid 2737 |
. . . . . . 7
⊢
(invg‘𝑆) = (invg‘𝑆) |
32 | | eqid 2737 |
. . . . . . 7
⊢
(invg‘𝑇) = (invg‘𝑇) |
33 | 1, 31, 32 | ghminv 18629 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆)) → (𝐹‘((invg‘𝑆)‘𝑐)) = ((invg‘𝑇)‘(𝐹‘𝑐))) |
34 | 16 | adantr 484 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆)) → 𝐹 Fn (Base‘𝑆)) |
35 | 1, 31 | grpinvcl 18415 |
. . . . . . . 8
⊢ ((𝑆 ∈ Grp ∧ 𝑐 ∈ (Base‘𝑆)) →
((invg‘𝑆)‘𝑐) ∈ (Base‘𝑆)) |
36 | 6, 35 | sylan 583 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆)) → ((invg‘𝑆)‘𝑐) ∈ (Base‘𝑆)) |
37 | | fnfvelrn 6901 |
. . . . . . 7
⊢ ((𝐹 Fn (Base‘𝑆) ∧
((invg‘𝑆)‘𝑐) ∈ (Base‘𝑆)) → (𝐹‘((invg‘𝑆)‘𝑐)) ∈ ran 𝐹) |
38 | 34, 36, 37 | syl2anc 587 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆)) → (𝐹‘((invg‘𝑆)‘𝑐)) ∈ ran 𝐹) |
39 | 33, 38 | eqeltrrd 2839 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆)) → ((invg‘𝑇)‘(𝐹‘𝑐)) ∈ ran 𝐹) |
40 | 30, 39 | jca 515 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆)) → (∀𝑏 ∈ ran 𝐹((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹 ∧ ((invg‘𝑇)‘(𝐹‘𝑐)) ∈ ran 𝐹)) |
41 | 40 | ralrimiva 3105 |
. . 3
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → ∀𝑐 ∈ (Base‘𝑆)(∀𝑏 ∈ ran 𝐹((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹 ∧ ((invg‘𝑇)‘(𝐹‘𝑐)) ∈ ran 𝐹)) |
42 | | oveq1 7220 |
. . . . . . . 8
⊢ (𝑎 = (𝐹‘𝑐) → (𝑎(+g‘𝑇)𝑏) = ((𝐹‘𝑐)(+g‘𝑇)𝑏)) |
43 | 42 | eleq1d 2822 |
. . . . . . 7
⊢ (𝑎 = (𝐹‘𝑐) → ((𝑎(+g‘𝑇)𝑏) ∈ ran 𝐹 ↔ ((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹)) |
44 | 43 | ralbidv 3118 |
. . . . . 6
⊢ (𝑎 = (𝐹‘𝑐) → (∀𝑏 ∈ ran 𝐹(𝑎(+g‘𝑇)𝑏) ∈ ran 𝐹 ↔ ∀𝑏 ∈ ran 𝐹((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹)) |
45 | | fveq2 6717 |
. . . . . . 7
⊢ (𝑎 = (𝐹‘𝑐) → ((invg‘𝑇)‘𝑎) = ((invg‘𝑇)‘(𝐹‘𝑐))) |
46 | 45 | eleq1d 2822 |
. . . . . 6
⊢ (𝑎 = (𝐹‘𝑐) → (((invg‘𝑇)‘𝑎) ∈ ran 𝐹 ↔ ((invg‘𝑇)‘(𝐹‘𝑐)) ∈ ran 𝐹)) |
47 | 44, 46 | anbi12d 634 |
. . . . 5
⊢ (𝑎 = (𝐹‘𝑐) → ((∀𝑏 ∈ ran 𝐹(𝑎(+g‘𝑇)𝑏) ∈ ran 𝐹 ∧ ((invg‘𝑇)‘𝑎) ∈ ran 𝐹) ↔ (∀𝑏 ∈ ran 𝐹((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹 ∧ ((invg‘𝑇)‘(𝐹‘𝑐)) ∈ ran 𝐹))) |
48 | 47 | ralrn 6907 |
. . . 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 260 |
. 2
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → ∀𝑎 ∈ ran 𝐹(∀𝑏 ∈ ran 𝐹(𝑎(+g‘𝑇)𝑏) ∈ ran 𝐹 ∧ ((invg‘𝑇)‘𝑎) ∈ ran 𝐹)) |
51 | | ghmgrp2 18625 |
. . 3
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑇 ∈ Grp) |
52 | 2, 14, 32 | issubg2 18558 |
. . 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 1344 |
1
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → ran 𝐹 ∈ (SubGrp‘𝑇)) |