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) (Proof shortened by AV, 4-Apr-2025)

Ref Expression
Hypotheses f1ghm0to0.a 
|- A = ( Base ` R )
f1ghm0to0.b 
|- B = ( Base ` S )
f1ghm0to0.n 
|- N = ( 0g ` R )
f1ghm0to0.0 
|- .0. = ( 0g ` S )
Assertion ghmf1 
|- ( F e. ( R GrpHom S ) -> ( F : A -1-1-> B <-> A. x e. A ( ( F ` x ) = .0. -> x = N ) ) )

Proof

Step Hyp Ref Expression
1 f1ghm0to0.a 
 |-  A = ( Base ` R )
2 f1ghm0to0.b 
 |-  B = ( Base ` S )
3 f1ghm0to0.n 
 |-  N = ( 0g ` R )
4 f1ghm0to0.0 
 |-  .0. = ( 0g ` S )
5 1 2 3 4 f1ghm0to0 
 |-  ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B /\ x e. A ) -> ( ( F ` x ) = .0. <-> x = N ) )
6 5 3expa 
 |-  ( ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B ) /\ x e. A ) -> ( ( F ` x ) = .0. <-> x = N ) )
7 6 biimpd 
 |-  ( ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B ) /\ x e. A ) -> ( ( F ` x ) = .0. -> x = N ) )
8 7 ralrimiva 
 |-  ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B ) -> A. x e. A ( ( F ` x ) = .0. -> x = N ) )
9 1 2 ghmf 
 |-  ( F e. ( R GrpHom S ) -> F : A --> B )
10 9 adantr 
 |-  ( ( F e. ( R GrpHom S ) /\ A. x e. A ( ( F ` x ) = .0. -> x = N ) ) -> F : A --> B )
11 eqid 
 |-  ( -g ` R ) = ( -g ` R )
12 eqid 
 |-  ( -g ` S ) = ( -g ` S )
13 1 11 12 ghmsub 
 |-  ( ( F e. ( R GrpHom S ) /\ y e. A /\ z e. A ) -> ( F ` ( y ( -g ` R ) z ) ) = ( ( F ` y ) ( -g ` S ) ( F ` z ) ) )
14 13 3expb 
 |-  ( ( F e. ( R GrpHom S ) /\ ( y e. A /\ z e. A ) ) -> ( F ` ( y ( -g ` R ) z ) ) = ( ( F ` y ) ( -g ` S ) ( F ` z ) ) )
15 14 adantlr 
 |-  ( ( ( F e. ( R GrpHom S ) /\ A. x e. A ( ( F ` x ) = .0. -> x = N ) ) /\ ( y e. A /\ z e. A ) ) -> ( F ` ( y ( -g ` R ) z ) ) = ( ( F ` y ) ( -g ` S ) ( F ` z ) ) )
16 15 eqeq1d 
 |-  ( ( ( F e. ( R GrpHom S ) /\ A. x e. A ( ( F ` x ) = .0. -> x = N ) ) /\ ( y e. A /\ z e. A ) ) -> ( ( F ` ( y ( -g ` R ) z ) ) = .0. <-> ( ( F ` y ) ( -g ` S ) ( F ` z ) ) = .0. ) )
17 fveqeq2 
 |-  ( x = ( y ( -g ` R ) z ) -> ( ( F ` x ) = .0. <-> ( F ` ( y ( -g ` R ) z ) ) = .0. ) )
18 eqeq1 
 |-  ( x = ( y ( -g ` R ) z ) -> ( x = N <-> ( y ( -g ` R ) z ) = N ) )
19 17 18 imbi12d 
 |-  ( x = ( y ( -g ` R ) z ) -> ( ( ( F ` x ) = .0. -> x = N ) <-> ( ( F ` ( y ( -g ` R ) z ) ) = .0. -> ( y ( -g ` R ) z ) = N ) ) )
20 simplr 
 |-  ( ( ( F e. ( R GrpHom S ) /\ A. x e. A ( ( F ` x ) = .0. -> x = N ) ) /\ ( y e. A /\ z e. A ) ) -> A. x e. A ( ( F ` x ) = .0. -> x = N ) )
21 ghmgrp1 
 |-  ( F e. ( R GrpHom S ) -> R e. Grp )
22 21 adantr 
 |-  ( ( F e. ( R GrpHom S ) /\ A. x e. A ( ( F ` x ) = .0. -> x = N ) ) -> R e. Grp )
23 1 11 grpsubcl 
 |-  ( ( R e. Grp /\ y e. A /\ z e. A ) -> ( y ( -g ` R ) z ) e. A )
24 23 3expb 
 |-  ( ( R e. Grp /\ ( y e. A /\ z e. A ) ) -> ( y ( -g ` R ) z ) e. A )
25 22 24 sylan 
 |-  ( ( ( F e. ( R GrpHom S ) /\ A. x e. A ( ( F ` x ) = .0. -> x = N ) ) /\ ( y e. A /\ z e. A ) ) -> ( y ( -g ` R ) z ) e. A )
26 19 20 25 rspcdva 
 |-  ( ( ( F e. ( R GrpHom S ) /\ A. x e. A ( ( F ` x ) = .0. -> x = N ) ) /\ ( y e. A /\ z e. A ) ) -> ( ( F ` ( y ( -g ` R ) z ) ) = .0. -> ( y ( -g ` R ) z ) = N ) )
27 16 26 sylbird 
 |-  ( ( ( F e. ( R GrpHom S ) /\ A. x e. A ( ( F ` x ) = .0. -> x = N ) ) /\ ( y e. A /\ z e. A ) ) -> ( ( ( F ` y ) ( -g ` S ) ( F ` z ) ) = .0. -> ( y ( -g ` R ) z ) = N ) )
28 ghmgrp2 
 |-  ( F e. ( R GrpHom S ) -> S e. Grp )
29 28 ad2antrr 
 |-  ( ( ( F e. ( R GrpHom S ) /\ A. x e. A ( ( F ` x ) = .0. -> x = N ) ) /\ ( y e. A /\ z e. A ) ) -> S e. Grp )
30 9 ad2antrr 
 |-  ( ( ( F e. ( R GrpHom S ) /\ A. x e. A ( ( F ` x ) = .0. -> x = N ) ) /\ ( y e. A /\ z e. A ) ) -> F : A --> B )
31 simprl 
 |-  ( ( ( F e. ( R GrpHom S ) /\ A. x e. A ( ( F ` x ) = .0. -> x = N ) ) /\ ( y e. A /\ z e. A ) ) -> y e. A )
32 30 31 ffvelcdmd 
 |-  ( ( ( F e. ( R GrpHom S ) /\ A. x e. A ( ( F ` x ) = .0. -> x = N ) ) /\ ( y e. A /\ z e. A ) ) -> ( F ` y ) e. B )
33 simprr 
 |-  ( ( ( F e. ( R GrpHom S ) /\ A. x e. A ( ( F ` x ) = .0. -> x = N ) ) /\ ( y e. A /\ z e. A ) ) -> z e. A )
34 30 33 ffvelcdmd 
 |-  ( ( ( F e. ( R GrpHom S ) /\ A. x e. A ( ( F ` x ) = .0. -> x = N ) ) /\ ( y e. A /\ z e. A ) ) -> ( F ` z ) e. B )
35 2 4 12 grpsubeq0 
 |-  ( ( S e. Grp /\ ( F ` y ) e. B /\ ( F ` z ) e. B ) -> ( ( ( F ` y ) ( -g ` S ) ( F ` z ) ) = .0. <-> ( F ` y ) = ( F ` z ) ) )
36 29 32 34 35 syl3anc 
 |-  ( ( ( F e. ( R GrpHom S ) /\ A. x e. A ( ( F ` x ) = .0. -> x = N ) ) /\ ( y e. A /\ z e. A ) ) -> ( ( ( F ` y ) ( -g ` S ) ( F ` z ) ) = .0. <-> ( F ` y ) = ( F ` z ) ) )
37 21 ad2antrr 
 |-  ( ( ( F e. ( R GrpHom S ) /\ A. x e. A ( ( F ` x ) = .0. -> x = N ) ) /\ ( y e. A /\ z e. A ) ) -> R e. Grp )
38 1 3 11 grpsubeq0 
 |-  ( ( R e. Grp /\ y e. A /\ z e. A ) -> ( ( y ( -g ` R ) z ) = N <-> y = z ) )
39 37 31 33 38 syl3anc 
 |-  ( ( ( F e. ( R GrpHom S ) /\ A. x e. A ( ( F ` x ) = .0. -> x = N ) ) /\ ( y e. A /\ z e. A ) ) -> ( ( y ( -g ` R ) z ) = N <-> y = z ) )
40 27 36 39 3imtr3d 
 |-  ( ( ( F e. ( R GrpHom S ) /\ A. x e. A ( ( F ` x ) = .0. -> x = N ) ) /\ ( y e. A /\ z e. A ) ) -> ( ( F ` y ) = ( F ` z ) -> y = z ) )
41 40 ralrimivva 
 |-  ( ( F e. ( R GrpHom S ) /\ A. x e. A ( ( F ` x ) = .0. -> x = N ) ) -> A. y e. A A. z e. A ( ( F ` y ) = ( F ` z ) -> y = z ) )
42 dff13 
 |-  ( F : A -1-1-> B <-> ( F : A --> B /\ A. y e. A A. z e. A ( ( F ` y ) = ( F ` z ) -> y = z ) ) )
43 10 41 42 sylanbrc 
 |-  ( ( F e. ( R GrpHom S ) /\ A. x e. A ( ( F ` x ) = .0. -> x = N ) ) -> F : A -1-1-> B )
44 8 43 impbida 
 |-  ( F e. ( R GrpHom S ) -> ( F : A -1-1-> B <-> A. x e. A ( ( F ` x ) = .0. -> x = N ) ) )