Theorem sylow3lem2 17866

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

Hypotheses

Ref	Expression
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

Ref	Expression
sylow3lem2	⊢ (𝜑 → 𝐻 = 𝑁)

Distinct variable groups:   𝑥,𝑢,𝑦,𝑧, −   𝑢, ⊕ ,𝑥,𝑦,𝑧   𝑥,𝐻,𝑦   𝑢,𝐾,𝑥,𝑦,𝑧   𝑢,𝑁,𝑧   𝑢,𝑋,𝑥,𝑦,𝑧   𝑢,𝐺,𝑥,𝑦,𝑧   𝜑,𝑢,𝑥,𝑦,𝑧   𝑢, + ,𝑥,𝑦,𝑧   𝑢,𝑃,𝑥,𝑦,𝑧

Allowed substitution hints:   𝐻(𝑧,𝑢)   𝑁(𝑥,𝑦)

Proof of Theorem sylow3lem2

Dummy variables 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sylow3lem2.n	. . . . 5 ⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝐾 ↔ (𝑦 + 𝑥) ∈ 𝐾)}
2		ssrab2 3650	. . . . 5 ⊢ {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝐾 ↔ (𝑦 + 𝑥) ∈ 𝐾)} ⊆ 𝑋
3	1, 2	eqsstri 3598	. . . 4 ⊢ 𝑁 ⊆ 𝑋
4		sseqin2 3779	. . . 4 ⊢ (𝑁 ⊆ 𝑋 ↔ (𝑋 ∩ 𝑁) = 𝑁)
5	3, 4	mpbi 219	. . 3 ⊢ (𝑋 ∩ 𝑁) = 𝑁
6		simpr 476	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → 𝑢 ∈ 𝑋)
7		sylow3lem2.k	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ (𝑃 pSyl 𝐺))
8	7	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → 𝐾 ∈ (𝑃 pSyl 𝐺))
9		mptexg 6389	. . . . . . . . 9 ⊢ (𝐾 ∈ (𝑃 pSyl 𝐺) → (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V)
10		rnexg 6990	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V → ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V)
11	8, 9, 10	3syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V)
12		simpr 476	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → 𝑦 = 𝐾)
13		simpl 472	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → 𝑥 = 𝑢)
14	13	oveq1d 6564	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → (𝑥 + 𝑧) = (𝑢 + 𝑧))
15	14, 13	oveq12d 6567	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → ((𝑥 + 𝑧) − 𝑥) = ((𝑢 + 𝑧) − 𝑢))
16	12, 15	mpteq12dv 4663	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
17	16	rneqd 5274	. . . . . . . . 9 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
18		sylow3lem1.m	. . . . . . . . 9 ⊢ ⊕ = (𝑥 ∈ 𝑋, 𝑦 ∈ (𝑃 pSyl 𝐺) ↦ ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)))
19	17, 18	ovmpt2ga 6688	. . . . . . . 8 ⊢ ((𝑢 ∈ 𝑋 ∧ 𝐾 ∈ (𝑃 pSyl 𝐺) ∧ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V) → (𝑢 ⊕ 𝐾) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
20	6, 8, 11, 19	syl3anc 1318	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → (𝑢 ⊕ 𝐾) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
21	20	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ 𝑢 ∈ 𝑁) → (𝑢 ⊕ 𝐾) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
22		slwsubg 17848	. . . . . . . . 9 ⊢ (𝐾 ∈ (𝑃 pSyl 𝐺) → 𝐾 ∈ (SubGrp‘𝐺))
23	7, 22	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺))
24	23	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → 𝐾 ∈ (SubGrp‘𝐺))
25		sylow3.x	. . . . . . . 8 ⊢ 𝑋 = (Base‘𝐺)
26		sylow3lem1.a	. . . . . . . 8 ⊢ + = (+g‘𝐺)
27		sylow3lem1.d	. . . . . . . 8 ⊢ − = (-g‘𝐺)
28		eqid 2610	. . . . . . . 8 ⊢ (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) = (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))
29	25, 26, 27, 28, 1	conjnmz 17517	. . . . . . 7 ⊢ ((𝐾 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑁) → 𝐾 = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
30	24, 29	sylan 487	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ 𝑢 ∈ 𝑁) → 𝐾 = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
31	21, 30	eqtr4d 2647	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ 𝑢 ∈ 𝑁) → (𝑢 ⊕ 𝐾) = 𝐾)
32		simplr 788	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ (𝑢 ⊕ 𝐾) = 𝐾) → 𝑢 ∈ 𝑋)
33		simprl 790	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → (𝑢 ⊕ 𝐾) = 𝐾)
34	20	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → (𝑢 ⊕ 𝐾) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
35	33, 34	eqtr3d 2646	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → 𝐾 = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
36	35	eleq2d 2673	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → ((𝑢 + 𝑤) ∈ 𝐾 ↔ (𝑢 + 𝑤) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))))
37		ovex 6577	. . . . . . . . . . . 12 ⊢ (𝑢 + 𝑤) ∈ V
38		eqeq1 2614	. . . . . . . . . . . . 13 ⊢ (𝑣 = (𝑢 + 𝑤) → (𝑣 = ((𝑢 + 𝑧) − 𝑢) ↔ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢)))
39	38	rexbidv 3034	. . . . . . . . . . . 12 ⊢ (𝑣 = (𝑢 + 𝑤) → (∃𝑧 ∈ 𝐾 𝑣 = ((𝑢 + 𝑧) − 𝑢) ↔ ∃𝑧 ∈ 𝐾 (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢)))
40	28	rnmpt 5292	. . . . . . . . . . . 12 ⊢ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) = {𝑣 ∣ ∃𝑧 ∈ 𝐾 𝑣 = ((𝑢 + 𝑧) − 𝑢)}
41	37, 39, 40	elab2 3323	. . . . . . . . . . 11 ⊢ ((𝑢 + 𝑤) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ↔ ∃𝑧 ∈ 𝐾 (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))
42		simprr 792	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))
43		sylow3.g	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐺 ∈ Grp)
44	43	ad3antrrr 762	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → 𝐺 ∈ Grp)
45		simpllr 795	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → 𝑢 ∈ 𝑋)
46	25	subgss 17418	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 ∈ (SubGrp‘𝐺) → 𝐾 ⊆ 𝑋)
47	23, 46	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 ⊆ 𝑋)
48	47	ad3antrrr 762	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → 𝐾 ⊆ 𝑋)
49		simprl 790	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → 𝑧 ∈ 𝐾)
50	48, 49	sseldd 3569	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → 𝑧 ∈ 𝑋)
51	25, 26, 27	grpaddsubass 17328	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ Grp ∧ (𝑢 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋)) → ((𝑢 + 𝑧) − 𝑢) = (𝑢 + (𝑧 − 𝑢)))
52	44, 45, 50, 45, 51	syl13anc 1320	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → ((𝑢 + 𝑧) − 𝑢) = (𝑢 + (𝑧 − 𝑢)))
53	42, 52	eqtr2d 2645	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → (𝑢 + (𝑧 − 𝑢)) = (𝑢 + 𝑤))
54	25, 27	grpsubcl 17318	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋) → (𝑧 − 𝑢) ∈ 𝑋)
55	44, 50, 45, 54	syl3anc 1318	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → (𝑧 − 𝑢) ∈ 𝑋)
56		simplrr 797	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → 𝑤 ∈ 𝑋)
57	25, 26	grplcan 17300	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ Grp ∧ ((𝑧 − 𝑢) ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋)) → ((𝑢 + (𝑧 − 𝑢)) = (𝑢 + 𝑤) ↔ (𝑧 − 𝑢) = 𝑤))
58	44, 55, 56, 45, 57	syl13anc 1320	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → ((𝑢 + (𝑧 − 𝑢)) = (𝑢 + 𝑤) ↔ (𝑧 − 𝑢) = 𝑤))
59	53, 58	mpbid 221	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → (𝑧 − 𝑢) = 𝑤)
60	25, 26, 27	grpsubadd 17326	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Grp ∧ (𝑧 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → ((𝑧 − 𝑢) = 𝑤 ↔ (𝑤 + 𝑢) = 𝑧))
61	44, 50, 45, 56, 60	syl13anc 1320	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → ((𝑧 − 𝑢) = 𝑤 ↔ (𝑤 + 𝑢) = 𝑧))
62	59, 61	mpbid 221	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → (𝑤 + 𝑢) = 𝑧)
63	62, 49	eqeltrd 2688	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → (𝑤 + 𝑢) ∈ 𝐾)
64	63	rexlimdvaa 3014	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → (∃𝑧 ∈ 𝐾 (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢) → (𝑤 + 𝑢) ∈ 𝐾))
65	41, 64	syl5bi 231	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → ((𝑢 + 𝑤) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) → (𝑤 + 𝑢) ∈ 𝐾))
66		simpr 476	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → (𝑤 + 𝑢) ∈ 𝐾)
67		oveq2 6557	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑤 + 𝑢) → (𝑢 + 𝑧) = (𝑢 + (𝑤 + 𝑢)))
68	67	oveq1d 6564	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑤 + 𝑢) → ((𝑢 + 𝑧) − 𝑢) = ((𝑢 + (𝑤 + 𝑢)) − 𝑢))
69		ovex 6577	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 + (𝑤 + 𝑢)) − 𝑢) ∈ V
70	68, 28, 69	fvmpt 6191	. . . . . . . . . . . . . 14 ⊢ ((𝑤 + 𝑢) ∈ 𝐾 → ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))‘(𝑤 + 𝑢)) = ((𝑢 + (𝑤 + 𝑢)) − 𝑢))
71	66, 70	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))‘(𝑤 + 𝑢)) = ((𝑢 + (𝑤 + 𝑢)) − 𝑢))
72	43	ad3antrrr 762	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → 𝐺 ∈ Grp)
73		simpllr 795	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → 𝑢 ∈ 𝑋)
74		simplrr 797	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → 𝑤 ∈ 𝑋)
75	25, 26	grpass 17254	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Grp ∧ (𝑢 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋)) → ((𝑢 + 𝑤) + 𝑢) = (𝑢 + (𝑤 + 𝑢)))
76	72, 73, 74, 73, 75	syl13anc 1320	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → ((𝑢 + 𝑤) + 𝑢) = (𝑢 + (𝑤 + 𝑢)))
77	76	oveq1d 6564	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → (((𝑢 + 𝑤) + 𝑢) − 𝑢) = ((𝑢 + (𝑤 + 𝑢)) − 𝑢))
78	25, 26	grpcl 17253	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑢 + 𝑤) ∈ 𝑋)
79	72, 73, 74, 78	syl3anc 1318	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → (𝑢 + 𝑤) ∈ 𝑋)
80	25, 26, 27	grppncan 17329	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ (𝑢 + 𝑤) ∈ 𝑋 ∧ 𝑢 ∈ 𝑋) → (((𝑢 + 𝑤) + 𝑢) − 𝑢) = (𝑢 + 𝑤))
81	72, 79, 73, 80	syl3anc 1318	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → (((𝑢 + 𝑤) + 𝑢) − 𝑢) = (𝑢 + 𝑤))
82	71, 77, 81	3eqtr2d 2650	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))‘(𝑤 + 𝑢)) = (𝑢 + 𝑤))
83		ovex 6577	. . . . . . . . . . . . . 14 ⊢ ((𝑢 + 𝑧) − 𝑢) ∈ V
84	83, 28	fnmpti 5935	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) Fn 𝐾
85		fnfvelrn 6264	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) Fn 𝐾 ∧ (𝑤 + 𝑢) ∈ 𝐾) → ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))‘(𝑤 + 𝑢)) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
86	84, 66, 85	sylancr 694	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))‘(𝑤 + 𝑢)) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
87	82, 86	eqeltrrd 2689	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → (𝑢 + 𝑤) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
88	87	ex 449	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → ((𝑤 + 𝑢) ∈ 𝐾 → (𝑢 + 𝑤) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))))
89	65, 88	impbid 201	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → ((𝑢 + 𝑤) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ↔ (𝑤 + 𝑢) ∈ 𝐾))
90	36, 89	bitrd 267	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → ((𝑢 + 𝑤) ∈ 𝐾 ↔ (𝑤 + 𝑢) ∈ 𝐾))
91	90	anassrs 678	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ (𝑢 ⊕ 𝐾) = 𝐾) ∧ 𝑤 ∈ 𝑋) → ((𝑢 + 𝑤) ∈ 𝐾 ↔ (𝑤 + 𝑢) ∈ 𝐾))
92	91	ralrimiva 2949	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ (𝑢 ⊕ 𝐾) = 𝐾) → ∀𝑤 ∈ 𝑋 ((𝑢 + 𝑤) ∈ 𝐾 ↔ (𝑤 + 𝑢) ∈ 𝐾))
93	1	elnmz 17456	. . . . . 6 ⊢ (𝑢 ∈ 𝑁 ↔ (𝑢 ∈ 𝑋 ∧ ∀𝑤 ∈ 𝑋 ((𝑢 + 𝑤) ∈ 𝐾 ↔ (𝑤 + 𝑢) ∈ 𝐾)))
94	32, 92, 93	sylanbrc 695	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ (𝑢 ⊕ 𝐾) = 𝐾) → 𝑢 ∈ 𝑁)
95	31, 94	impbida 873	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → (𝑢 ∈ 𝑁 ↔ (𝑢 ⊕ 𝐾) = 𝐾))
96	95	rabbi2dva 3783	. . 3 ⊢ (𝜑 → (𝑋 ∩ 𝑁) = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐾) = 𝐾})
97	5, 96	syl5eqr 2658	. 2 ⊢ (𝜑 → 𝑁 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐾) = 𝐾})
98		sylow3lem2.h	. 2 ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐾) = 𝐾}
99	97, 98	syl6reqr 2663	1 ⊢ (𝜑 → 𝐻 = 𝑁)

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173   ∩ cin 3539   ⊆ wss 3540   ↦ cmpt 4643  ran crn 5039   Fn wfn 5799  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551  Fincfn 7841  ℙcprime 15223  Basecbs 15695  +_gcplusg 15768  Grpcgrp 17245  -_gcsg 17247  SubGrpcsubg 17411   pSyl cslw 17770

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-1st 7059  df-2nd 7060  df-0g 15925  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-grp 17248  df-minusg 17249  df-sbg 17250  df-subg 17414  df-slw 17774

This theorem is referenced by:  sylow3lem3  17867