Theorem 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={\mathrm{Base}}_R$$
	f1ghm0to0.b	$$⊢B={\mathrm{Base}}_S$$
	f1ghm0to0.n	$$⊢N=0_S$$
	f1ghm0to0.1	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	f1ghm0to0	$$⊢\left(F\in \left(R\mathrm{GrpHom}S\right)\wedge F:A\underset{1-1}{⟶}B\wedge X\in A\right)\to \left(F\left(X\right)=N\leftrightarrow X=\underset{\dot{}}{0}\right)$$

Proof

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