grpokerinj

Description: A group homomorphism is injective if and only if its kernel is zero. (Contributed by Jeff Madsen, 16-Jun-2011)

	Ref	Expression
Hypotheses	grpkerinj.1	$⊢ X = ran G$
	grpkerinj.2	$⊢ W = GId (G)$
	grpkerinj.3	$⊢ Y = ran H$
	grpkerinj.4	$⊢ U = GId (H)$
Assertion	grpokerinj	$⊢ (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to (F : X \underset{1-1}{⟶} Y \leftrightarrow F^{-1} [\{U\}] = \{W\})$

Proof

Step	Hyp	Ref	Expression
1		grpkerinj.1	$⊢ X = ran G$
2		grpkerinj.2	$⊢ W = GId (G)$
3		grpkerinj.3	$⊢ Y = ran H$
4		grpkerinj.4	$⊢ U = GId (H)$
5	2 4	ghomidOLD	$⊢ (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to F (W) = U$
6	5	sneqd	$⊢ (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to \{F (W)\} = \{U\}$
7	1 3	ghomf	$⊢ (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to F : X ⟶ Y$
8	7	ffnd	$⊢ (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to F Fn X$
9	1 2	grpoidcl	$⊢ G \in GrpOp \to W \in X$
10	9	3ad2ant1	$⊢ (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to W \in X$
11		fnsnfv	$⊢ (F Fn X \land W \in X) \to \{F (W)\} = F [\{W\}]$
12	8 10 11	syl2anc	$⊢ (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to \{F (W)\} = F [\{W\}]$
13	6 12	eqtr3d	$⊢ (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to \{U\} = F [\{W\}]$
14	13	imaeq2d	$⊢ (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to F^{-1} [\{U\}] = F^{-1} [F [\{W\}]]$
15	14	adantl	$⊢ (F : X \underset{1-1}{⟶} Y \land (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H))) \to F^{-1} [\{U\}] = F^{-1} [F [\{W\}]]$
16	9	snssd	$⊢ G \in GrpOp \to \{W\} \subseteq X$
17	16	3ad2ant1	$⊢ (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to \{W\} \subseteq X$
18		f1imacnv	$⊢ (F : X \underset{1-1}{⟶} Y \land \{W\} \subseteq X) \to F^{-1} [F [\{W\}]] = \{W\}$
19	17 18	sylan2	$⊢ (F : X \underset{1-1}{⟶} Y \land (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H))) \to F^{-1} [F [\{W\}]] = \{W\}$
20	15 19	eqtrd	$⊢ (F : X \underset{1-1}{⟶} Y \land (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H))) \to F^{-1} [\{U\}] = \{W\}$
21	20	expcom	$⊢ (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to (F : X \underset{1-1}{⟶} Y \to F^{-1} [\{U\}] = \{W\})$
22	7	adantr	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land F^{-1} [\{U\}] = \{W\}) \to F : X ⟶ Y$
23		simpl2	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (x \in X \land y \in X)) \to H \in GrpOp$
24	7	ffvelcdmda	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land x \in X) \to F (x) \in Y$
25	24	adantrr	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (x \in X \land y \in X)) \to F (x) \in Y$
26	7	ffvelcdmda	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land y \in X) \to F (y) \in Y$
27	26	adantrl	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (x \in X \land y \in X)) \to F (y) \in Y$
28		eqid	$⊢ /_{g} (H) = /_{g} (H)$
29	3 4 28	grpoeqdivid	$⊢ (H \in GrpOp \land F (x) \in Y \land F (y) \in Y) \to (F (x) = F (y) \leftrightarrow F (x) /_{g} (H) F (y) = U)$
30	23 25 27 29	syl3anc	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (x \in X \land y \in X)) \to (F (x) = F (y) \leftrightarrow F (x) /_{g} (H) F (y) = U)$
31	30	adantlr	$⊢ (((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land F^{-1} [\{U\}] = \{W\}) \land (x \in X \land y \in X)) \to (F (x) = F (y) \leftrightarrow F (x) /_{g} (H) F (y) = U)$
32		eqid	$⊢ /_{g} (G) = /_{g} (G)$
33	1 32 28	ghomdiv	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (x \in X \land y \in X)) \to F (x /_{g} (G) y) = F (x) /_{g} (H) F (y)$
34	33	adantlr	$⊢ (((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land F^{-1} [\{U\}] = \{W\}) \land (x \in X \land y \in X)) \to F (x /_{g} (G) y) = F (x) /_{g} (H) F (y)$
35	34	eqeq1d	$⊢ (((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land F^{-1} [\{U\}] = \{W\}) \land (x \in X \land y \in X)) \to (F (x /_{g} (G) y) = U \leftrightarrow F (x) /_{g} (H) F (y) = U)$
36	4	fvexi	$⊢ U \in V$
37	36	snid	$⊢ U \in \{U\}$
38		eleq1	$⊢ F (x /_{g} (G) y) = U \to (F (x /_{g} (G) y) \in \{U\} \leftrightarrow U \in \{U\})$
39	37 38	mpbiri	$⊢ F (x /_{g} (G) y) = U \to F (x /_{g} (G) y) \in \{U\}$
40	7	ffund	$⊢ (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to Fun F$
41	40	adantr	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (x \in X \land y \in X)) \to Fun F$
42	1 32	grpodivcl	$⊢ (G \in GrpOp \land x \in X \land y \in X) \to x /_{g} (G) y \in X$
43	42	3expb	$⊢ (G \in GrpOp \land (x \in X \land y \in X)) \to x /_{g} (G) y \in X$
44	43	3ad2antl1	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (x \in X \land y \in X)) \to x /_{g} (G) y \in X$
45	7	fdmd	$⊢ (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to dom F = X$
46	45	adantr	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (x \in X \land y \in X)) \to dom F = X$
47	44 46	eleqtrrd	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (x \in X \land y \in X)) \to x /_{g} (G) y \in dom F$
48		fvimacnv	$⊢ (Fun F \land x /_{g} (G) y \in dom F) \to (F (x /_{g} (G) y) \in \{U\} \leftrightarrow x /_{g} (G) y \in F^{-1} [\{U\}])$
49	41 47 48	syl2anc	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (x \in X \land y \in X)) \to (F (x /_{g} (G) y) \in \{U\} \leftrightarrow x /_{g} (G) y \in F^{-1} [\{U\}])$
50		eleq2	$⊢ F^{-1} [\{U\}] = \{W\} \to (x /_{g} (G) y \in F^{-1} [\{U\}] \leftrightarrow x /_{g} (G) y \in \{W\})$
51	49 50	sylan9bb	$⊢ (((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (x \in X \land y \in X)) \land F^{-1} [\{U\}] = \{W\}) \to (F (x /_{g} (G) y) \in \{U\} \leftrightarrow x /_{g} (G) y \in \{W\})$
52	51	an32s	$⊢ (((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land F^{-1} [\{U\}] = \{W\}) \land (x \in X \land y \in X)) \to (F (x /_{g} (G) y) \in \{U\} \leftrightarrow x /_{g} (G) y \in \{W\})$
53		elsni	$⊢ x /_{g} (G) y \in \{W\} \to x /_{g} (G) y = W$
54	1 2 32	grpoeqdivid	$⊢ (G \in GrpOp \land x \in X \land y \in X) \to (x = y \leftrightarrow x /_{g} (G) y = W)$
55	54	biimprd	$⊢ (G \in GrpOp \land x \in X \land y \in X) \to (x /_{g} (G) y = W \to x = y)$
56	55	3expb	$⊢ (G \in GrpOp \land (x \in X \land y \in X)) \to (x /_{g} (G) y = W \to x = y)$
57	56	3ad2antl1	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (x \in X \land y \in X)) \to (x /_{g} (G) y = W \to x = y)$
58	53 57	syl5	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (x \in X \land y \in X)) \to (x /_{g} (G) y \in \{W\} \to x = y)$
59	58	adantlr	$⊢ (((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land F^{-1} [\{U\}] = \{W\}) \land (x \in X \land y \in X)) \to (x /_{g} (G) y \in \{W\} \to x = y)$
60	52 59	sylbid	$⊢ (((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land F^{-1} [\{U\}] = \{W\}) \land (x \in X \land y \in X)) \to (F (x /_{g} (G) y) \in \{U\} \to x = y)$
61	39 60	syl5	$⊢ (((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land F^{-1} [\{U\}] = \{W\}) \land (x \in X \land y \in X)) \to (F (x /_{g} (G) y) = U \to x = y)$
62	35 61	sylbird	$⊢ (((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land F^{-1} [\{U\}] = \{W\}) \land (x \in X \land y \in X)) \to (F (x) /_{g} (H) F (y) = U \to x = y)$
63	31 62	sylbid	$⊢ (((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land F^{-1} [\{U\}] = \{W\}) \land (x \in X \land y \in X)) \to (F (x) = F (y) \to x = y)$
64	63	ralrimivva	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land F^{-1} [\{U\}] = \{W\}) \to \forall x \in X \forall y \in X (F (x) = F (y) \to x = y)$
65		dff13	$⊢ F : X \underset{1-1}{⟶} Y \leftrightarrow (F : X ⟶ Y \land \forall x \in X \forall y \in X (F (x) = F (y) \to x = y))$
66	22 64 65	sylanbrc	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land F^{-1} [\{U\}] = \{W\}) \to F : X \underset{1-1}{⟶} Y$
67	66	ex	$⊢ (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to (F^{-1} [\{U\}] = \{W\} \to F : X \underset{1-1}{⟶} Y)$
68	21 67	impbid	$⊢ (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to (F : X \underset{1-1}{⟶} Y \leftrightarrow F^{-1} [\{U\}] = \{W\})$

Metamath Proof Explorer

Theorem grpokerinj

Proof