Metamath Proof Explorer


Theorem pgpssslw

Description: Every P -subgroup is contained in a Sylow P -subgroup. (Contributed by Mario Carneiro, 16-Jan-2015)

Ref Expression
Hypotheses pgpssslw.1 X = Base G
pgpssslw.2 S = G 𝑠 H
pgpssslw.3 F = x y SubGrp G | P pGrp G 𝑠 y H y x
Assertion pgpssslw H SubGrp G X Fin P pGrp S k P pSyl G H k

Proof

Step Hyp Ref Expression
1 pgpssslw.1 X = Base G
2 pgpssslw.2 S = G 𝑠 H
3 pgpssslw.3 F = x y SubGrp G | P pGrp G 𝑠 y H y x
4 simp2 H SubGrp G X Fin P pGrp S X Fin
5 elrabi x y SubGrp G | P pGrp G 𝑠 y H y x SubGrp G
6 1 subgss x SubGrp G x X
7 5 6 syl x y SubGrp G | P pGrp G 𝑠 y H y x X
8 ssfi X Fin x X x Fin
9 4 7 8 syl2an H SubGrp G X Fin P pGrp S x y SubGrp G | P pGrp G 𝑠 y H y x Fin
10 hashcl x Fin x 0
11 9 10 syl H SubGrp G X Fin P pGrp S x y SubGrp G | P pGrp G 𝑠 y H y x 0
12 11 nn0zd H SubGrp G X Fin P pGrp S x y SubGrp G | P pGrp G 𝑠 y H y x
13 12 3 fmptd H SubGrp G X Fin P pGrp S F : y SubGrp G | P pGrp G 𝑠 y H y
14 13 frnd H SubGrp G X Fin P pGrp S ran F
15 fvex x V
16 15 3 fnmpti F Fn y SubGrp G | P pGrp G 𝑠 y H y
17 eqimss2 y = H H y
18 17 biantrud y = H P pGrp G 𝑠 y P pGrp G 𝑠 y H y
19 oveq2 y = H G 𝑠 y = G 𝑠 H
20 19 2 eqtr4di y = H G 𝑠 y = S
21 20 breq2d y = H P pGrp G 𝑠 y P pGrp S
22 18 21 bitr3d y = H P pGrp G 𝑠 y H y P pGrp S
23 simp1 H SubGrp G X Fin P pGrp S H SubGrp G
24 simp3 H SubGrp G X Fin P pGrp S P pGrp S
25 22 23 24 elrabd H SubGrp G X Fin P pGrp S H y SubGrp G | P pGrp G 𝑠 y H y
26 fnfvelrn F Fn y SubGrp G | P pGrp G 𝑠 y H y H y SubGrp G | P pGrp G 𝑠 y H y F H ran F
27 16 25 26 sylancr H SubGrp G X Fin P pGrp S F H ran F
28 27 ne0d H SubGrp G X Fin P pGrp S ran F
29 hashcl X Fin X 0
30 4 29 syl H SubGrp G X Fin P pGrp S X 0
31 30 nn0red H SubGrp G X Fin P pGrp S X
32 fveq2 x = m x = m
33 fvex m V
34 32 3 33 fvmpt m y SubGrp G | P pGrp G 𝑠 y H y F m = m
35 34 adantl H SubGrp G X Fin P pGrp S m y SubGrp G | P pGrp G 𝑠 y H y F m = m
36 oveq2 y = m G 𝑠 y = G 𝑠 m
37 36 breq2d y = m P pGrp G 𝑠 y P pGrp G 𝑠 m
38 sseq2 y = m H y H m
39 37 38 anbi12d y = m P pGrp G 𝑠 y H y P pGrp G 𝑠 m H m
40 39 elrab m y SubGrp G | P pGrp G 𝑠 y H y m SubGrp G P pGrp G 𝑠 m H m
41 4 adantr H SubGrp G X Fin P pGrp S m SubGrp G P pGrp G 𝑠 m H m X Fin
42 1 subgss m SubGrp G m X
43 42 ad2antrl H SubGrp G X Fin P pGrp S m SubGrp G P pGrp G 𝑠 m H m m X
44 ssdomg X Fin m X m X
45 41 43 44 sylc H SubGrp G X Fin P pGrp S m SubGrp G P pGrp G 𝑠 m H m m X
46 41 43 ssfid H SubGrp G X Fin P pGrp S m SubGrp G P pGrp G 𝑠 m H m m Fin
47 hashdom m Fin X Fin m X m X
48 46 41 47 syl2anc H SubGrp G X Fin P pGrp S m SubGrp G P pGrp G 𝑠 m H m m X m X
49 45 48 mpbird H SubGrp G X Fin P pGrp S m SubGrp G P pGrp G 𝑠 m H m m X
50 40 49 sylan2b H SubGrp G X Fin P pGrp S m y SubGrp G | P pGrp G 𝑠 y H y m X
51 35 50 eqbrtrd H SubGrp G X Fin P pGrp S m y SubGrp G | P pGrp G 𝑠 y H y F m X
52 51 ralrimiva H SubGrp G X Fin P pGrp S m y SubGrp G | P pGrp G 𝑠 y H y F m X
53 breq1 w = F m w X F m X
54 53 ralrn F Fn y SubGrp G | P pGrp G 𝑠 y H y w ran F w X m y SubGrp G | P pGrp G 𝑠 y H y F m X
55 16 54 ax-mp w ran F w X m y SubGrp G | P pGrp G 𝑠 y H y F m X
56 52 55 sylibr H SubGrp G X Fin P pGrp S w ran F w X
57 brralrspcev X w ran F w X z w ran F w z
58 31 56 57 syl2anc H SubGrp G X Fin P pGrp S z w ran F w z
59 suprzcl ran F ran F z w ran F w z sup ran F < ran F
60 14 28 58 59 syl3anc H SubGrp G X Fin P pGrp S sup ran F < ran F
61 fvelrnb F Fn y SubGrp G | P pGrp G 𝑠 y H y sup ran F < ran F k y SubGrp G | P pGrp G 𝑠 y H y F k = sup ran F <
62 16 61 ax-mp sup ran F < ran F k y SubGrp G | P pGrp G 𝑠 y H y F k = sup ran F <
63 60 62 sylib H SubGrp G X Fin P pGrp S k y SubGrp G | P pGrp G 𝑠 y H y F k = sup ran F <
64 oveq2 y = k G 𝑠 y = G 𝑠 k
65 64 breq2d y = k P pGrp G 𝑠 y P pGrp G 𝑠 k
66 sseq2 y = k H y H k
67 65 66 anbi12d y = k P pGrp G 𝑠 y H y P pGrp G 𝑠 k H k
68 67 rexrab k y SubGrp G | P pGrp G 𝑠 y H y F k = sup ran F < k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F <
69 63 68 sylib H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F <
70 simpl3 H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < P pGrp S
71 pgpprm P pGrp S P
72 70 71 syl H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < P
73 simprl H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < k SubGrp G
74 zssre
75 14 74 sstrdi H SubGrp G X Fin P pGrp S ran F
76 75 ad2antrr H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m ran F
77 28 ad2antrr H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m ran F
78 58 ad2antrr H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m z w ran F w z
79 simprl H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m m SubGrp G
80 simprrr H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m P pGrp G 𝑠 m
81 simprrl H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < P pGrp G 𝑠 k H k
82 81 adantr H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m P pGrp G 𝑠 k H k
83 82 simprd H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m H k
84 simprrl H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m k m
85 83 84 sstrd H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m H m
86 80 85 jca H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m P pGrp G 𝑠 m H m
87 39 79 86 elrabd H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m m y SubGrp G | P pGrp G 𝑠 y H y
88 87 34 syl H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m F m = m
89 fnfvelrn F Fn y SubGrp G | P pGrp G 𝑠 y H y m y SubGrp G | P pGrp G 𝑠 y H y F m ran F
90 16 87 89 sylancr H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m F m ran F
91 88 90 eqeltrrd H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m m ran F
92 76 77 78 91 suprubd H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m m sup ran F <
93 simprrr H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < F k = sup ran F <
94 93 adantr H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m F k = sup ran F <
95 73 adantr H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m k SubGrp G
96 67 95 82 elrabd H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m k y SubGrp G | P pGrp G 𝑠 y H y
97 fveq2 x = k x = k
98 fvex k V
99 97 3 98 fvmpt k y SubGrp G | P pGrp G 𝑠 y H y F k = k
100 96 99 syl H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m F k = k
101 94 100 eqtr3d H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m sup ran F < = k
102 92 101 breqtrd H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m m k
103 simpll2 H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m X Fin
104 42 ad2antrl H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m m X
105 103 104 ssfid H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m m Fin
106 105 84 ssfid H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m k Fin
107 hashcl m Fin m 0
108 hashcl k Fin k 0
109 nn0re m 0 m
110 nn0re k 0 k
111 lenlt m k m k ¬ k < m
112 109 110 111 syl2an m 0 k 0 m k ¬ k < m
113 107 108 112 syl2an m Fin k Fin m k ¬ k < m
114 105 106 113 syl2anc H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m m k ¬ k < m
115 102 114 mpbid H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m ¬ k < m
116 php3 m Fin k m k m
117 116 ex m Fin k m k m
118 105 117 syl H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m k m k m
119 hashsdom k Fin m Fin k < m k m
120 106 105 119 syl2anc H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m k < m k m
121 118 120 sylibrd H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m k m k < m
122 115 121 mtod H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m ¬ k m
123 sspss k m k m k = m
124 84 123 sylib H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m k m k = m
125 124 ord H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m ¬ k m k = m
126 122 125 mpd H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m k = m
127 126 expr H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m k = m
128 81 simpld H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < P pGrp G 𝑠 k
129 128 adantr H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G P pGrp G 𝑠 k
130 oveq2 k = m G 𝑠 k = G 𝑠 m
131 130 breq2d k = m P pGrp G 𝑠 k P pGrp G 𝑠 m
132 eqimss k = m k m
133 132 biantrurd k = m P pGrp G 𝑠 m k m P pGrp G 𝑠 m
134 131 133 bitrd k = m P pGrp G 𝑠 k k m P pGrp G 𝑠 m
135 129 134 syl5ibcom H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k = m k m P pGrp G 𝑠 m
136 127 135 impbid H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m k = m
137 136 ralrimiva H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < m SubGrp G k m P pGrp G 𝑠 m k = m
138 isslw k P pSyl G P k SubGrp G m SubGrp G k m P pGrp G 𝑠 m k = m
139 72 73 137 138 syl3anbrc H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < k P pSyl G
140 81 simprd H SubGrp G X Fin P pGrp S k SubGrp G P pGrp G 𝑠 k H k F k = sup ran F < H k
141 69 139 140 reximssdv H SubGrp G X Fin P pGrp S k P pSyl G H k