qusker

Description: The kernel of a quotient map. (Contributed by Thierry Arnoux, 20-May-2023)

	Ref	Expression
Hypotheses	qusker.b	$⊢ V = {Base}_{M}$
	qusker.f	$⊢ F = (x \in V ⟼ [x] (M ~_{QG} G))$
	qusker.n	$⊢ N = M /_{𝑠} (M ~_{QG} G)$
	qusker.1	$⊢ \underset{˙}{0} = 0_{N}$
Assertion	qusker	$⊢ G \in NrmSGrp (M) \to F^{-1} [\{\underset{˙}{0}\}] = G$

Proof

Step	Hyp	Ref	Expression
1		qusker.b	$⊢ V = {Base}_{M}$
2		qusker.f	$⊢ F = (x \in V ⟼ [x] (M ~_{QG} G))$
3		qusker.n	$⊢ N = M /_{𝑠} (M ~_{QG} G)$
4		qusker.1	$⊢ \underset{˙}{0} = 0_{N}$
5	3	a1i	$⊢ G \in NrmSGrp (M) \to N = M /_{𝑠} (M ~_{QG} G)$
6	1	a1i	$⊢ G \in NrmSGrp (M) \to V = {Base}_{M}$
7		ovex	$⊢ M ~_{QG} G \in V$
8	7	a1i	$⊢ G \in NrmSGrp (M) \to M ~_{QG} G \in V$
9		nsgsubg	$⊢ G \in NrmSGrp (M) \to G \in SubGrp (M)$
10		subgrcl	$⊢ G \in SubGrp (M) \to M \in Grp$
11	9 10	syl	$⊢ G \in NrmSGrp (M) \to M \in Grp$
12	5 6 2 8 11	quslem	$⊢ G \in NrmSGrp (M) \to F : V \underset{onto}{⟶} V / (M ~_{QG} G)$
13		fofn	$⊢ F : V \underset{onto}{⟶} V / (M ~_{QG} G) \to F Fn V$
14		fniniseg2	$⊢ F Fn V \to F^{-1} [\{\underset{˙}{0}\}] = \{y \in V \| F (y) = \underset{˙}{0}\}$
15	12 13 14	3syl	$⊢ G \in NrmSGrp (M) \to F^{-1} [\{\underset{˙}{0}\}] = \{y \in V \| F (y) = \underset{˙}{0}\}$
16		eqid	$⊢ 0_{M} = 0_{M}$
17	3 16	qus0	$⊢ G \in NrmSGrp (M) \to [0_{M}] (M ~_{QG} G) = 0_{N}$
18	4 17	eqtr4id	$⊢ G \in NrmSGrp (M) \to \underset{˙}{0} = [0_{M}] (M ~_{QG} G)$
19		eceq1	$⊢ x = y \to [x] (M ~_{QG} G) = [y] (M ~_{QG} G)$
20		ecexg	$⊢ M ~_{QG} G \in V \to [y] (M ~_{QG} G) \in V$
21	7 20	ax-mp	$⊢ [y] (M ~_{QG} G) \in V$
22	19 2 21	fvmpt	$⊢ y \in V \to F (y) = [y] (M ~_{QG} G)$
23	18 22	eqeqan12d	$⊢ (G \in NrmSGrp (M) \land y \in V) \to (\underset{˙}{0} = F (y) \leftrightarrow [0_{M}] (M ~_{QG} G) = [y] (M ~_{QG} G))$
24		eqcom	$⊢ \underset{˙}{0} = F (y) \leftrightarrow F (y) = \underset{˙}{0}$
25	24	a1i	$⊢ (G \in NrmSGrp (M) \land y \in V) \to (\underset{˙}{0} = F (y) \leftrightarrow F (y) = \underset{˙}{0})$
26		simpl	$⊢ (G \in NrmSGrp (M) \land y \in V) \to G \in NrmSGrp (M)$
27		simpr	$⊢ (G \in NrmSGrp (M) \land y \in V) \to y \in V$
28	1 16	grpidcl	$⊢ M \in Grp \to 0_{M} \in V$
29	26 11 28	3syl	$⊢ (G \in NrmSGrp (M) \land y \in V) \to 0_{M} \in V$
30	1	subgss	$⊢ G \in SubGrp (M) \to G \subseteq V$
31	9 30	syl	$⊢ G \in NrmSGrp (M) \to G \subseteq V$
32		eqid	$⊢ {inv}_{g} (M) = {inv}_{g} (M)$
33		eqid	$⊢ +_{M} = +_{M}$
34		eqid	$⊢ M ~_{QG} G = M ~_{QG} G$
35	1 32 33 34	eqgval	$⊢ (M \in Grp \land G \subseteq V) \to (0_{M} (M ~_{QG} G) y \leftrightarrow (0_{M} \in V \land y \in V \land {inv}_{g} (M) (0_{M}) +_{M} y \in G))$
36	11 31 35	syl2anc	$⊢ G \in NrmSGrp (M) \to (0_{M} (M ~_{QG} G) y \leftrightarrow (0_{M} \in V \land y \in V \land {inv}_{g} (M) (0_{M}) +_{M} y \in G))$
37	36	adantr	$⊢ (G \in NrmSGrp (M) \land y \in V) \to (0_{M} (M ~_{QG} G) y \leftrightarrow (0_{M} \in V \land y \in V \land {inv}_{g} (M) (0_{M}) +_{M} y \in G))$
38		df-3an	$⊢ (0_{M} \in V \land y \in V \land {inv}_{g} (M) (0_{M}) +_{M} y \in G) \leftrightarrow ((0_{M} \in V \land y \in V) \land {inv}_{g} (M) (0_{M}) +_{M} y \in G)$
39	38	biancomi	$⊢ (0_{M} \in V \land y \in V \land {inv}_{g} (M) (0_{M}) +_{M} y \in G) \leftrightarrow ({inv}_{g} (M) (0_{M}) +_{M} y \in G \land (0_{M} \in V \land y \in V))$
40	37 39	bitrdi	$⊢ (G \in NrmSGrp (M) \land y \in V) \to (0_{M} (M ~_{QG} G) y \leftrightarrow ({inv}_{g} (M) (0_{M}) +_{M} y \in G \land (0_{M} \in V \land y \in V)))$
41	40	rbaibd	$⊢ ((G \in NrmSGrp (M) \land y \in V) \land (0_{M} \in V \land y \in V)) \to (0_{M} (M ~_{QG} G) y \leftrightarrow {inv}_{g} (M) (0_{M}) +_{M} y \in G)$
42	26 27 29 27 41	syl22anc	$⊢ (G \in NrmSGrp (M) \land y \in V) \to (0_{M} (M ~_{QG} G) y \leftrightarrow {inv}_{g} (M) (0_{M}) +_{M} y \in G)$
43	1 34	eqger	$⊢ G \in SubGrp (M) \to (M ~_{QG} G) Er V$
44	9 43	syl	$⊢ G \in NrmSGrp (M) \to (M ~_{QG} G) Er V$
45	44	adantr	$⊢ (G \in NrmSGrp (M) \land y \in V) \to (M ~_{QG} G) Er V$
46	45 27	erth2	$⊢ (G \in NrmSGrp (M) \land y \in V) \to (0_{M} (M ~_{QG} G) y \leftrightarrow [0_{M}] (M ~_{QG} G) = [y] (M ~_{QG} G))$
47	16 32	grpinvid	$⊢ M \in Grp \to {inv}_{g} (M) (0_{M}) = 0_{M}$
48	26 11 47	3syl	$⊢ (G \in NrmSGrp (M) \land y \in V) \to {inv}_{g} (M) (0_{M}) = 0_{M}$
49	48	oveq1d	$⊢ (G \in NrmSGrp (M) \land y \in V) \to {inv}_{g} (M) (0_{M}) +_{M} y = 0_{M} +_{M} y$
50	1 33 16	grplid	$⊢ (M \in Grp \land y \in V) \to 0_{M} +_{M} y = y$
51	11 50	sylan	$⊢ (G \in NrmSGrp (M) \land y \in V) \to 0_{M} +_{M} y = y$
52	49 51	eqtrd	$⊢ (G \in NrmSGrp (M) \land y \in V) \to {inv}_{g} (M) (0_{M}) +_{M} y = y$
53	52	eleq1d	$⊢ (G \in NrmSGrp (M) \land y \in V) \to ({inv}_{g} (M) (0_{M}) +_{M} y \in G \leftrightarrow y \in G)$
54	42 46 53	3bitr3d	$⊢ (G \in NrmSGrp (M) \land y \in V) \to ([0_{M}] (M ~_{QG} G) = [y] (M ~_{QG} G) \leftrightarrow y \in G)$
55	23 25 54	3bitr3d	$⊢ (G \in NrmSGrp (M) \land y \in V) \to (F (y) = \underset{˙}{0} \leftrightarrow y \in G)$
56	55	rabbidva	$⊢ G \in NrmSGrp (M) \to \{y \in V \| F (y) = \underset{˙}{0}\} = \{y \in V \| y \in G\}$
57		dfss7	$⊢ G \subseteq V \leftrightarrow \{y \in V \| y \in G\} = G$
58	31 57	sylib	$⊢ G \in NrmSGrp (M) \to \{y \in V \| y \in G\} = G$
59	15 56 58	3eqtrd	$⊢ G \in NrmSGrp (M) \to F^{-1} [\{\underset{˙}{0}\}] = G$

Metamath Proof Explorer

Theorem qusker

Proof