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