Theorem sylow3lem2 19822

Description: Lemma for sylow3 19827, 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.h	. 2 ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐾) = 𝐾}
2		sylow3lem2.n	. . . . 5 ⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝐾 ↔ (𝑦 + 𝑥) ∈ 𝐾)}
3	2	ssrab3 4030	. . . 4 ⊢ 𝑁 ⊆ 𝑋
4		sseqin2 4169	. . . 4 ⊢ (𝑁 ⊆ 𝑋 ↔ (𝑋 ∩ 𝑁) = 𝑁)
5	3, 4	mpbi 233	. . 3 ⊢ (𝑋 ∩ 𝑁) = 𝑁
6		simpr 490	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → 𝑢 ∈ 𝑋)
7		sylow3lem2.k	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ (𝑃 pSyl 𝐺))
8	7	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → 𝐾 ∈ (𝑃 pSyl 𝐺))
9		mptexg 7219	. . . . . . . . 9 ⊢ (𝐾 ∈ (𝑃 pSyl 𝐺) → (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V)
10		rnexg 7903	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V → ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V)
11	8, 9, 10	3syl 19	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V)
12		simpr 490	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → 𝑦 = 𝐾)
13		simpl 488	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → 𝑥 = 𝑢)
14	13	oveq1d 7427	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → (𝑥 + 𝑧) = (𝑢 + 𝑧))
15	14, 13	oveq12d 7430	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → ((𝑥 + 𝑧) − 𝑥) = ((𝑢 + 𝑧) − 𝑢))
16	12, 15	mpteq12dv 5192	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
17	16	rneqd 5920	. . . . . . . . 9 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
18		sylow3lem1.m	. . . . . . . . 9 ⊢ ⊕ = (𝑥 ∈ 𝑋, 𝑦 ∈ (𝑃 pSyl 𝐺) ↦ ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)))
19	17, 18	ovmpoga 7566	. . . . . . . 8 ⊢ ((𝑢 ∈ 𝑋 ∧ 𝐾 ∈ (𝑃 pSyl 𝐺) ∧ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V) → (𝑢 ⊕ 𝐾) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
20	6, 8, 11, 19	syl3anc 1398	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → (𝑢 ⊕ 𝐾) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
21	20	adantr 486	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ 𝑢 ∈ 𝑁) → (𝑢 ⊕ 𝐾) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
22		slwsubg 19804	. . . . . . . . 9 ⊢ (𝐾 ∈ (𝑃 pSyl 𝐺) → 𝐾 ∈ (SubGrp‘𝐺))
23	7, 22	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺))
24	23	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → 𝐾 ∈ (SubGrp‘𝐺))
25		sylow3.x	. . . . . . . 8 ⊢ 𝑋 = (Base‘𝐺)
26		sylow3lem1.a	. . . . . . . 8 ⊢ + = (+g‘𝐺)
27		sylow3lem1.d	. . . . . . . 8 ⊢ − = (-g‘𝐺)
28		eqid 2761	. . . . . . . 8 ⊢ (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) = (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))
29	25, 26, 27, 28, 2	conjnmz 19446	. . . . . . 7 ⊢ ((𝐾 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑁) → 𝐾 = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
30	24, 29	sylan 592	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ 𝑢 ∈ 𝑁) → 𝐾 = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
31	21, 30	eqtr4d 2799	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ 𝑢 ∈ 𝑁) → (𝑢 ⊕ 𝐾) = 𝐾)
32		simplr 781	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ (𝑢 ⊕ 𝐾) = 𝐾) → 𝑢 ∈ 𝑋)
33		simprl 783	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → (𝑢 ⊕ 𝐾) = 𝐾)
34	20	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → (𝑢 ⊕ 𝐾) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
35	33, 34	eqtr3d 2798	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → 𝐾 = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
36	35	eleq2d 2847	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → ((𝑢 + 𝑤) ∈ 𝐾 ↔ (𝑢 + 𝑤) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))))
37		ovex 7445	. . . . . . . . . . . 12 ⊢ (𝑢 + 𝑤) ∈ V
38		eqeq1 2765	. . . . . . . . . . . . 13 ⊢ (𝑣 = (𝑢 + 𝑤) → (𝑣 = ((𝑢 + 𝑧) − 𝑢) ↔ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢)))
39	38	rexbidv 3187	. . . . . . . . . . . 12 ⊢ (𝑣 = (𝑢 + 𝑤) → (∃𝑧 ∈ 𝐾 𝑣 = ((𝑢 + 𝑧) − 𝑢) ↔ ∃𝑧 ∈ 𝐾 (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢)))
40	28	rnmpt 5939	. . . . . . . . . . . 12 ⊢ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) = {𝑣 ∣ ∃𝑧 ∈ 𝐾 𝑣 = ((𝑢 + 𝑧) − 𝑢)}
41	37, 39, 40	elab2 3636	. . . . . . . . . . 11 ⊢ ((𝑢 + 𝑤) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ↔ ∃𝑧 ∈ 𝐾 (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))
42		simprr 785	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))
43		sylow3.g	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐺 ∈ Grp)
44	43	ad3antrrr 743	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → 𝐺 ∈ Grp)
45		simpllr 788	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → 𝑢 ∈ 𝑋)
46	25	subgss 19317	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 ∈ (SubGrp‘𝐺) → 𝐾 ⊆ 𝑋)
47	23, 46	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 ⊆ 𝑋)
48	47	ad3antrrr 743	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → 𝐾 ⊆ 𝑋)
49		simprl 783	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → 𝑧 ∈ 𝐾)
50	48, 49	sseldd 3932	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → 𝑧 ∈ 𝑋)
51	25, 26, 27	grpaddsubass 19220	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ Grp ∧ (𝑢 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋)) → ((𝑢 + 𝑧) − 𝑢) = (𝑢 + (𝑧 − 𝑢)))
52	44, 45, 50, 45, 51	syl13anc 1399	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → ((𝑢 + 𝑧) − 𝑢) = (𝑢 + (𝑧 − 𝑢)))
53	42, 52	eqtr2d 2797	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → (𝑢 + (𝑧 − 𝑢)) = (𝑢 + 𝑤))
54	25, 27	grpsubcl 19210	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋) → (𝑧 − 𝑢) ∈ 𝑋)
55	44, 50, 45, 54	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → (𝑧 − 𝑢) ∈ 𝑋)
56		simplrr 790	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → 𝑤 ∈ 𝑋)
57	25, 26	grplcan 19191	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ Grp ∧ ((𝑧 − 𝑢) ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋)) → ((𝑢 + (𝑧 − 𝑢)) = (𝑢 + 𝑤) ↔ (𝑧 − 𝑢) = 𝑤))
58	44, 55, 56, 45, 57	syl13anc 1399	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → ((𝑢 + (𝑧 − 𝑢)) = (𝑢 + 𝑤) ↔ (𝑧 − 𝑢) = 𝑤))
59	53, 58	mpbid 235	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → (𝑧 − 𝑢) = 𝑤)
60	25, 26, 27	grpsubadd 19218	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Grp ∧ (𝑧 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → ((𝑧 − 𝑢) = 𝑤 ↔ (𝑤 + 𝑢) = 𝑧))
61	44, 50, 45, 56, 60	syl13anc 1399	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → ((𝑧 − 𝑢) = 𝑤 ↔ (𝑤 + 𝑢) = 𝑧))
62	59, 61	mpbid 235	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → (𝑤 + 𝑢) = 𝑧)
63	62, 49	eqeltrd 2861	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → (𝑤 + 𝑢) ∈ 𝐾)
64	63	rexlimdvaa 3165	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → (∃𝑧 ∈ 𝐾 (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢) → (𝑤 + 𝑢) ∈ 𝐾))
65	41, 64	biimtrid 245	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → ((𝑢 + 𝑤) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) → (𝑤 + 𝑢) ∈ 𝐾))
66		simpr 490	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → (𝑤 + 𝑢) ∈ 𝐾)
67		oveq2 7420	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑤 + 𝑢) → (𝑢 + 𝑧) = (𝑢 + (𝑤 + 𝑢)))
68	67	oveq1d 7427	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑤 + 𝑢) → ((𝑢 + 𝑧) − 𝑢) = ((𝑢 + (𝑤 + 𝑢)) − 𝑢))
69		ovex 7445	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 + (𝑤 + 𝑢)) − 𝑢) ∈ V
70	68, 28, 69	fvmpt 6985	. . . . . . . . . . . . . 14 ⊢ ((𝑤 + 𝑢) ∈ 𝐾 → ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))‘(𝑤 + 𝑢)) = ((𝑢 + (𝑤 + 𝑢)) − 𝑢))
71	66, 70	syl 18	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))‘(𝑤 + 𝑢)) = ((𝑢 + (𝑤 + 𝑢)) − 𝑢))
72	43	ad3antrrr 743	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → 𝐺 ∈ Grp)
73		simpllr 788	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → 𝑢 ∈ 𝑋)
74		simplrr 790	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → 𝑤 ∈ 𝑋)
75	25, 26	grpass 19133	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Grp ∧ (𝑢 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋)) → ((𝑢 + 𝑤) + 𝑢) = (𝑢 + (𝑤 + 𝑢)))
76	72, 73, 74, 73, 75	syl13anc 1399	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → ((𝑢 + 𝑤) + 𝑢) = (𝑢 + (𝑤 + 𝑢)))
77	76	oveq1d 7427	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → (((𝑢 + 𝑤) + 𝑢) − 𝑢) = ((𝑢 + (𝑤 + 𝑢)) − 𝑢))
78	25, 26	grpcl 19132	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑢 + 𝑤) ∈ 𝑋)
79	72, 73, 74, 78	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → (𝑢 + 𝑤) ∈ 𝑋)
80	25, 26, 27	grppncan 19221	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ (𝑢 + 𝑤) ∈ 𝑋 ∧ 𝑢 ∈ 𝑋) → (((𝑢 + 𝑤) + 𝑢) − 𝑢) = (𝑢 + 𝑤))
81	72, 79, 73, 80	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → (((𝑢 + 𝑤) + 𝑢) − 𝑢) = (𝑢 + 𝑤))
82	71, 77, 81	3eqtr2d 2802	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))‘(𝑤 + 𝑢)) = (𝑢 + 𝑤))
83		ovex 7445	. . . . . . . . . . . . . 14 ⊢ ((𝑢 + 𝑧) − 𝑢) ∈ V
84	83, 28	fnmpti 6674	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) Fn 𝐾
85		fnfvelrn 7072	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) Fn 𝐾 ∧ (𝑤 + 𝑢) ∈ 𝐾) → ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))‘(𝑤 + 𝑢)) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
86	84, 66, 85	sylancr 599	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))‘(𝑤 + 𝑢)) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
87	82, 86	eqeltrrd 2862	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → (𝑢 + 𝑤) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
88	87	ex 418	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → ((𝑤 + 𝑢) ∈ 𝐾 → (𝑢 + 𝑤) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))))
89	65, 88	impbid 215	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → ((𝑢 + 𝑤) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ↔ (𝑤 + 𝑢) ∈ 𝐾))
90	36, 89	bitrd 282	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → ((𝑢 + 𝑤) ∈ 𝐾 ↔ (𝑤 + 𝑢) ∈ 𝐾))
91	90	anassrs 473	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ (𝑢 ⊕ 𝐾) = 𝐾) ∧ 𝑤 ∈ 𝑋) → ((𝑢 + 𝑤) ∈ 𝐾 ↔ (𝑤 + 𝑢) ∈ 𝐾))
92	91	ralrimiva 3155	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ (𝑢 ⊕ 𝐾) = 𝐾) → ∀𝑤 ∈ 𝑋 ((𝑢 + 𝑤) ∈ 𝐾 ↔ (𝑤 + 𝑢) ∈ 𝐾))
93	2	elnmz 19353	. . . . . 6 ⊢ (𝑢 ∈ 𝑁 ↔ (𝑢 ∈ 𝑋 ∧ ∀𝑤 ∈ 𝑋 ((𝑢 + 𝑤) ∈ 𝐾 ↔ (𝑤 + 𝑢) ∈ 𝐾)))
94	32, 92, 93	sylanbrc 595	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ (𝑢 ⊕ 𝐾) = 𝐾) → 𝑢 ∈ 𝑁)
95	31, 94	impbida 813	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → (𝑢 ∈ 𝑁 ↔ (𝑢 ⊕ 𝐾) = 𝐾))
96	95	rabbi2dva 4171	. . 3 ⊢ (𝜑 → (𝑋 ∩ 𝑁) = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐾) = 𝐾})
97	5, 96	eqtr3id 2810	. 2 ⊢ (𝜑 → 𝑁 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐾) = 𝐾})
98	1, 97	eqtr4id 2815	1 ⊢ (𝜑 → 𝐻 = 𝑁)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3077  ∃wrex 3087  {crab 3413  Vcvv 3451   ∩ cin 3898   ⊆ wss 3899   ↦ cmpt 5186  ran crn 5652   Fn wfn 6526  ‘cfv 6531  (class class class)co 7412   ∈ cmpo 7414  Fincfn 8957  ℙcprime 16826  Basecbs 17367  +_gcplusg 17408  Grpcgrp 19124  -_gcsg 19126  SubGrpcsubg 19310   pSyl cslw 19721

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1st 7990  df-2nd 7991  df-0g 17592  df-mgm 18796  df-sgrp 18888  df-mnd 18904  df-grp 19127  df-minusg 19128  df-sbg 19129  df-subg 19313  df-slw 19725

This theorem is used by:  sylow3lem3  19823