Theorem sylow2blem3 17860

Description: Sylow's second theorem. Putting together the results of sylow2a 17857 and the orbit-stabilizer theorem to show that 𝑃 does not divide the set of all fixed points under the group action, we get that there is a fixed point of the group action, so that there is some 𝑔 ∈ 𝑋 with ℎ𝑔𝐾 = 𝑔𝐾 for all ℎ ∈ 𝐻. This implies that inv_g(𝑔)ℎ𝑔 ∈ 𝐾, so ℎ is in the conjugated subgroup 𝑔𝐾inv_g(𝑔). (Contributed by Mario Carneiro, 18-Jan-2015.)

Hypotheses

Ref	Expression
sylow2b.x	⊢ 𝑋 = (Base‘𝐺)
sylow2b.xf	⊢ (𝜑 → 𝑋 ∈ Fin)
sylow2b.h	⊢ (𝜑 → 𝐻 ∈ (SubGrp‘𝐺))
sylow2b.k	⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺))
sylow2b.a	⊢ + = (+g‘𝐺)
sylow2b.r	⊢ ∼ = (𝐺 ~QG 𝐾)
sylow2b.m	⊢ · = (𝑥 ∈ 𝐻, 𝑦 ∈ (𝑋 / ∼ ) ↦ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)))
sylow2blem3.hp	⊢ (𝜑 → 𝑃 pGrp (𝐺 ↾s 𝐻))
sylow2blem3.kn	⊢ (𝜑 → (#‘𝐾) = (𝑃↑(𝑃 pCnt (#‘𝑋))))
sylow2blem3.d	⊢ − = (-g‘𝐺)

Assertion

Ref	Expression
sylow2blem3	⊢ (𝜑 → ∃𝑔 ∈ 𝑋 𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)))

Distinct variable groups:   𝑥,𝑔,𝑦,𝑧,𝐺   𝑔,𝐾,𝑥,𝑦,𝑧   · ,𝑔,𝑥,𝑦,𝑧   + ,𝑔,𝑥,𝑦,𝑧   ∼ ,𝑔,𝑥,𝑦,𝑧   𝜑,𝑔,𝑧   𝑥, − ,𝑧   𝑔,𝐻,𝑥,𝑦,𝑧   𝑔,𝑋,𝑥,𝑦,𝑧

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝑃(𝑥,𝑦,𝑧,𝑔)   − (𝑦,𝑔)

Proof of Theorem sylow2blem3

Dummy variable 𝑢 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sylow2blem3.hp	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 pGrp (𝐺 ↾s 𝐻))
2		pgpprm 17831	. . . . . . . . 9 ⊢ (𝑃 pGrp (𝐺 ↾s 𝐻) → 𝑃 ∈ ℙ)
3	1, 2	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ ℙ)
4		sylow2b.h	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻 ∈ (SubGrp‘𝐺))
5		subgrcl 17422	. . . . . . . . . . 11 ⊢ (𝐻 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp)
6	4, 5	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ Grp)
7		sylow2b.x	. . . . . . . . . . 11 ⊢ 𝑋 = (Base‘𝐺)
8	7	grpbn0 17274	. . . . . . . . . 10 ⊢ (𝐺 ∈ Grp → 𝑋 ≠ ∅)
9	6, 8	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ≠ ∅)
10		sylow2b.xf	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ Fin)
11		hashnncl 13018	. . . . . . . . . 10 ⊢ (𝑋 ∈ Fin → ((#‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅))
12	10, 11	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((#‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅))
13	9, 12	mpbird 246	. . . . . . . 8 ⊢ (𝜑 → (#‘𝑋) ∈ ℕ)
14		pcndvds2 15410	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ (#‘𝑋) ∈ ℕ) → ¬ 𝑃 ∥ ((#‘𝑋) / (𝑃↑(𝑃 pCnt (#‘𝑋)))))
15	3, 13, 14	syl2anc 691	. . . . . . 7 ⊢ (𝜑 → ¬ 𝑃 ∥ ((#‘𝑋) / (𝑃↑(𝑃 pCnt (#‘𝑋)))))
16		sylow2b.r	. . . . . . . . . . 11 ⊢ ∼ = (𝐺 ~QG 𝐾)
17		sylow2b.k	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺))
18	7, 16, 17, 10	lagsubg2 17478	. . . . . . . . . 10 ⊢ (𝜑 → (#‘𝑋) = ((#‘(𝑋 / ∼ )) · (#‘𝐾)))
19	18	oveq1d 6564	. . . . . . . . 9 ⊢ (𝜑 → ((#‘𝑋) / (#‘𝐾)) = (((#‘(𝑋 / ∼ )) · (#‘𝐾)) / (#‘𝐾)))
20		sylow2blem3.kn	. . . . . . . . . 10 ⊢ (𝜑 → (#‘𝐾) = (𝑃↑(𝑃 pCnt (#‘𝑋))))
21	20	oveq2d 6565	. . . . . . . . 9 ⊢ (𝜑 → ((#‘𝑋) / (#‘𝐾)) = ((#‘𝑋) / (𝑃↑(𝑃 pCnt (#‘𝑋)))))
22		pwfi 8144	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ Fin ↔ 𝒫 𝑋 ∈ Fin)
23	10, 22	sylib 207	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝒫 𝑋 ∈ Fin)
24	7, 16	eqger 17467	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (SubGrp‘𝐺) → ∼ Er 𝑋)
25	17, 24	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∼ Er 𝑋)
26	25	qsss 7695	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 / ∼ ) ⊆ 𝒫 𝑋)
27		ssfi 8065	. . . . . . . . . . . . 13 ⊢ ((𝒫 𝑋 ∈ Fin ∧ (𝑋 / ∼ ) ⊆ 𝒫 𝑋) → (𝑋 / ∼ ) ∈ Fin)
28	23, 26, 27	syl2anc 691	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 / ∼ ) ∈ Fin)
29		hashcl 13009	. . . . . . . . . . . 12 ⊢ ((𝑋 / ∼ ) ∈ Fin → (#‘(𝑋 / ∼ )) ∈ ℕ0)
30	28, 29	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (#‘(𝑋 / ∼ )) ∈ ℕ0)
31	30	nn0cnd 11230	. . . . . . . . . 10 ⊢ (𝜑 → (#‘(𝑋 / ∼ )) ∈ ℂ)
32		eqid 2610	. . . . . . . . . . . . . . 15 ⊢ (0g‘𝐺) = (0g‘𝐺)
33	32	subg0cl 17425	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (SubGrp‘𝐺) → (0g‘𝐺) ∈ 𝐾)
34	17, 33	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0g‘𝐺) ∈ 𝐾)
35		ne0i 3880	. . . . . . . . . . . . 13 ⊢ ((0g‘𝐺) ∈ 𝐾 → 𝐾 ≠ ∅)
36	34, 35	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ≠ ∅)
37	7	subgss 17418	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (SubGrp‘𝐺) → 𝐾 ⊆ 𝑋)
38	17, 37	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ⊆ 𝑋)
39		ssfi 8065	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∈ Fin ∧ 𝐾 ⊆ 𝑋) → 𝐾 ∈ Fin)
40	10, 38, 39	syl2anc 691	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐾 ∈ Fin)
41		hashnncl 13018	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ Fin → ((#‘𝐾) ∈ ℕ ↔ 𝐾 ≠ ∅))
42	40, 41	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((#‘𝐾) ∈ ℕ ↔ 𝐾 ≠ ∅))
43	36, 42	mpbird 246	. . . . . . . . . . 11 ⊢ (𝜑 → (#‘𝐾) ∈ ℕ)
44	43	nncnd 10913	. . . . . . . . . 10 ⊢ (𝜑 → (#‘𝐾) ∈ ℂ)
45	43	nnne0d 10942	. . . . . . . . . 10 ⊢ (𝜑 → (#‘𝐾) ≠ 0)
46	31, 44, 45	divcan4d 10686	. . . . . . . . 9 ⊢ (𝜑 → (((#‘(𝑋 / ∼ )) · (#‘𝐾)) / (#‘𝐾)) = (#‘(𝑋 / ∼ )))
47	19, 21, 46	3eqtr3d 2652	. . . . . . . 8 ⊢ (𝜑 → ((#‘𝑋) / (𝑃↑(𝑃 pCnt (#‘𝑋)))) = (#‘(𝑋 / ∼ )))
48	47	breq2d 4595	. . . . . . 7 ⊢ (𝜑 → (𝑃 ∥ ((#‘𝑋) / (𝑃↑(𝑃 pCnt (#‘𝑋)))) ↔ 𝑃 ∥ (#‘(𝑋 / ∼ ))))
49	15, 48	mtbid 313	. . . . . 6 ⊢ (𝜑 → ¬ 𝑃 ∥ (#‘(𝑋 / ∼ )))
50		prmz 15227	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
51	3, 50	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ ℤ)
52	30	nn0zd 11356	. . . . . . 7 ⊢ (𝜑 → (#‘(𝑋 / ∼ )) ∈ ℤ)
53		ssrab2 3650	. . . . . . . . . 10 ⊢ {𝑧 ∈ (𝑋 / ∼ ) ∣ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧} ⊆ (𝑋 / ∼ )
54		ssfi 8065	. . . . . . . . . 10 ⊢ (((𝑋 / ∼ ) ∈ Fin ∧ {𝑧 ∈ (𝑋 / ∼ ) ∣ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧} ⊆ (𝑋 / ∼ )) → {𝑧 ∈ (𝑋 / ∼ ) ∣ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin)
55	28, 53, 54	sylancl 693	. . . . . . . . 9 ⊢ (𝜑 → {𝑧 ∈ (𝑋 / ∼ ) ∣ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin)
56		hashcl 13009	. . . . . . . . 9 ⊢ ({𝑧 ∈ (𝑋 / ∼ ) ∣ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin → (#‘{𝑧 ∈ (𝑋 / ∼ ) ∣ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈ ℕ0)
57	55, 56	syl 17	. . . . . . . 8 ⊢ (𝜑 → (#‘{𝑧 ∈ (𝑋 / ∼ ) ∣ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈ ℕ0)
58	57	nn0zd 11356	. . . . . . 7 ⊢ (𝜑 → (#‘{𝑧 ∈ (𝑋 / ∼ ) ∣ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈ ℤ)
59		eqid 2610	. . . . . . . 8 ⊢ (Base‘(𝐺 ↾s 𝐻)) = (Base‘(𝐺 ↾s 𝐻))
60		sylow2b.a	. . . . . . . . 9 ⊢ + = (+g‘𝐺)
61		sylow2b.m	. . . . . . . . 9 ⊢ · = (𝑥 ∈ 𝐻, 𝑦 ∈ (𝑋 / ∼ ) ↦ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)))
62	7, 10, 4, 17, 60, 16, 61	sylow2blem2 17859	. . . . . . . 8 ⊢ (𝜑 → · ∈ ((𝐺 ↾s 𝐻) GrpAct (𝑋 / ∼ )))
63		eqid 2610	. . . . . . . . . . 11 ⊢ (𝐺 ↾s 𝐻) = (𝐺 ↾s 𝐻)
64	63	subgbas 17421	. . . . . . . . . 10 ⊢ (𝐻 ∈ (SubGrp‘𝐺) → 𝐻 = (Base‘(𝐺 ↾s 𝐻)))
65	4, 64	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐻 = (Base‘(𝐺 ↾s 𝐻)))
66	7	subgss 17418	. . . . . . . . . . 11 ⊢ (𝐻 ∈ (SubGrp‘𝐺) → 𝐻 ⊆ 𝑋)
67	4, 66	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐻 ⊆ 𝑋)
68		ssfi 8065	. . . . . . . . . 10 ⊢ ((𝑋 ∈ Fin ∧ 𝐻 ⊆ 𝑋) → 𝐻 ∈ Fin)
69	10, 67, 68	syl2anc 691	. . . . . . . . 9 ⊢ (𝜑 → 𝐻 ∈ Fin)
70	65, 69	eqeltrrd 2689	. . . . . . . 8 ⊢ (𝜑 → (Base‘(𝐺 ↾s 𝐻)) ∈ Fin)
71		eqid 2610	. . . . . . . 8 ⊢ {𝑧 ∈ (𝑋 / ∼ ) ∣ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧} = {𝑧 ∈ (𝑋 / ∼ ) ∣ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧}
72		eqid 2610	. . . . . . . 8 ⊢ {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑋 / ∼ ) ∧ ∃𝑔 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑔 · 𝑥) = 𝑦)} = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑋 / ∼ ) ∧ ∃𝑔 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑔 · 𝑥) = 𝑦)}
73	59, 62, 1, 70, 28, 71, 72	sylow2a 17857	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∥ ((#‘(𝑋 / ∼ )) − (#‘{𝑧 ∈ (𝑋 / ∼ ) ∣ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧})))
74		dvdssub2 14861	. . . . . . 7 ⊢ (((𝑃 ∈ ℤ ∧ (#‘(𝑋 / ∼ )) ∈ ℤ ∧ (#‘{𝑧 ∈ (𝑋 / ∼ ) ∣ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈ ℤ) ∧ 𝑃 ∥ ((#‘(𝑋 / ∼ )) − (#‘{𝑧 ∈ (𝑋 / ∼ ) ∣ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧}))) → (𝑃 ∥ (#‘(𝑋 / ∼ )) ↔ 𝑃 ∥ (#‘{𝑧 ∈ (𝑋 / ∼ ) ∣ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧})))
75	51, 52, 58, 73, 74	syl31anc 1321	. . . . . 6 ⊢ (𝜑 → (𝑃 ∥ (#‘(𝑋 / ∼ )) ↔ 𝑃 ∥ (#‘{𝑧 ∈ (𝑋 / ∼ ) ∣ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧})))
76	49, 75	mtbid 313	. . . . 5 ⊢ (𝜑 → ¬ 𝑃 ∥ (#‘{𝑧 ∈ (𝑋 / ∼ ) ∣ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧}))
77		hasheq0 13015	. . . . . . . 8 ⊢ ({𝑧 ∈ (𝑋 / ∼ ) ∣ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin → ((#‘{𝑧 ∈ (𝑋 / ∼ ) ∣ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧}) = 0 ↔ {𝑧 ∈ (𝑋 / ∼ ) ∣ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧} = ∅))
78	55, 77	syl 17	. . . . . . 7 ⊢ (𝜑 → ((#‘{𝑧 ∈ (𝑋 / ∼ ) ∣ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧}) = 0 ↔ {𝑧 ∈ (𝑋 / ∼ ) ∣ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧} = ∅))
79		dvds0 14835	. . . . . . . . 9 ⊢ (𝑃 ∈ ℤ → 𝑃 ∥ 0)
80	51, 79	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∥ 0)
81		breq2 4587	. . . . . . . 8 ⊢ ((#‘{𝑧 ∈ (𝑋 / ∼ ) ∣ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧}) = 0 → (𝑃 ∥ (#‘{𝑧 ∈ (𝑋 / ∼ ) ∣ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧}) ↔ 𝑃 ∥ 0))
82	80, 81	syl5ibrcom 236	. . . . . . 7 ⊢ (𝜑 → ((#‘{𝑧 ∈ (𝑋 / ∼ ) ∣ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧}) = 0 → 𝑃 ∥ (#‘{𝑧 ∈ (𝑋 / ∼ ) ∣ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧})))
83	78, 82	sylbird 249	. . . . . 6 ⊢ (𝜑 → ({𝑧 ∈ (𝑋 / ∼ ) ∣ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧} = ∅ → 𝑃 ∥ (#‘{𝑧 ∈ (𝑋 / ∼ ) ∣ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧})))
84	83	necon3bd 2796	. . . . 5 ⊢ (𝜑 → (¬ 𝑃 ∥ (#‘{𝑧 ∈ (𝑋 / ∼ ) ∣ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧}) → {𝑧 ∈ (𝑋 / ∼ ) ∣ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧} ≠ ∅))
85	76, 84	mpd 15	. . . 4 ⊢ (𝜑 → {𝑧 ∈ (𝑋 / ∼ ) ∣ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧} ≠ ∅)
86		rabn0 3912	. . . 4 ⊢ ({𝑧 ∈ (𝑋 / ∼ ) ∣ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧} ≠ ∅ ↔ ∃𝑧 ∈ (𝑋 / ∼ )∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧)
87	85, 86	sylib 207	. . 3 ⊢ (𝜑 → ∃𝑧 ∈ (𝑋 / ∼ )∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧)
88	65	raleqdv 3121	. . . 4 ⊢ (𝜑 → (∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧 ↔ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧))
89	88	rexbidv 3034	. . 3 ⊢ (𝜑 → (∃𝑧 ∈ (𝑋 / ∼ )∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧 ↔ ∃𝑧 ∈ (𝑋 / ∼ )∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧))
90	87, 89	mpbird 246	. 2 ⊢ (𝜑 → ∃𝑧 ∈ (𝑋 / ∼ )∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧)
91		vex 3176	. . . . 5 ⊢ 𝑧 ∈ V
92	91	elqs 7686	. . . 4 ⊢ (𝑧 ∈ (𝑋 / ∼ ) ↔ ∃𝑔 ∈ 𝑋 𝑧 = [𝑔] ∼ )
93		simplrr 797	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑧 = [𝑔] ∼ )
94	93	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 · 𝑧) = (𝑢 · [𝑔] ∼ ))
95		simprr 792	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 · 𝑧) = 𝑧)
96		simpll 786	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝜑)
97		simprl 790	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑢 ∈ 𝐻)
98		simplrl 796	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑔 ∈ 𝑋)
99	7, 10, 4, 17, 60, 16, 61	sylow2blem1 17858	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐻 ∧ 𝑔 ∈ 𝑋) → (𝑢 · [𝑔] ∼ ) = [(𝑢 + 𝑔)] ∼ )
100	96, 97, 98, 99	syl3anc 1318	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 · [𝑔] ∼ ) = [(𝑢 + 𝑔)] ∼ )
101	94, 95, 100	3eqtr3d 2652	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑧 = [(𝑢 + 𝑔)] ∼ )
102	93, 101	eqtr3d 2646	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → [𝑔] ∼ = [(𝑢 + 𝑔)] ∼ )
103	25	ad2antrr 758	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ∼ Er 𝑋)
104	103, 98	erth 7678	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 ∼ (𝑢 + 𝑔) ↔ [𝑔] ∼ = [(𝑢 + 𝑔)] ∼ ))
105	102, 104	mpbird 246	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑔 ∼ (𝑢 + 𝑔))
106	6	ad2antrr 758	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝐺 ∈ Grp)
107	38	ad2antrr 758	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝐾 ⊆ 𝑋)
108		eqid 2610	. . . . . . . . . . . . . . . . . . . 20 ⊢ (invg‘𝐺) = (invg‘𝐺)
109	7, 108, 60, 16	eqgval 17466	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 ∈ Grp ∧ 𝐾 ⊆ 𝑋) → (𝑔 ∼ (𝑢 + 𝑔) ↔ (𝑔 ∈ 𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾)))
110	106, 107, 109	syl2anc 691	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 ∼ (𝑢 + 𝑔) ↔ (𝑔 ∈ 𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾)))
111	105, 110	mpbid 221	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 ∈ 𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾))
112	111	simp3d 1068	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾)
113		oveq2 6557	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔)) → (𝑔 + 𝑥) = (𝑔 + (((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))))
114	113	oveq1d 6564	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔)) → ((𝑔 + 𝑥) − 𝑔) = ((𝑔 + (((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) − 𝑔))
115		eqid 2610	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)) = (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))
116		ovex 6577	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 + (((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) − 𝑔) ∈ V
117	114, 115, 116	fvmpt 6191	. . . . . . . . . . . . . . . 16 ⊢ ((((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾 → ((𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))‘(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) = ((𝑔 + (((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) − 𝑔))
118	112, 117	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))‘(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) = ((𝑔 + (((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) − 𝑔))
119	7, 60, 32, 108	grprinv 17292	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 ∈ Grp ∧ 𝑔 ∈ 𝑋) → (𝑔 + ((invg‘𝐺)‘𝑔)) = (0g‘𝐺))
120	106, 98, 119	syl2anc 691	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 + ((invg‘𝐺)‘𝑔)) = (0g‘𝐺))
121	120	oveq1d 6564	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑔 + ((invg‘𝐺)‘𝑔)) + (𝑢 + 𝑔)) = ((0g‘𝐺) + (𝑢 + 𝑔)))
122	7, 108	grpinvcl 17290	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 ∈ Grp ∧ 𝑔 ∈ 𝑋) → ((invg‘𝐺)‘𝑔) ∈ 𝑋)
123	106, 98, 122	syl2anc 691	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((invg‘𝐺)‘𝑔) ∈ 𝑋)
124	67	ad2antrr 758	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝐻 ⊆ 𝑋)
125	124, 97	sseldd 3569	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑢 ∈ 𝑋)
126	7, 60	grpcl 17253	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋) → (𝑢 + 𝑔) ∈ 𝑋)
127	106, 125, 98, 126	syl3anc 1318	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 + 𝑔) ∈ 𝑋)
128	7, 60	grpass 17254	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺 ∈ Grp ∧ (𝑔 ∈ 𝑋 ∧ ((invg‘𝐺)‘𝑔) ∈ 𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋)) → ((𝑔 + ((invg‘𝐺)‘𝑔)) + (𝑢 + 𝑔)) = (𝑔 + (((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))))
129	106, 98, 123, 127, 128	syl13anc 1320	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑔 + ((invg‘𝐺)‘𝑔)) + (𝑢 + 𝑔)) = (𝑔 + (((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))))
130	7, 60, 32	grplid 17275	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺 ∈ Grp ∧ (𝑢 + 𝑔) ∈ 𝑋) → ((0g‘𝐺) + (𝑢 + 𝑔)) = (𝑢 + 𝑔))
131	106, 127, 130	syl2anc 691	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((0g‘𝐺) + (𝑢 + 𝑔)) = (𝑢 + 𝑔))
132	121, 129, 131	3eqtr3d 2652	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 + (((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) = (𝑢 + 𝑔))
133	132	oveq1d 6564	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑔 + (((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) − 𝑔) = ((𝑢 + 𝑔) − 𝑔))
134		sylow2blem3.d	. . . . . . . . . . . . . . . . 17 ⊢ − = (-g‘𝐺)
135	7, 60, 134	grppncan 17329	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋) → ((𝑢 + 𝑔) − 𝑔) = 𝑢)
136	106, 125, 98, 135	syl3anc 1318	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑢 + 𝑔) − 𝑔) = 𝑢)
137	118, 133, 136	3eqtrd 2648	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))‘(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) = 𝑢)
138		ovex 6577	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 + 𝑥) − 𝑔) ∈ V
139	138, 115	fnmpti 5935	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)) Fn 𝐾
140		fnfvelrn 6264	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)) Fn 𝐾 ∧ (((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾) → ((𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))‘(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) ∈ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)))
141	139, 112, 140	sylancr 694	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))‘(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) ∈ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)))
142	137, 141	eqeltrrd 2689	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑢 ∈ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)))
143	142	expr 641	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ 𝑢 ∈ 𝐻) → ((𝑢 · 𝑧) = 𝑧 → 𝑢 ∈ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))))
144	143	ralimdva 2945	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) → (∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧 → ∀𝑢 ∈ 𝐻 𝑢 ∈ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))))
145	144	imp 444	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ ∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧) → ∀𝑢 ∈ 𝐻 𝑢 ∈ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)))
146	145	an32s 842	. . . . . . . . 9 ⊢ (((𝜑 ∧ ∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧) ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) → ∀𝑢 ∈ 𝐻 𝑢 ∈ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)))
147		dfss3 3558	. . . . . . . . 9 ⊢ (𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)) ↔ ∀𝑢 ∈ 𝐻 𝑢 ∈ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)))
148	146, 147	sylibr 223	. . . . . . . 8 ⊢ (((𝜑 ∧ ∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧) ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) → 𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)))
149	148	expr 641	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧) ∧ 𝑔 ∈ 𝑋) → (𝑧 = [𝑔] ∼ → 𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))))
150	149	reximdva 3000	. . . . . 6 ⊢ ((𝜑 ∧ ∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧) → (∃𝑔 ∈ 𝑋 𝑧 = [𝑔] ∼ → ∃𝑔 ∈ 𝑋 𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))))
151	150	ex 449	. . . . 5 ⊢ (𝜑 → (∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧 → (∃𝑔 ∈ 𝑋 𝑧 = [𝑔] ∼ → ∃𝑔 ∈ 𝑋 𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)))))
152	151	com23 84	. . . 4 ⊢ (𝜑 → (∃𝑔 ∈ 𝑋 𝑧 = [𝑔] ∼ → (∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧 → ∃𝑔 ∈ 𝑋 𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)))))
153	92, 152	syl5bi 231	. . 3 ⊢ (𝜑 → (𝑧 ∈ (𝑋 / ∼ ) → (∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧 → ∃𝑔 ∈ 𝑋 𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)))))
154	153	rexlimdv 3012	. 2 ⊢ (𝜑 → (∃𝑧 ∈ (𝑋 / ∼ )∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧 → ∃𝑔 ∈ 𝑋 𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))))
155	90, 154	mpd 15	1 ⊢ (𝜑 → ∃𝑔 ∈ 𝑋 𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108  {cpr 4127   class class class wbr 4583  {copab 4642   ↦ cmpt 4643  ran crn 5039   Fn wfn 5799  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551   Er wer 7626  [cec 7627   / cqs 7628  Fincfn 7841  0cc0 9815   · cmul 9820   − cmin 10145   / cdiv 10563  ℕcn 10897  ℕ₀cn0 11169  ℤcz 11254  ↑cexp 12722  #chash 12979   ∥ cdvds 14821  ℙcprime 15223   pCnt cpc 15379  Basecbs 15695   ↾_s cress 15696  +_gcplusg 15768  0_gc0g 15923  Grpcgrp 17245  inv_gcminusg 17246  -_gcsg 17247  SubGrpcsubg 17411   ~_QG cqg 17413   pGrp cpgp 17769

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  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  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-nel 2783  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-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-disj 4554  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  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-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  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-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-omul 7452  df-er 7629  df-ec 7631  df-qs 7635  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-acn 8651  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-xnn0 11241  df-z 11255  df-uz 11564  df-q 11665  df-rp 11709  df-fz 12198  df-fzo 12335  df-fl 12455  df-mod 12531  df-seq 12664  df-exp 12723  df-fac 12923  df-bc 12952  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-sum 14265  df-dvds 14822  df-gcd 15055  df-prm 15224  df-pc 15380  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-0g 15925  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-submnd 17159  df-grp 17248  df-minusg 17249  df-sbg 17250  df-mulg 17364  df-subg 17414  df-eqg 17416  df-ga 17546  df-od 17771  df-pgp 17773

This theorem is referenced by:  sylow2b  17861