Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . 4
⊢
(Base‘𝑆) =
(Base‘𝑆) |
2 | | eqid 2610 |
. . . 4
⊢
(Base‘𝑇) =
(Base‘𝑇) |
3 | 1, 2 | ghmf 17487 |
. . 3
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
4 | | frn 5966 |
. . 3
⊢ (𝐹:(Base‘𝑆)⟶(Base‘𝑇) → ran 𝐹 ⊆ (Base‘𝑇)) |
5 | 3, 4 | syl 17 |
. 2
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → ran 𝐹 ⊆ (Base‘𝑇)) |
6 | | fdm 5964 |
. . . . 5
⊢ (𝐹:(Base‘𝑆)⟶(Base‘𝑇) → dom 𝐹 = (Base‘𝑆)) |
7 | 3, 6 | syl 17 |
. . . 4
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → dom 𝐹 = (Base‘𝑆)) |
8 | | ghmgrp1 17485 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑆 ∈ Grp) |
9 | 1 | grpbn0 17274 |
. . . . 5
⊢ (𝑆 ∈ Grp →
(Base‘𝑆) ≠
∅) |
10 | 8, 9 | syl 17 |
. . . 4
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (Base‘𝑆) ≠ ∅) |
11 | 7, 10 | eqnetrd 2849 |
. . 3
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → dom 𝐹 ≠ ∅) |
12 | | dm0rn0 5263 |
. . . 4
⊢ (dom
𝐹 = ∅ ↔ ran
𝐹 =
∅) |
13 | 12 | necon3bii 2834 |
. . 3
⊢ (dom
𝐹 ≠ ∅ ↔ ran
𝐹 ≠
∅) |
14 | 11, 13 | sylib 207 |
. 2
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → ran 𝐹 ≠ ∅) |
15 | | eqid 2610 |
. . . . . . . . . 10
⊢
(+g‘𝑆) = (+g‘𝑆) |
16 | | eqid 2610 |
. . . . . . . . . 10
⊢
(+g‘𝑇) = (+g‘𝑇) |
17 | 1, 15, 16 | ghmlin 17488 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆) ∧ 𝑎 ∈ (Base‘𝑆)) → (𝐹‘(𝑐(+g‘𝑆)𝑎)) = ((𝐹‘𝑐)(+g‘𝑇)(𝐹‘𝑎))) |
18 | | ffn 5958 |
. . . . . . . . . . . 12
⊢ (𝐹:(Base‘𝑆)⟶(Base‘𝑇) → 𝐹 Fn (Base‘𝑆)) |
19 | 3, 18 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹 Fn (Base‘𝑆)) |
20 | 19 | 3ad2ant1 1075 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆) ∧ 𝑎 ∈ (Base‘𝑆)) → 𝐹 Fn (Base‘𝑆)) |
21 | 1, 15 | grpcl 17253 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Grp ∧ 𝑐 ∈ (Base‘𝑆) ∧ 𝑎 ∈ (Base‘𝑆)) → (𝑐(+g‘𝑆)𝑎) ∈ (Base‘𝑆)) |
22 | 8, 21 | syl3an1 1351 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆) ∧ 𝑎 ∈ (Base‘𝑆)) → (𝑐(+g‘𝑆)𝑎) ∈ (Base‘𝑆)) |
23 | | fnfvelrn 6264 |
. . . . . . . . . 10
⊢ ((𝐹 Fn (Base‘𝑆) ∧ (𝑐(+g‘𝑆)𝑎) ∈ (Base‘𝑆)) → (𝐹‘(𝑐(+g‘𝑆)𝑎)) ∈ ran 𝐹) |
24 | 20, 22, 23 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆) ∧ 𝑎 ∈ (Base‘𝑆)) → (𝐹‘(𝑐(+g‘𝑆)𝑎)) ∈ ran 𝐹) |
25 | 17, 24 | eqeltrrd 2689 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆) ∧ 𝑎 ∈ (Base‘𝑆)) → ((𝐹‘𝑐)(+g‘𝑇)(𝐹‘𝑎)) ∈ ran 𝐹) |
26 | 25 | 3expia 1259 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆)) → (𝑎 ∈ (Base‘𝑆) → ((𝐹‘𝑐)(+g‘𝑇)(𝐹‘𝑎)) ∈ ran 𝐹)) |
27 | 26 | ralrimiv 2948 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆)) → ∀𝑎 ∈ (Base‘𝑆)((𝐹‘𝑐)(+g‘𝑇)(𝐹‘𝑎)) ∈ ran 𝐹) |
28 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑏 = (𝐹‘𝑎) → ((𝐹‘𝑐)(+g‘𝑇)𝑏) = ((𝐹‘𝑐)(+g‘𝑇)(𝐹‘𝑎))) |
29 | 28 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑏 = (𝐹‘𝑎) → (((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹 ↔ ((𝐹‘𝑐)(+g‘𝑇)(𝐹‘𝑎)) ∈ ran 𝐹)) |
30 | 29 | ralrn 6270 |
. . . . . . . 8
⊢ (𝐹 Fn (Base‘𝑆) → (∀𝑏 ∈ ran 𝐹((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹 ↔ ∀𝑎 ∈ (Base‘𝑆)((𝐹‘𝑐)(+g‘𝑇)(𝐹‘𝑎)) ∈ ran 𝐹)) |
31 | 19, 30 | syl 17 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (∀𝑏 ∈ ran 𝐹((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹 ↔ ∀𝑎 ∈ (Base‘𝑆)((𝐹‘𝑐)(+g‘𝑇)(𝐹‘𝑎)) ∈ ran 𝐹)) |
32 | 31 | adantr 480 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆)) → (∀𝑏 ∈ ran 𝐹((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹 ↔ ∀𝑎 ∈ (Base‘𝑆)((𝐹‘𝑐)(+g‘𝑇)(𝐹‘𝑎)) ∈ ran 𝐹)) |
33 | 27, 32 | mpbird 246 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆)) → ∀𝑏 ∈ ran 𝐹((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹) |
34 | | eqid 2610 |
. . . . . . 7
⊢
(invg‘𝑆) = (invg‘𝑆) |
35 | | eqid 2610 |
. . . . . . 7
⊢
(invg‘𝑇) = (invg‘𝑇) |
36 | 1, 34, 35 | ghminv 17490 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆)) → (𝐹‘((invg‘𝑆)‘𝑐)) = ((invg‘𝑇)‘(𝐹‘𝑐))) |
37 | 19 | adantr 480 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆)) → 𝐹 Fn (Base‘𝑆)) |
38 | 1, 34 | grpinvcl 17290 |
. . . . . . . 8
⊢ ((𝑆 ∈ Grp ∧ 𝑐 ∈ (Base‘𝑆)) →
((invg‘𝑆)‘𝑐) ∈ (Base‘𝑆)) |
39 | 8, 38 | sylan 487 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆)) → ((invg‘𝑆)‘𝑐) ∈ (Base‘𝑆)) |
40 | | fnfvelrn 6264 |
. . . . . . 7
⊢ ((𝐹 Fn (Base‘𝑆) ∧
((invg‘𝑆)‘𝑐) ∈ (Base‘𝑆)) → (𝐹‘((invg‘𝑆)‘𝑐)) ∈ ran 𝐹) |
41 | 37, 39, 40 | syl2anc 691 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆)) → (𝐹‘((invg‘𝑆)‘𝑐)) ∈ ran 𝐹) |
42 | 36, 41 | eqeltrrd 2689 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆)) → ((invg‘𝑇)‘(𝐹‘𝑐)) ∈ ran 𝐹) |
43 | 33, 42 | jca 553 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑐 ∈ (Base‘𝑆)) → (∀𝑏 ∈ ran 𝐹((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹 ∧ ((invg‘𝑇)‘(𝐹‘𝑐)) ∈ ran 𝐹)) |
44 | 43 | ralrimiva 2949 |
. . 3
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → ∀𝑐 ∈ (Base‘𝑆)(∀𝑏 ∈ ran 𝐹((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹 ∧ ((invg‘𝑇)‘(𝐹‘𝑐)) ∈ ran 𝐹)) |
45 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑎 = (𝐹‘𝑐) → (𝑎(+g‘𝑇)𝑏) = ((𝐹‘𝑐)(+g‘𝑇)𝑏)) |
46 | 45 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑎 = (𝐹‘𝑐) → ((𝑎(+g‘𝑇)𝑏) ∈ ran 𝐹 ↔ ((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹)) |
47 | 46 | ralbidv 2969 |
. . . . . 6
⊢ (𝑎 = (𝐹‘𝑐) → (∀𝑏 ∈ ran 𝐹(𝑎(+g‘𝑇)𝑏) ∈ ran 𝐹 ↔ ∀𝑏 ∈ ran 𝐹((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹)) |
48 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑎 = (𝐹‘𝑐) → ((invg‘𝑇)‘𝑎) = ((invg‘𝑇)‘(𝐹‘𝑐))) |
49 | 48 | eleq1d 2672 |
. . . . . 6
⊢ (𝑎 = (𝐹‘𝑐) → (((invg‘𝑇)‘𝑎) ∈ ran 𝐹 ↔ ((invg‘𝑇)‘(𝐹‘𝑐)) ∈ ran 𝐹)) |
50 | 47, 49 | anbi12d 743 |
. . . . 5
⊢ (𝑎 = (𝐹‘𝑐) → ((∀𝑏 ∈ ran 𝐹(𝑎(+g‘𝑇)𝑏) ∈ ran 𝐹 ∧ ((invg‘𝑇)‘𝑎) ∈ ran 𝐹) ↔ (∀𝑏 ∈ ran 𝐹((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹 ∧ ((invg‘𝑇)‘(𝐹‘𝑐)) ∈ ran 𝐹))) |
51 | 50 | ralrn 6270 |
. . . 4
⊢ (𝐹 Fn (Base‘𝑆) → (∀𝑎 ∈ ran 𝐹(∀𝑏 ∈ ran 𝐹(𝑎(+g‘𝑇)𝑏) ∈ ran 𝐹 ∧ ((invg‘𝑇)‘𝑎) ∈ ran 𝐹) ↔ ∀𝑐 ∈ (Base‘𝑆)(∀𝑏 ∈ ran 𝐹((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹 ∧ ((invg‘𝑇)‘(𝐹‘𝑐)) ∈ ran 𝐹))) |
52 | 19, 51 | syl 17 |
. . 3
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (∀𝑎 ∈ ran 𝐹(∀𝑏 ∈ ran 𝐹(𝑎(+g‘𝑇)𝑏) ∈ ran 𝐹 ∧ ((invg‘𝑇)‘𝑎) ∈ ran 𝐹) ↔ ∀𝑐 ∈ (Base‘𝑆)(∀𝑏 ∈ ran 𝐹((𝐹‘𝑐)(+g‘𝑇)𝑏) ∈ ran 𝐹 ∧ ((invg‘𝑇)‘(𝐹‘𝑐)) ∈ ran 𝐹))) |
53 | 44, 52 | mpbird 246 |
. 2
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → ∀𝑎 ∈ ran 𝐹(∀𝑏 ∈ ran 𝐹(𝑎(+g‘𝑇)𝑏) ∈ ran 𝐹 ∧ ((invg‘𝑇)‘𝑎) ∈ ran 𝐹)) |
54 | | ghmgrp2 17486 |
. . 3
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑇 ∈ Grp) |
55 | 2, 16, 35 | issubg2 17432 |
. . 3
⊢ (𝑇 ∈ Grp → (ran 𝐹 ∈ (SubGrp‘𝑇) ↔ (ran 𝐹 ⊆ (Base‘𝑇) ∧ ran 𝐹 ≠ ∅ ∧ ∀𝑎 ∈ ran 𝐹(∀𝑏 ∈ ran 𝐹(𝑎(+g‘𝑇)𝑏) ∈ ran 𝐹 ∧ ((invg‘𝑇)‘𝑎) ∈ ran 𝐹)))) |
56 | 54, 55 | syl 17 |
. 2
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (ran 𝐹 ∈ (SubGrp‘𝑇) ↔ (ran 𝐹 ⊆ (Base‘𝑇) ∧ ran 𝐹 ≠ ∅ ∧ ∀𝑎 ∈ ran 𝐹(∀𝑏 ∈ ran 𝐹(𝑎(+g‘𝑇)𝑏) ∈ ran 𝐹 ∧ ((invg‘𝑇)‘𝑎) ∈ ran 𝐹)))) |
57 | 5, 14, 53, 56 | mpbir3and 1238 |
1
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → ran 𝐹 ∈ (SubGrp‘𝑇)) |