sylow2a

Description: A named lemma of Sylow's second and third theorems. If G is a finite P -group that acts on the finite set Y , then the set Z of all points of Y fixed by every element of G has cardinality equivalent to the cardinality of Y , mod P . (Contributed by Mario Carneiro, 17-Jan-2015)

	Ref	Expression
Hypotheses	sylow2a.x	$⊢ X = {Base}_{G}$
	sylow2a.m	$⊢ φ \to \underset{˙}{\oplus} \in (G GrpAct Y)$
	sylow2a.p	$⊢ φ \to P pGrp G$
	sylow2a.f	$⊢ φ \to X \in Fin$
	sylow2a.y	$⊢ φ \to Y \in Fin$
	sylow2a.z	$⊢ Z = \{u \in Y \| \forall h \in X h \underset{˙}{\oplus} u = u\}$
	sylow2a.r	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| (\{x, y\} \subseteq Y \land \exists g \in X g \underset{˙}{\oplus} x = y)\}$
Assertion	sylow2a	$⊢ φ \to P ∥ (\|Y\| - \|Z\|)$

Proof

Step	Hyp	Ref	Expression
1		sylow2a.x	$⊢ X = {Base}_{G}$
2		sylow2a.m	$⊢ φ \to \underset{˙}{\oplus} \in (G GrpAct Y)$
3		sylow2a.p	$⊢ φ \to P pGrp G$
4		sylow2a.f	$⊢ φ \to X \in Fin$
5		sylow2a.y	$⊢ φ \to Y \in Fin$
6		sylow2a.z	$⊢ Z = \{u \in Y \| \forall h \in X h \underset{˙}{\oplus} u = u\}$
7		sylow2a.r	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| (\{x, y\} \subseteq Y \land \exists g \in X g \underset{˙}{\oplus} x = y)\}$
8	1 2 3 4 5 6 7	sylow2alem2	$⊢ φ \to P ∥ \sum_{z \in (Y / \underset{˙}{\sim}) ∖ 𝒫 Z} \|z\|$
9		inass	$⊢ ((Y / \underset{˙}{\sim}) \cap 𝒫 Z) \cap ((Y / \underset{˙}{\sim}) ∖ 𝒫 Z) = (Y / \underset{˙}{\sim}) \cap (𝒫 Z \cap ((Y / \underset{˙}{\sim}) ∖ 𝒫 Z))$
10		disjdif	$⊢ 𝒫 Z \cap ((Y / \underset{˙}{\sim}) ∖ 𝒫 Z) = \emptyset$
11	10	ineq2i	$⊢ (Y / \underset{˙}{\sim}) \cap (𝒫 Z \cap ((Y / \underset{˙}{\sim}) ∖ 𝒫 Z)) = (Y / \underset{˙}{\sim}) \cap \emptyset$
12		in0	$⊢ (Y / \underset{˙}{\sim}) \cap \emptyset = \emptyset$
13	9 11 12	3eqtri	$⊢ ((Y / \underset{˙}{\sim}) \cap 𝒫 Z) \cap ((Y / \underset{˙}{\sim}) ∖ 𝒫 Z) = \emptyset$
14	13	a1i	$⊢ φ \to ((Y / \underset{˙}{\sim}) \cap 𝒫 Z) \cap ((Y / \underset{˙}{\sim}) ∖ 𝒫 Z) = \emptyset$
15		inundif	$⊢ ((Y / \underset{˙}{\sim}) \cap 𝒫 Z) \cup ((Y / \underset{˙}{\sim}) ∖ 𝒫 Z) = Y / \underset{˙}{\sim}$
16	15	eqcomi	$⊢ Y / \underset{˙}{\sim} = ((Y / \underset{˙}{\sim}) \cap 𝒫 Z) \cup ((Y / \underset{˙}{\sim}) ∖ 𝒫 Z)$
17	16	a1i	$⊢ φ \to Y / \underset{˙}{\sim} = ((Y / \underset{˙}{\sim}) \cap 𝒫 Z) \cup ((Y / \underset{˙}{\sim}) ∖ 𝒫 Z)$
18		pwfi	$⊢ Y \in Fin \leftrightarrow 𝒫 Y \in Fin$
19	5 18	sylib	$⊢ φ \to 𝒫 Y \in Fin$
20	7 1	gaorber	$⊢ \underset{˙}{\oplus} \in (G GrpAct Y) \to \underset{˙}{\sim} Er Y$
21	2 20	syl	$⊢ φ \to \underset{˙}{\sim} Er Y$
22	21	qsss	$⊢ φ \to Y / \underset{˙}{\sim} \subseteq 𝒫 Y$
23	19 22	ssfid	$⊢ φ \to Y / \underset{˙}{\sim} \in Fin$
24	5	adantr	$⊢ (φ \land z \in (Y / \underset{˙}{\sim})) \to Y \in Fin$
25	22	sselda	$⊢ (φ \land z \in (Y / \underset{˙}{\sim})) \to z \in 𝒫 Y$
26	25	elpwid	$⊢ (φ \land z \in (Y / \underset{˙}{\sim})) \to z \subseteq Y$
27	24 26	ssfid	$⊢ (φ \land z \in (Y / \underset{˙}{\sim})) \to z \in Fin$
28		hashcl	$⊢ z \in Fin \to \|z\| \in ℕ_{0}$
29	27 28	syl	$⊢ (φ \land z \in (Y / \underset{˙}{\sim})) \to \|z\| \in ℕ_{0}$
30	29	nn0cnd	$⊢ (φ \land z \in (Y / \underset{˙}{\sim})) \to \|z\| \in ℂ$
31	14 17 23 30	fsumsplit	$⊢ φ \to \sum_{z \in Y / \underset{˙}{\sim}} \|z\| = \sum_{z \in (Y / \underset{˙}{\sim}) \cap 𝒫 Z} \|z\| + \sum_{z \in (Y / \underset{˙}{\sim}) ∖ 𝒫 Z} \|z\|$
32	21 5	qshash	$⊢ φ \to \|Y\| = \sum_{z \in Y / \underset{˙}{\sim}} \|z\|$
33		inss1	$⊢ (Y / \underset{˙}{\sim}) \cap 𝒫 Z \subseteq Y / \underset{˙}{\sim}$
34		ssfi	$⊢ (Y / \underset{˙}{\sim} \in Fin \land (Y / \underset{˙}{\sim}) \cap 𝒫 Z \subseteq Y / \underset{˙}{\sim}) \to (Y / \underset{˙}{\sim}) \cap 𝒫 Z \in Fin$
35	23 33 34	sylancl	$⊢ φ \to (Y / \underset{˙}{\sim}) \cap 𝒫 Z \in Fin$
36		ax-1cn	$⊢ 1 \in ℂ$
37		fsumconst	$⊢ ((Y / \underset{˙}{\sim}) \cap 𝒫 Z \in Fin \land 1 \in ℂ) \to \sum_{z \in (Y / \underset{˙}{\sim}) \cap 𝒫 Z} 1 = \|(Y / \underset{˙}{\sim}) \cap 𝒫 Z\| \cdot 1$
38	35 36 37	sylancl	$⊢ φ \to \sum_{z \in (Y / \underset{˙}{\sim}) \cap 𝒫 Z} 1 = \|(Y / \underset{˙}{\sim}) \cap 𝒫 Z\| \cdot 1$
39		elin	$⊢ z \in ((Y / \underset{˙}{\sim}) \cap 𝒫 Z) \leftrightarrow (z \in (Y / \underset{˙}{\sim}) \land z \in 𝒫 Z)$
40		eqid	$⊢ Y / \underset{˙}{\sim} = Y / \underset{˙}{\sim}$
41		sseq1	$⊢ [w] \underset{˙}{\sim} = z \to ([w] \underset{˙}{\sim} \subseteq Z \leftrightarrow z \subseteq Z)$
42		velpw	$⊢ z \in 𝒫 Z \leftrightarrow z \subseteq Z$
43	41 42	bitr4di	$⊢ [w] \underset{˙}{\sim} = z \to ([w] \underset{˙}{\sim} \subseteq Z \leftrightarrow z \in 𝒫 Z)$
44		breq1	$⊢ [w] \underset{˙}{\sim} = z \to ([w] \underset{˙}{\sim} \approx 1_{𝑜} \leftrightarrow z \approx 1_{𝑜})$
45	43 44	imbi12d	$⊢ [w] \underset{˙}{\sim} = z \to (([w] \underset{˙}{\sim} \subseteq Z \to [w] \underset{˙}{\sim} \approx 1_{𝑜}) \leftrightarrow (z \in 𝒫 Z \to z \approx 1_{𝑜}))$
46	21	adantr	$⊢ (φ \land w \in Y) \to \underset{˙}{\sim} Er Y$
47		simpr	$⊢ (φ \land w \in Y) \to w \in Y$
48	46 47	erref	$⊢ (φ \land w \in Y) \to w \underset{˙}{\sim} w$
49		vex	$⊢ w \in V$
50	49 49	elec	$⊢ w \in [w] \underset{˙}{\sim} \leftrightarrow w \underset{˙}{\sim} w$
51	48 50	sylibr	$⊢ (φ \land w \in Y) \to w \in [w] \underset{˙}{\sim}$
52		ssel	$⊢ [w] \underset{˙}{\sim} \subseteq Z \to (w \in [w] \underset{˙}{\sim} \to w \in Z)$
53	51 52	syl5com	$⊢ (φ \land w \in Y) \to ([w] \underset{˙}{\sim} \subseteq Z \to w \in Z)$
54	1 2 3 4 5 6 7	sylow2alem1	$⊢ (φ \land w \in Z) \to [w] \underset{˙}{\sim} = \{w\}$
55	49	ensn1	$⊢ \{w\} \approx 1_{𝑜}$
56	54 55	eqbrtrdi	$⊢ (φ \land w \in Z) \to [w] \underset{˙}{\sim} \approx 1_{𝑜}$
57	56	ex	$⊢ φ \to (w \in Z \to [w] \underset{˙}{\sim} \approx 1_{𝑜})$
58	57	adantr	$⊢ (φ \land w \in Y) \to (w \in Z \to [w] \underset{˙}{\sim} \approx 1_{𝑜})$
59	53 58	syld	$⊢ (φ \land w \in Y) \to ([w] \underset{˙}{\sim} \subseteq Z \to [w] \underset{˙}{\sim} \approx 1_{𝑜})$
60	40 45 59	ectocld	$⊢ (φ \land z \in (Y / \underset{˙}{\sim})) \to (z \in 𝒫 Z \to z \approx 1_{𝑜})$
61	60	impr	$⊢ (φ \land (z \in (Y / \underset{˙}{\sim}) \land z \in 𝒫 Z)) \to z \approx 1_{𝑜}$
62	39 61	sylan2b	$⊢ (φ \land z \in ((Y / \underset{˙}{\sim}) \cap 𝒫 Z)) \to z \approx 1_{𝑜}$
63		en1b	$⊢ z \approx 1_{𝑜} \leftrightarrow z = \{⋃ z\}$
64	62 63	sylib	$⊢ (φ \land z \in ((Y / \underset{˙}{\sim}) \cap 𝒫 Z)) \to z = \{⋃ z\}$
65	64	fveq2d	$⊢ (φ \land z \in ((Y / \underset{˙}{\sim}) \cap 𝒫 Z)) \to \|z\| = \|\{⋃ z\}\|$
66		vuniex	$⊢ ⋃ z \in V$
67		hashsng	$⊢ ⋃ z \in V \to \|\{⋃ z\}\| = 1$
68	66 67	ax-mp	$⊢ \|\{⋃ z\}\| = 1$
69	65 68	eqtrdi	$⊢ (φ \land z \in ((Y / \underset{˙}{\sim}) \cap 𝒫 Z)) \to \|z\| = 1$
70	69	sumeq2dv	$⊢ φ \to \sum_{z \in (Y / \underset{˙}{\sim}) \cap 𝒫 Z} \|z\| = \sum_{z \in (Y / \underset{˙}{\sim}) \cap 𝒫 Z} 1$
71	6	ssrab3	$⊢ Z \subseteq Y$
72		ssfi	$⊢ (Y \in Fin \land Z \subseteq Y) \to Z \in Fin$
73	5 71 72	sylancl	$⊢ φ \to Z \in Fin$
74		hashcl	$⊢ Z \in Fin \to \|Z\| \in ℕ_{0}$
75	73 74	syl	$⊢ φ \to \|Z\| \in ℕ_{0}$
76	75	nn0cnd	$⊢ φ \to \|Z\| \in ℂ$
77	76	mulridd	$⊢ φ \to \|Z\| \cdot 1 = \|Z\|$
78	6 5	rabexd	$⊢ φ \to Z \in V$
79		eqid	$⊢ (w \in Z ⟼ \{w\}) = (w \in Z ⟼ \{w\})$
80	7	relopabiv	$⊢ Rel \underset{˙}{\sim}$
81		relssdmrn	$⊢ Rel \underset{˙}{\sim} \to \underset{˙}{\sim} \subseteq dom \underset{˙}{\sim} \times ran \underset{˙}{\sim}$
82	80 81	ax-mp	$⊢ \underset{˙}{\sim} \subseteq dom \underset{˙}{\sim} \times ran \underset{˙}{\sim}$
83		erdm	$⊢ \underset{˙}{\sim} Er Y \to dom \underset{˙}{\sim} = Y$
84	21 83	syl	$⊢ φ \to dom \underset{˙}{\sim} = Y$
85	84 5	eqeltrd	$⊢ φ \to dom \underset{˙}{\sim} \in Fin$
86		errn	$⊢ \underset{˙}{\sim} Er Y \to ran \underset{˙}{\sim} = Y$
87	21 86	syl	$⊢ φ \to ran \underset{˙}{\sim} = Y$
88	87 5	eqeltrd	$⊢ φ \to ran \underset{˙}{\sim} \in Fin$
89	85 88	xpexd	$⊢ φ \to dom \underset{˙}{\sim} \times ran \underset{˙}{\sim} \in V$
90		ssexg	$⊢ (\underset{˙}{\sim} \subseteq dom \underset{˙}{\sim} \times ran \underset{˙}{\sim} \land dom \underset{˙}{\sim} \times ran \underset{˙}{\sim} \in V) \to \underset{˙}{\sim} \in V$
91	82 89 90	sylancr	$⊢ φ \to \underset{˙}{\sim} \in V$
92		simpr	$⊢ (φ \land w \in Z) \to w \in Z$
93	71 92	sselid	$⊢ (φ \land w \in Z) \to w \in Y$
94		ecelqsg	$⊢ (\underset{˙}{\sim} \in V \land w \in Y) \to [w] \underset{˙}{\sim} \in (Y / \underset{˙}{\sim})$
95	91 93 94	syl2an2r	$⊢ (φ \land w \in Z) \to [w] \underset{˙}{\sim} \in (Y / \underset{˙}{\sim})$
96	54 95	eqeltrrd	$⊢ (φ \land w \in Z) \to \{w\} \in (Y / \underset{˙}{\sim})$
97		snelpwi	$⊢ w \in Z \to \{w\} \in 𝒫 Z$
98	97	adantl	$⊢ (φ \land w \in Z) \to \{w\} \in 𝒫 Z$
99	96 98	elind	$⊢ (φ \land w \in Z) \to \{w\} \in ((Y / \underset{˙}{\sim}) \cap 𝒫 Z)$
100		simpr	$⊢ (φ \land z \in ((Y / \underset{˙}{\sim}) \cap 𝒫 Z)) \to z \in ((Y / \underset{˙}{\sim}) \cap 𝒫 Z)$
101	100	elin2d	$⊢ (φ \land z \in ((Y / \underset{˙}{\sim}) \cap 𝒫 Z)) \to z \in 𝒫 Z$
102	101	elpwid	$⊢ (φ \land z \in ((Y / \underset{˙}{\sim}) \cap 𝒫 Z)) \to z \subseteq Z$
103	64 102	eqsstrrd	$⊢ (φ \land z \in ((Y / \underset{˙}{\sim}) \cap 𝒫 Z)) \to \{⋃ z\} \subseteq Z$
104	66	snss	$⊢ ⋃ z \in Z \leftrightarrow \{⋃ z\} \subseteq Z$
105	103 104	sylibr	$⊢ (φ \land z \in ((Y / \underset{˙}{\sim}) \cap 𝒫 Z)) \to ⋃ z \in Z$
106		sneq	$⊢ w = ⋃ z \to \{w\} = \{⋃ z\}$
107	106	eqeq2d	$⊢ w = ⋃ z \to (z = \{w\} \leftrightarrow z = \{⋃ z\})$
108	64 107	syl5ibrcom	$⊢ (φ \land z \in ((Y / \underset{˙}{\sim}) \cap 𝒫 Z)) \to (w = ⋃ z \to z = \{w\})$
109	108	adantrl	$⊢ (φ \land (w \in Z \land z \in ((Y / \underset{˙}{\sim}) \cap 𝒫 Z))) \to (w = ⋃ z \to z = \{w\})$
110		unieq	$⊢ z = \{w\} \to ⋃ z = ⋃ \{w\}$
111		unisnv	$⊢ ⋃ \{w\} = w$
112	110 111	eqtr2di	$⊢ z = \{w\} \to w = ⋃ z$
113	109 112	impbid1	$⊢ (φ \land (w \in Z \land z \in ((Y / \underset{˙}{\sim}) \cap 𝒫 Z))) \to (w = ⋃ z \leftrightarrow z = \{w\})$
114	79 99 105 113	f1o2d	$⊢ φ \to (w \in Z ⟼ \{w\}) : Z \underset{1-1 onto}{⟶} (Y / \underset{˙}{\sim}) \cap 𝒫 Z$
115	78 114	hasheqf1od	$⊢ φ \to \|Z\| = \|(Y / \underset{˙}{\sim}) \cap 𝒫 Z\|$
116	115	oveq1d	$⊢ φ \to \|Z\| \cdot 1 = \|(Y / \underset{˙}{\sim}) \cap 𝒫 Z\| \cdot 1$
117	77 116	eqtr3d	$⊢ φ \to \|Z\| = \|(Y / \underset{˙}{\sim}) \cap 𝒫 Z\| \cdot 1$
118	38 70 117	3eqtr4rd	$⊢ φ \to \|Z\| = \sum_{z \in (Y / \underset{˙}{\sim}) \cap 𝒫 Z} \|z\|$
119	118	oveq1d	$⊢ φ \to \|Z\| + \sum_{z \in (Y / \underset{˙}{\sim}) ∖ 𝒫 Z} \|z\| = \sum_{z \in (Y / \underset{˙}{\sim}) \cap 𝒫 Z} \|z\| + \sum_{z \in (Y / \underset{˙}{\sim}) ∖ 𝒫 Z} \|z\|$
120	31 32 119	3eqtr4rd	$⊢ φ \to \|Z\| + \sum_{z \in (Y / \underset{˙}{\sim}) ∖ 𝒫 Z} \|z\| = \|Y\|$
121		hashcl	$⊢ Y \in Fin \to \|Y\| \in ℕ_{0}$
122	5 121	syl	$⊢ φ \to \|Y\| \in ℕ_{0}$
123	122	nn0cnd	$⊢ φ \to \|Y\| \in ℂ$
124		diffi	$⊢ Y / \underset{˙}{\sim} \in Fin \to (Y / \underset{˙}{\sim}) ∖ 𝒫 Z \in Fin$
125	23 124	syl	$⊢ φ \to (Y / \underset{˙}{\sim}) ∖ 𝒫 Z \in Fin$
126		eldifi	$⊢ z \in ((Y / \underset{˙}{\sim}) ∖ 𝒫 Z) \to z \in (Y / \underset{˙}{\sim})$
127	126 30	sylan2	$⊢ (φ \land z \in ((Y / \underset{˙}{\sim}) ∖ 𝒫 Z)) \to \|z\| \in ℂ$
128	125 127	fsumcl	$⊢ φ \to \sum_{z \in (Y / \underset{˙}{\sim}) ∖ 𝒫 Z} \|z\| \in ℂ$
129	123 76 128	subaddd	$⊢ φ \to (\|Y\| - \|Z\| = \sum_{z \in (Y / \underset{˙}{\sim}) ∖ 𝒫 Z} \|z\| \leftrightarrow \|Z\| + \sum_{z \in (Y / \underset{˙}{\sim}) ∖ 𝒫 Z} \|z\| = \|Y\|)$
130	120 129	mpbird	$⊢ φ \to \|Y\| - \|Z\| = \sum_{z \in (Y / \underset{˙}{\sim}) ∖ 𝒫 Z} \|z\|$
131	8 130	breqtrrd	$⊢ φ \to P ∥ (\|Y\| - \|Z\|)$

Metamath Proof Explorer

Theorem sylow2a

Proof