Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|- ( Base ` S ) = ( Base ` S ) |
2 |
|
eqid |
|- ( Base ` T ) = ( Base ` T ) |
3 |
1 2
|
ghmf |
|- ( F e. ( S GrpHom T ) -> F : ( Base ` S ) --> ( Base ` T ) ) |
4 |
3
|
frnd |
|- ( F e. ( S GrpHom T ) -> ran F C_ ( Base ` T ) ) |
5 |
3
|
fdmd |
|- ( F e. ( S GrpHom T ) -> dom F = ( Base ` S ) ) |
6 |
|
ghmgrp1 |
|- ( F e. ( S GrpHom T ) -> S e. Grp ) |
7 |
1
|
grpbn0 |
|- ( S e. Grp -> ( Base ` S ) =/= (/) ) |
8 |
6 7
|
syl |
|- ( F e. ( S GrpHom T ) -> ( Base ` S ) =/= (/) ) |
9 |
5 8
|
eqnetrd |
|- ( F e. ( S GrpHom T ) -> dom F =/= (/) ) |
10 |
|
dm0rn0 |
|- ( dom F = (/) <-> ran F = (/) ) |
11 |
10
|
necon3bii |
|- ( dom F =/= (/) <-> ran F =/= (/) ) |
12 |
9 11
|
sylib |
|- ( F e. ( S GrpHom T ) -> ran F =/= (/) ) |
13 |
|
eqid |
|- ( +g ` S ) = ( +g ` S ) |
14 |
|
eqid |
|- ( +g ` T ) = ( +g ` T ) |
15 |
1 13 14
|
ghmlin |
|- ( ( F e. ( S GrpHom T ) /\ c e. ( Base ` S ) /\ a e. ( Base ` S ) ) -> ( F ` ( c ( +g ` S ) a ) ) = ( ( F ` c ) ( +g ` T ) ( F ` a ) ) ) |
16 |
3
|
ffnd |
|- ( F e. ( S GrpHom T ) -> F Fn ( Base ` S ) ) |
17 |
16
|
3ad2ant1 |
|- ( ( F e. ( S GrpHom T ) /\ c e. ( Base ` S ) /\ a e. ( Base ` S ) ) -> F Fn ( Base ` S ) ) |
18 |
1 13
|
grpcl |
|- ( ( S e. Grp /\ c e. ( Base ` S ) /\ a e. ( Base ` S ) ) -> ( c ( +g ` S ) a ) e. ( Base ` S ) ) |
19 |
6 18
|
syl3an1 |
|- ( ( F e. ( S GrpHom T ) /\ c e. ( Base ` S ) /\ a e. ( Base ` S ) ) -> ( c ( +g ` S ) a ) e. ( Base ` S ) ) |
20 |
|
fnfvelrn |
|- ( ( F Fn ( Base ` S ) /\ ( c ( +g ` S ) a ) e. ( Base ` S ) ) -> ( F ` ( c ( +g ` S ) a ) ) e. ran F ) |
21 |
17 19 20
|
syl2anc |
|- ( ( F e. ( S GrpHom T ) /\ c e. ( Base ` S ) /\ a e. ( Base ` S ) ) -> ( F ` ( c ( +g ` S ) a ) ) e. ran F ) |
22 |
15 21
|
eqeltrrd |
|- ( ( F e. ( S GrpHom T ) /\ c e. ( Base ` S ) /\ a e. ( Base ` S ) ) -> ( ( F ` c ) ( +g ` T ) ( F ` a ) ) e. ran F ) |
23 |
22
|
3expia |
|- ( ( F e. ( S GrpHom T ) /\ c e. ( Base ` S ) ) -> ( a e. ( Base ` S ) -> ( ( F ` c ) ( +g ` T ) ( F ` a ) ) e. ran F ) ) |
24 |
23
|
ralrimiv |
|- ( ( F e. ( S GrpHom T ) /\ c e. ( Base ` S ) ) -> A. a e. ( Base ` S ) ( ( F ` c ) ( +g ` T ) ( F ` a ) ) e. ran F ) |
25 |
|
oveq2 |
|- ( b = ( F ` a ) -> ( ( F ` c ) ( +g ` T ) b ) = ( ( F ` c ) ( +g ` T ) ( F ` a ) ) ) |
26 |
25
|
eleq1d |
|- ( b = ( F ` a ) -> ( ( ( F ` c ) ( +g ` T ) b ) e. ran F <-> ( ( F ` c ) ( +g ` T ) ( F ` a ) ) e. ran F ) ) |
27 |
26
|
ralrn |
|- ( F Fn ( Base ` S ) -> ( A. b e. ran F ( ( F ` c ) ( +g ` T ) b ) e. ran F <-> A. a e. ( Base ` S ) ( ( F ` c ) ( +g ` T ) ( F ` a ) ) e. ran F ) ) |
28 |
16 27
|
syl |
|- ( F e. ( S GrpHom T ) -> ( A. b e. ran F ( ( F ` c ) ( +g ` T ) b ) e. ran F <-> A. a e. ( Base ` S ) ( ( F ` c ) ( +g ` T ) ( F ` a ) ) e. ran F ) ) |
29 |
28
|
adantr |
|- ( ( F e. ( S GrpHom T ) /\ c e. ( Base ` S ) ) -> ( A. b e. ran F ( ( F ` c ) ( +g ` T ) b ) e. ran F <-> A. a e. ( Base ` S ) ( ( F ` c ) ( +g ` T ) ( F ` a ) ) e. ran F ) ) |
30 |
24 29
|
mpbird |
|- ( ( F e. ( S GrpHom T ) /\ c e. ( Base ` S ) ) -> A. b e. ran F ( ( F ` c ) ( +g ` T ) b ) e. ran F ) |
31 |
|
eqid |
|- ( invg ` S ) = ( invg ` S ) |
32 |
|
eqid |
|- ( invg ` T ) = ( invg ` T ) |
33 |
1 31 32
|
ghminv |
|- ( ( F e. ( S GrpHom T ) /\ c e. ( Base ` S ) ) -> ( F ` ( ( invg ` S ) ` c ) ) = ( ( invg ` T ) ` ( F ` c ) ) ) |
34 |
16
|
adantr |
|- ( ( F e. ( S GrpHom T ) /\ c e. ( Base ` S ) ) -> F Fn ( Base ` S ) ) |
35 |
1 31
|
grpinvcl |
|- ( ( S e. Grp /\ c e. ( Base ` S ) ) -> ( ( invg ` S ) ` c ) e. ( Base ` S ) ) |
36 |
6 35
|
sylan |
|- ( ( F e. ( S GrpHom T ) /\ c e. ( Base ` S ) ) -> ( ( invg ` S ) ` c ) e. ( Base ` S ) ) |
37 |
|
fnfvelrn |
|- ( ( F Fn ( Base ` S ) /\ ( ( invg ` S ) ` c ) e. ( Base ` S ) ) -> ( F ` ( ( invg ` S ) ` c ) ) e. ran F ) |
38 |
34 36 37
|
syl2anc |
|- ( ( F e. ( S GrpHom T ) /\ c e. ( Base ` S ) ) -> ( F ` ( ( invg ` S ) ` c ) ) e. ran F ) |
39 |
33 38
|
eqeltrrd |
|- ( ( F e. ( S GrpHom T ) /\ c e. ( Base ` S ) ) -> ( ( invg ` T ) ` ( F ` c ) ) e. ran F ) |
40 |
30 39
|
jca |
|- ( ( F e. ( S GrpHom T ) /\ c e. ( Base ` S ) ) -> ( A. b e. ran F ( ( F ` c ) ( +g ` T ) b ) e. ran F /\ ( ( invg ` T ) ` ( F ` c ) ) e. ran F ) ) |
41 |
40
|
ralrimiva |
|- ( F e. ( S GrpHom T ) -> A. c e. ( Base ` S ) ( A. b e. ran F ( ( F ` c ) ( +g ` T ) b ) e. ran F /\ ( ( invg ` T ) ` ( F ` c ) ) e. ran F ) ) |
42 |
|
oveq1 |
|- ( a = ( F ` c ) -> ( a ( +g ` T ) b ) = ( ( F ` c ) ( +g ` T ) b ) ) |
43 |
42
|
eleq1d |
|- ( a = ( F ` c ) -> ( ( a ( +g ` T ) b ) e. ran F <-> ( ( F ` c ) ( +g ` T ) b ) e. ran F ) ) |
44 |
43
|
ralbidv |
|- ( a = ( F ` c ) -> ( A. b e. ran F ( a ( +g ` T ) b ) e. ran F <-> A. b e. ran F ( ( F ` c ) ( +g ` T ) b ) e. ran F ) ) |
45 |
|
fveq2 |
|- ( a = ( F ` c ) -> ( ( invg ` T ) ` a ) = ( ( invg ` T ) ` ( F ` c ) ) ) |
46 |
45
|
eleq1d |
|- ( a = ( F ` c ) -> ( ( ( invg ` T ) ` a ) e. ran F <-> ( ( invg ` T ) ` ( F ` c ) ) e. ran F ) ) |
47 |
44 46
|
anbi12d |
|- ( a = ( F ` c ) -> ( ( A. b e. ran F ( a ( +g ` T ) b ) e. ran F /\ ( ( invg ` T ) ` a ) e. ran F ) <-> ( A. b e. ran F ( ( F ` c ) ( +g ` T ) b ) e. ran F /\ ( ( invg ` T ) ` ( F ` c ) ) e. ran F ) ) ) |
48 |
47
|
ralrn |
|- ( F Fn ( Base ` S ) -> ( A. a e. ran F ( A. b e. ran F ( a ( +g ` T ) b ) e. ran F /\ ( ( invg ` T ) ` a ) e. ran F ) <-> A. c e. ( Base ` S ) ( A. b e. ran F ( ( F ` c ) ( +g ` T ) b ) e. ran F /\ ( ( invg ` T ) ` ( F ` c ) ) e. ran F ) ) ) |
49 |
16 48
|
syl |
|- ( F e. ( S GrpHom T ) -> ( A. a e. ran F ( A. b e. ran F ( a ( +g ` T ) b ) e. ran F /\ ( ( invg ` T ) ` a ) e. ran F ) <-> A. c e. ( Base ` S ) ( A. b e. ran F ( ( F ` c ) ( +g ` T ) b ) e. ran F /\ ( ( invg ` T ) ` ( F ` c ) ) e. ran F ) ) ) |
50 |
41 49
|
mpbird |
|- ( F e. ( S GrpHom T ) -> A. a e. ran F ( A. b e. ran F ( a ( +g ` T ) b ) e. ran F /\ ( ( invg ` T ) ` a ) e. ran F ) ) |
51 |
|
ghmgrp2 |
|- ( F e. ( S GrpHom T ) -> T e. Grp ) |
52 |
2 14 32
|
issubg2 |
|- ( T e. Grp -> ( ran F e. ( SubGrp ` T ) <-> ( ran F C_ ( Base ` T ) /\ ran F =/= (/) /\ A. a e. ran F ( A. b e. ran F ( a ( +g ` T ) b ) e. ran F /\ ( ( invg ` T ) ` a ) e. ran F ) ) ) ) |
53 |
51 52
|
syl |
|- ( F e. ( S GrpHom T ) -> ( ran F e. ( SubGrp ` T ) <-> ( ran F C_ ( Base ` T ) /\ ran F =/= (/) /\ A. a e. ran F ( A. b e. ran F ( a ( +g ` T ) b ) e. ran F /\ ( ( invg ` T ) ` a ) e. ran F ) ) ) ) |
54 |
4 12 50 53
|
mpbir3and |
|- ( F e. ( S GrpHom T ) -> ran F e. ( SubGrp ` T ) ) |