Metamath Proof Explorer


Theorem sylow2

Description: Sylow's second theorem. See also sylow2b for the "hard" part of the proof. Any two Sylow P -subgroups are conjugate to one another, and hence the same size, namely P ^ ( P pCnt | X | ) (see fislw ). This is part of Metamath 100 proof #72. (Contributed by Mario Carneiro, 18-Jan-2015)

Ref Expression
Hypotheses sylow2.x X = Base G
sylow2.f φ X Fin
sylow2.h φ H P pSyl G
sylow2.k φ K P pSyl G
sylow2.a + ˙ = + G
sylow2.d - ˙ = - G
Assertion sylow2 φ g X H = ran x K g + ˙ x - ˙ g

Proof

Step Hyp Ref Expression
1 sylow2.x X = Base G
2 sylow2.f φ X Fin
3 sylow2.h φ H P pSyl G
4 sylow2.k φ K P pSyl G
5 sylow2.a + ˙ = + G
6 sylow2.d - ˙ = - G
7 2 adantr φ g X H ran x K g + ˙ x - ˙ g X Fin
8 slwsubg K P pSyl G K SubGrp G
9 4 8 syl φ K SubGrp G
10 simprl φ g X H ran x K g + ˙ x - ˙ g g X
11 eqid x K g + ˙ x - ˙ g = x K g + ˙ x - ˙ g
12 1 5 6 11 conjsubg K SubGrp G g X ran x K g + ˙ x - ˙ g SubGrp G
13 9 10 12 syl2an2r φ g X H ran x K g + ˙ x - ˙ g ran x K g + ˙ x - ˙ g SubGrp G
14 1 subgss ran x K g + ˙ x - ˙ g SubGrp G ran x K g + ˙ x - ˙ g X
15 13 14 syl φ g X H ran x K g + ˙ x - ˙ g ran x K g + ˙ x - ˙ g X
16 7 15 ssfid φ g X H ran x K g + ˙ x - ˙ g ran x K g + ˙ x - ˙ g Fin
17 simprr φ g X H ran x K g + ˙ x - ˙ g H ran x K g + ˙ x - ˙ g
18 1 2 3 slwhash φ H = P P pCnt X
19 1 2 4 slwhash φ K = P P pCnt X
20 18 19 eqtr4d φ H = K
21 slwsubg H P pSyl G H SubGrp G
22 3 21 syl φ H SubGrp G
23 1 subgss H SubGrp G H X
24 22 23 syl φ H X
25 2 24 ssfid φ H Fin
26 1 subgss K SubGrp G K X
27 9 26 syl φ K X
28 2 27 ssfid φ K Fin
29 hashen H Fin K Fin H = K H K
30 25 28 29 syl2anc φ H = K H K
31 20 30 mpbid φ H K
32 1 5 6 11 conjsubgen K SubGrp G g X K ran x K g + ˙ x - ˙ g
33 9 10 32 syl2an2r φ g X H ran x K g + ˙ x - ˙ g K ran x K g + ˙ x - ˙ g
34 entr H K K ran x K g + ˙ x - ˙ g H ran x K g + ˙ x - ˙ g
35 31 33 34 syl2an2r φ g X H ran x K g + ˙ x - ˙ g H ran x K g + ˙ x - ˙ g
36 fisseneq ran x K g + ˙ x - ˙ g Fin H ran x K g + ˙ x - ˙ g H ran x K g + ˙ x - ˙ g H = ran x K g + ˙ x - ˙ g
37 16 17 35 36 syl3anc φ g X H ran x K g + ˙ x - ˙ g H = ran x K g + ˙ x - ˙ g
38 eqid G 𝑠 H = G 𝑠 H
39 38 slwpgp H P pSyl G P pGrp G 𝑠 H
40 3 39 syl φ P pGrp G 𝑠 H
41 1 2 22 9 5 40 19 6 sylow2b φ g X H ran x K g + ˙ x - ˙ g
42 37 41 reximddv φ g X H = ran x K g + ˙ x - ˙ g