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 gim0to0ALT.a A = Base R
gim0to0ALT.b B = Base S
gim0to0ALT.n N = 0 S
gim0to0ALT.0 0 ˙ = 0 R
Assertion gim0to0 F R GrpIso S X A F X = N X = 0 ˙

Proof

Step Hyp Ref Expression
1 gim0to0ALT.a A = Base R
2 gim0to0ALT.b B = Base S
3 gim0to0ALT.n N = 0 S
4 gim0to0ALT.0 0 ˙ = 0 R
5 gimghm F R GrpIso S F R GrpHom S
6 1 2 gimf1o F 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 R GrpIso S F : A 1-1 B
9 5 8 jca F R GrpIso S F R GrpHom S F : A 1-1 B
10 9 anim1i F R GrpIso S X A F R GrpHom S F : A 1-1 B X A
11 df-3an F R GrpHom S F : A 1-1 B X A F R GrpHom S F : A 1-1 B X A
12 10 11 sylibr F R GrpIso S X A F R GrpHom S F : A 1-1 B X A
13 1 2 3 4 f1ghm0to0 F R GrpHom S F : A 1-1 B X A F X = N X = 0 ˙
14 12 13 syl F R GrpIso S X A F X = N X = 0 ˙