This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gim0to0

Description: A group isomorphism maps the zero of one group (and only the zero) to the zero of the other group. (Contributed by AV, 24-Oct-2019) (Revised by Thierry Arnoux, 23-May-2023)

Ref Expression
Hypotheses gim0to0.a 
|- A = ( Base ` R )
gim0to0.b 
|- B = ( Base ` S )
gim0to0.n 
|- N = ( 0g ` S )
gim0to0.0 
|- .0. = ( 0g ` R )
Assertion gim0to0 
|- ( ( F e. ( R GrpIso S ) /\ X e. A ) -> ( ( F ` X ) = N <-> X = .0. ) )

Proof

Step Hyp Ref Expression
1 gim0to0.a 
 |-  A = ( Base ` R )
2 gim0to0.b 
 |-  B = ( Base ` S )
3 gim0to0.n 
 |-  N = ( 0g ` S )
4 gim0to0.0 
 |-  .0. = ( 0g ` R )
5 gimghm 
 |-  ( F e. ( R GrpIso S ) -> F e. ( R GrpHom S ) )
6 1 2 gimf1o 
 |-  ( F e. ( R GrpIso S ) -> F : A -1-1-onto-> B )
7 f1of1 
 |-  ( F : A -1-1-onto-> B -> F : A -1-1-> B )
8 6 7 syl 
 |-  ( F e. ( R GrpIso S ) -> F : A -1-1-> B )
9 5 8 jca 
 |-  ( F e. ( R GrpIso S ) -> ( F e. ( R GrpHom S ) /\ F : A -1-1-> B ) )
10 9 anim1i 
 |-  ( ( F e. ( R GrpIso S ) /\ X e. A ) -> ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B ) /\ X e. A ) )
11 df-3an 
 |-  ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B /\ X e. A ) <-> ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B ) /\ X e. A ) )
12 10 11 sylibr 
 |-  ( ( F e. ( R GrpIso S ) /\ X e. A ) -> ( F e. ( R GrpHom S ) /\ F : A -1-1-> B /\ X e. A ) )
13 1 2 4 3 f1ghm0to0 
 |-  ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B /\ X e. A ) -> ( ( F ` X ) = N <-> X = .0. ) )
14 12 13 syl 
 |-  ( ( F e. ( R GrpIso S ) /\ X e. A ) -> ( ( F ` X ) = N <-> X = .0. ) )