Theorem sylow3lem2 19330

Description: Lemma for sylow3 19335, 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 4032	. . . 4 ⊢ 𝑁 ⊆ 𝑋
4		sseqin2 4167	. . . 4 ⊢ (𝑁 ⊆ 𝑋 ↔ (𝑋 ∩ 𝑁) = 𝑁)
5	3, 4	mpbi 229	. . 3 ⊢ (𝑋 ∩ 𝑁) = 𝑁
6		simpr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → 𝑢 ∈ 𝑋)
7		sylow3lem2.k	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ (𝑃 pSyl 𝐺))
8	7	adantr 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → 𝐾 ∈ (𝑃 pSyl 𝐺))
9		mptexg 7158	. . . . . . . . 9 ⊢ (𝐾 ∈ (𝑃 pSyl 𝐺) → (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V)
10		rnexg 7824	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V → ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V)
11	8, 9, 10	3syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V)
12		simpr 486	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → 𝑦 = 𝐾)
13		simpl 484	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → 𝑥 = 𝑢)
14	13	oveq1d 7357	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → (𝑥 + 𝑧) = (𝑢 + 𝑧))
15	14, 13	oveq12d 7360	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → ((𝑥 + 𝑧) − 𝑥) = ((𝑢 + 𝑧) − 𝑢))
16	12, 15	mpteq12dv 5188	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
17	16	rneqd 5884	. . . . . . . . 9 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
18		sylow3lem1.m	. . . . . . . . 9 ⊢ ⊕ = (𝑥 ∈ 𝑋, 𝑦 ∈ (𝑃 pSyl 𝐺) ↦ ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)))
19	17, 18	ovmpoga 7494	. . . . . . . 8 ⊢ ((𝑢 ∈ 𝑋 ∧ 𝐾 ∈ (𝑃 pSyl 𝐺) ∧ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V) → (𝑢 ⊕ 𝐾) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
20	6, 8, 11, 19	syl3anc 1371	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → (𝑢 ⊕ 𝐾) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
21	20	adantr 482	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ 𝑢 ∈ 𝑁) → (𝑢 ⊕ 𝐾) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
22		slwsubg 19312	. . . . . . . . 9 ⊢ (𝐾 ∈ (𝑃 pSyl 𝐺) → 𝐾 ∈ (SubGrp‘𝐺))
23	7, 22	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺))
24	23	adantr 482	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → 𝐾 ∈ (SubGrp‘𝐺))
25		sylow3.x	. . . . . . . 8 ⊢ 𝑋 = (Base‘𝐺)
26		sylow3lem1.a	. . . . . . . 8 ⊢ + = (+g‘𝐺)
27		sylow3lem1.d	. . . . . . . 8 ⊢ − = (-g‘𝐺)
28		eqid 2737	. . . . . . . 8 ⊢ (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) = (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))
29	25, 26, 27, 28, 2	conjnmz 18965	. . . . . . 7 ⊢ ((𝐾 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑁) → 𝐾 = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
30	24, 29	sylan 581	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ 𝑢 ∈ 𝑁) → 𝐾 = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
31	21, 30	eqtr4d 2780	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ 𝑢 ∈ 𝑁) → (𝑢 ⊕ 𝐾) = 𝐾)
32		simplr 767	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ (𝑢 ⊕ 𝐾) = 𝐾) → 𝑢 ∈ 𝑋)
33		simprl 769	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → (𝑢 ⊕ 𝐾) = 𝐾)
34	20	adantr 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → (𝑢 ⊕ 𝐾) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
35	33, 34	eqtr3d 2779	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → 𝐾 = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
36	35	eleq2d 2823	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → ((𝑢 + 𝑤) ∈ 𝐾 ↔ (𝑢 + 𝑤) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))))
37		ovex 7375	. . . . . . . . . . . 12 ⊢ (𝑢 + 𝑤) ∈ V
38		eqeq1 2741	. . . . . . . . . . . . 13 ⊢ (𝑣 = (𝑢 + 𝑤) → (𝑣 = ((𝑢 + 𝑧) − 𝑢) ↔ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢)))
39	38	rexbidv 3172	. . . . . . . . . . . 12 ⊢ (𝑣 = (𝑢 + 𝑤) → (∃𝑧 ∈ 𝐾 𝑣 = ((𝑢 + 𝑧) − 𝑢) ↔ ∃𝑧 ∈ 𝐾 (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢)))
40	28	rnmpt 5901	. . . . . . . . . . . 12 ⊢ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) = {𝑣 ∣ ∃𝑧 ∈ 𝐾 𝑣 = ((𝑢 + 𝑧) − 𝑢)}
41	37, 39, 40	elab2 3627	. . . . . . . . . . 11 ⊢ ((𝑢 + 𝑤) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ↔ ∃𝑧 ∈ 𝐾 (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))
42		simprr 771	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))
43		sylow3.g	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐺 ∈ Grp)
44	43	ad3antrrr 728	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → 𝐺 ∈ Grp)
45		simpllr 774	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → 𝑢 ∈ 𝑋)
46	25	subgss 18853	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 ∈ (SubGrp‘𝐺) → 𝐾 ⊆ 𝑋)
47	23, 46	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 ⊆ 𝑋)
48	47	ad3antrrr 728	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → 𝐾 ⊆ 𝑋)
49		simprl 769	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → 𝑧 ∈ 𝐾)
50	48, 49	sseldd 3937	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → 𝑧 ∈ 𝑋)
51	25, 26, 27	grpaddsubass 18762	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ Grp ∧ (𝑢 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋)) → ((𝑢 + 𝑧) − 𝑢) = (𝑢 + (𝑧 − 𝑢)))
52	44, 45, 50, 45, 51	syl13anc 1372	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → ((𝑢 + 𝑧) − 𝑢) = (𝑢 + (𝑧 − 𝑢)))
53	42, 52	eqtr2d 2778	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → (𝑢 + (𝑧 − 𝑢)) = (𝑢 + 𝑤))
54	25, 27	grpsubcl 18752	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋) → (𝑧 − 𝑢) ∈ 𝑋)
55	44, 50, 45, 54	syl3anc 1371	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → (𝑧 − 𝑢) ∈ 𝑋)
56		simplrr 776	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → 𝑤 ∈ 𝑋)
57	25, 26	grplcan 18734	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ Grp ∧ ((𝑧 − 𝑢) ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋)) → ((𝑢 + (𝑧 − 𝑢)) = (𝑢 + 𝑤) ↔ (𝑧 − 𝑢) = 𝑤))
58	44, 55, 56, 45, 57	syl13anc 1372	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → ((𝑢 + (𝑧 − 𝑢)) = (𝑢 + 𝑤) ↔ (𝑧 − 𝑢) = 𝑤))
59	53, 58	mpbid 231	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → (𝑧 − 𝑢) = 𝑤)
60	25, 26, 27	grpsubadd 18760	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Grp ∧ (𝑧 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → ((𝑧 − 𝑢) = 𝑤 ↔ (𝑤 + 𝑢) = 𝑧))
61	44, 50, 45, 56, 60	syl13anc 1372	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → ((𝑧 − 𝑢) = 𝑤 ↔ (𝑤 + 𝑢) = 𝑧))
62	59, 61	mpbid 231	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → (𝑤 + 𝑢) = 𝑧)
63	62, 49	eqeltrd 2838	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → (𝑤 + 𝑢) ∈ 𝐾)
64	63	rexlimdvaa 3150	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → (∃𝑧 ∈ 𝐾 (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢) → (𝑤 + 𝑢) ∈ 𝐾))
65	41, 64	biimtrid 241	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → ((𝑢 + 𝑤) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) → (𝑤 + 𝑢) ∈ 𝐾))
66		simpr 486	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → (𝑤 + 𝑢) ∈ 𝐾)
67		oveq2 7350	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑤 + 𝑢) → (𝑢 + 𝑧) = (𝑢 + (𝑤 + 𝑢)))
68	67	oveq1d 7357	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑤 + 𝑢) → ((𝑢 + 𝑧) − 𝑢) = ((𝑢 + (𝑤 + 𝑢)) − 𝑢))
69		ovex 7375	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 + (𝑤 + 𝑢)) − 𝑢) ∈ V
70	68, 28, 69	fvmpt 6936	. . . . . . . . . . . . . 14 ⊢ ((𝑤 + 𝑢) ∈ 𝐾 → ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))‘(𝑤 + 𝑢)) = ((𝑢 + (𝑤 + 𝑢)) − 𝑢))
71	66, 70	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))‘(𝑤 + 𝑢)) = ((𝑢 + (𝑤 + 𝑢)) − 𝑢))
72	43	ad3antrrr 728	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → 𝐺 ∈ Grp)
73		simpllr 774	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → 𝑢 ∈ 𝑋)
74		simplrr 776	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → 𝑤 ∈ 𝑋)
75	25, 26	grpass 18683	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Grp ∧ (𝑢 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋)) → ((𝑢 + 𝑤) + 𝑢) = (𝑢 + (𝑤 + 𝑢)))
76	72, 73, 74, 73, 75	syl13anc 1372	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → ((𝑢 + 𝑤) + 𝑢) = (𝑢 + (𝑤 + 𝑢)))
77	76	oveq1d 7357	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → (((𝑢 + 𝑤) + 𝑢) − 𝑢) = ((𝑢 + (𝑤 + 𝑢)) − 𝑢))
78	25, 26	grpcl 18682	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑢 + 𝑤) ∈ 𝑋)
79	72, 73, 74, 78	syl3anc 1371	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → (𝑢 + 𝑤) ∈ 𝑋)
80	25, 26, 27	grppncan 18763	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ (𝑢 + 𝑤) ∈ 𝑋 ∧ 𝑢 ∈ 𝑋) → (((𝑢 + 𝑤) + 𝑢) − 𝑢) = (𝑢 + 𝑤))
81	72, 79, 73, 80	syl3anc 1371	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → (((𝑢 + 𝑤) + 𝑢) − 𝑢) = (𝑢 + 𝑤))
82	71, 77, 81	3eqtr2d 2783	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))‘(𝑤 + 𝑢)) = (𝑢 + 𝑤))
83		ovex 7375	. . . . . . . . . . . . . 14 ⊢ ((𝑢 + 𝑧) − 𝑢) ∈ V
84	83, 28	fnmpti 6632	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) Fn 𝐾
85		fnfvelrn 7019	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) Fn 𝐾 ∧ (𝑤 + 𝑢) ∈ 𝐾) → ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))‘(𝑤 + 𝑢)) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
86	84, 66, 85	sylancr 588	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))‘(𝑤 + 𝑢)) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
87	82, 86	eqeltrrd 2839	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → (𝑢 + 𝑤) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
88	87	ex 414	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → ((𝑤 + 𝑢) ∈ 𝐾 → (𝑢 + 𝑤) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))))
89	65, 88	impbid 211	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → ((𝑢 + 𝑤) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ↔ (𝑤 + 𝑢) ∈ 𝐾))
90	36, 89	bitrd 279	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → ((𝑢 + 𝑤) ∈ 𝐾 ↔ (𝑤 + 𝑢) ∈ 𝐾))
91	90	anassrs 469	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ (𝑢 ⊕ 𝐾) = 𝐾) ∧ 𝑤 ∈ 𝑋) → ((𝑢 + 𝑤) ∈ 𝐾 ↔ (𝑤 + 𝑢) ∈ 𝐾))
92	91	ralrimiva 3140	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ (𝑢 ⊕ 𝐾) = 𝐾) → ∀𝑤 ∈ 𝑋 ((𝑢 + 𝑤) ∈ 𝐾 ↔ (𝑤 + 𝑢) ∈ 𝐾))
93	2	elnmz 18888	. . . . . 6 ⊢ (𝑢 ∈ 𝑁 ↔ (𝑢 ∈ 𝑋 ∧ ∀𝑤 ∈ 𝑋 ((𝑢 + 𝑤) ∈ 𝐾 ↔ (𝑤 + 𝑢) ∈ 𝐾)))
94	32, 92, 93	sylanbrc 584	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ (𝑢 ⊕ 𝐾) = 𝐾) → 𝑢 ∈ 𝑁)
95	31, 94	impbida 799	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → (𝑢 ∈ 𝑁 ↔ (𝑢 ⊕ 𝐾) = 𝐾))
96	95	rabbi2dva 4169	. . 3 ⊢ (𝜑 → (𝑋 ∩ 𝑁) = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐾) = 𝐾})
97	5, 96	eqtr3id 2791	. 2 ⊢ (𝜑 → 𝑁 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐾) = 𝐾})
98	1, 97	eqtr4id 2796	1 ⊢ (𝜑 → 𝐻 = 𝑁)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1541   ∈ wcel 2106  ∀wral 3062  ∃wrex 3071  {crab 3404  Vcvv 3442   ∩ cin 3901   ⊆ wss 3902   ↦ cmpt 5180  ran crn 5626   Fn wfn 6479  ‘cfv 6484  (class class class)co 7342   ∈ cmpo 7344  Fincfn 8809  ℙcprime 16474  Basecbs 17010  +_gcplusg 17060  Grpcgrp 18674  -_gcsg 18676  SubGrpcsubg 18846   pSyl cslw 19232

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5234  ax-sep 5248  ax-nul 5255  ax-pow 5313  ax-pr 5377  ax-un 7655

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3444  df-sbc 3732  df-csb 3848  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4275  df-if 4479  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4858  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5181  df-id 5523  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6436  df-fun 6486  df-fn 6487  df-f 6488  df-f1 6489  df-fo 6490  df-f1o 6491  df-fv 6492  df-riota 7298  df-ov 7345  df-oprab 7346  df-mpo 7347  df-1st 7904  df-2nd 7905  df-0g 17250  df-mgm 18424  df-sgrp 18473  df-mnd 18484  df-grp 18677  df-minusg 18678  df-sbg 18679  df-subg 18849  df-slw 19236

This theorem is referenced by:  sylow3lem3  19331