ghmf1

Description: Two ways of saying a group homomorphism is 1-1 into its codomain. (Contributed by Paul Chapman, 3-Mar-2008) (Revised by Mario Carneiro, 13-Jan-2015) (Proof shortened by AV, 4-Apr-2025)

	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	ghmf1	$⊢ F \in (R GrpHom S) \to (F : A \underset{1-1}{⟶} B \leftrightarrow \forall x \in A (F (x) = \underset{˙}{0} \to 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	1 2 3 4	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)$
6	5	3expa	$⊢ ((F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B) \land x \in A) \to (F (x) = \underset{˙}{0} \leftrightarrow x = N)$
7	6	biimpd	$⊢ ((F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B) \land x \in A) \to (F (x) = \underset{˙}{0} \to x = N)$
8	7	ralrimiva	$⊢ (F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B) \to \forall x \in A (F (x) = \underset{˙}{0} \to x = N)$
9	1 2	ghmf	$⊢ F \in (R GrpHom S) \to F : A ⟶ B$
10	9	adantr	$⊢ (F \in (R GrpHom S) \land \forall x \in A (F (x) = \underset{˙}{0} \to x = N)) \to F : A ⟶ B$
11		eqid	$⊢ -_{R} = -_{R}$
12		eqid	$⊢ -_{S} = -_{S}$
13	1 11 12	ghmsub	$⊢ (F \in (R GrpHom S) \land y \in A \land z \in A) \to F (y -_{R} z) = F (y) -_{S} F (z)$
14	13	3expb	$⊢ (F \in (R GrpHom S) \land (y \in A \land z \in A)) \to F (y -_{R} z) = F (y) -_{S} F (z)$
15	14	adantlr	$⊢ ((F \in (R GrpHom S) \land \forall x \in A (F (x) = \underset{˙}{0} \to x = N)) \land (y \in A \land z \in A)) \to F (y -_{R} z) = F (y) -_{S} F (z)$
16	15	eqeq1d	$⊢ ((F \in (R GrpHom S) \land \forall x \in A (F (x) = \underset{˙}{0} \to x = N)) \land (y \in A \land z \in A)) \to (F (y -_{R} z) = \underset{˙}{0} \leftrightarrow F (y) -_{S} F (z) = \underset{˙}{0})$
17		fveqeq2	$⊢ x = y -_{R} z \to (F (x) = \underset{˙}{0} \leftrightarrow F (y -_{R} z) = \underset{˙}{0})$
18		eqeq1	$⊢ x = y -_{R} z \to (x = N \leftrightarrow y -_{R} z = N)$
19	17 18	imbi12d	$⊢ x = y -_{R} z \to ((F (x) = \underset{˙}{0} \to x = N) \leftrightarrow (F (y -_{R} z) = \underset{˙}{0} \to y -_{R} z = N))$
20		simplr	$⊢ ((F \in (R GrpHom S) \land \forall x \in A (F (x) = \underset{˙}{0} \to x = N)) \land (y \in A \land z \in A)) \to \forall x \in A (F (x) = \underset{˙}{0} \to x = N)$
21		ghmgrp1	$⊢ F \in (R GrpHom S) \to R \in Grp$
22	21	adantr	$⊢ (F \in (R GrpHom S) \land \forall x \in A (F (x) = \underset{˙}{0} \to x = N)) \to R \in Grp$
23	1 11	grpsubcl	$⊢ (R \in Grp \land y \in A \land z \in A) \to y -_{R} z \in A$
24	23	3expb	$⊢ (R \in Grp \land (y \in A \land z \in A)) \to y -_{R} z \in A$
25	22 24	sylan	$⊢ ((F \in (R GrpHom S) \land \forall x \in A (F (x) = \underset{˙}{0} \to x = N)) \land (y \in A \land z \in A)) \to y -_{R} z \in A$
26	19 20 25	rspcdva	$⊢ ((F \in (R GrpHom S) \land \forall x \in A (F (x) = \underset{˙}{0} \to x = N)) \land (y \in A \land z \in A)) \to (F (y -_{R} z) = \underset{˙}{0} \to y -_{R} z = N)$
27	16 26	sylbird	$⊢ ((F \in (R GrpHom S) \land \forall x \in A (F (x) = \underset{˙}{0} \to x = N)) \land (y \in A \land z \in A)) \to (F (y) -_{S} F (z) = \underset{˙}{0} \to y -_{R} z = N)$
28		ghmgrp2	$⊢ F \in (R GrpHom S) \to S \in Grp$
29	28	ad2antrr	$⊢ ((F \in (R GrpHom S) \land \forall x \in A (F (x) = \underset{˙}{0} \to x = N)) \land (y \in A \land z \in A)) \to S \in Grp$
30	9	ad2antrr	$⊢ ((F \in (R GrpHom S) \land \forall x \in A (F (x) = \underset{˙}{0} \to x = N)) \land (y \in A \land z \in A)) \to F : A ⟶ B$
31		simprl	$⊢ ((F \in (R GrpHom S) \land \forall x \in A (F (x) = \underset{˙}{0} \to x = N)) \land (y \in A \land z \in A)) \to y \in A$
32	30 31	ffvelcdmd	$⊢ ((F \in (R GrpHom S) \land \forall x \in A (F (x) = \underset{˙}{0} \to x = N)) \land (y \in A \land z \in A)) \to F (y) \in B$
33		simprr	$⊢ ((F \in (R GrpHom S) \land \forall x \in A (F (x) = \underset{˙}{0} \to x = N)) \land (y \in A \land z \in A)) \to z \in A$
34	30 33	ffvelcdmd	$⊢ ((F \in (R GrpHom S) \land \forall x \in A (F (x) = \underset{˙}{0} \to x = N)) \land (y \in A \land z \in A)) \to F (z) \in B$
35	2 4 12	grpsubeq0	$⊢ (S \in Grp \land F (y) \in B \land F (z) \in B) \to (F (y) -_{S} F (z) = \underset{˙}{0} \leftrightarrow F (y) = F (z))$
36	29 32 34 35	syl3anc	$⊢ ((F \in (R GrpHom S) \land \forall x \in A (F (x) = \underset{˙}{0} \to x = N)) \land (y \in A \land z \in A)) \to (F (y) -_{S} F (z) = \underset{˙}{0} \leftrightarrow F (y) = F (z))$
37	21	ad2antrr	$⊢ ((F \in (R GrpHom S) \land \forall x \in A (F (x) = \underset{˙}{0} \to x = N)) \land (y \in A \land z \in A)) \to R \in Grp$
38	1 3 11	grpsubeq0	$⊢ (R \in Grp \land y \in A \land z \in A) \to (y -_{R} z = N \leftrightarrow y = z)$
39	37 31 33 38	syl3anc	$⊢ ((F \in (R GrpHom S) \land \forall x \in A (F (x) = \underset{˙}{0} \to x = N)) \land (y \in A \land z \in A)) \to (y -_{R} z = N \leftrightarrow y = z)$
40	27 36 39	3imtr3d	$⊢ ((F \in (R GrpHom S) \land \forall x \in A (F (x) = \underset{˙}{0} \to x = N)) \land (y \in A \land z \in A)) \to (F (y) = F (z) \to y = z)$
41	40	ralrimivva	$⊢ (F \in (R GrpHom S) \land \forall x \in A (F (x) = \underset{˙}{0} \to x = N)) \to \forall y \in A \forall z \in A (F (y) = F (z) \to y = z)$
42		dff13	$⊢ F : A \underset{1-1}{⟶} B \leftrightarrow (F : A ⟶ B \land \forall y \in A \forall z \in A (F (y) = F (z) \to y = z))$
43	10 41 42	sylanbrc	$⊢ (F \in (R GrpHom S) \land \forall x \in A (F (x) = \underset{˙}{0} \to x = N)) \to F : A \underset{1-1}{⟶} B$
44	8 43	impbida	$⊢ F \in (R GrpHom S) \to (F : A \underset{1-1}{⟶} B \leftrightarrow \forall x \in A (F (x) = \underset{˙}{0} \to x = N))$

Metamath Proof Explorer

Theorem ghmf1

Proof