Theorem sylow3lem2 19233

Description: Lemma for sylow3 19238, 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 4015	. . . 4 ⊢ 𝑁 ⊆ 𝑋
4		sseqin2 4149	. . . 4 ⊢ (𝑁 ⊆ 𝑋 ↔ (𝑋 ∩ 𝑁) = 𝑁)
5	3, 4	mpbi 229	. . 3 ⊢ (𝑋 ∩ 𝑁) = 𝑁
6		simpr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → 𝑢 ∈ 𝑋)
7		sylow3lem2.k	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ (𝑃 pSyl 𝐺))
8	7	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → 𝐾 ∈ (𝑃 pSyl 𝐺))
9		mptexg 7097	. . . . . . . . 9 ⊢ (𝐾 ∈ (𝑃 pSyl 𝐺) → (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V)
10		rnexg 7751	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V → ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V)
11	8, 9, 10	3syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V)
12		simpr 485	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → 𝑦 = 𝐾)
13		simpl 483	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → 𝑥 = 𝑢)
14	13	oveq1d 7290	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → (𝑥 + 𝑧) = (𝑢 + 𝑧))
15	14, 13	oveq12d 7293	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → ((𝑥 + 𝑧) − 𝑥) = ((𝑢 + 𝑧) − 𝑢))
16	12, 15	mpteq12dv 5165	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
17	16	rneqd 5847	. . . . . . . . 9 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
18		sylow3lem1.m	. . . . . . . . 9 ⊢ ⊕ = (𝑥 ∈ 𝑋, 𝑦 ∈ (𝑃 pSyl 𝐺) ↦ ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)))
19	17, 18	ovmpoga 7427	. . . . . . . 8 ⊢ ((𝑢 ∈ 𝑋 ∧ 𝐾 ∈ (𝑃 pSyl 𝐺) ∧ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V) → (𝑢 ⊕ 𝐾) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
20	6, 8, 11, 19	syl3anc 1370	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → (𝑢 ⊕ 𝐾) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
21	20	adantr 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ 𝑢 ∈ 𝑁) → (𝑢 ⊕ 𝐾) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
22		slwsubg 19215	. . . . . . . . 9 ⊢ (𝐾 ∈ (𝑃 pSyl 𝐺) → 𝐾 ∈ (SubGrp‘𝐺))
23	7, 22	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺))
24	23	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → 𝐾 ∈ (SubGrp‘𝐺))
25		sylow3.x	. . . . . . . 8 ⊢ 𝑋 = (Base‘𝐺)
26		sylow3lem1.a	. . . . . . . 8 ⊢ + = (+g‘𝐺)
27		sylow3lem1.d	. . . . . . . 8 ⊢ − = (-g‘𝐺)
28		eqid 2738	. . . . . . . 8 ⊢ (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) = (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))
29	25, 26, 27, 28, 2	conjnmz 18868	. . . . . . 7 ⊢ ((𝐾 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑁) → 𝐾 = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
30	24, 29	sylan 580	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ 𝑢 ∈ 𝑁) → 𝐾 = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
31	21, 30	eqtr4d 2781	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ 𝑢 ∈ 𝑁) → (𝑢 ⊕ 𝐾) = 𝐾)
32		simplr 766	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ (𝑢 ⊕ 𝐾) = 𝐾) → 𝑢 ∈ 𝑋)
33		simprl 768	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → (𝑢 ⊕ 𝐾) = 𝐾)
34	20	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → (𝑢 ⊕ 𝐾) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
35	33, 34	eqtr3d 2780	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → 𝐾 = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
36	35	eleq2d 2824	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → ((𝑢 + 𝑤) ∈ 𝐾 ↔ (𝑢 + 𝑤) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))))
37		ovex 7308	. . . . . . . . . . . 12 ⊢ (𝑢 + 𝑤) ∈ V
38		eqeq1 2742	. . . . . . . . . . . . 13 ⊢ (𝑣 = (𝑢 + 𝑤) → (𝑣 = ((𝑢 + 𝑧) − 𝑢) ↔ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢)))
39	38	rexbidv 3226	. . . . . . . . . . . 12 ⊢ (𝑣 = (𝑢 + 𝑤) → (∃𝑧 ∈ 𝐾 𝑣 = ((𝑢 + 𝑧) − 𝑢) ↔ ∃𝑧 ∈ 𝐾 (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢)))
40	28	rnmpt 5864	. . . . . . . . . . . 12 ⊢ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) = {𝑣 ∣ ∃𝑧 ∈ 𝐾 𝑣 = ((𝑢 + 𝑧) − 𝑢)}
41	37, 39, 40	elab2 3613	. . . . . . . . . . 11 ⊢ ((𝑢 + 𝑤) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ↔ ∃𝑧 ∈ 𝐾 (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))
42		simprr 770	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))
43		sylow3.g	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐺 ∈ Grp)
44	43	ad3antrrr 727	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → 𝐺 ∈ Grp)
45		simpllr 773	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → 𝑢 ∈ 𝑋)
46	25	subgss 18756	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 ∈ (SubGrp‘𝐺) → 𝐾 ⊆ 𝑋)
47	23, 46	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 ⊆ 𝑋)
48	47	ad3antrrr 727	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → 𝐾 ⊆ 𝑋)
49		simprl 768	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → 𝑧 ∈ 𝐾)
50	48, 49	sseldd 3922	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → 𝑧 ∈ 𝑋)
51	25, 26, 27	grpaddsubass 18665	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ Grp ∧ (𝑢 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋)) → ((𝑢 + 𝑧) − 𝑢) = (𝑢 + (𝑧 − 𝑢)))
52	44, 45, 50, 45, 51	syl13anc 1371	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → ((𝑢 + 𝑧) − 𝑢) = (𝑢 + (𝑧 − 𝑢)))
53	42, 52	eqtr2d 2779	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → (𝑢 + (𝑧 − 𝑢)) = (𝑢 + 𝑤))
54	25, 27	grpsubcl 18655	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋) → (𝑧 − 𝑢) ∈ 𝑋)
55	44, 50, 45, 54	syl3anc 1370	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → (𝑧 − 𝑢) ∈ 𝑋)
56		simplrr 775	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → 𝑤 ∈ 𝑋)
57	25, 26	grplcan 18637	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ Grp ∧ ((𝑧 − 𝑢) ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋)) → ((𝑢 + (𝑧 − 𝑢)) = (𝑢 + 𝑤) ↔ (𝑧 − 𝑢) = 𝑤))
58	44, 55, 56, 45, 57	syl13anc 1371	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → ((𝑢 + (𝑧 − 𝑢)) = (𝑢 + 𝑤) ↔ (𝑧 − 𝑢) = 𝑤))
59	53, 58	mpbid 231	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → (𝑧 − 𝑢) = 𝑤)
60	25, 26, 27	grpsubadd 18663	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Grp ∧ (𝑧 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → ((𝑧 − 𝑢) = 𝑤 ↔ (𝑤 + 𝑢) = 𝑧))
61	44, 50, 45, 56, 60	syl13anc 1371	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → ((𝑧 − 𝑢) = 𝑤 ↔ (𝑤 + 𝑢) = 𝑧))
62	59, 61	mpbid 231	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → (𝑤 + 𝑢) = 𝑧)
63	62, 49	eqeltrd 2839	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → (𝑤 + 𝑢) ∈ 𝐾)
64	63	rexlimdvaa 3214	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → (∃𝑧 ∈ 𝐾 (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢) → (𝑤 + 𝑢) ∈ 𝐾))
65	41, 64	syl5bi 241	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → ((𝑢 + 𝑤) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) → (𝑤 + 𝑢) ∈ 𝐾))
66		simpr 485	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → (𝑤 + 𝑢) ∈ 𝐾)
67		oveq2 7283	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑤 + 𝑢) → (𝑢 + 𝑧) = (𝑢 + (𝑤 + 𝑢)))
68	67	oveq1d 7290	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑤 + 𝑢) → ((𝑢 + 𝑧) − 𝑢) = ((𝑢 + (𝑤 + 𝑢)) − 𝑢))
69		ovex 7308	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 + (𝑤 + 𝑢)) − 𝑢) ∈ V
70	68, 28, 69	fvmpt 6875	. . . . . . . . . . . . . 14 ⊢ ((𝑤 + 𝑢) ∈ 𝐾 → ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))‘(𝑤 + 𝑢)) = ((𝑢 + (𝑤 + 𝑢)) − 𝑢))
71	66, 70	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))‘(𝑤 + 𝑢)) = ((𝑢 + (𝑤 + 𝑢)) − 𝑢))
72	43	ad3antrrr 727	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → 𝐺 ∈ Grp)
73		simpllr 773	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → 𝑢 ∈ 𝑋)
74		simplrr 775	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → 𝑤 ∈ 𝑋)
75	25, 26	grpass 18586	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Grp ∧ (𝑢 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋)) → ((𝑢 + 𝑤) + 𝑢) = (𝑢 + (𝑤 + 𝑢)))
76	72, 73, 74, 73, 75	syl13anc 1371	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → ((𝑢 + 𝑤) + 𝑢) = (𝑢 + (𝑤 + 𝑢)))
77	76	oveq1d 7290	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → (((𝑢 + 𝑤) + 𝑢) − 𝑢) = ((𝑢 + (𝑤 + 𝑢)) − 𝑢))
78	25, 26	grpcl 18585	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑢 + 𝑤) ∈ 𝑋)
79	72, 73, 74, 78	syl3anc 1370	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → (𝑢 + 𝑤) ∈ 𝑋)
80	25, 26, 27	grppncan 18666	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ (𝑢 + 𝑤) ∈ 𝑋 ∧ 𝑢 ∈ 𝑋) → (((𝑢 + 𝑤) + 𝑢) − 𝑢) = (𝑢 + 𝑤))
81	72, 79, 73, 80	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → (((𝑢 + 𝑤) + 𝑢) − 𝑢) = (𝑢 + 𝑤))
82	71, 77, 81	3eqtr2d 2784	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))‘(𝑤 + 𝑢)) = (𝑢 + 𝑤))
83		ovex 7308	. . . . . . . . . . . . . 14 ⊢ ((𝑢 + 𝑧) − 𝑢) ∈ V
84	83, 28	fnmpti 6576	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) Fn 𝐾
85		fnfvelrn 6958	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) Fn 𝐾 ∧ (𝑤 + 𝑢) ∈ 𝐾) → ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))‘(𝑤 + 𝑢)) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
86	84, 66, 85	sylancr 587	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))‘(𝑤 + 𝑢)) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
87	82, 86	eqeltrrd 2840	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → (𝑢 + 𝑤) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
88	87	ex 413	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → ((𝑤 + 𝑢) ∈ 𝐾 → (𝑢 + 𝑤) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))))
89	65, 88	impbid 211	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → ((𝑢 + 𝑤) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ↔ (𝑤 + 𝑢) ∈ 𝐾))
90	36, 89	bitrd 278	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → ((𝑢 + 𝑤) ∈ 𝐾 ↔ (𝑤 + 𝑢) ∈ 𝐾))
91	90	anassrs 468	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ (𝑢 ⊕ 𝐾) = 𝐾) ∧ 𝑤 ∈ 𝑋) → ((𝑢 + 𝑤) ∈ 𝐾 ↔ (𝑤 + 𝑢) ∈ 𝐾))
92	91	ralrimiva 3103	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ (𝑢 ⊕ 𝐾) = 𝐾) → ∀𝑤 ∈ 𝑋 ((𝑢 + 𝑤) ∈ 𝐾 ↔ (𝑤 + 𝑢) ∈ 𝐾))
93	2	elnmz 18791	. . . . . 6 ⊢ (𝑢 ∈ 𝑁 ↔ (𝑢 ∈ 𝑋 ∧ ∀𝑤 ∈ 𝑋 ((𝑢 + 𝑤) ∈ 𝐾 ↔ (𝑤 + 𝑢) ∈ 𝐾)))
94	32, 92, 93	sylanbrc 583	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ (𝑢 ⊕ 𝐾) = 𝐾) → 𝑢 ∈ 𝑁)
95	31, 94	impbida 798	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → (𝑢 ∈ 𝑁 ↔ (𝑢 ⊕ 𝐾) = 𝐾))
96	95	rabbi2dva 4151	. . 3 ⊢ (𝜑 → (𝑋 ∩ 𝑁) = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐾) = 𝐾})
97	5, 96	eqtr3id 2792	. 2 ⊢ (𝜑 → 𝑁 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐾) = 𝐾})
98	1, 97	eqtr4id 2797	1 ⊢ (𝜑 → 𝐻 = 𝑁)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2106  ∀wral 3064  ∃wrex 3065  {crab 3068  Vcvv 3432   ∩ cin 3886   ⊆ wss 3887   ↦ cmpt 5157  ran crn 5590   Fn wfn 6428  ‘cfv 6433  (class class class)co 7275   ∈ cmpo 7277  Fincfn 8733  ℙcprime 16376  Basecbs 16912  +_gcplusg 16962  Grpcgrp 18577  -_gcsg 18579  SubGrpcsubg 18749   pSyl cslw 19135

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-1st 7831  df-2nd 7832  df-0g 17152  df-mgm 18326  df-sgrp 18375  df-mnd 18386  df-grp 18580  df-minusg 18581  df-sbg 18582  df-subg 18752  df-slw 19139

This theorem is referenced by:  sylow3lem3  19234