Metamath Proof Explorer

Theorem ghmf1

Description: Two ways of saying a group homomorphism is 1-1 into its codomain. (Contributed by Paul Chapman, 3-Mar-2008) (Revised by Mario Carneiro, 13-Jan-2015)

Ref Expression
Hypotheses ghmf1.x 
|- X = ( Base ` S )
ghmf1.y 
|- Y = ( Base ` T )
ghmf1.z 
|- .0. = ( 0g ` S )
ghmf1.u 
|- U = ( 0g ` T )
Assertion ghmf1 
|- ( F e. ( S GrpHom T ) -> ( F : X -1-1-> Y <-> A. x e. X ( ( F ` x ) = U -> x = .0. ) ) )

Proof

Step Hyp Ref Expression
1 ghmf1.x 
 |-  X = ( Base ` S )
2 ghmf1.y 
 |-  Y = ( Base ` T )
3 ghmf1.z 
 |-  .0. = ( 0g ` S )
4 ghmf1.u 
 |-  U = ( 0g ` T )
5 3 4 ghmid 
 |-  ( F e. ( S GrpHom T ) -> ( F ` .0. ) = U )
6 5 ad2antrr 
 |-  ( ( ( F e. ( S GrpHom T ) /\ F : X -1-1-> Y ) /\ x e. X ) -> ( F ` .0. ) = U )
7 6 eqeq2d 
 |-  ( ( ( F e. ( S GrpHom T ) /\ F : X -1-1-> Y ) /\ x e. X ) -> ( ( F ` x ) = ( F ` .0. ) <-> ( F ` x ) = U ) )
8 simplr 
 |-  ( ( ( F e. ( S GrpHom T ) /\ F : X -1-1-> Y ) /\ x e. X ) -> F : X -1-1-> Y )
9 simpr 
 |-  ( ( ( F e. ( S GrpHom T ) /\ F : X -1-1-> Y ) /\ x e. X ) -> x e. X )
10 ghmgrp1 
 |-  ( F e. ( S GrpHom T ) -> S e. Grp )
11 10 ad2antrr 
 |-  ( ( ( F e. ( S GrpHom T ) /\ F : X -1-1-> Y ) /\ x e. X ) -> S e. Grp )
12 1 3 grpidcl 
 |-  ( S e. Grp -> .0. e. X )
13 11 12 syl 
 |-  ( ( ( F e. ( S GrpHom T ) /\ F : X -1-1-> Y ) /\ x e. X ) -> .0. e. X )
14 f1fveq 
 |-  ( ( F : X -1-1-> Y /\ ( x e. X /\ .0. e. X ) ) -> ( ( F ` x ) = ( F ` .0. ) <-> x = .0. ) )
15 8 9 13 14 syl12anc 
 |-  ( ( ( F e. ( S GrpHom T ) /\ F : X -1-1-> Y ) /\ x e. X ) -> ( ( F ` x ) = ( F ` .0. ) <-> x = .0. ) )
16 7 15 bitr3d 
 |-  ( ( ( F e. ( S GrpHom T ) /\ F : X -1-1-> Y ) /\ x e. X ) -> ( ( F ` x ) = U <-> x = .0. ) )
17 16 biimpd 
 |-  ( ( ( F e. ( S GrpHom T ) /\ F : X -1-1-> Y ) /\ x e. X ) -> ( ( F ` x ) = U -> x = .0. ) )
18 17 ralrimiva 
 |-  ( ( F e. ( S GrpHom T ) /\ F : X -1-1-> Y ) -> A. x e. X ( ( F ` x ) = U -> x = .0. ) )
19 1 2 ghmf 
 |-  ( F e. ( S GrpHom T ) -> F : X --> Y )
20 19 adantr 
 |-  ( ( F e. ( S GrpHom T ) /\ A. x e. X ( ( F ` x ) = U -> x = .0. ) ) -> F : X --> Y )
21 eqid 
 |-  ( -g ` S ) = ( -g ` S )
22 eqid 
 |-  ( -g ` T ) = ( -g ` T )
23 1 21 22 ghmsub 
 |-  ( ( F e. ( S GrpHom T ) /\ y e. X /\ z e. X ) -> ( F ` ( y ( -g ` S ) z ) ) = ( ( F ` y ) ( -g ` T ) ( F ` z ) ) )
24 23 3expb 
 |-  ( ( F e. ( S GrpHom T ) /\ ( y e. X /\ z e. X ) ) -> ( F ` ( y ( -g ` S ) z ) ) = ( ( F ` y ) ( -g ` T ) ( F ` z ) ) )
25 24 adantlr 
 |-  ( ( ( F e. ( S GrpHom T ) /\ A. x e. X ( ( F ` x ) = U -> x = .0. ) ) /\ ( y e. X /\ z e. X ) ) -> ( F ` ( y ( -g ` S ) z ) ) = ( ( F ` y ) ( -g ` T ) ( F ` z ) ) )
26 25 eqeq1d 
 |-  ( ( ( F e. ( S GrpHom T ) /\ A. x e. X ( ( F ` x ) = U -> x = .0. ) ) /\ ( y e. X /\ z e. X ) ) -> ( ( F ` ( y ( -g ` S ) z ) ) = U <-> ( ( F ` y ) ( -g ` T ) ( F ` z ) ) = U ) )
27 fveqeq2 
 |-  ( x = ( y ( -g ` S ) z ) -> ( ( F ` x ) = U <-> ( F ` ( y ( -g ` S ) z ) ) = U ) )
28 eqeq1 
 |-  ( x = ( y ( -g ` S ) z ) -> ( x = .0. <-> ( y ( -g ` S ) z ) = .0. ) )
29 27 28 imbi12d 
 |-  ( x = ( y ( -g ` S ) z ) -> ( ( ( F ` x ) = U -> x = .0. ) <-> ( ( F ` ( y ( -g ` S ) z ) ) = U -> ( y ( -g ` S ) z ) = .0. ) ) )
30 simplr 
 |-  ( ( ( F e. ( S GrpHom T ) /\ A. x e. X ( ( F ` x ) = U -> x = .0. ) ) /\ ( y e. X /\ z e. X ) ) -> A. x e. X ( ( F ` x ) = U -> x = .0. ) )
31 10 adantr 
 |-  ( ( F e. ( S GrpHom T ) /\ A. x e. X ( ( F ` x ) = U -> x = .0. ) ) -> S e. Grp )
32 1 21 grpsubcl 
 |-  ( ( S e. Grp /\ y e. X /\ z e. X ) -> ( y ( -g ` S ) z ) e. X )
33 32 3expb 
 |-  ( ( S e. Grp /\ ( y e. X /\ z e. X ) ) -> ( y ( -g ` S ) z ) e. X )
34 31 33 sylan 
 |-  ( ( ( F e. ( S GrpHom T ) /\ A. x e. X ( ( F ` x ) = U -> x = .0. ) ) /\ ( y e. X /\ z e. X ) ) -> ( y ( -g ` S ) z ) e. X )
35 29 30 34 rspcdva 
 |-  ( ( ( F e. ( S GrpHom T ) /\ A. x e. X ( ( F ` x ) = U -> x = .0. ) ) /\ ( y e. X /\ z e. X ) ) -> ( ( F ` ( y ( -g ` S ) z ) ) = U -> ( y ( -g ` S ) z ) = .0. ) )
36 26 35 sylbird 
 |-  ( ( ( F e. ( S GrpHom T ) /\ A. x e. X ( ( F ` x ) = U -> x = .0. ) ) /\ ( y e. X /\ z e. X ) ) -> ( ( ( F ` y ) ( -g ` T ) ( F ` z ) ) = U -> ( y ( -g ` S ) z ) = .0. ) )
37 ghmgrp2 
 |-  ( F e. ( S GrpHom T ) -> T e. Grp )
38 37 ad2antrr 
 |-  ( ( ( F e. ( S GrpHom T ) /\ A. x e. X ( ( F ` x ) = U -> x = .0. ) ) /\ ( y e. X /\ z e. X ) ) -> T e. Grp )
39 19 ad2antrr 
 |-  ( ( ( F e. ( S GrpHom T ) /\ A. x e. X ( ( F ` x ) = U -> x = .0. ) ) /\ ( y e. X /\ z e. X ) ) -> F : X --> Y )
40 simprl 
 |-  ( ( ( F e. ( S GrpHom T ) /\ A. x e. X ( ( F ` x ) = U -> x = .0. ) ) /\ ( y e. X /\ z e. X ) ) -> y e. X )
41 39 40 ffvelrnd 
 |-  ( ( ( F e. ( S GrpHom T ) /\ A. x e. X ( ( F ` x ) = U -> x = .0. ) ) /\ ( y e. X /\ z e. X ) ) -> ( F ` y ) e. Y )
42 simprr 
 |-  ( ( ( F e. ( S GrpHom T ) /\ A. x e. X ( ( F ` x ) = U -> x = .0. ) ) /\ ( y e. X /\ z e. X ) ) -> z e. X )
43 39 42 ffvelrnd 
 |-  ( ( ( F e. ( S GrpHom T ) /\ A. x e. X ( ( F ` x ) = U -> x = .0. ) ) /\ ( y e. X /\ z e. X ) ) -> ( F ` z ) e. Y )
44 2 4 22 grpsubeq0 
 |-  ( ( T e. Grp /\ ( F ` y ) e. Y /\ ( F ` z ) e. Y ) -> ( ( ( F ` y ) ( -g ` T ) ( F ` z ) ) = U <-> ( F ` y ) = ( F ` z ) ) )
45 38 41 43 44 syl3anc 
 |-  ( ( ( F e. ( S GrpHom T ) /\ A. x e. X ( ( F ` x ) = U -> x = .0. ) ) /\ ( y e. X /\ z e. X ) ) -> ( ( ( F ` y ) ( -g ` T ) ( F ` z ) ) = U <-> ( F ` y ) = ( F ` z ) ) )
46 10 ad2antrr 
 |-  ( ( ( F e. ( S GrpHom T ) /\ A. x e. X ( ( F ` x ) = U -> x = .0. ) ) /\ ( y e. X /\ z e. X ) ) -> S e. Grp )
47 1 3 21 grpsubeq0 
 |-  ( ( S e. Grp /\ y e. X /\ z e. X ) -> ( ( y ( -g ` S ) z ) = .0. <-> y = z ) )
48 46 40 42 47 syl3anc 
 |-  ( ( ( F e. ( S GrpHom T ) /\ A. x e. X ( ( F ` x ) = U -> x = .0. ) ) /\ ( y e. X /\ z e. X ) ) -> ( ( y ( -g ` S ) z ) = .0. <-> y = z ) )
49 36 45 48 3imtr3d 
 |-  ( ( ( F e. ( S GrpHom T ) /\ A. x e. X ( ( F ` x ) = U -> x = .0. ) ) /\ ( y e. X /\ z e. X ) ) -> ( ( F ` y ) = ( F ` z ) -> y = z ) )
50 49 ralrimivva 
 |-  ( ( F e. ( S GrpHom T ) /\ A. x e. X ( ( F ` x ) = U -> x = .0. ) ) -> A. y e. X A. z e. X ( ( F ` y ) = ( F ` z ) -> y = z ) )
51 dff13 
 |-  ( F : X -1-1-> Y <-> ( F : X --> Y /\ A. y e. X A. z e. X ( ( F ` y ) = ( F ` z ) -> y = z ) ) )
52 20 50 51 sylanbrc 
 |-  ( ( F e. ( S GrpHom T ) /\ A. x e. X ( ( F ` x ) = U -> x = .0. ) ) -> F : X -1-1-> Y )
53 18 52 impbida 
 |-  ( F e. ( S GrpHom T ) -> ( F : X -1-1-> Y <-> A. x e. X ( ( F ` x ) = U -> x = .0. ) ) )