Theorem sylow3lem2

Description: Lemma for sylow3 , first part. The stabilizer of a given Sylow subgroup K in the group action .(+) acting on all of G is the normalizer N_G(K). (Contributed by Mario Carneiro, 19-Jan-2015)

	Ref	Expression
Hypotheses	sylow3.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
	sylow3.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	sylow3.xf	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	sylow3.p	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	sylow3lem1.a	⊢ + = ( +g ‘ 𝐺 )
	sylow3lem1.d	⊢ − = ( -g ‘ 𝐺 )
	sylow3lem1.m	⊢ ⊕ = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) )
	sylow3lem2.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) )
	sylow3lem2.h	⊢ 𝐻 = { 𝑢 ∈ 𝑋 ∣ ( 𝑢 ⊕ 𝐾 ) = 𝐾 }
	sylow3lem2.n	⊢ 𝑁 = { 𝑥 ∈ 𝑋 ∣ ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝐾 ↔ ( 𝑦 + 𝑥 ) ∈ 𝐾 ) }
Assertion	sylow3lem2	⊢ ( 𝜑 → 𝐻 = 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		sylow3.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		sylow3.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
3		sylow3.xf	⊢ ( 𝜑 → 𝑋 ∈ Fin )
4		sylow3.p	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
5		sylow3lem1.a	⊢ + = ( +g ‘ 𝐺 )
6		sylow3lem1.d	⊢ − = ( -g ‘ 𝐺 )
7		sylow3lem1.m	⊢ ⊕ = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) )
8		sylow3lem2.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) )
9		sylow3lem2.h	⊢ 𝐻 = { 𝑢 ∈ 𝑋 ∣ ( 𝑢 ⊕ 𝐾 ) = 𝐾 }
10		sylow3lem2.n	⊢ 𝑁 = { 𝑥 ∈ 𝑋 ∣ ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝐾 ↔ ( 𝑦 + 𝑥 ) ∈ 𝐾 ) }
11	10	ssrab3	⊢ 𝑁 ⊆ 𝑋
12		sseqin2	⊢ ( 𝑁 ⊆ 𝑋 ↔ ( 𝑋 ∩ 𝑁 ) = 𝑁 )
13	11 12	mpbi	⊢ ( 𝑋 ∩ 𝑁 ) = 𝑁
14		simpr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) → 𝑢 ∈ 𝑋 )
15	8	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) → 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) )
16		mptexg	⊢ ( 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) → ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ∈ V )
17		rnexg	⊢ ( ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ∈ V → ran ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ∈ V )
18	15 16 17	3syl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) → ran ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ∈ V )
19		simpr	⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝐾 ) → 𝑦 = 𝐾 )
20		simpl	⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝐾 ) → 𝑥 = 𝑢 )
21	20	oveq1d	⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝐾 ) → ( 𝑥 + 𝑧 ) = ( 𝑢 + 𝑧 ) )
22	21 20	oveq12d	⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝐾 ) → ( ( 𝑥 + 𝑧 ) − 𝑥 ) = ( ( 𝑢 + 𝑧 ) − 𝑢 ) )
23	19 22	mpteq12dv	⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝐾 ) → ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) = ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) )
24	23	rneqd	⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝐾 ) → ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) = ran ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) )
25	24 7	ovmpoga	⊢ ( ( 𝑢 ∈ 𝑋 ∧ 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ∧ ran ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ∈ V ) → ( 𝑢 ⊕ 𝐾 ) = ran ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) )
26	14 15 18 25	syl3anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) → ( 𝑢 ⊕ 𝐾 ) = ran ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) )
27	26	adantr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ 𝑢 ∈ 𝑁 ) → ( 𝑢 ⊕ 𝐾 ) = ran ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) )
28		slwsubg	⊢ ( 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) )
29	8 28	syl	⊢ ( 𝜑 → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) )
30	29	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) )
31		eqid	⊢ ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) = ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) )
32	1 5 6 31 10	conjnmz	⊢ ( ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑢 ∈ 𝑁 ) → 𝐾 = ran ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) )
33	30 32	sylan	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ 𝑢 ∈ 𝑁 ) → 𝐾 = ran ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) )
34	27 33	eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ 𝑢 ∈ 𝑁 ) → ( 𝑢 ⊕ 𝐾 ) = 𝐾 )
35		simplr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( 𝑢 ⊕ 𝐾 ) = 𝐾 ) → 𝑢 ∈ 𝑋 )
36		simprl	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝑢 ⊕ 𝐾 ) = 𝐾 )
37	26	adantr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝑢 ⊕ 𝐾 ) = ran ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) )
38	36 37	eqtr3d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) → 𝐾 = ran ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) )
39	38	eleq2d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( 𝑢 + 𝑤 ) ∈ 𝐾 ↔ ( 𝑢 + 𝑤 ) ∈ ran ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ) )
40		ovex	⊢ ( 𝑢 + 𝑤 ) ∈ V
41		eqeq1	⊢ ( 𝑣 = ( 𝑢 + 𝑤 ) → ( 𝑣 = ( ( 𝑢 + 𝑧 ) − 𝑢 ) ↔ ( 𝑢 + 𝑤 ) = ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) )
42	41	rexbidv	⊢ ( 𝑣 = ( 𝑢 + 𝑤 ) → ( ∃ 𝑧 ∈ 𝐾 𝑣 = ( ( 𝑢 + 𝑧 ) − 𝑢 ) ↔ ∃ 𝑧 ∈ 𝐾 ( 𝑢 + 𝑤 ) = ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) )
43	31	rnmpt	⊢ ran ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) = { 𝑣 ∣ ∃ 𝑧 ∈ 𝐾 𝑣 = ( ( 𝑢 + 𝑧 ) − 𝑢 ) }
44	40 42 43	elab2	⊢ ( ( 𝑢 + 𝑤 ) ∈ ran ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ↔ ∃ 𝑧 ∈ 𝐾 ( 𝑢 + 𝑤 ) = ( ( 𝑢 + 𝑧 ) − 𝑢 ) )
45		simprr	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 ∈ 𝐾 ∧ ( 𝑢 + 𝑤 ) = ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ) → ( 𝑢 + 𝑤 ) = ( ( 𝑢 + 𝑧 ) − 𝑢 ) )
46	2	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 ∈ 𝐾 ∧ ( 𝑢 + 𝑤 ) = ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ) → 𝐺 ∈ Grp )
47		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 ∈ 𝐾 ∧ ( 𝑢 + 𝑤 ) = ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ) → 𝑢 ∈ 𝑋 )
48	1	subgss	⊢ ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) → 𝐾 ⊆ 𝑋 )
49	29 48	syl	⊢ ( 𝜑 → 𝐾 ⊆ 𝑋 )
50	49	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 ∈ 𝐾 ∧ ( 𝑢 + 𝑤 ) = ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ) → 𝐾 ⊆ 𝑋 )
51		simprl	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 ∈ 𝐾 ∧ ( 𝑢 + 𝑤 ) = ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ) → 𝑧 ∈ 𝐾 )
52	50 51	sseldd	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 ∈ 𝐾 ∧ ( 𝑢 + 𝑤 ) = ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ) → 𝑧 ∈ 𝑋 )
53	1 5 6	grpaddsubass	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋 ) ) → ( ( 𝑢 + 𝑧 ) − 𝑢 ) = ( 𝑢 + ( 𝑧 − 𝑢 ) ) )
54	46 47 52 47 53	syl13anc	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 ∈ 𝐾 ∧ ( 𝑢 + 𝑤 ) = ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ) → ( ( 𝑢 + 𝑧 ) − 𝑢 ) = ( 𝑢 + ( 𝑧 − 𝑢 ) ) )
55	45 54	eqtr2d	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 ∈ 𝐾 ∧ ( 𝑢 + 𝑤 ) = ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ) → ( 𝑢 + ( 𝑧 − 𝑢 ) ) = ( 𝑢 + 𝑤 ) )
56	1 6	grpsubcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋 ) → ( 𝑧 − 𝑢 ) ∈ 𝑋 )
57	46 52 47 56	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 ∈ 𝐾 ∧ ( 𝑢 + 𝑤 ) = ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ) → ( 𝑧 − 𝑢 ) ∈ 𝑋 )
58		simplrr	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 ∈ 𝐾 ∧ ( 𝑢 + 𝑤 ) = ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ) → 𝑤 ∈ 𝑋 )
59	1 5	grplcan	⊢ ( ( 𝐺 ∈ Grp ∧ ( ( 𝑧 − 𝑢 ) ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋 ) ) → ( ( 𝑢 + ( 𝑧 − 𝑢 ) ) = ( 𝑢 + 𝑤 ) ↔ ( 𝑧 − 𝑢 ) = 𝑤 ) )
60	46 57 58 47 59	syl13anc	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 ∈ 𝐾 ∧ ( 𝑢 + 𝑤 ) = ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ) → ( ( 𝑢 + ( 𝑧 − 𝑢 ) ) = ( 𝑢 + 𝑤 ) ↔ ( 𝑧 − 𝑢 ) = 𝑤 ) )
61	55 60	mpbid	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 ∈ 𝐾 ∧ ( 𝑢 + 𝑤 ) = ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ) → ( 𝑧 − 𝑢 ) = 𝑤 )
62	1 5 6	grpsubadd	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( 𝑧 − 𝑢 ) = 𝑤 ↔ ( 𝑤 + 𝑢 ) = 𝑧 ) )
63	46 52 47 58 62	syl13anc	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 ∈ 𝐾 ∧ ( 𝑢 + 𝑤 ) = ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ) → ( ( 𝑧 − 𝑢 ) = 𝑤 ↔ ( 𝑤 + 𝑢 ) = 𝑧 ) )
64	61 63	mpbid	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 ∈ 𝐾 ∧ ( 𝑢 + 𝑤 ) = ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ) → ( 𝑤 + 𝑢 ) = 𝑧 )
65	64 51	eqeltrd	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 ∈ 𝐾 ∧ ( 𝑢 + 𝑤 ) = ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ) → ( 𝑤 + 𝑢 ) ∈ 𝐾 )
66	65	rexlimdvaa	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) → ( ∃ 𝑧 ∈ 𝐾 ( 𝑢 + 𝑤 ) = ( ( 𝑢 + 𝑧 ) − 𝑢 ) → ( 𝑤 + 𝑢 ) ∈ 𝐾 ) )
67	44 66	biimtrid	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( 𝑢 + 𝑤 ) ∈ ran ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) → ( 𝑤 + 𝑢 ) ∈ 𝐾 ) )
68		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑤 + 𝑢 ) ∈ 𝐾 ) → ( 𝑤 + 𝑢 ) ∈ 𝐾 )
69		oveq2	⊢ ( 𝑧 = ( 𝑤 + 𝑢 ) → ( 𝑢 + 𝑧 ) = ( 𝑢 + ( 𝑤 + 𝑢 ) ) )
70	69	oveq1d	⊢ ( 𝑧 = ( 𝑤 + 𝑢 ) → ( ( 𝑢 + 𝑧 ) − 𝑢 ) = ( ( 𝑢 + ( 𝑤 + 𝑢 ) ) − 𝑢 ) )
71		ovex	⊢ ( ( 𝑢 + ( 𝑤 + 𝑢 ) ) − 𝑢 ) ∈ V
72	70 31 71	fvmpt	⊢ ( ( 𝑤 + 𝑢 ) ∈ 𝐾 → ( ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ‘ ( 𝑤 + 𝑢 ) ) = ( ( 𝑢 + ( 𝑤 + 𝑢 ) ) − 𝑢 ) )
73	68 72	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑤 + 𝑢 ) ∈ 𝐾 ) → ( ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ‘ ( 𝑤 + 𝑢 ) ) = ( ( 𝑢 + ( 𝑤 + 𝑢 ) ) − 𝑢 ) )
74	2	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑤 + 𝑢 ) ∈ 𝐾 ) → 𝐺 ∈ Grp )
75		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑤 + 𝑢 ) ∈ 𝐾 ) → 𝑢 ∈ 𝑋 )
76		simplrr	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑤 + 𝑢 ) ∈ 𝐾 ) → 𝑤 ∈ 𝑋 )
77	1 5	grpass	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋 ) ) → ( ( 𝑢 + 𝑤 ) + 𝑢 ) = ( 𝑢 + ( 𝑤 + 𝑢 ) ) )
78	74 75 76 75 77	syl13anc	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑤 + 𝑢 ) ∈ 𝐾 ) → ( ( 𝑢 + 𝑤 ) + 𝑢 ) = ( 𝑢 + ( 𝑤 + 𝑢 ) ) )
79	78	oveq1d	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑤 + 𝑢 ) ∈ 𝐾 ) → ( ( ( 𝑢 + 𝑤 ) + 𝑢 ) − 𝑢 ) = ( ( 𝑢 + ( 𝑤 + 𝑢 ) ) − 𝑢 ) )
80	1 5	grpcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑢 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( 𝑢 + 𝑤 ) ∈ 𝑋 )
81	74 75 76 80	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑤 + 𝑢 ) ∈ 𝐾 ) → ( 𝑢 + 𝑤 ) ∈ 𝑋 )
82	1 5 6	grppncan	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑢 + 𝑤 ) ∈ 𝑋 ∧ 𝑢 ∈ 𝑋 ) → ( ( ( 𝑢 + 𝑤 ) + 𝑢 ) − 𝑢 ) = ( 𝑢 + 𝑤 ) )
83	74 81 75 82	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑤 + 𝑢 ) ∈ 𝐾 ) → ( ( ( 𝑢 + 𝑤 ) + 𝑢 ) − 𝑢 ) = ( 𝑢 + 𝑤 ) )
84	73 79 83	3eqtr2d	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑤 + 𝑢 ) ∈ 𝐾 ) → ( ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ‘ ( 𝑤 + 𝑢 ) ) = ( 𝑢 + 𝑤 ) )
85		ovex	⊢ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ∈ V
86	85 31	fnmpti	⊢ ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) Fn 𝐾
87		fnfvelrn	⊢ ( ( ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) Fn 𝐾 ∧ ( 𝑤 + 𝑢 ) ∈ 𝐾 ) → ( ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ‘ ( 𝑤 + 𝑢 ) ) ∈ ran ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) )
88	86 68 87	sylancr	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑤 + 𝑢 ) ∈ 𝐾 ) → ( ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ‘ ( 𝑤 + 𝑢 ) ) ∈ ran ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) )
89	84 88	eqeltrrd	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑤 + 𝑢 ) ∈ 𝐾 ) → ( 𝑢 + 𝑤 ) ∈ ran ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) )
90	89	ex	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( 𝑤 + 𝑢 ) ∈ 𝐾 → ( 𝑢 + 𝑤 ) ∈ ran ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ) )
91	67 90	impbid	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( 𝑢 + 𝑤 ) ∈ ran ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ↔ ( 𝑤 + 𝑢 ) ∈ 𝐾 ) )
92	39 91	bitrd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( ( 𝑢 ⊕ 𝐾 ) = 𝐾 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( 𝑢 + 𝑤 ) ∈ 𝐾 ↔ ( 𝑤 + 𝑢 ) ∈ 𝐾 ) )
93	92	anassrs	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( 𝑢 ⊕ 𝐾 ) = 𝐾 ) ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝑢 + 𝑤 ) ∈ 𝐾 ↔ ( 𝑤 + 𝑢 ) ∈ 𝐾 ) )
94	93	ralrimiva	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( 𝑢 ⊕ 𝐾 ) = 𝐾 ) → ∀ 𝑤 ∈ 𝑋 ( ( 𝑢 + 𝑤 ) ∈ 𝐾 ↔ ( 𝑤 + 𝑢 ) ∈ 𝐾 ) )
95	10	elnmz	⊢ ( 𝑢 ∈ 𝑁 ↔ ( 𝑢 ∈ 𝑋 ∧ ∀ 𝑤 ∈ 𝑋 ( ( 𝑢 + 𝑤 ) ∈ 𝐾 ↔ ( 𝑤 + 𝑢 ) ∈ 𝐾 ) ) )
96	35 94 95	sylanbrc	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) ∧ ( 𝑢 ⊕ 𝐾 ) = 𝐾 ) → 𝑢 ∈ 𝑁 )
97	34 96	impbida	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) → ( 𝑢 ∈ 𝑁 ↔ ( 𝑢 ⊕ 𝐾 ) = 𝐾 ) )
98	97	rabbi2dva	⊢ ( 𝜑 → ( 𝑋 ∩ 𝑁 ) = { 𝑢 ∈ 𝑋 ∣ ( 𝑢 ⊕ 𝐾 ) = 𝐾 } )
99	13 98	eqtr3id	⊢ ( 𝜑 → 𝑁 = { 𝑢 ∈ 𝑋 ∣ ( 𝑢 ⊕ 𝐾 ) = 𝐾 } )
100	9 99	eqtr4id	⊢ ( 𝜑 → 𝐻 = 𝑁 )