This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝐻 = 𝑁 )