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	$⊢ \underset{˙}{0} = 0_{R}$
	Assertion	gim0to0	$⊢ (F \in (R GrpIso S) \land X \in A) \to (F (X) = N \leftrightarrow X = \underset{˙}{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	$⊢ \underset{˙}{0} = 0_{R}$
5		gimghm	$⊢ F \in (R GrpIso S) \to F \in (R GrpHom S)$
6	1 2	gimf1o	$⊢ F \in (R GrpIso S) \to F : A \underset{1-1 onto}{⟶} B$
7		f1of1	$⊢ F : A \underset{1-1 onto}{⟶} B \to F : A \underset{1-1}{⟶} B$
8	6 7	syl	$⊢ F \in (R GrpIso S) \to F : A \underset{1-1}{⟶} B$
9	5 8	jca	$⊢ F \in (R GrpIso S) \to (F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B)$
10	9	anim1i	$⊢ (F \in (R GrpIso S) \land X \in A) \to ((F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B) \land X \in A)$
11		df-3an	$⊢ (F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B \land X \in A) \leftrightarrow ((F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B) \land X \in A)$
12	10 11	sylibr	$⊢ (F \in (R GrpIso S) \land X \in A) \to (F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B \land X \in A)$
13	1 2 3 4	f1ghm0to0	$⊢ (F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B \land X \in A) \to (F (X) = N \leftrightarrow X = \underset{˙}{0})$
14	12 13	syl	$⊢ (F \in (R GrpIso S) \land X \in A) \to (F (X) = N \leftrightarrow X = \underset{˙}{0})$