Theorem qusker

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

	Ref	Expression
Hypotheses	qusker.b	⊢ 𝑉 = ( Base ‘ 𝑀 )
	qusker.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) )
	qusker.n	⊢ 𝑁 = ( 𝑀 /s ( 𝑀 ~QG 𝐺 ) )
	qusker.1	⊢ 0 = ( 0g ‘ 𝑁 )
Assertion	qusker	⊢ ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) → ( ◡ 𝐹 “ { 0 } ) = 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		qusker.b	⊢ 𝑉 = ( Base ‘ 𝑀 )
2		qusker.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) )
3		qusker.n	⊢ 𝑁 = ( 𝑀 /s ( 𝑀 ~QG 𝐺 ) )
4		qusker.1	⊢ 0 = ( 0g ‘ 𝑁 )
5	3	a1i	⊢ ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) → 𝑁 = ( 𝑀 /s ( 𝑀 ~QG 𝐺 ) ) )
6	1	a1i	⊢ ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) → 𝑉 = ( Base ‘ 𝑀 ) )
7		ovex	⊢ ( 𝑀 ~QG 𝐺 ) ∈ V
8	7	a1i	⊢ ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) → ( 𝑀 ~QG 𝐺 ) ∈ V )
9		nsgsubg	⊢ ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) → 𝐺 ∈ ( SubGrp ‘ 𝑀 ) )
10		subgrcl	⊢ ( 𝐺 ∈ ( SubGrp ‘ 𝑀 ) → 𝑀 ∈ Grp )
11	9 10	syl	⊢ ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) → 𝑀 ∈ Grp )
12	5 6 2 8 11	quslem	⊢ ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) → 𝐹 : 𝑉 –onto→ ( 𝑉 / ( 𝑀 ~QG 𝐺 ) ) )
13		fofn	⊢ ( 𝐹 : 𝑉 –onto→ ( 𝑉 / ( 𝑀 ~QG 𝐺 ) ) → 𝐹 Fn 𝑉 )
14		fniniseg2	⊢ ( 𝐹 Fn 𝑉 → ( ◡ 𝐹 “ { 0 } ) = { 𝑦 ∈ 𝑉 ∣ ( 𝐹 ‘ 𝑦 ) = 0 } )
15	12 13 14	3syl	⊢ ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) → ( ◡ 𝐹 “ { 0 } ) = { 𝑦 ∈ 𝑉 ∣ ( 𝐹 ‘ 𝑦 ) = 0 } )
16		eqid	⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
17	3 16	qus0	⊢ ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) → [ ( 0g ‘ 𝑀 ) ] ( 𝑀 ~QG 𝐺 ) = ( 0g ‘ 𝑁 ) )
18	4 17	eqtr4id	⊢ ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) → 0 = [ ( 0g ‘ 𝑀 ) ] ( 𝑀 ~QG 𝐺 ) )
19		eceq1	⊢ ( 𝑥 = 𝑦 → [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) = [ 𝑦 ] ( 𝑀 ~QG 𝐺 ) )
20		ecexg	⊢ ( ( 𝑀 ~QG 𝐺 ) ∈ V → [ 𝑦 ] ( 𝑀 ~QG 𝐺 ) ∈ V )
21	7 20	ax-mp	⊢ [ 𝑦 ] ( 𝑀 ~QG 𝐺 ) ∈ V
22	19 2 21	fvmpt	⊢ ( 𝑦 ∈ 𝑉 → ( 𝐹 ‘ 𝑦 ) = [ 𝑦 ] ( 𝑀 ~QG 𝐺 ) )
23	18 22	eqeqan12d	⊢ ( ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) ∧ 𝑦 ∈ 𝑉 ) → ( 0 = ( 𝐹 ‘ 𝑦 ) ↔ [ ( 0g ‘ 𝑀 ) ] ( 𝑀 ~QG 𝐺 ) = [ 𝑦 ] ( 𝑀 ~QG 𝐺 ) ) )
24		eqcom	⊢ ( 0 = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑦 ) = 0 )
25	24	a1i	⊢ ( ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) ∧ 𝑦 ∈ 𝑉 ) → ( 0 = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑦 ) = 0 ) )
26		simpl	⊢ ( ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) ∧ 𝑦 ∈ 𝑉 ) → 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) )
27		simpr	⊢ ( ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) ∧ 𝑦 ∈ 𝑉 ) → 𝑦 ∈ 𝑉 )
28	1 16	grpidcl	⊢ ( 𝑀 ∈ Grp → ( 0g ‘ 𝑀 ) ∈ 𝑉 )
29	26 11 28	3syl	⊢ ( ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) ∧ 𝑦 ∈ 𝑉 ) → ( 0g ‘ 𝑀 ) ∈ 𝑉 )
30	1	subgss	⊢ ( 𝐺 ∈ ( SubGrp ‘ 𝑀 ) → 𝐺 ⊆ 𝑉 )
31	9 30	syl	⊢ ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) → 𝐺 ⊆ 𝑉 )
32		eqid	⊢ ( invg ‘ 𝑀 ) = ( invg ‘ 𝑀 )
33		eqid	⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
34		eqid	⊢ ( 𝑀 ~QG 𝐺 ) = ( 𝑀 ~QG 𝐺 )
35	1 32 33 34	eqgval	⊢ ( ( 𝑀 ∈ Grp ∧ 𝐺 ⊆ 𝑉 ) → ( ( 0g ‘ 𝑀 ) ( 𝑀 ~QG 𝐺 ) 𝑦 ↔ ( ( 0g ‘ 𝑀 ) ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ ( ( ( invg ‘ 𝑀 ) ‘ ( 0g ‘ 𝑀 ) ) ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐺 ) ) )
36	11 31 35	syl2anc	⊢ ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) → ( ( 0g ‘ 𝑀 ) ( 𝑀 ~QG 𝐺 ) 𝑦 ↔ ( ( 0g ‘ 𝑀 ) ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ ( ( ( invg ‘ 𝑀 ) ‘ ( 0g ‘ 𝑀 ) ) ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐺 ) ) )
37	36	adantr	⊢ ( ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) ∧ 𝑦 ∈ 𝑉 ) → ( ( 0g ‘ 𝑀 ) ( 𝑀 ~QG 𝐺 ) 𝑦 ↔ ( ( 0g ‘ 𝑀 ) ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ ( ( ( invg ‘ 𝑀 ) ‘ ( 0g ‘ 𝑀 ) ) ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐺 ) ) )
38		df-3an	⊢ ( ( ( 0g ‘ 𝑀 ) ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ ( ( ( invg ‘ 𝑀 ) ‘ ( 0g ‘ 𝑀 ) ) ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐺 ) ↔ ( ( ( 0g ‘ 𝑀 ) ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( ( invg ‘ 𝑀 ) ‘ ( 0g ‘ 𝑀 ) ) ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐺 ) )
39	38	biancomi	⊢ ( ( ( 0g ‘ 𝑀 ) ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ ( ( ( invg ‘ 𝑀 ) ‘ ( 0g ‘ 𝑀 ) ) ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐺 ) ↔ ( ( ( ( invg ‘ 𝑀 ) ‘ ( 0g ‘ 𝑀 ) ) ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐺 ∧ ( ( 0g ‘ 𝑀 ) ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) )
40	37 39	bitrdi	⊢ ( ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) ∧ 𝑦 ∈ 𝑉 ) → ( ( 0g ‘ 𝑀 ) ( 𝑀 ~QG 𝐺 ) 𝑦 ↔ ( ( ( ( invg ‘ 𝑀 ) ‘ ( 0g ‘ 𝑀 ) ) ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐺 ∧ ( ( 0g ‘ 𝑀 ) ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ) )
41	40	rbaibd	⊢ ( ( ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 0g ‘ 𝑀 ) ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( 0g ‘ 𝑀 ) ( 𝑀 ~QG 𝐺 ) 𝑦 ↔ ( ( ( invg ‘ 𝑀 ) ‘ ( 0g ‘ 𝑀 ) ) ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐺 ) )
42	26 27 29 27 41	syl22anc	⊢ ( ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) ∧ 𝑦 ∈ 𝑉 ) → ( ( 0g ‘ 𝑀 ) ( 𝑀 ~QG 𝐺 ) 𝑦 ↔ ( ( ( invg ‘ 𝑀 ) ‘ ( 0g ‘ 𝑀 ) ) ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐺 ) )
43	1 34	eqger	⊢ ( 𝐺 ∈ ( SubGrp ‘ 𝑀 ) → ( 𝑀 ~QG 𝐺 ) Er 𝑉 )
44	9 43	syl	⊢ ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) → ( 𝑀 ~QG 𝐺 ) Er 𝑉 )
45	44	adantr	⊢ ( ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) ∧ 𝑦 ∈ 𝑉 ) → ( 𝑀 ~QG 𝐺 ) Er 𝑉 )
46	45 27	erth2	⊢ ( ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) ∧ 𝑦 ∈ 𝑉 ) → ( ( 0g ‘ 𝑀 ) ( 𝑀 ~QG 𝐺 ) 𝑦 ↔ [ ( 0g ‘ 𝑀 ) ] ( 𝑀 ~QG 𝐺 ) = [ 𝑦 ] ( 𝑀 ~QG 𝐺 ) ) )
47	16 32	grpinvid	⊢ ( 𝑀 ∈ Grp → ( ( invg ‘ 𝑀 ) ‘ ( 0g ‘ 𝑀 ) ) = ( 0g ‘ 𝑀 ) )
48	26 11 47	3syl	⊢ ( ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) ∧ 𝑦 ∈ 𝑉 ) → ( ( invg ‘ 𝑀 ) ‘ ( 0g ‘ 𝑀 ) ) = ( 0g ‘ 𝑀 ) )
49	48	oveq1d	⊢ ( ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) ∧ 𝑦 ∈ 𝑉 ) → ( ( ( invg ‘ 𝑀 ) ‘ ( 0g ‘ 𝑀 ) ) ( +g ‘ 𝑀 ) 𝑦 ) = ( ( 0g ‘ 𝑀 ) ( +g ‘ 𝑀 ) 𝑦 ) )
50	1 33 16	grplid	⊢ ( ( 𝑀 ∈ Grp ∧ 𝑦 ∈ 𝑉 ) → ( ( 0g ‘ 𝑀 ) ( +g ‘ 𝑀 ) 𝑦 ) = 𝑦 )
51	11 50	sylan	⊢ ( ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) ∧ 𝑦 ∈ 𝑉 ) → ( ( 0g ‘ 𝑀 ) ( +g ‘ 𝑀 ) 𝑦 ) = 𝑦 )
52	49 51	eqtrd	⊢ ( ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) ∧ 𝑦 ∈ 𝑉 ) → ( ( ( invg ‘ 𝑀 ) ‘ ( 0g ‘ 𝑀 ) ) ( +g ‘ 𝑀 ) 𝑦 ) = 𝑦 )
53	52	eleq1d	⊢ ( ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) ∧ 𝑦 ∈ 𝑉 ) → ( ( ( ( invg ‘ 𝑀 ) ‘ ( 0g ‘ 𝑀 ) ) ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐺 ↔ 𝑦 ∈ 𝐺 ) )
54	42 46 53	3bitr3d	⊢ ( ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) ∧ 𝑦 ∈ 𝑉 ) → ( [ ( 0g ‘ 𝑀 ) ] ( 𝑀 ~QG 𝐺 ) = [ 𝑦 ] ( 𝑀 ~QG 𝐺 ) ↔ 𝑦 ∈ 𝐺 ) )
55	23 25 54	3bitr3d	⊢ ( ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) ∧ 𝑦 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑦 ) = 0 ↔ 𝑦 ∈ 𝐺 ) )
56	55	rabbidva	⊢ ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) → { 𝑦 ∈ 𝑉 ∣ ( 𝐹 ‘ 𝑦 ) = 0 } = { 𝑦 ∈ 𝑉 ∣ 𝑦 ∈ 𝐺 } )
57		dfss7	⊢ ( 𝐺 ⊆ 𝑉 ↔ { 𝑦 ∈ 𝑉 ∣ 𝑦 ∈ 𝐺 } = 𝐺 )
58	31 57	sylib	⊢ ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) → { 𝑦 ∈ 𝑉 ∣ 𝑦 ∈ 𝐺 } = 𝐺 )
59	15 56 58	3eqtrd	⊢ ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) → ( ◡ 𝐹 “ { 0 } ) = 𝐺 )