sylow2blem3

Description: Sylow's second theorem. Putting together the results of sylow2a and the orbit-stabilizer theorem to show that P 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 g e. X with h g K = g K for all h e. H . This implies that invg ( g ) h g e. K , so h is in the conjugated subgroup g K invg ( g ) . (Contributed by Mario Carneiro, 18-Jan-2015)

	Ref	Expression
Hypotheses	sylow2b.x	$⊢ X = {Base}_{G}$
	sylow2b.xf	$⊢ φ \to X \in Fin$
	sylow2b.h	$⊢ φ \to H \in SubGrp (G)$
	sylow2b.k	$⊢ φ \to K \in SubGrp (G)$
	sylow2b.a	$⊢ \underset{˙}{+} = +_{G}$
	sylow2b.r	$⊢ \underset{˙}{\sim} = G ~_{QG} K$
	sylow2b.m	$⊢ \underset{˙}{\cdot} = (x \in H, y \in (X / \underset{˙}{\sim}) ⟼ ran (z \in y ⟼ x \underset{˙}{+} z))$
	sylow2blem3.hp	$⊢ φ \to P pGrp (G ↾_{𝑠} H)$
	sylow2blem3.kn	$⊢ φ \to \|K\| = P^{P pCnt \|X\|}$
	sylow2blem3.d	$⊢ \underset{˙}{-} = -_{G}$
Assertion	sylow2blem3	$⊢ φ \to \exists g \in X H \subseteq ran (x \in K ⟼ (g \underset{˙}{+} x) \underset{˙}{-} g)$

Proof

Step	Hyp	Ref	Expression
1		sylow2b.x	$⊢ X = {Base}_{G}$
2		sylow2b.xf	$⊢ φ \to X \in Fin$
3		sylow2b.h	$⊢ φ \to H \in SubGrp (G)$
4		sylow2b.k	$⊢ φ \to K \in SubGrp (G)$
5		sylow2b.a	$⊢ \underset{˙}{+} = +_{G}$
6		sylow2b.r	$⊢ \underset{˙}{\sim} = G ~_{QG} K$
7		sylow2b.m	$⊢ \underset{˙}{\cdot} = (x \in H, y \in (X / \underset{˙}{\sim}) ⟼ ran (z \in y ⟼ x \underset{˙}{+} z))$
8		sylow2blem3.hp	$⊢ φ \to P pGrp (G ↾_{𝑠} H)$
9		sylow2blem3.kn	$⊢ φ \to \|K\| = P^{P pCnt \|X\|}$
10		sylow2blem3.d	$⊢ \underset{˙}{-} = -_{G}$
11		pgpprm	$⊢ P pGrp (G ↾_{𝑠} H) \to P \in ℙ$
12	8 11	syl	$⊢ φ \to P \in ℙ$
13		subgrcl	$⊢ H \in SubGrp (G) \to G \in Grp$
14	3 13	syl	$⊢ φ \to G \in Grp$
15	1	grpbn0	$⊢ G \in Grp \to X \neq \emptyset$
16	14 15	syl	$⊢ φ \to X \neq \emptyset$
17		hashnncl	$⊢ X \in Fin \to (\|X\| \in ℕ \leftrightarrow X \neq \emptyset)$
18	2 17	syl	$⊢ φ \to (\|X\| \in ℕ \leftrightarrow X \neq \emptyset)$
19	16 18	mpbird	$⊢ φ \to \|X\| \in ℕ$
20		pcndvds2	$⊢ (P \in ℙ \land \|X\| \in ℕ) \to \neg P ∥ (\frac{\|X\|}{P^{P pCnt \|X\|}})$
21	12 19 20	syl2anc	$⊢ φ \to \neg P ∥ (\frac{\|X\|}{P^{P pCnt \|X\|}})$
22	1 6 4 2	lagsubg2	$⊢ φ \to \|X\| = \|X / \underset{˙}{\sim}\| \|K\|$
23	22	oveq1d	$⊢ φ \to \frac{\|X\|}{\|K\|} = \frac{\|X / \underset{˙}{\sim}\| \|K\|}{\|K\|}$
24	9	oveq2d	$⊢ φ \to \frac{\|X\|}{\|K\|} = \frac{\|X\|}{P^{P pCnt \|X\|}}$
25		pwfi	$⊢ X \in Fin \leftrightarrow 𝒫 X \in Fin$
26	2 25	sylib	$⊢ φ \to 𝒫 X \in Fin$
27	1 6	eqger	$⊢ K \in SubGrp (G) \to \underset{˙}{\sim} Er X$
28	4 27	syl	$⊢ φ \to \underset{˙}{\sim} Er X$
29	28	qsss	$⊢ φ \to X / \underset{˙}{\sim} \subseteq 𝒫 X$
30	26 29	ssfid	$⊢ φ \to X / \underset{˙}{\sim} \in Fin$
31		hashcl	$⊢ X / \underset{˙}{\sim} \in Fin \to \|X / \underset{˙}{\sim}\| \in ℕ_{0}$
32	30 31	syl	$⊢ φ \to \|X / \underset{˙}{\sim}\| \in ℕ_{0}$
33	32	nn0cnd	$⊢ φ \to \|X / \underset{˙}{\sim}\| \in ℂ$
34		eqid	$⊢ 0_{G} = 0_{G}$
35	34	subg0cl	$⊢ K \in SubGrp (G) \to 0_{G} \in K$
36	4 35	syl	$⊢ φ \to 0_{G} \in K$
37	36	ne0d	$⊢ φ \to K \neq \emptyset$
38	1	subgss	$⊢ K \in SubGrp (G) \to K \subseteq X$
39	4 38	syl	$⊢ φ \to K \subseteq X$
40	2 39	ssfid	$⊢ φ \to K \in Fin$
41		hashnncl	$⊢ K \in Fin \to (\|K\| \in ℕ \leftrightarrow K \neq \emptyset)$
42	40 41	syl	$⊢ φ \to (\|K\| \in ℕ \leftrightarrow K \neq \emptyset)$
43	37 42	mpbird	$⊢ φ \to \|K\| \in ℕ$
44	43	nncnd	$⊢ φ \to \|K\| \in ℂ$
45	43	nnne0d	$⊢ φ \to \|K\| \neq 0$
46	33 44 45	divcan4d	$⊢ φ \to \frac{\|X / \underset{˙}{\sim}\| \|K\|}{\|K\|} = \|X / \underset{˙}{\sim}\|$
47	23 24 46	3eqtr3d	$⊢ φ \to \frac{\|X\|}{P^{P pCnt \|X\|}} = \|X / \underset{˙}{\sim}\|$
48	47	breq2d	$⊢ φ \to (P ∥ (\frac{\|X\|}{P^{P pCnt \|X\|}}) \leftrightarrow P ∥ \|X / \underset{˙}{\sim}\|)$
49	21 48	mtbid	$⊢ φ \to \neg P ∥ \|X / \underset{˙}{\sim}\|$
50		prmz	$⊢ P \in ℙ \to P \in ℤ$
51	12 50	syl	$⊢ φ \to P \in ℤ$
52	32	nn0zd	$⊢ φ \to \|X / \underset{˙}{\sim}\| \in ℤ$
53		ssrab2	$⊢ \{z \in (X / \underset{˙}{\sim}) \| \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z\} \subseteq X / \underset{˙}{\sim}$
54		ssfi	$⊢ (X / \underset{˙}{\sim} \in Fin \land \{z \in (X / \underset{˙}{\sim}) \| \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z\} \subseteq X / \underset{˙}{\sim}) \to \{z \in (X / \underset{˙}{\sim}) \| \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z\} \in Fin$
55	30 53 54	sylancl	$⊢ φ \to \{z \in (X / \underset{˙}{\sim}) \| \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z\} \in Fin$
56		hashcl	$⊢ \{z \in (X / \underset{˙}{\sim}) \| \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z\} \in Fin \to \|\{z \in (X / \underset{˙}{\sim}) \| \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z\}\| \in ℕ_{0}$
57	55 56	syl	$⊢ φ \to \|\{z \in (X / \underset{˙}{\sim}) \| \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z\}\| \in ℕ_{0}$
58	57	nn0zd	$⊢ φ \to \|\{z \in (X / \underset{˙}{\sim}) \| \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z\}\| \in ℤ$
59		eqid	$⊢ {Base}_{(G ↾_{𝑠} H)} = {Base}_{(G ↾_{𝑠} H)}$
60	1 2 3 4 5 6 7	sylow2blem2	$⊢ φ \to \underset{˙}{\cdot} \in ((G ↾_{𝑠} H) GrpAct (X / \underset{˙}{\sim}))$
61		eqid	$⊢ G ↾_{𝑠} H = G ↾_{𝑠} H$
62	61	subgbas	$⊢ H \in SubGrp (G) \to H = {Base}_{(G ↾_{𝑠} H)}$
63	3 62	syl	$⊢ φ \to H = {Base}_{(G ↾_{𝑠} H)}$
64	1	subgss	$⊢ H \in SubGrp (G) \to H \subseteq X$
65	3 64	syl	$⊢ φ \to H \subseteq X$
66	2 65	ssfid	$⊢ φ \to H \in Fin$
67	63 66	eqeltrrd	$⊢ φ \to {Base}_{(G ↾_{𝑠} H)} \in Fin$
68		eqid	$⊢ \{z \in (X / \underset{˙}{\sim}) \| \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z\} = \{z \in (X / \underset{˙}{\sim}) \| \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z\}$
69		eqid	$⊢ \{⟨x, y⟩ \| (\{x, y\} \subseteq X / \underset{˙}{\sim} \land \exists g \in {Base}_{(G ↾_{𝑠} H)} g \underset{˙}{\cdot} x = y)\} = \{⟨x, y⟩ \| (\{x, y\} \subseteq X / \underset{˙}{\sim} \land \exists g \in {Base}_{(G ↾_{𝑠} H)} g \underset{˙}{\cdot} x = y)\}$
70	59 60 8 67 30 68 69	sylow2a	$⊢ φ \to P ∥ (\|X / \underset{˙}{\sim}\| - \|\{z \in (X / \underset{˙}{\sim}) \| \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z\}\|)$
71		dvdssub2	$⊢ ((P \in ℤ \land \|X / \underset{˙}{\sim}\| \in ℤ \land \|\{z \in (X / \underset{˙}{\sim}) \| \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z\}\| \in ℤ) \land P ∥ (\|X / \underset{˙}{\sim}\| - \|\{z \in (X / \underset{˙}{\sim}) \| \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z\}\|)) \to (P ∥ \|X / \underset{˙}{\sim}\| \leftrightarrow P ∥ \|\{z \in (X / \underset{˙}{\sim}) \| \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z\}\|)$
72	51 52 58 70 71	syl31anc	$⊢ φ \to (P ∥ \|X / \underset{˙}{\sim}\| \leftrightarrow P ∥ \|\{z \in (X / \underset{˙}{\sim}) \| \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z\}\|)$
73	49 72	mtbid	$⊢ φ \to \neg P ∥ \|\{z \in (X / \underset{˙}{\sim}) \| \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z\}\|$
74		hasheq0	$⊢ \{z \in (X / \underset{˙}{\sim}) \| \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z\} \in Fin \to (\|\{z \in (X / \underset{˙}{\sim}) \| \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z\}\| = 0 \leftrightarrow \{z \in (X / \underset{˙}{\sim}) \| \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z\} = \emptyset)$
75	55 74	syl	$⊢ φ \to (\|\{z \in (X / \underset{˙}{\sim}) \| \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z\}\| = 0 \leftrightarrow \{z \in (X / \underset{˙}{\sim}) \| \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z\} = \emptyset)$
76		dvds0	$⊢ P \in ℤ \to P ∥ 0$
77	51 76	syl	$⊢ φ \to P ∥ 0$
78		breq2	$⊢ \|\{z \in (X / \underset{˙}{\sim}) \| \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z\}\| = 0 \to (P ∥ \|\{z \in (X / \underset{˙}{\sim}) \| \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z\}\| \leftrightarrow P ∥ 0)$
79	77 78	syl5ibrcom	$⊢ φ \to (\|\{z \in (X / \underset{˙}{\sim}) \| \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z\}\| = 0 \to P ∥ \|\{z \in (X / \underset{˙}{\sim}) \| \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z\}\|)$
80	75 79	sylbird	$⊢ φ \to (\{z \in (X / \underset{˙}{\sim}) \| \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z\} = \emptyset \to P ∥ \|\{z \in (X / \underset{˙}{\sim}) \| \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z\}\|)$
81	80	necon3bd	$⊢ φ \to (\neg P ∥ \|\{z \in (X / \underset{˙}{\sim}) \| \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z\}\| \to \{z \in (X / \underset{˙}{\sim}) \| \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z\} \neq \emptyset)$
82	73 81	mpd	$⊢ φ \to \{z \in (X / \underset{˙}{\sim}) \| \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z\} \neq \emptyset$
83		rabn0	$⊢ \{z \in (X / \underset{˙}{\sim}) \| \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z\} \neq \emptyset \leftrightarrow \exists z \in (X / \underset{˙}{\sim}) \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z$
84	82 83	sylib	$⊢ φ \to \exists z \in (X / \underset{˙}{\sim}) \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z$
85	63	raleqdv	$⊢ φ \to (\forall u \in H u \underset{˙}{\cdot} z = z \leftrightarrow \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z)$
86	85	rexbidv	$⊢ φ \to (\exists z \in (X / \underset{˙}{\sim}) \forall u \in H u \underset{˙}{\cdot} z = z \leftrightarrow \exists z \in (X / \underset{˙}{\sim}) \forall u \in {Base}_{(G ↾_{𝑠} H)} u \underset{˙}{\cdot} z = z)$
87	84 86	mpbird	$⊢ φ \to \exists z \in (X / \underset{˙}{\sim}) \forall u \in H u \underset{˙}{\cdot} z = z$
88		vex	$⊢ z \in V$
89	88	elqs	$⊢ z \in (X / \underset{˙}{\sim}) \leftrightarrow \exists g \in X z = [g] \underset{˙}{\sim}$
90		simplrr	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to z = [g] \underset{˙}{\sim}$
91	90	oveq2d	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to u \underset{˙}{\cdot} z = u \underset{˙}{\cdot} [g] \underset{˙}{\sim}$
92		simprr	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to u \underset{˙}{\cdot} z = z$
93		simpll	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to φ$
94		simprl	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to u \in H$
95		simplrl	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to g \in X$
96	1 2 3 4 5 6 7	sylow2blem1	$⊢ (φ \land u \in H \land g \in X) \to u \underset{˙}{\cdot} [g] \underset{˙}{\sim} = [(u \underset{˙}{+} g)] \underset{˙}{\sim}$
97	93 94 95 96	syl3anc	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to u \underset{˙}{\cdot} [g] \underset{˙}{\sim} = [(u \underset{˙}{+} g)] \underset{˙}{\sim}$
98	91 92 97	3eqtr3d	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to z = [(u \underset{˙}{+} g)] \underset{˙}{\sim}$
99	90 98	eqtr3d	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to [g] \underset{˙}{\sim} = [(u \underset{˙}{+} g)] \underset{˙}{\sim}$
100	28	ad2antrr	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to \underset{˙}{\sim} Er X$
101	100 95	erth	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to (g \underset{˙}{\sim} (u \underset{˙}{+} g) \leftrightarrow [g] \underset{˙}{\sim} = [(u \underset{˙}{+} g)] \underset{˙}{\sim})$
102	99 101	mpbird	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to g \underset{˙}{\sim} (u \underset{˙}{+} g)$
103	14	ad2antrr	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to G \in Grp$
104	39	ad2antrr	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to K \subseteq X$
105		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
106	1 105 5 6	eqgval	$⊢ (G \in Grp \land K \subseteq X) \to (g \underset{˙}{\sim} (u \underset{˙}{+} g) \leftrightarrow (g \in X \land u \underset{˙}{+} g \in X \land {inv}_{g} (G) (g) \underset{˙}{+} (u \underset{˙}{+} g) \in K))$
107	103 104 106	syl2anc	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to (g \underset{˙}{\sim} (u \underset{˙}{+} g) \leftrightarrow (g \in X \land u \underset{˙}{+} g \in X \land {inv}_{g} (G) (g) \underset{˙}{+} (u \underset{˙}{+} g) \in K))$
108	102 107	mpbid	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to (g \in X \land u \underset{˙}{+} g \in X \land {inv}_{g} (G) (g) \underset{˙}{+} (u \underset{˙}{+} g) \in K)$
109	108	simp3d	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to {inv}_{g} (G) (g) \underset{˙}{+} (u \underset{˙}{+} g) \in K$
110		oveq2	$⊢ x = {inv}_{g} (G) (g) \underset{˙}{+} (u \underset{˙}{+} g) \to g \underset{˙}{+} x = g \underset{˙}{+} ({inv}_{g} (G) (g) \underset{˙}{+} (u \underset{˙}{+} g))$
111	110	oveq1d	$⊢ x = {inv}_{g} (G) (g) \underset{˙}{+} (u \underset{˙}{+} g) \to (g \underset{˙}{+} x) \underset{˙}{-} g = (g \underset{˙}{+} ({inv}_{g} (G) (g) \underset{˙}{+} (u \underset{˙}{+} g))) \underset{˙}{-} g$
112		eqid	$⊢ (x \in K ⟼ (g \underset{˙}{+} x) \underset{˙}{-} g) = (x \in K ⟼ (g \underset{˙}{+} x) \underset{˙}{-} g)$
113		ovex	$⊢ (g \underset{˙}{+} ({inv}_{g} (G) (g) \underset{˙}{+} (u \underset{˙}{+} g))) \underset{˙}{-} g \in V$
114	111 112 113	fvmpt	$⊢ {inv}_{g} (G) (g) \underset{˙}{+} (u \underset{˙}{+} g) \in K \to (x \in K ⟼ (g \underset{˙}{+} x) \underset{˙}{-} g) ({inv}_{g} (G) (g) \underset{˙}{+} (u \underset{˙}{+} g)) = (g \underset{˙}{+} ({inv}_{g} (G) (g) \underset{˙}{+} (u \underset{˙}{+} g))) \underset{˙}{-} g$
115	109 114	syl	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to (x \in K ⟼ (g \underset{˙}{+} x) \underset{˙}{-} g) ({inv}_{g} (G) (g) \underset{˙}{+} (u \underset{˙}{+} g)) = (g \underset{˙}{+} ({inv}_{g} (G) (g) \underset{˙}{+} (u \underset{˙}{+} g))) \underset{˙}{-} g$
116	1 5 34 105	grprinv	$⊢ (G \in Grp \land g \in X) \to g \underset{˙}{+} {inv}_{g} (G) (g) = 0_{G}$
117	103 95 116	syl2anc	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to g \underset{˙}{+} {inv}_{g} (G) (g) = 0_{G}$
118	117	oveq1d	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to (g \underset{˙}{+} {inv}_{g} (G) (g)) \underset{˙}{+} (u \underset{˙}{+} g) = 0_{G} \underset{˙}{+} (u \underset{˙}{+} g)$
119	1 105	grpinvcl	$⊢ (G \in Grp \land g \in X) \to {inv}_{g} (G) (g) \in X$
120	103 95 119	syl2anc	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to {inv}_{g} (G) (g) \in X$
121	65	ad2antrr	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to H \subseteq X$
122	121 94	sseldd	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to u \in X$
123	1 5	grpcl	$⊢ (G \in Grp \land u \in X \land g \in X) \to u \underset{˙}{+} g \in X$
124	103 122 95 123	syl3anc	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to u \underset{˙}{+} g \in X$
125	1 5	grpass	$⊢ (G \in Grp \land (g \in X \land {inv}_{g} (G) (g) \in X \land u \underset{˙}{+} g \in X)) \to (g \underset{˙}{+} {inv}_{g} (G) (g)) \underset{˙}{+} (u \underset{˙}{+} g) = g \underset{˙}{+} ({inv}_{g} (G) (g) \underset{˙}{+} (u \underset{˙}{+} g))$
126	103 95 120 124 125	syl13anc	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to (g \underset{˙}{+} {inv}_{g} (G) (g)) \underset{˙}{+} (u \underset{˙}{+} g) = g \underset{˙}{+} ({inv}_{g} (G) (g) \underset{˙}{+} (u \underset{˙}{+} g))$
127	1 5 34	grplid	$⊢ (G \in Grp \land u \underset{˙}{+} g \in X) \to 0_{G} \underset{˙}{+} (u \underset{˙}{+} g) = u \underset{˙}{+} g$
128	103 124 127	syl2anc	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to 0_{G} \underset{˙}{+} (u \underset{˙}{+} g) = u \underset{˙}{+} g$
129	118 126 128	3eqtr3d	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to g \underset{˙}{+} ({inv}_{g} (G) (g) \underset{˙}{+} (u \underset{˙}{+} g)) = u \underset{˙}{+} g$
130	129	oveq1d	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to (g \underset{˙}{+} ({inv}_{g} (G) (g) \underset{˙}{+} (u \underset{˙}{+} g))) \underset{˙}{-} g = (u \underset{˙}{+} g) \underset{˙}{-} g$
131	1 5 10	grppncan	$⊢ (G \in Grp \land u \in X \land g \in X) \to (u \underset{˙}{+} g) \underset{˙}{-} g = u$
132	103 122 95 131	syl3anc	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to (u \underset{˙}{+} g) \underset{˙}{-} g = u$
133	115 130 132	3eqtrd	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to (x \in K ⟼ (g \underset{˙}{+} x) \underset{˙}{-} g) ({inv}_{g} (G) (g) \underset{˙}{+} (u \underset{˙}{+} g)) = u$
134		ovex	$⊢ (g \underset{˙}{+} x) \underset{˙}{-} g \in V$
135	134 112	fnmpti	$⊢ (x \in K ⟼ (g \underset{˙}{+} x) \underset{˙}{-} g) Fn K$
136		fnfvelrn	$⊢ ((x \in K ⟼ (g \underset{˙}{+} x) \underset{˙}{-} g) Fn K \land {inv}_{g} (G) (g) \underset{˙}{+} (u \underset{˙}{+} g) \in K) \to (x \in K ⟼ (g \underset{˙}{+} x) \underset{˙}{-} g) ({inv}_{g} (G) (g) \underset{˙}{+} (u \underset{˙}{+} g)) \in ran (x \in K ⟼ (g \underset{˙}{+} x) \underset{˙}{-} g)$
137	135 109 136	sylancr	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to (x \in K ⟼ (g \underset{˙}{+} x) \underset{˙}{-} g) ({inv}_{g} (G) (g) \underset{˙}{+} (u \underset{˙}{+} g)) \in ran (x \in K ⟼ (g \underset{˙}{+} x) \underset{˙}{-} g)$
138	133 137	eqeltrrd	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land (u \in H \land u \underset{˙}{\cdot} z = z)) \to u \in ran (x \in K ⟼ (g \underset{˙}{+} x) \underset{˙}{-} g)$
139	138	expr	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land u \in H) \to (u \underset{˙}{\cdot} z = z \to u \in ran (x \in K ⟼ (g \underset{˙}{+} x) \underset{˙}{-} g))$
140	139	ralimdva	$⊢ (φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \to (\forall u \in H u \underset{˙}{\cdot} z = z \to \forall u \in H u \in ran (x \in K ⟼ (g \underset{˙}{+} x) \underset{˙}{-} g))$
141	140	imp	$⊢ ((φ \land (g \in X \land z = [g] \underset{˙}{\sim})) \land \forall u \in H u \underset{˙}{\cdot} z = z) \to \forall u \in H u \in ran (x \in K ⟼ (g \underset{˙}{+} x) \underset{˙}{-} g)$
142	141	an32s	$⊢ ((φ \land \forall u \in H u \underset{˙}{\cdot} z = z) \land (g \in X \land z = [g] \underset{˙}{\sim})) \to \forall u \in H u \in ran (x \in K ⟼ (g \underset{˙}{+} x) \underset{˙}{-} g)$
143		dfss3	$⊢ H \subseteq ran (x \in K ⟼ (g \underset{˙}{+} x) \underset{˙}{-} g) \leftrightarrow \forall u \in H u \in ran (x \in K ⟼ (g \underset{˙}{+} x) \underset{˙}{-} g)$
144	142 143	sylibr	$⊢ ((φ \land \forall u \in H u \underset{˙}{\cdot} z = z) \land (g \in X \land z = [g] \underset{˙}{\sim})) \to H \subseteq ran (x \in K ⟼ (g \underset{˙}{+} x) \underset{˙}{-} g)$
145	144	expr	$⊢ ((φ \land \forall u \in H u \underset{˙}{\cdot} z = z) \land g \in X) \to (z = [g] \underset{˙}{\sim} \to H \subseteq ran (x \in K ⟼ (g \underset{˙}{+} x) \underset{˙}{-} g))$
146	145	reximdva	$⊢ (φ \land \forall u \in H u \underset{˙}{\cdot} z = z) \to (\exists g \in X z = [g] \underset{˙}{\sim} \to \exists g \in X H \subseteq ran (x \in K ⟼ (g \underset{˙}{+} x) \underset{˙}{-} g))$
147	146	ex	$⊢ φ \to (\forall u \in H u \underset{˙}{\cdot} z = z \to (\exists g \in X z = [g] \underset{˙}{\sim} \to \exists g \in X H \subseteq ran (x \in K ⟼ (g \underset{˙}{+} x) \underset{˙}{-} g)))$
148	147	com23	$⊢ φ \to (\exists g \in X z = [g] \underset{˙}{\sim} \to (\forall u \in H u \underset{˙}{\cdot} z = z \to \exists g \in X H \subseteq ran (x \in K ⟼ (g \underset{˙}{+} x) \underset{˙}{-} g)))$
149	89 148	syl5bi	$⊢ φ \to (z \in (X / \underset{˙}{\sim}) \to (\forall u \in H u \underset{˙}{\cdot} z = z \to \exists g \in X H \subseteq ran (x \in K ⟼ (g \underset{˙}{+} x) \underset{˙}{-} g)))$
150	149	rexlimdv	$⊢ φ \to (\exists z \in (X / \underset{˙}{\sim}) \forall u \in H u \underset{˙}{\cdot} z = z \to \exists g \in X H \subseteq ran (x \in K ⟼ (g \underset{˙}{+} x) \underset{˙}{-} g))$
151	87 150	mpd	$⊢ φ \to \exists g \in X H \subseteq ran (x \in K ⟼ (g \underset{˙}{+} x) \underset{˙}{-} g)$

Metamath Proof Explorer

Theorem sylow2blem3

Proof