f1ghm0to0

Description: If a group homomorphism F is injective, it 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, 13-May-2023)

	Ref	Expression
Hypotheses	f1ghm0to0.a	$⊢ A = {Base}_{R}$
	f1ghm0to0.b	$⊢ B = {Base}_{S}$
	f1ghm0to0.n	$⊢ N = 0_{R}$
	f1ghm0to0.0	$⊢ \underset{˙}{0} = 0_{S}$
Assertion	f1ghm0to0	$⊢ (F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B \land X \in A) \to (F (X) = \underset{˙}{0} \leftrightarrow X = N)$

Proof

Step	Hyp	Ref	Expression
1		f1ghm0to0.a	$⊢ A = {Base}_{R}$
2		f1ghm0to0.b	$⊢ B = {Base}_{S}$
3		f1ghm0to0.n	$⊢ N = 0_{R}$
4		f1ghm0to0.0	$⊢ \underset{˙}{0} = 0_{S}$
5	3 4	ghmid	$⊢ F \in (R GrpHom S) \to F (N) = \underset{˙}{0}$
6	5	3ad2ant1	$⊢ (F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B \land X \in A) \to F (N) = \underset{˙}{0}$
7	6	eqeq2d	$⊢ (F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B \land X \in A) \to (F (X) = F (N) \leftrightarrow F (X) = \underset{˙}{0})$
8		simp2	$⊢ (F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B \land X \in A) \to F : A \underset{1-1}{⟶} B$
9		simp3	$⊢ (F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B \land X \in A) \to X \in A$
10		ghmgrp1	$⊢ F \in (R GrpHom S) \to R \in Grp$
11	1 3	grpidcl	$⊢ R \in Grp \to N \in A$
12	10 11	syl	$⊢ F \in (R GrpHom S) \to N \in A$
13	12	3ad2ant1	$⊢ (F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B \land X \in A) \to N \in A$
14		f1veqaeq	$⊢ (F : A \underset{1-1}{⟶} B \land (X \in A \land N \in A)) \to (F (X) = F (N) \to X = N)$
15	8 9 13 14	syl12anc	$⊢ (F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B \land X \in A) \to (F (X) = F (N) \to X = N)$
16	7 15	sylbird	$⊢ (F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B \land X \in A) \to (F (X) = \underset{˙}{0} \to X = N)$
17		fveq2	$⊢ X = N \to F (X) = F (N)$
18	17 6	sylan9eqr	$⊢ ((F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B \land X \in A) \land X = N) \to F (X) = \underset{˙}{0}$
19	18	ex	$⊢ (F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B \land X \in A) \to (X = N \to F (X) = \underset{˙}{0})$
20	16 19	impbid	$⊢ (F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B \land X \in A) \to (F (X) = \underset{˙}{0} \leftrightarrow X = N)$

Metamath Proof Explorer

Theorem f1ghm0to0

Proof