Metamath Proof Explorer


Theorem ghmrn

Description: The range of a homomorphism is a subgroup. (Contributed by Stefan O'Rear, 31-Dec-2014)

Ref Expression
Assertion ghmrn
|- ( F e. ( S GrpHom T ) -> ran F e. ( SubGrp ` T ) )

Proof

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 ) )