kerf1ghm

Description: A group homomorphism F is injective if and only if its kernel is the singleton { N } . (Contributed by Thierry Arnoux, 27-Oct-2017) (Proof shortened 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	kerf1ghm	$⊢ F \in (R GrpHom S) \to (F : A \underset{1-1}{⟶} B \leftrightarrow F^{-1} [\{\underset{˙}{0}\}] = \{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		simpl	$⊢ ((F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B) \land x \in F^{-1} [\{\underset{˙}{0}\}]) \to (F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B)$
6		f1fn	$⊢ F : A \underset{1-1}{⟶} B \to F Fn A$
7	6	adantl	$⊢ (F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B) \to F Fn A$
8		elpreima	$⊢ F Fn A \to (x \in F^{-1} [\{\underset{˙}{0}\}] \leftrightarrow (x \in A \land F (x) \in \{\underset{˙}{0}\}))$
9	7 8	syl	$⊢ (F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B) \to (x \in F^{-1} [\{\underset{˙}{0}\}] \leftrightarrow (x \in A \land F (x) \in \{\underset{˙}{0}\}))$
10	9	biimpa	$⊢ ((F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B) \land x \in F^{-1} [\{\underset{˙}{0}\}]) \to (x \in A \land F (x) \in \{\underset{˙}{0}\})$
11	10	simpld	$⊢ ((F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B) \land x \in F^{-1} [\{\underset{˙}{0}\}]) \to x \in A$
12	10	simprd	$⊢ ((F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B) \land x \in F^{-1} [\{\underset{˙}{0}\}]) \to F (x) \in \{\underset{˙}{0}\}$
13		fvex	$⊢ F (x) \in V$
14	13	elsn	$⊢ F (x) \in \{\underset{˙}{0}\} \leftrightarrow F (x) = \underset{˙}{0}$
15	12 14	sylib	$⊢ ((F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B) \land x \in F^{-1} [\{\underset{˙}{0}\}]) \to F (x) = \underset{˙}{0}$
16	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)$
17	16	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)$
18	17	3expa	$⊢ ((F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B) \land x \in A) \to (F (x) = \underset{˙}{0} \to x = N)$
19	18	imp	$⊢ (((F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B) \land x \in A) \land F (x) = \underset{˙}{0}) \to x = N$
20	5 11 15 19	syl21anc	$⊢ ((F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B) \land x \in F^{-1} [\{\underset{˙}{0}\}]) \to x = N$
21	20	ex	$⊢ (F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B) \to (x \in F^{-1} [\{\underset{˙}{0}\}] \to x = N)$
22		velsn	$⊢ x \in \{N\} \leftrightarrow x = N$
23	21 22	imbitrrdi	$⊢ (F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B) \to (x \in F^{-1} [\{\underset{˙}{0}\}] \to x \in \{N\})$
24	23	ssrdv	$⊢ (F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B) \to F^{-1} [\{\underset{˙}{0}\}] \subseteq \{N\}$
25		ghmgrp1	$⊢ F \in (R GrpHom S) \to R \in Grp$
26	1 3	grpidcl	$⊢ R \in Grp \to N \in A$
27	25 26	syl	$⊢ F \in (R GrpHom S) \to N \in A$
28	3 4	ghmid	$⊢ F \in (R GrpHom S) \to F (N) = \underset{˙}{0}$
29		fvex	$⊢ F (N) \in V$
30	29	elsn	$⊢ F (N) \in \{\underset{˙}{0}\} \leftrightarrow F (N) = \underset{˙}{0}$
31	28 30	sylibr	$⊢ F \in (R GrpHom S) \to F (N) \in \{\underset{˙}{0}\}$
32	1 2	ghmf	$⊢ F \in (R GrpHom S) \to F : A ⟶ B$
33		ffn	$⊢ F : A ⟶ B \to F Fn A$
34		elpreima	$⊢ F Fn A \to (N \in F^{-1} [\{\underset{˙}{0}\}] \leftrightarrow (N \in A \land F (N) \in \{\underset{˙}{0}\}))$
35	32 33 34	3syl	$⊢ F \in (R GrpHom S) \to (N \in F^{-1} [\{\underset{˙}{0}\}] \leftrightarrow (N \in A \land F (N) \in \{\underset{˙}{0}\}))$
36	27 31 35	mpbir2and	$⊢ F \in (R GrpHom S) \to N \in F^{-1} [\{\underset{˙}{0}\}]$
37	36	snssd	$⊢ F \in (R GrpHom S) \to \{N\} \subseteq F^{-1} [\{\underset{˙}{0}\}]$
38	37	adantr	$⊢ (F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B) \to \{N\} \subseteq F^{-1} [\{\underset{˙}{0}\}]$
39	24 38	eqssd	$⊢ (F \in (R GrpHom S) \land F : A \underset{1-1}{⟶} B) \to F^{-1} [\{\underset{˙}{0}\}] = \{N\}$
40	32	adantr	$⊢ (F \in (R GrpHom S) \land F^{-1} [\{\underset{˙}{0}\}] = \{N\}) \to F : A ⟶ B$
41		simpl	$⊢ (F \in (R GrpHom S) \land (F^{-1} [\{\underset{˙}{0}\}] = \{N\} \land (x \in A \land y \in A) \land F (x) = F (y))) \to F \in (R GrpHom S)$
42		simpr2l	$⊢ (F \in (R GrpHom S) \land (F^{-1} [\{\underset{˙}{0}\}] = \{N\} \land (x \in A \land y \in A) \land F (x) = F (y))) \to x \in A$
43		simpr2r	$⊢ (F \in (R GrpHom S) \land (F^{-1} [\{\underset{˙}{0}\}] = \{N\} \land (x \in A \land y \in A) \land F (x) = F (y))) \to y \in A$
44		simpr3	$⊢ (F \in (R GrpHom S) \land (F^{-1} [\{\underset{˙}{0}\}] = \{N\} \land (x \in A \land y \in A) \land F (x) = F (y))) \to F (x) = F (y)$
45		eqid	$⊢ F^{-1} [\{\underset{˙}{0}\}] = F^{-1} [\{\underset{˙}{0}\}]$
46		eqid	$⊢ -_{R} = -_{R}$
47	1 4 45 46	ghmeqker	$⊢ (F \in (R GrpHom S) \land x \in A \land y \in A) \to (F (x) = F (y) \leftrightarrow x -_{R} y \in F^{-1} [\{\underset{˙}{0}\}])$
48	47	biimpa	$⊢ ((F \in (R GrpHom S) \land x \in A \land y \in A) \land F (x) = F (y)) \to x -_{R} y \in F^{-1} [\{\underset{˙}{0}\}]$
49	41 42 43 44 48	syl31anc	$⊢ (F \in (R GrpHom S) \land (F^{-1} [\{\underset{˙}{0}\}] = \{N\} \land (x \in A \land y \in A) \land F (x) = F (y))) \to x -_{R} y \in F^{-1} [\{\underset{˙}{0}\}]$
50		simpr1	$⊢ (F \in (R GrpHom S) \land (F^{-1} [\{\underset{˙}{0}\}] = \{N\} \land (x \in A \land y \in A) \land F (x) = F (y))) \to F^{-1} [\{\underset{˙}{0}\}] = \{N\}$
51	49 50	eleqtrd	$⊢ (F \in (R GrpHom S) \land (F^{-1} [\{\underset{˙}{0}\}] = \{N\} \land (x \in A \land y \in A) \land F (x) = F (y))) \to x -_{R} y \in \{N\}$
52		ovex	$⊢ x -_{R} y \in V$
53	52	elsn	$⊢ x -_{R} y \in \{N\} \leftrightarrow x -_{R} y = N$
54	51 53	sylib	$⊢ (F \in (R GrpHom S) \land (F^{-1} [\{\underset{˙}{0}\}] = \{N\} \land (x \in A \land y \in A) \land F (x) = F (y))) \to x -_{R} y = N$
55	25	adantr	$⊢ (F \in (R GrpHom S) \land (F^{-1} [\{\underset{˙}{0}\}] = \{N\} \land (x \in A \land y \in A) \land F (x) = F (y))) \to R \in Grp$
56	1 3 46	grpsubeq0	$⊢ (R \in Grp \land x \in A \land y \in A) \to (x -_{R} y = N \leftrightarrow x = y)$
57	55 42 43 56	syl3anc	$⊢ (F \in (R GrpHom S) \land (F^{-1} [\{\underset{˙}{0}\}] = \{N\} \land (x \in A \land y \in A) \land F (x) = F (y))) \to (x -_{R} y = N \leftrightarrow x = y)$
58	54 57	mpbid	$⊢ (F \in (R GrpHom S) \land (F^{-1} [\{\underset{˙}{0}\}] = \{N\} \land (x \in A \land y \in A) \land F (x) = F (y))) \to x = y$
59	58	3anassrs	$⊢ (((F \in (R GrpHom S) \land F^{-1} [\{\underset{˙}{0}\}] = \{N\}) \land (x \in A \land y \in A)) \land F (x) = F (y)) \to x = y$
60	59	ex	$⊢ ((F \in (R GrpHom S) \land F^{-1} [\{\underset{˙}{0}\}] = \{N\}) \land (x \in A \land y \in A)) \to (F (x) = F (y) \to x = y)$
61	60	ralrimivva	$⊢ (F \in (R GrpHom S) \land F^{-1} [\{\underset{˙}{0}\}] = \{N\}) \to \forall x \in A \forall y \in A (F (x) = F (y) \to x = y)$
62		dff13	$⊢ F : A \underset{1-1}{⟶} B \leftrightarrow (F : A ⟶ B \land \forall x \in A \forall y \in A (F (x) = F (y) \to x = y))$
63	40 61 62	sylanbrc	$⊢ (F \in (R GrpHom S) \land F^{-1} [\{\underset{˙}{0}\}] = \{N\}) \to F : A \underset{1-1}{⟶} B$
64	39 63	impbida	$⊢ F \in (R GrpHom S) \to (F : A \underset{1-1}{⟶} B \leftrightarrow F^{-1} [\{\underset{˙}{0}\}] = \{N\})$

Metamath Proof Explorer

Theorem kerf1ghm

Proof