MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylow1lem2 Structured version   Visualization version   GIF version

Theorem sylow1lem2 19467
Description: Lemma for sylow1 19471. The function βŠ• is a group action on 𝑆. (Contributed by Mario Carneiro, 15-Jan-2015.)
Hypotheses
Ref Expression
sylow1.x 𝑋 = (Baseβ€˜πΊ)
sylow1.g (πœ‘ β†’ 𝐺 ∈ Grp)
sylow1.f (πœ‘ β†’ 𝑋 ∈ Fin)
sylow1.p (πœ‘ β†’ 𝑃 ∈ β„™)
sylow1.n (πœ‘ β†’ 𝑁 ∈ β„•0)
sylow1.d (πœ‘ β†’ (𝑃↑𝑁) βˆ₯ (β™―β€˜π‘‹))
sylow1lem.a + = (+gβ€˜πΊ)
sylow1lem.s 𝑆 = {𝑠 ∈ 𝒫 𝑋 ∣ (β™―β€˜π‘ ) = (𝑃↑𝑁)}
sylow1lem.m βŠ• = (π‘₯ ∈ 𝑋, 𝑦 ∈ 𝑆 ↦ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)))
Assertion
Ref Expression
sylow1lem2 (πœ‘ β†’ βŠ• ∈ (𝐺 GrpAct 𝑆))
Distinct variable groups:   π‘₯,𝑠,𝑦,𝑧   π‘₯,𝑆,𝑦,𝑧   𝑁,𝑠,π‘₯,𝑦,𝑧   𝑋,𝑠,π‘₯,𝑦,𝑧   + ,𝑠,π‘₯,𝑦,𝑧   π‘₯, βŠ• ,𝑦,𝑧   𝐺,𝑠,π‘₯,𝑦,𝑧   𝑃,𝑠,π‘₯,𝑦,𝑧   πœ‘,π‘₯,𝑦,𝑧
Allowed substitution hints:   πœ‘(𝑠)   βŠ• (𝑠)   𝑆(𝑠)

Proof of Theorem sylow1lem2
Dummy variables π‘Ž 𝑏 𝑐 𝑒 𝑀 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sylow1.g . . 3 (πœ‘ β†’ 𝐺 ∈ Grp)
2 sylow1lem.s . . . 4 𝑆 = {𝑠 ∈ 𝒫 𝑋 ∣ (β™―β€˜π‘ ) = (𝑃↑𝑁)}
3 sylow1.x . . . . . 6 𝑋 = (Baseβ€˜πΊ)
43fvexi 6906 . . . . 5 𝑋 ∈ V
54pwex 5379 . . . 4 𝒫 𝑋 ∈ V
62, 5rabex2 5335 . . 3 𝑆 ∈ V
71, 6jctir 522 . 2 (πœ‘ β†’ (𝐺 ∈ Grp ∧ 𝑆 ∈ V))
8 simprl 770 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ π‘₯ ∈ 𝑋)
9 sylow1lem.a . . . . . . . . . . . . 13 + = (+gβ€˜πΊ)
10 eqid 2733 . . . . . . . . . . . . 13 (𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)) = (𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧))
113, 9, 10grplmulf1o 18897 . . . . . . . . . . . 12 ((𝐺 ∈ Grp ∧ π‘₯ ∈ 𝑋) β†’ (𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)):𝑋–1-1-onto→𝑋)
121, 8, 11syl2an2r 684 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ (𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)):𝑋–1-1-onto→𝑋)
13 f1of1 6833 . . . . . . . . . . 11 ((𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)):𝑋–1-1-onto→𝑋 β†’ (𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)):𝑋–1-1→𝑋)
1412, 13syl 17 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ (𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)):𝑋–1-1→𝑋)
15 simprr 772 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ 𝑦 ∈ 𝑆)
16 fveqeq2 6901 . . . . . . . . . . . . . 14 (𝑠 = 𝑦 β†’ ((β™―β€˜π‘ ) = (𝑃↑𝑁) ↔ (β™―β€˜π‘¦) = (𝑃↑𝑁)))
1716, 2elrab2 3687 . . . . . . . . . . . . 13 (𝑦 ∈ 𝑆 ↔ (𝑦 ∈ 𝒫 𝑋 ∧ (β™―β€˜π‘¦) = (𝑃↑𝑁)))
1815, 17sylib 217 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ (𝑦 ∈ 𝒫 𝑋 ∧ (β™―β€˜π‘¦) = (𝑃↑𝑁)))
1918simpld 496 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ 𝑦 ∈ 𝒫 𝑋)
2019elpwid 4612 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ 𝑦 βŠ† 𝑋)
21 f1ssres 6796 . . . . . . . . . 10 (((𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)):𝑋–1-1→𝑋 ∧ 𝑦 βŠ† 𝑋) β†’ ((𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)) β†Ύ 𝑦):𝑦–1-1→𝑋)
2214, 20, 21syl2anc 585 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ ((𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)) β†Ύ 𝑦):𝑦–1-1→𝑋)
23 resmpt 6038 . . . . . . . . . 10 (𝑦 βŠ† 𝑋 β†’ ((𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)) β†Ύ 𝑦) = (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)))
24 f1eq1 6783 . . . . . . . . . 10 (((𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)) β†Ύ 𝑦) = (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) β†’ (((𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)) β†Ύ 𝑦):𝑦–1-1→𝑋 ↔ (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)):𝑦–1-1→𝑋))
2520, 23, 243syl 18 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ (((𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)) β†Ύ 𝑦):𝑦–1-1→𝑋 ↔ (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)):𝑦–1-1→𝑋))
2622, 25mpbid 231 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)):𝑦–1-1→𝑋)
27 f1f 6788 . . . . . . . 8 ((𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)):𝑦–1-1→𝑋 β†’ (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)):π‘¦βŸΆπ‘‹)
28 frn 6725 . . . . . . . 8 ((𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)):π‘¦βŸΆπ‘‹ β†’ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) βŠ† 𝑋)
2926, 27, 283syl 18 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) βŠ† 𝑋)
304elpw2 5346 . . . . . . 7 (ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) ∈ 𝒫 𝑋 ↔ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) βŠ† 𝑋)
3129, 30sylibr 233 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) ∈ 𝒫 𝑋)
32 f1f1orn 6845 . . . . . . . . 9 ((𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)):𝑦–1-1→𝑋 β†’ (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)):𝑦–1-1-ontoβ†’ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)))
33 vex 3479 . . . . . . . . . 10 𝑦 ∈ V
3433f1oen 8969 . . . . . . . . 9 ((𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)):𝑦–1-1-ontoβ†’ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) β†’ 𝑦 β‰ˆ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)))
3526, 32, 343syl 18 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ 𝑦 β‰ˆ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)))
36 sylow1.f . . . . . . . . . 10 (πœ‘ β†’ 𝑋 ∈ Fin)
37 ssfi 9173 . . . . . . . . . 10 ((𝑋 ∈ Fin ∧ 𝑦 βŠ† 𝑋) β†’ 𝑦 ∈ Fin)
3836, 20, 37syl2an2r 684 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ 𝑦 ∈ Fin)
39 ssfi 9173 . . . . . . . . . 10 ((𝑋 ∈ Fin ∧ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) βŠ† 𝑋) β†’ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) ∈ Fin)
4036, 29, 39syl2an2r 684 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) ∈ Fin)
41 hashen 14307 . . . . . . . . 9 ((𝑦 ∈ Fin ∧ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) ∈ Fin) β†’ ((β™―β€˜π‘¦) = (β™―β€˜ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧))) ↔ 𝑦 β‰ˆ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧))))
4238, 40, 41syl2anc 585 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ ((β™―β€˜π‘¦) = (β™―β€˜ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧))) ↔ 𝑦 β‰ˆ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧))))
4335, 42mpbird 257 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ (β™―β€˜π‘¦) = (β™―β€˜ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧))))
4418simprd 497 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ (β™―β€˜π‘¦) = (𝑃↑𝑁))
4543, 44eqtr3d 2775 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ (β™―β€˜ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧))) = (𝑃↑𝑁))
46 fveqeq2 6901 . . . . . . 7 (𝑠 = ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) β†’ ((β™―β€˜π‘ ) = (𝑃↑𝑁) ↔ (β™―β€˜ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧))) = (𝑃↑𝑁)))
4746, 2elrab2 3687 . . . . . 6 (ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) ∈ 𝑆 ↔ (ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) ∈ 𝒫 𝑋 ∧ (β™―β€˜ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧))) = (𝑃↑𝑁)))
4831, 45, 47sylanbrc 584 . . . . 5 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) ∈ 𝑆)
4948ralrimivva 3201 . . . 4 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ 𝑆 ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) ∈ 𝑆)
50 sylow1lem.m . . . . 5 βŠ• = (π‘₯ ∈ 𝑋, 𝑦 ∈ 𝑆 ↦ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)))
5150fmpo 8054 . . . 4 (βˆ€π‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ 𝑆 ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) ∈ 𝑆 ↔ βŠ• :(𝑋 Γ— 𝑆)βŸΆπ‘†)
5249, 51sylib 217 . . 3 (πœ‘ β†’ βŠ• :(𝑋 Γ— 𝑆)βŸΆπ‘†)
531adantr 482 . . . . . . . 8 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ 𝐺 ∈ Grp)
54 eqid 2733 . . . . . . . . 9 (0gβ€˜πΊ) = (0gβ€˜πΊ)
553, 54grpidcl 18850 . . . . . . . 8 (𝐺 ∈ Grp β†’ (0gβ€˜πΊ) ∈ 𝑋)
5653, 55syl 17 . . . . . . 7 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ (0gβ€˜πΊ) ∈ 𝑋)
57 simpr 486 . . . . . . 7 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ π‘Ž ∈ 𝑆)
58 simpr 486 . . . . . . . . . 10 ((π‘₯ = (0gβ€˜πΊ) ∧ 𝑦 = π‘Ž) β†’ 𝑦 = π‘Ž)
59 simpl 484 . . . . . . . . . . 11 ((π‘₯ = (0gβ€˜πΊ) ∧ 𝑦 = π‘Ž) β†’ π‘₯ = (0gβ€˜πΊ))
6059oveq1d 7424 . . . . . . . . . 10 ((π‘₯ = (0gβ€˜πΊ) ∧ 𝑦 = π‘Ž) β†’ (π‘₯ + 𝑧) = ((0gβ€˜πΊ) + 𝑧))
6158, 60mpteq12dv 5240 . . . . . . . . 9 ((π‘₯ = (0gβ€˜πΊ) ∧ 𝑦 = π‘Ž) β†’ (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) = (𝑧 ∈ π‘Ž ↦ ((0gβ€˜πΊ) + 𝑧)))
6261rneqd 5938 . . . . . . . 8 ((π‘₯ = (0gβ€˜πΊ) ∧ 𝑦 = π‘Ž) β†’ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) = ran (𝑧 ∈ π‘Ž ↦ ((0gβ€˜πΊ) + 𝑧)))
63 vex 3479 . . . . . . . . . 10 π‘Ž ∈ V
6463mptex 7225 . . . . . . . . 9 (𝑧 ∈ π‘Ž ↦ ((0gβ€˜πΊ) + 𝑧)) ∈ V
6564rnex 7903 . . . . . . . 8 ran (𝑧 ∈ π‘Ž ↦ ((0gβ€˜πΊ) + 𝑧)) ∈ V
6662, 50, 65ovmpoa 7563 . . . . . . 7 (((0gβ€˜πΊ) ∈ 𝑋 ∧ π‘Ž ∈ 𝑆) β†’ ((0gβ€˜πΊ) βŠ• π‘Ž) = ran (𝑧 ∈ π‘Ž ↦ ((0gβ€˜πΊ) + 𝑧)))
6756, 57, 66syl2anc 585 . . . . . 6 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ ((0gβ€˜πΊ) βŠ• π‘Ž) = ran (𝑧 ∈ π‘Ž ↦ ((0gβ€˜πΊ) + 𝑧)))
682ssrab3 4081 . . . . . . . . . . . . . 14 𝑆 βŠ† 𝒫 𝑋
6968, 57sselid 3981 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ π‘Ž ∈ 𝒫 𝑋)
7069elpwid 4612 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ π‘Ž βŠ† 𝑋)
7170sselda 3983 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ 𝑧 ∈ π‘Ž) β†’ 𝑧 ∈ 𝑋)
723, 9, 54grplid 18852 . . . . . . . . . . 11 ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋) β†’ ((0gβ€˜πΊ) + 𝑧) = 𝑧)
7353, 71, 72syl2an2r 684 . . . . . . . . . 10 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ 𝑧 ∈ π‘Ž) β†’ ((0gβ€˜πΊ) + 𝑧) = 𝑧)
7473mpteq2dva 5249 . . . . . . . . 9 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ (𝑧 ∈ π‘Ž ↦ ((0gβ€˜πΊ) + 𝑧)) = (𝑧 ∈ π‘Ž ↦ 𝑧))
75 mptresid 6051 . . . . . . . . 9 ( I β†Ύ π‘Ž) = (𝑧 ∈ π‘Ž ↦ 𝑧)
7674, 75eqtr4di 2791 . . . . . . . 8 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ (𝑧 ∈ π‘Ž ↦ ((0gβ€˜πΊ) + 𝑧)) = ( I β†Ύ π‘Ž))
7776rneqd 5938 . . . . . . 7 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ ran (𝑧 ∈ π‘Ž ↦ ((0gβ€˜πΊ) + 𝑧)) = ran ( I β†Ύ π‘Ž))
78 rnresi 6075 . . . . . . 7 ran ( I β†Ύ π‘Ž) = π‘Ž
7977, 78eqtrdi 2789 . . . . . 6 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ ran (𝑧 ∈ π‘Ž ↦ ((0gβ€˜πΊ) + 𝑧)) = π‘Ž)
8067, 79eqtrd 2773 . . . . 5 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ ((0gβ€˜πΊ) βŠ• π‘Ž) = π‘Ž)
81 ovex 7442 . . . . . . . . . 10 (𝑐 + 𝑧) ∈ V
82 oveq2 7417 . . . . . . . . . 10 (𝑀 = (𝑐 + 𝑧) β†’ (𝑏 + 𝑀) = (𝑏 + (𝑐 + 𝑧)))
8381, 82abrexco 7243 . . . . . . . . 9 {𝑒 ∣ βˆƒπ‘€ ∈ {𝑣 ∣ βˆƒπ‘§ ∈ π‘Ž 𝑣 = (𝑐 + 𝑧)}𝑒 = (𝑏 + 𝑀)} = {𝑒 ∣ βˆƒπ‘§ ∈ π‘Ž 𝑒 = (𝑏 + (𝑐 + 𝑧))}
84 simprr 772 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ 𝑐 ∈ 𝑋)
8557adantr 482 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ π‘Ž ∈ 𝑆)
86 simpr 486 . . . . . . . . . . . . . . . 16 ((π‘₯ = 𝑐 ∧ 𝑦 = π‘Ž) β†’ 𝑦 = π‘Ž)
87 simpl 484 . . . . . . . . . . . . . . . . 17 ((π‘₯ = 𝑐 ∧ 𝑦 = π‘Ž) β†’ π‘₯ = 𝑐)
8887oveq1d 7424 . . . . . . . . . . . . . . . 16 ((π‘₯ = 𝑐 ∧ 𝑦 = π‘Ž) β†’ (π‘₯ + 𝑧) = (𝑐 + 𝑧))
8986, 88mpteq12dv 5240 . . . . . . . . . . . . . . 15 ((π‘₯ = 𝑐 ∧ 𝑦 = π‘Ž) β†’ (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) = (𝑧 ∈ π‘Ž ↦ (𝑐 + 𝑧)))
9089rneqd 5938 . . . . . . . . . . . . . 14 ((π‘₯ = 𝑐 ∧ 𝑦 = π‘Ž) β†’ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) = ran (𝑧 ∈ π‘Ž ↦ (𝑐 + 𝑧)))
9163mptex 7225 . . . . . . . . . . . . . . 15 (𝑧 ∈ π‘Ž ↦ (𝑐 + 𝑧)) ∈ V
9291rnex 7903 . . . . . . . . . . . . . 14 ran (𝑧 ∈ π‘Ž ↦ (𝑐 + 𝑧)) ∈ V
9390, 50, 92ovmpoa 7563 . . . . . . . . . . . . 13 ((𝑐 ∈ 𝑋 ∧ π‘Ž ∈ 𝑆) β†’ (𝑐 βŠ• π‘Ž) = ran (𝑧 ∈ π‘Ž ↦ (𝑐 + 𝑧)))
9484, 85, 93syl2anc 585 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ (𝑐 βŠ• π‘Ž) = ran (𝑧 ∈ π‘Ž ↦ (𝑐 + 𝑧)))
95 eqid 2733 . . . . . . . . . . . . 13 (𝑧 ∈ π‘Ž ↦ (𝑐 + 𝑧)) = (𝑧 ∈ π‘Ž ↦ (𝑐 + 𝑧))
9695rnmpt 5955 . . . . . . . . . . . 12 ran (𝑧 ∈ π‘Ž ↦ (𝑐 + 𝑧)) = {𝑣 ∣ βˆƒπ‘§ ∈ π‘Ž 𝑣 = (𝑐 + 𝑧)}
9794, 96eqtrdi 2789 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ (𝑐 βŠ• π‘Ž) = {𝑣 ∣ βˆƒπ‘§ ∈ π‘Ž 𝑣 = (𝑐 + 𝑧)})
9897rexeqdv 3327 . . . . . . . . . 10 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ (βˆƒπ‘€ ∈ (𝑐 βŠ• π‘Ž)𝑒 = (𝑏 + 𝑀) ↔ βˆƒπ‘€ ∈ {𝑣 ∣ βˆƒπ‘§ ∈ π‘Ž 𝑣 = (𝑐 + 𝑧)}𝑒 = (𝑏 + 𝑀)))
9998abbidv 2802 . . . . . . . . 9 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ {𝑒 ∣ βˆƒπ‘€ ∈ (𝑐 βŠ• π‘Ž)𝑒 = (𝑏 + 𝑀)} = {𝑒 ∣ βˆƒπ‘€ ∈ {𝑣 ∣ βˆƒπ‘§ ∈ π‘Ž 𝑣 = (𝑐 + 𝑧)}𝑒 = (𝑏 + 𝑀)})
10053ad2antrr 725 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ π‘Ž) β†’ 𝐺 ∈ Grp)
101 simprl 770 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ 𝑏 ∈ 𝑋)
102101adantr 482 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ π‘Ž) β†’ 𝑏 ∈ 𝑋)
10384adantr 482 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ π‘Ž) β†’ 𝑐 ∈ 𝑋)
10471adantlr 714 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ π‘Ž) β†’ 𝑧 ∈ 𝑋)
1053, 9grpass 18828 . . . . . . . . . . . . 13 ((𝐺 ∈ Grp ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) β†’ ((𝑏 + 𝑐) + 𝑧) = (𝑏 + (𝑐 + 𝑧)))
106100, 102, 103, 104, 105syl13anc 1373 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ π‘Ž) β†’ ((𝑏 + 𝑐) + 𝑧) = (𝑏 + (𝑐 + 𝑧)))
107106eqeq2d 2744 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ π‘Ž) β†’ (𝑒 = ((𝑏 + 𝑐) + 𝑧) ↔ 𝑒 = (𝑏 + (𝑐 + 𝑧))))
108107rexbidva 3177 . . . . . . . . . 10 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ (βˆƒπ‘§ ∈ π‘Ž 𝑒 = ((𝑏 + 𝑐) + 𝑧) ↔ βˆƒπ‘§ ∈ π‘Ž 𝑒 = (𝑏 + (𝑐 + 𝑧))))
109108abbidv 2802 . . . . . . . . 9 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ {𝑒 ∣ βˆƒπ‘§ ∈ π‘Ž 𝑒 = ((𝑏 + 𝑐) + 𝑧)} = {𝑒 ∣ βˆƒπ‘§ ∈ π‘Ž 𝑒 = (𝑏 + (𝑐 + 𝑧))})
11083, 99, 1093eqtr4a 2799 . . . . . . . 8 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ {𝑒 ∣ βˆƒπ‘€ ∈ (𝑐 βŠ• π‘Ž)𝑒 = (𝑏 + 𝑀)} = {𝑒 ∣ βˆƒπ‘§ ∈ π‘Ž 𝑒 = ((𝑏 + 𝑐) + 𝑧)})
111 eqid 2733 . . . . . . . . 9 (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀)) = (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀))
112111rnmpt 5955 . . . . . . . 8 ran (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀)) = {𝑒 ∣ βˆƒπ‘€ ∈ (𝑐 βŠ• π‘Ž)𝑒 = (𝑏 + 𝑀)}
113 eqid 2733 . . . . . . . . 9 (𝑧 ∈ π‘Ž ↦ ((𝑏 + 𝑐) + 𝑧)) = (𝑧 ∈ π‘Ž ↦ ((𝑏 + 𝑐) + 𝑧))
114113rnmpt 5955 . . . . . . . 8 ran (𝑧 ∈ π‘Ž ↦ ((𝑏 + 𝑐) + 𝑧)) = {𝑒 ∣ βˆƒπ‘§ ∈ π‘Ž 𝑒 = ((𝑏 + 𝑐) + 𝑧)}
115110, 112, 1143eqtr4g 2798 . . . . . . 7 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ ran (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀)) = ran (𝑧 ∈ π‘Ž ↦ ((𝑏 + 𝑐) + 𝑧)))
11652ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ βŠ• :(𝑋 Γ— 𝑆)βŸΆπ‘†)
117116, 84, 85fovcdmd 7579 . . . . . . . 8 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ (𝑐 βŠ• π‘Ž) ∈ 𝑆)
118 simpr 486 . . . . . . . . . . . 12 ((π‘₯ = 𝑏 ∧ 𝑦 = (𝑐 βŠ• π‘Ž)) β†’ 𝑦 = (𝑐 βŠ• π‘Ž))
119 simpl 484 . . . . . . . . . . . . 13 ((π‘₯ = 𝑏 ∧ 𝑦 = (𝑐 βŠ• π‘Ž)) β†’ π‘₯ = 𝑏)
120119oveq1d 7424 . . . . . . . . . . . 12 ((π‘₯ = 𝑏 ∧ 𝑦 = (𝑐 βŠ• π‘Ž)) β†’ (π‘₯ + 𝑧) = (𝑏 + 𝑧))
121118, 120mpteq12dv 5240 . . . . . . . . . . 11 ((π‘₯ = 𝑏 ∧ 𝑦 = (𝑐 βŠ• π‘Ž)) β†’ (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) = (𝑧 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑧)))
122 oveq2 7417 . . . . . . . . . . . 12 (𝑧 = 𝑀 β†’ (𝑏 + 𝑧) = (𝑏 + 𝑀))
123122cbvmptv 5262 . . . . . . . . . . 11 (𝑧 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑧)) = (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀))
124121, 123eqtrdi 2789 . . . . . . . . . 10 ((π‘₯ = 𝑏 ∧ 𝑦 = (𝑐 βŠ• π‘Ž)) β†’ (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) = (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀)))
125124rneqd 5938 . . . . . . . . 9 ((π‘₯ = 𝑏 ∧ 𝑦 = (𝑐 βŠ• π‘Ž)) β†’ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) = ran (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀)))
126 ovex 7442 . . . . . . . . . . 11 (𝑐 βŠ• π‘Ž) ∈ V
127126mptex 7225 . . . . . . . . . 10 (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀)) ∈ V
128127rnex 7903 . . . . . . . . 9 ran (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀)) ∈ V
129125, 50, 128ovmpoa 7563 . . . . . . . 8 ((𝑏 ∈ 𝑋 ∧ (𝑐 βŠ• π‘Ž) ∈ 𝑆) β†’ (𝑏 βŠ• (𝑐 βŠ• π‘Ž)) = ran (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀)))
130101, 117, 129syl2anc 585 . . . . . . 7 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ (𝑏 βŠ• (𝑐 βŠ• π‘Ž)) = ran (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀)))
1311ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ 𝐺 ∈ Grp)
1323, 9grpcl 18827 . . . . . . . . 9 ((𝐺 ∈ Grp ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋) β†’ (𝑏 + 𝑐) ∈ 𝑋)
133131, 101, 84, 132syl3anc 1372 . . . . . . . 8 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ (𝑏 + 𝑐) ∈ 𝑋)
134 simpr 486 . . . . . . . . . . 11 ((π‘₯ = (𝑏 + 𝑐) ∧ 𝑦 = π‘Ž) β†’ 𝑦 = π‘Ž)
135 simpl 484 . . . . . . . . . . . 12 ((π‘₯ = (𝑏 + 𝑐) ∧ 𝑦 = π‘Ž) β†’ π‘₯ = (𝑏 + 𝑐))
136135oveq1d 7424 . . . . . . . . . . 11 ((π‘₯ = (𝑏 + 𝑐) ∧ 𝑦 = π‘Ž) β†’ (π‘₯ + 𝑧) = ((𝑏 + 𝑐) + 𝑧))
137134, 136mpteq12dv 5240 . . . . . . . . . 10 ((π‘₯ = (𝑏 + 𝑐) ∧ 𝑦 = π‘Ž) β†’ (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) = (𝑧 ∈ π‘Ž ↦ ((𝑏 + 𝑐) + 𝑧)))
138137rneqd 5938 . . . . . . . . 9 ((π‘₯ = (𝑏 + 𝑐) ∧ 𝑦 = π‘Ž) β†’ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) = ran (𝑧 ∈ π‘Ž ↦ ((𝑏 + 𝑐) + 𝑧)))
13963mptex 7225 . . . . . . . . . 10 (𝑧 ∈ π‘Ž ↦ ((𝑏 + 𝑐) + 𝑧)) ∈ V
140139rnex 7903 . . . . . . . . 9 ran (𝑧 ∈ π‘Ž ↦ ((𝑏 + 𝑐) + 𝑧)) ∈ V
141138, 50, 140ovmpoa 7563 . . . . . . . 8 (((𝑏 + 𝑐) ∈ 𝑋 ∧ π‘Ž ∈ 𝑆) β†’ ((𝑏 + 𝑐) βŠ• π‘Ž) = ran (𝑧 ∈ π‘Ž ↦ ((𝑏 + 𝑐) + 𝑧)))
142133, 85, 141syl2anc 585 . . . . . . 7 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ ((𝑏 + 𝑐) βŠ• π‘Ž) = ran (𝑧 ∈ π‘Ž ↦ ((𝑏 + 𝑐) + 𝑧)))
143115, 130, 1423eqtr4rd 2784 . . . . . 6 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ ((𝑏 + 𝑐) βŠ• π‘Ž) = (𝑏 βŠ• (𝑐 βŠ• π‘Ž)))
144143ralrimivva 3201 . . . . 5 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ βˆ€π‘ ∈ 𝑋 βˆ€π‘ ∈ 𝑋 ((𝑏 + 𝑐) βŠ• π‘Ž) = (𝑏 βŠ• (𝑐 βŠ• π‘Ž)))
14580, 144jca 513 . . . 4 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ (((0gβ€˜πΊ) βŠ• π‘Ž) = π‘Ž ∧ βˆ€π‘ ∈ 𝑋 βˆ€π‘ ∈ 𝑋 ((𝑏 + 𝑐) βŠ• π‘Ž) = (𝑏 βŠ• (𝑐 βŠ• π‘Ž))))
146145ralrimiva 3147 . . 3 (πœ‘ β†’ βˆ€π‘Ž ∈ 𝑆 (((0gβ€˜πΊ) βŠ• π‘Ž) = π‘Ž ∧ βˆ€π‘ ∈ 𝑋 βˆ€π‘ ∈ 𝑋 ((𝑏 + 𝑐) βŠ• π‘Ž) = (𝑏 βŠ• (𝑐 βŠ• π‘Ž))))
14752, 146jca 513 . 2 (πœ‘ β†’ ( βŠ• :(𝑋 Γ— 𝑆)βŸΆπ‘† ∧ βˆ€π‘Ž ∈ 𝑆 (((0gβ€˜πΊ) βŠ• π‘Ž) = π‘Ž ∧ βˆ€π‘ ∈ 𝑋 βˆ€π‘ ∈ 𝑋 ((𝑏 + 𝑐) βŠ• π‘Ž) = (𝑏 βŠ• (𝑐 βŠ• π‘Ž)))))
1483, 9, 54isga 19155 . 2 ( βŠ• ∈ (𝐺 GrpAct 𝑆) ↔ ((𝐺 ∈ Grp ∧ 𝑆 ∈ V) ∧ ( βŠ• :(𝑋 Γ— 𝑆)βŸΆπ‘† ∧ βˆ€π‘Ž ∈ 𝑆 (((0gβ€˜πΊ) βŠ• π‘Ž) = π‘Ž ∧ βˆ€π‘ ∈ 𝑋 βˆ€π‘ ∈ 𝑋 ((𝑏 + 𝑐) βŠ• π‘Ž) = (𝑏 βŠ• (𝑐 βŠ• π‘Ž))))))
1497, 147, 148sylanbrc 584 1 (πœ‘ β†’ βŠ• ∈ (𝐺 GrpAct 𝑆))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  {cab 2710  βˆ€wral 3062  βˆƒwrex 3071  {crab 3433  Vcvv 3475   βŠ† wss 3949  π’« cpw 4603   class class class wbr 5149   ↦ cmpt 5232   I cid 5574   Γ— cxp 5675  ran crn 5678   β†Ύ cres 5679  βŸΆwf 6540  β€“1-1β†’wf1 6541  β€“1-1-ontoβ†’wf1o 6543  β€˜cfv 6544  (class class class)co 7409   ∈ cmpo 7411   β‰ˆ cen 8936  Fincfn 8939  β„•0cn0 12472  β†‘cexp 14027  β™―chash 14290   βˆ₯ cdvds 16197  β„™cprime 16608  Basecbs 17144  +gcplusg 17197  0gc0g 17385  Grpcgrp 18819   GrpAct cga 19153
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-er 8703  df-map 8822  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-nn 12213  df-n0 12473  df-z 12559  df-uz 12823  df-hash 14291  df-0g 17387  df-mgm 18561  df-sgrp 18610  df-mnd 18626  df-grp 18822  df-minusg 18823  df-ga 19154
This theorem is referenced by:  sylow1lem3  19468  sylow1lem5  19470
  Copyright terms: Public domain W3C validator