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)

	Ref	Expression
Hypotheses	ghmf1.x	$⊢ X = {Base}_{S}$
	ghmf1.y	$⊢ Y = {Base}_{T}$
	ghmf1.z	$⊢ \underset{˙}{0} = 0_{S}$
	ghmf1.u	$⊢ U = 0_{T}$
Assertion	ghmf1	$⊢ F \in (S GrpHom T) \to (F : X \underset{1-1}{⟶} Y \leftrightarrow \forall x \in X (F (x) = U \to x = \underset{˙}{0}))$

Proof

Step	Hyp	Ref	Expression
1		ghmf1.x	$⊢ X = {Base}_{S}$
2		ghmf1.y	$⊢ Y = {Base}_{T}$
3		ghmf1.z	$⊢ \underset{˙}{0} = 0_{S}$
4		ghmf1.u	$⊢ U = 0_{T}$
5	3 4	ghmid	$⊢ F \in (S GrpHom T) \to F (\underset{˙}{0}) = U$
6	5	ad2antrr	$⊢ ((F \in (S GrpHom T) \land F : X \underset{1-1}{⟶} Y) \land x \in X) \to F (\underset{˙}{0}) = U$
7	6	eqeq2d	$⊢ ((F \in (S GrpHom T) \land F : X \underset{1-1}{⟶} Y) \land x \in X) \to (F (x) = F (\underset{˙}{0}) \leftrightarrow F (x) = U)$
8		simplr	$⊢ ((F \in (S GrpHom T) \land F : X \underset{1-1}{⟶} Y) \land x \in X) \to F : X \underset{1-1}{⟶} Y$
9		simpr	$⊢ ((F \in (S GrpHom T) \land F : X \underset{1-1}{⟶} Y) \land x \in X) \to x \in X$
10		ghmgrp1	$⊢ F \in (S GrpHom T) \to S \in Grp$
11	10	ad2antrr	$⊢ ((F \in (S GrpHom T) \land F : X \underset{1-1}{⟶} Y) \land x \in X) \to S \in Grp$
12	1 3	grpidcl	$⊢ S \in Grp \to \underset{˙}{0} \in X$
13	11 12	syl	$⊢ ((F \in (S GrpHom T) \land F : X \underset{1-1}{⟶} Y) \land x \in X) \to \underset{˙}{0} \in X$
14		f1fveq	$⊢ (F : X \underset{1-1}{⟶} Y \land (x \in X \land \underset{˙}{0} \in X)) \to (F (x) = F (\underset{˙}{0}) \leftrightarrow x = \underset{˙}{0})$
15	8 9 13 14	syl12anc	$⊢ ((F \in (S GrpHom T) \land F : X \underset{1-1}{⟶} Y) \land x \in X) \to (F (x) = F (\underset{˙}{0}) \leftrightarrow x = \underset{˙}{0})$
16	7 15	bitr3d	$⊢ ((F \in (S GrpHom T) \land F : X \underset{1-1}{⟶} Y) \land x \in X) \to (F (x) = U \leftrightarrow x = \underset{˙}{0})$
17	16	biimpd	$⊢ ((F \in (S GrpHom T) \land F : X \underset{1-1}{⟶} Y) \land x \in X) \to (F (x) = U \to x = \underset{˙}{0})$
18	17	ralrimiva	$⊢ (F \in (S GrpHom T) \land F : X \underset{1-1}{⟶} Y) \to \forall x \in X (F (x) = U \to x = \underset{˙}{0})$
19	1 2	ghmf	$⊢ F \in (S GrpHom T) \to F : X ⟶ Y$
20	19	adantr	$⊢ (F \in (S GrpHom T) \land \forall x \in X (F (x) = U \to x = \underset{˙}{0})) \to F : X ⟶ Y$
21		eqid	$⊢ -_{S} = -_{S}$
22		eqid	$⊢ -_{T} = -_{T}$
23	1 21 22	ghmsub	$⊢ (F \in (S GrpHom T) \land y \in X \land z \in X) \to F (y -_{S} z) = F (y) -_{T} F (z)$
24	23	3expb	$⊢ (F \in (S GrpHom T) \land (y \in X \land z \in X)) \to F (y -_{S} z) = F (y) -_{T} F (z)$
25	24	adantlr	$⊢ ((F \in (S GrpHom T) \land \forall x \in X (F (x) = U \to x = \underset{˙}{0})) \land (y \in X \land z \in X)) \to F (y -_{S} z) = F (y) -_{T} F (z)$
26	25	eqeq1d	$⊢ ((F \in (S GrpHom T) \land \forall x \in X (F (x) = U \to x = \underset{˙}{0})) \land (y \in X \land z \in X)) \to (F (y -_{S} z) = U \leftrightarrow F (y) -_{T} F (z) = U)$
27		fveqeq2	$⊢ x = y -_{S} z \to (F (x) = U \leftrightarrow F (y -_{S} z) = U)$
28		eqeq1	$⊢ x = y -_{S} z \to (x = \underset{˙}{0} \leftrightarrow y -_{S} z = \underset{˙}{0})$
29	27 28	imbi12d	$⊢ x = y -_{S} z \to ((F (x) = U \to x = \underset{˙}{0}) \leftrightarrow (F (y -_{S} z) = U \to y -_{S} z = \underset{˙}{0}))$
30		simplr	$⊢ ((F \in (S GrpHom T) \land \forall x \in X (F (x) = U \to x = \underset{˙}{0})) \land (y \in X \land z \in X)) \to \forall x \in X (F (x) = U \to x = \underset{˙}{0})$
31	10	adantr	$⊢ (F \in (S GrpHom T) \land \forall x \in X (F (x) = U \to x = \underset{˙}{0})) \to S \in Grp$
32	1 21	grpsubcl	$⊢ (S \in Grp \land y \in X \land z \in X) \to y -_{S} z \in X$
33	32	3expb	$⊢ (S \in Grp \land (y \in X \land z \in X)) \to y -_{S} z \in X$
34	31 33	sylan	$⊢ ((F \in (S GrpHom T) \land \forall x \in X (F (x) = U \to x = \underset{˙}{0})) \land (y \in X \land z \in X)) \to y -_{S} z \in X$
35	29 30 34	rspcdva	$⊢ ((F \in (S GrpHom T) \land \forall x \in X (F (x) = U \to x = \underset{˙}{0})) \land (y \in X \land z \in X)) \to (F (y -_{S} z) = U \to y -_{S} z = \underset{˙}{0})$
36	26 35	sylbird	$⊢ ((F \in (S GrpHom T) \land \forall x \in X (F (x) = U \to x = \underset{˙}{0})) \land (y \in X \land z \in X)) \to (F (y) -_{T} F (z) = U \to y -_{S} z = \underset{˙}{0})$
37		ghmgrp2	$⊢ F \in (S GrpHom T) \to T \in Grp$
38	37	ad2antrr	$⊢ ((F \in (S GrpHom T) \land \forall x \in X (F (x) = U \to x = \underset{˙}{0})) \land (y \in X \land z \in X)) \to T \in Grp$
39	19	ad2antrr	$⊢ ((F \in (S GrpHom T) \land \forall x \in X (F (x) = U \to x = \underset{˙}{0})) \land (y \in X \land z \in X)) \to F : X ⟶ Y$
40		simprl	$⊢ ((F \in (S GrpHom T) \land \forall x \in X (F (x) = U \to x = \underset{˙}{0})) \land (y \in X \land z \in X)) \to y \in X$
41	39 40	ffvelcdmd	$⊢ ((F \in (S GrpHom T) \land \forall x \in X (F (x) = U \to x = \underset{˙}{0})) \land (y \in X \land z \in X)) \to F (y) \in Y$
42		simprr	$⊢ ((F \in (S GrpHom T) \land \forall x \in X (F (x) = U \to x = \underset{˙}{0})) \land (y \in X \land z \in X)) \to z \in X$
43	39 42	ffvelcdmd	$⊢ ((F \in (S GrpHom T) \land \forall x \in X (F (x) = U \to x = \underset{˙}{0})) \land (y \in X \land z \in X)) \to F (z) \in Y$
44	2 4 22	grpsubeq0	$⊢ (T \in Grp \land F (y) \in Y \land F (z) \in Y) \to (F (y) -_{T} F (z) = U \leftrightarrow F (y) = F (z))$
45	38 41 43 44	syl3anc	$⊢ ((F \in (S GrpHom T) \land \forall x \in X (F (x) = U \to x = \underset{˙}{0})) \land (y \in X \land z \in X)) \to (F (y) -_{T} F (z) = U \leftrightarrow F (y) = F (z))$
46	10	ad2antrr	$⊢ ((F \in (S GrpHom T) \land \forall x \in X (F (x) = U \to x = \underset{˙}{0})) \land (y \in X \land z \in X)) \to S \in Grp$
47	1 3 21	grpsubeq0	$⊢ (S \in Grp \land y \in X \land z \in X) \to (y -_{S} z = \underset{˙}{0} \leftrightarrow y = z)$
48	46 40 42 47	syl3anc	$⊢ ((F \in (S GrpHom T) \land \forall x \in X (F (x) = U \to x = \underset{˙}{0})) \land (y \in X \land z \in X)) \to (y -_{S} z = \underset{˙}{0} \leftrightarrow y = z)$
49	36 45 48	3imtr3d	$⊢ ((F \in (S GrpHom T) \land \forall x \in X (F (x) = U \to x = \underset{˙}{0})) \land (y \in X \land z \in X)) \to (F (y) = F (z) \to y = z)$
50	49	ralrimivva	$⊢ (F \in (S GrpHom T) \land \forall x \in X (F (x) = U \to x = \underset{˙}{0})) \to \forall y \in X \forall z \in X (F (y) = F (z) \to y = z)$
51		dff13	$⊢ F : X \underset{1-1}{⟶} Y \leftrightarrow (F : X ⟶ Y \land \forall y \in X \forall z \in X (F (y) = F (z) \to y = z))$
52	20 50 51	sylanbrc	$⊢ (F \in (S GrpHom T) \land \forall x \in X (F (x) = U \to x = \underset{˙}{0})) \to F : X \underset{1-1}{⟶} Y$
53	18 52	impbida	$⊢ F \in (S GrpHom T) \to (F : X \underset{1-1}{⟶} Y \leftrightarrow \forall x \in X (F (x) = U \to x = \underset{˙}{0}))$

Metamath Proof Explorer

Theorem ghmf1

Proof