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

Theorem sylow1lem2 19466
Description: Lemma for sylow1 19470. 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 6905 . . . . 5 𝑋 ∈ V
54pwex 5378 . . . 4 𝒫 𝑋 ∈ V
62, 5rabex2 5334 . . 3 𝑆 ∈ V
71, 6jctir 521 . 2 (πœ‘ β†’ (𝐺 ∈ Grp ∧ 𝑆 ∈ V))
8 simprl 769 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ π‘₯ ∈ 𝑋)
9 sylow1lem.a . . . . . . . . . . . . 13 + = (+gβ€˜πΊ)
10 eqid 2732 . . . . . . . . . . . . 13 (𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)) = (𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧))
113, 9, 10grplmulf1o 18896 . . . . . . . . . . . 12 ((𝐺 ∈ Grp ∧ π‘₯ ∈ 𝑋) β†’ (𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)):𝑋–1-1-onto→𝑋)
121, 8, 11syl2an2r 683 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ (𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)):𝑋–1-1-onto→𝑋)
13 f1of1 6832 . . . . . . . . . . 11 ((𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)):𝑋–1-1-onto→𝑋 β†’ (𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)):𝑋–1-1→𝑋)
1412, 13syl 17 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ (𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)):𝑋–1-1→𝑋)
15 simprr 771 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ 𝑦 ∈ 𝑆)
16 fveqeq2 6900 . . . . . . . . . . . . . 14 (𝑠 = 𝑦 β†’ ((β™―β€˜π‘ ) = (𝑃↑𝑁) ↔ (β™―β€˜π‘¦) = (𝑃↑𝑁)))
1716, 2elrab2 3686 . . . . . . . . . . . . 13 (𝑦 ∈ 𝑆 ↔ (𝑦 ∈ 𝒫 𝑋 ∧ (β™―β€˜π‘¦) = (𝑃↑𝑁)))
1815, 17sylib 217 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ (𝑦 ∈ 𝒫 𝑋 ∧ (β™―β€˜π‘¦) = (𝑃↑𝑁)))
1918simpld 495 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ 𝑦 ∈ 𝒫 𝑋)
2019elpwid 4611 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ 𝑦 βŠ† 𝑋)
21 f1ssres 6795 . . . . . . . . . 10 (((𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)):𝑋–1-1→𝑋 ∧ 𝑦 βŠ† 𝑋) β†’ ((𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)) β†Ύ 𝑦):𝑦–1-1→𝑋)
2214, 20, 21syl2anc 584 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ ((𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)) β†Ύ 𝑦):𝑦–1-1→𝑋)
23 resmpt 6037 . . . . . . . . . 10 (𝑦 βŠ† 𝑋 β†’ ((𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)) β†Ύ 𝑦) = (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)))
24 f1eq1 6782 . . . . . . . . . 10 (((𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)) β†Ύ 𝑦) = (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) β†’ (((𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)) β†Ύ 𝑦):𝑦–1-1→𝑋 ↔ (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)):𝑦–1-1→𝑋))
2520, 23, 243syl 18 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ (((𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)) β†Ύ 𝑦):𝑦–1-1→𝑋 ↔ (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)):𝑦–1-1→𝑋))
2622, 25mpbid 231 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)):𝑦–1-1→𝑋)
27 f1f 6787 . . . . . . . 8 ((𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)):𝑦–1-1→𝑋 β†’ (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)):π‘¦βŸΆπ‘‹)
28 frn 6724 . . . . . . . 8 ((𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)):π‘¦βŸΆπ‘‹ β†’ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) βŠ† 𝑋)
2926, 27, 283syl 18 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) βŠ† 𝑋)
304elpw2 5345 . . . . . . 7 (ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) ∈ 𝒫 𝑋 ↔ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) βŠ† 𝑋)
3129, 30sylibr 233 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) ∈ 𝒫 𝑋)
32 f1f1orn 6844 . . . . . . . . 9 ((𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)):𝑦–1-1→𝑋 β†’ (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)):𝑦–1-1-ontoβ†’ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)))
33 vex 3478 . . . . . . . . . 10 𝑦 ∈ V
3433f1oen 8968 . . . . . . . . 9 ((𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)):𝑦–1-1-ontoβ†’ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) β†’ 𝑦 β‰ˆ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)))
3526, 32, 343syl 18 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ 𝑦 β‰ˆ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)))
36 sylow1.f . . . . . . . . . 10 (πœ‘ β†’ 𝑋 ∈ Fin)
37 ssfi 9172 . . . . . . . . . 10 ((𝑋 ∈ Fin ∧ 𝑦 βŠ† 𝑋) β†’ 𝑦 ∈ Fin)
3836, 20, 37syl2an2r 683 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ 𝑦 ∈ Fin)
39 ssfi 9172 . . . . . . . . . 10 ((𝑋 ∈ Fin ∧ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) βŠ† 𝑋) β†’ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) ∈ Fin)
4036, 29, 39syl2an2r 683 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) ∈ Fin)
41 hashen 14306 . . . . . . . . 9 ((𝑦 ∈ Fin ∧ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) ∈ Fin) β†’ ((β™―β€˜π‘¦) = (β™―β€˜ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧))) ↔ 𝑦 β‰ˆ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧))))
4238, 40, 41syl2anc 584 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ ((β™―β€˜π‘¦) = (β™―β€˜ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧))) ↔ 𝑦 β‰ˆ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧))))
4335, 42mpbird 256 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ (β™―β€˜π‘¦) = (β™―β€˜ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧))))
4418simprd 496 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ (β™―β€˜π‘¦) = (𝑃↑𝑁))
4543, 44eqtr3d 2774 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ (β™―β€˜ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧))) = (𝑃↑𝑁))
46 fveqeq2 6900 . . . . . . 7 (𝑠 = ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) β†’ ((β™―β€˜π‘ ) = (𝑃↑𝑁) ↔ (β™―β€˜ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧))) = (𝑃↑𝑁)))
4746, 2elrab2 3686 . . . . . 6 (ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) ∈ 𝑆 ↔ (ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) ∈ 𝒫 𝑋 ∧ (β™―β€˜ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧))) = (𝑃↑𝑁)))
4831, 45, 47sylanbrc 583 . . . . 5 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) ∈ 𝑆)
4948ralrimivva 3200 . . . 4 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ 𝑆 ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) ∈ 𝑆)
50 sylow1lem.m . . . . 5 βŠ• = (π‘₯ ∈ 𝑋, 𝑦 ∈ 𝑆 ↦ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)))
5150fmpo 8053 . . . 4 (βˆ€π‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ 𝑆 ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) ∈ 𝑆 ↔ βŠ• :(𝑋 Γ— 𝑆)βŸΆπ‘†)
5249, 51sylib 217 . . 3 (πœ‘ β†’ βŠ• :(𝑋 Γ— 𝑆)βŸΆπ‘†)
531adantr 481 . . . . . . . 8 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ 𝐺 ∈ Grp)
54 eqid 2732 . . . . . . . . 9 (0gβ€˜πΊ) = (0gβ€˜πΊ)
553, 54grpidcl 18849 . . . . . . . 8 (𝐺 ∈ Grp β†’ (0gβ€˜πΊ) ∈ 𝑋)
5653, 55syl 17 . . . . . . 7 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ (0gβ€˜πΊ) ∈ 𝑋)
57 simpr 485 . . . . . . 7 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ π‘Ž ∈ 𝑆)
58 simpr 485 . . . . . . . . . 10 ((π‘₯ = (0gβ€˜πΊ) ∧ 𝑦 = π‘Ž) β†’ 𝑦 = π‘Ž)
59 simpl 483 . . . . . . . . . . 11 ((π‘₯ = (0gβ€˜πΊ) ∧ 𝑦 = π‘Ž) β†’ π‘₯ = (0gβ€˜πΊ))
6059oveq1d 7423 . . . . . . . . . 10 ((π‘₯ = (0gβ€˜πΊ) ∧ 𝑦 = π‘Ž) β†’ (π‘₯ + 𝑧) = ((0gβ€˜πΊ) + 𝑧))
6158, 60mpteq12dv 5239 . . . . . . . . 9 ((π‘₯ = (0gβ€˜πΊ) ∧ 𝑦 = π‘Ž) β†’ (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) = (𝑧 ∈ π‘Ž ↦ ((0gβ€˜πΊ) + 𝑧)))
6261rneqd 5937 . . . . . . . 8 ((π‘₯ = (0gβ€˜πΊ) ∧ 𝑦 = π‘Ž) β†’ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) = ran (𝑧 ∈ π‘Ž ↦ ((0gβ€˜πΊ) + 𝑧)))
63 vex 3478 . . . . . . . . . 10 π‘Ž ∈ V
6463mptex 7224 . . . . . . . . 9 (𝑧 ∈ π‘Ž ↦ ((0gβ€˜πΊ) + 𝑧)) ∈ V
6564rnex 7902 . . . . . . . 8 ran (𝑧 ∈ π‘Ž ↦ ((0gβ€˜πΊ) + 𝑧)) ∈ V
6662, 50, 65ovmpoa 7562 . . . . . . 7 (((0gβ€˜πΊ) ∈ 𝑋 ∧ π‘Ž ∈ 𝑆) β†’ ((0gβ€˜πΊ) βŠ• π‘Ž) = ran (𝑧 ∈ π‘Ž ↦ ((0gβ€˜πΊ) + 𝑧)))
6756, 57, 66syl2anc 584 . . . . . 6 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ ((0gβ€˜πΊ) βŠ• π‘Ž) = ran (𝑧 ∈ π‘Ž ↦ ((0gβ€˜πΊ) + 𝑧)))
682ssrab3 4080 . . . . . . . . . . . . . 14 𝑆 βŠ† 𝒫 𝑋
6968, 57sselid 3980 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ π‘Ž ∈ 𝒫 𝑋)
7069elpwid 4611 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ π‘Ž βŠ† 𝑋)
7170sselda 3982 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ 𝑧 ∈ π‘Ž) β†’ 𝑧 ∈ 𝑋)
723, 9, 54grplid 18851 . . . . . . . . . . 11 ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋) β†’ ((0gβ€˜πΊ) + 𝑧) = 𝑧)
7353, 71, 72syl2an2r 683 . . . . . . . . . 10 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ 𝑧 ∈ π‘Ž) β†’ ((0gβ€˜πΊ) + 𝑧) = 𝑧)
7473mpteq2dva 5248 . . . . . . . . 9 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ (𝑧 ∈ π‘Ž ↦ ((0gβ€˜πΊ) + 𝑧)) = (𝑧 ∈ π‘Ž ↦ 𝑧))
75 mptresid 6050 . . . . . . . . 9 ( I β†Ύ π‘Ž) = (𝑧 ∈ π‘Ž ↦ 𝑧)
7674, 75eqtr4di 2790 . . . . . . . 8 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ (𝑧 ∈ π‘Ž ↦ ((0gβ€˜πΊ) + 𝑧)) = ( I β†Ύ π‘Ž))
7776rneqd 5937 . . . . . . 7 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ ran (𝑧 ∈ π‘Ž ↦ ((0gβ€˜πΊ) + 𝑧)) = ran ( I β†Ύ π‘Ž))
78 rnresi 6074 . . . . . . 7 ran ( I β†Ύ π‘Ž) = π‘Ž
7977, 78eqtrdi 2788 . . . . . 6 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ ran (𝑧 ∈ π‘Ž ↦ ((0gβ€˜πΊ) + 𝑧)) = π‘Ž)
8067, 79eqtrd 2772 . . . . 5 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ ((0gβ€˜πΊ) βŠ• π‘Ž) = π‘Ž)
81 ovex 7441 . . . . . . . . . 10 (𝑐 + 𝑧) ∈ V
82 oveq2 7416 . . . . . . . . . 10 (𝑀 = (𝑐 + 𝑧) β†’ (𝑏 + 𝑀) = (𝑏 + (𝑐 + 𝑧)))
8381, 82abrexco 7242 . . . . . . . . 9 {𝑒 ∣ βˆƒπ‘€ ∈ {𝑣 ∣ βˆƒπ‘§ ∈ π‘Ž 𝑣 = (𝑐 + 𝑧)}𝑒 = (𝑏 + 𝑀)} = {𝑒 ∣ βˆƒπ‘§ ∈ π‘Ž 𝑒 = (𝑏 + (𝑐 + 𝑧))}
84 simprr 771 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ 𝑐 ∈ 𝑋)
8557adantr 481 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ π‘Ž ∈ 𝑆)
86 simpr 485 . . . . . . . . . . . . . . . 16 ((π‘₯ = 𝑐 ∧ 𝑦 = π‘Ž) β†’ 𝑦 = π‘Ž)
87 simpl 483 . . . . . . . . . . . . . . . . 17 ((π‘₯ = 𝑐 ∧ 𝑦 = π‘Ž) β†’ π‘₯ = 𝑐)
8887oveq1d 7423 . . . . . . . . . . . . . . . 16 ((π‘₯ = 𝑐 ∧ 𝑦 = π‘Ž) β†’ (π‘₯ + 𝑧) = (𝑐 + 𝑧))
8986, 88mpteq12dv 5239 . . . . . . . . . . . . . . 15 ((π‘₯ = 𝑐 ∧ 𝑦 = π‘Ž) β†’ (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) = (𝑧 ∈ π‘Ž ↦ (𝑐 + 𝑧)))
9089rneqd 5937 . . . . . . . . . . . . . 14 ((π‘₯ = 𝑐 ∧ 𝑦 = π‘Ž) β†’ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) = ran (𝑧 ∈ π‘Ž ↦ (𝑐 + 𝑧)))
9163mptex 7224 . . . . . . . . . . . . . . 15 (𝑧 ∈ π‘Ž ↦ (𝑐 + 𝑧)) ∈ V
9291rnex 7902 . . . . . . . . . . . . . 14 ran (𝑧 ∈ π‘Ž ↦ (𝑐 + 𝑧)) ∈ V
9390, 50, 92ovmpoa 7562 . . . . . . . . . . . . 13 ((𝑐 ∈ 𝑋 ∧ π‘Ž ∈ 𝑆) β†’ (𝑐 βŠ• π‘Ž) = ran (𝑧 ∈ π‘Ž ↦ (𝑐 + 𝑧)))
9484, 85, 93syl2anc 584 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ (𝑐 βŠ• π‘Ž) = ran (𝑧 ∈ π‘Ž ↦ (𝑐 + 𝑧)))
95 eqid 2732 . . . . . . . . . . . . 13 (𝑧 ∈ π‘Ž ↦ (𝑐 + 𝑧)) = (𝑧 ∈ π‘Ž ↦ (𝑐 + 𝑧))
9695rnmpt 5954 . . . . . . . . . . . 12 ran (𝑧 ∈ π‘Ž ↦ (𝑐 + 𝑧)) = {𝑣 ∣ βˆƒπ‘§ ∈ π‘Ž 𝑣 = (𝑐 + 𝑧)}
9794, 96eqtrdi 2788 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ (𝑐 βŠ• π‘Ž) = {𝑣 ∣ βˆƒπ‘§ ∈ π‘Ž 𝑣 = (𝑐 + 𝑧)})
9897rexeqdv 3326 . . . . . . . . . 10 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ (βˆƒπ‘€ ∈ (𝑐 βŠ• π‘Ž)𝑒 = (𝑏 + 𝑀) ↔ βˆƒπ‘€ ∈ {𝑣 ∣ βˆƒπ‘§ ∈ π‘Ž 𝑣 = (𝑐 + 𝑧)}𝑒 = (𝑏 + 𝑀)))
9998abbidv 2801 . . . . . . . . 9 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ {𝑒 ∣ βˆƒπ‘€ ∈ (𝑐 βŠ• π‘Ž)𝑒 = (𝑏 + 𝑀)} = {𝑒 ∣ βˆƒπ‘€ ∈ {𝑣 ∣ βˆƒπ‘§ ∈ π‘Ž 𝑣 = (𝑐 + 𝑧)}𝑒 = (𝑏 + 𝑀)})
10053ad2antrr 724 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ π‘Ž) β†’ 𝐺 ∈ Grp)
101 simprl 769 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ 𝑏 ∈ 𝑋)
102101adantr 481 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ π‘Ž) β†’ 𝑏 ∈ 𝑋)
10384adantr 481 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ π‘Ž) β†’ 𝑐 ∈ 𝑋)
10471adantlr 713 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ π‘Ž) β†’ 𝑧 ∈ 𝑋)
1053, 9grpass 18827 . . . . . . . . . . . . 13 ((𝐺 ∈ Grp ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) β†’ ((𝑏 + 𝑐) + 𝑧) = (𝑏 + (𝑐 + 𝑧)))
106100, 102, 103, 104, 105syl13anc 1372 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ π‘Ž) β†’ ((𝑏 + 𝑐) + 𝑧) = (𝑏 + (𝑐 + 𝑧)))
107106eqeq2d 2743 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ π‘Ž) β†’ (𝑒 = ((𝑏 + 𝑐) + 𝑧) ↔ 𝑒 = (𝑏 + (𝑐 + 𝑧))))
108107rexbidva 3176 . . . . . . . . . 10 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ (βˆƒπ‘§ ∈ π‘Ž 𝑒 = ((𝑏 + 𝑐) + 𝑧) ↔ βˆƒπ‘§ ∈ π‘Ž 𝑒 = (𝑏 + (𝑐 + 𝑧))))
109108abbidv 2801 . . . . . . . . 9 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ {𝑒 ∣ βˆƒπ‘§ ∈ π‘Ž 𝑒 = ((𝑏 + 𝑐) + 𝑧)} = {𝑒 ∣ βˆƒπ‘§ ∈ π‘Ž 𝑒 = (𝑏 + (𝑐 + 𝑧))})
11083, 99, 1093eqtr4a 2798 . . . . . . . 8 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ {𝑒 ∣ βˆƒπ‘€ ∈ (𝑐 βŠ• π‘Ž)𝑒 = (𝑏 + 𝑀)} = {𝑒 ∣ βˆƒπ‘§ ∈ π‘Ž 𝑒 = ((𝑏 + 𝑐) + 𝑧)})
111 eqid 2732 . . . . . . . . 9 (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀)) = (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀))
112111rnmpt 5954 . . . . . . . 8 ran (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀)) = {𝑒 ∣ βˆƒπ‘€ ∈ (𝑐 βŠ• π‘Ž)𝑒 = (𝑏 + 𝑀)}
113 eqid 2732 . . . . . . . . 9 (𝑧 ∈ π‘Ž ↦ ((𝑏 + 𝑐) + 𝑧)) = (𝑧 ∈ π‘Ž ↦ ((𝑏 + 𝑐) + 𝑧))
114113rnmpt 5954 . . . . . . . 8 ran (𝑧 ∈ π‘Ž ↦ ((𝑏 + 𝑐) + 𝑧)) = {𝑒 ∣ βˆƒπ‘§ ∈ π‘Ž 𝑒 = ((𝑏 + 𝑐) + 𝑧)}
115110, 112, 1143eqtr4g 2797 . . . . . . 7 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ ran (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀)) = ran (𝑧 ∈ π‘Ž ↦ ((𝑏 + 𝑐) + 𝑧)))
11652ad2antrr 724 . . . . . . . . 9 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ βŠ• :(𝑋 Γ— 𝑆)βŸΆπ‘†)
117116, 84, 85fovcdmd 7578 . . . . . . . 8 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ (𝑐 βŠ• π‘Ž) ∈ 𝑆)
118 simpr 485 . . . . . . . . . . . 12 ((π‘₯ = 𝑏 ∧ 𝑦 = (𝑐 βŠ• π‘Ž)) β†’ 𝑦 = (𝑐 βŠ• π‘Ž))
119 simpl 483 . . . . . . . . . . . . 13 ((π‘₯ = 𝑏 ∧ 𝑦 = (𝑐 βŠ• π‘Ž)) β†’ π‘₯ = 𝑏)
120119oveq1d 7423 . . . . . . . . . . . 12 ((π‘₯ = 𝑏 ∧ 𝑦 = (𝑐 βŠ• π‘Ž)) β†’ (π‘₯ + 𝑧) = (𝑏 + 𝑧))
121118, 120mpteq12dv 5239 . . . . . . . . . . 11 ((π‘₯ = 𝑏 ∧ 𝑦 = (𝑐 βŠ• π‘Ž)) β†’ (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) = (𝑧 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑧)))
122 oveq2 7416 . . . . . . . . . . . 12 (𝑧 = 𝑀 β†’ (𝑏 + 𝑧) = (𝑏 + 𝑀))
123122cbvmptv 5261 . . . . . . . . . . 11 (𝑧 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑧)) = (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀))
124121, 123eqtrdi 2788 . . . . . . . . . 10 ((π‘₯ = 𝑏 ∧ 𝑦 = (𝑐 βŠ• π‘Ž)) β†’ (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) = (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀)))
125124rneqd 5937 . . . . . . . . 9 ((π‘₯ = 𝑏 ∧ 𝑦 = (𝑐 βŠ• π‘Ž)) β†’ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) = ran (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀)))
126 ovex 7441 . . . . . . . . . . 11 (𝑐 βŠ• π‘Ž) ∈ V
127126mptex 7224 . . . . . . . . . 10 (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀)) ∈ V
128127rnex 7902 . . . . . . . . 9 ran (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀)) ∈ V
129125, 50, 128ovmpoa 7562 . . . . . . . 8 ((𝑏 ∈ 𝑋 ∧ (𝑐 βŠ• π‘Ž) ∈ 𝑆) β†’ (𝑏 βŠ• (𝑐 βŠ• π‘Ž)) = ran (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀)))
130101, 117, 129syl2anc 584 . . . . . . 7 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ (𝑏 βŠ• (𝑐 βŠ• π‘Ž)) = ran (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀)))
1311ad2antrr 724 . . . . . . . . 9 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ 𝐺 ∈ Grp)
1323, 9grpcl 18826 . . . . . . . . 9 ((𝐺 ∈ Grp ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋) β†’ (𝑏 + 𝑐) ∈ 𝑋)
133131, 101, 84, 132syl3anc 1371 . . . . . . . 8 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ (𝑏 + 𝑐) ∈ 𝑋)
134 simpr 485 . . . . . . . . . . 11 ((π‘₯ = (𝑏 + 𝑐) ∧ 𝑦 = π‘Ž) β†’ 𝑦 = π‘Ž)
135 simpl 483 . . . . . . . . . . . 12 ((π‘₯ = (𝑏 + 𝑐) ∧ 𝑦 = π‘Ž) β†’ π‘₯ = (𝑏 + 𝑐))
136135oveq1d 7423 . . . . . . . . . . 11 ((π‘₯ = (𝑏 + 𝑐) ∧ 𝑦 = π‘Ž) β†’ (π‘₯ + 𝑧) = ((𝑏 + 𝑐) + 𝑧))
137134, 136mpteq12dv 5239 . . . . . . . . . 10 ((π‘₯ = (𝑏 + 𝑐) ∧ 𝑦 = π‘Ž) β†’ (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) = (𝑧 ∈ π‘Ž ↦ ((𝑏 + 𝑐) + 𝑧)))
138137rneqd 5937 . . . . . . . . 9 ((π‘₯ = (𝑏 + 𝑐) ∧ 𝑦 = π‘Ž) β†’ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) = ran (𝑧 ∈ π‘Ž ↦ ((𝑏 + 𝑐) + 𝑧)))
13963mptex 7224 . . . . . . . . . 10 (𝑧 ∈ π‘Ž ↦ ((𝑏 + 𝑐) + 𝑧)) ∈ V
140139rnex 7902 . . . . . . . . 9 ran (𝑧 ∈ π‘Ž ↦ ((𝑏 + 𝑐) + 𝑧)) ∈ V
141138, 50, 140ovmpoa 7562 . . . . . . . 8 (((𝑏 + 𝑐) ∈ 𝑋 ∧ π‘Ž ∈ 𝑆) β†’ ((𝑏 + 𝑐) βŠ• π‘Ž) = ran (𝑧 ∈ π‘Ž ↦ ((𝑏 + 𝑐) + 𝑧)))
142133, 85, 141syl2anc 584 . . . . . . 7 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ ((𝑏 + 𝑐) βŠ• π‘Ž) = ran (𝑧 ∈ π‘Ž ↦ ((𝑏 + 𝑐) + 𝑧)))
143115, 130, 1423eqtr4rd 2783 . . . . . 6 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ ((𝑏 + 𝑐) βŠ• π‘Ž) = (𝑏 βŠ• (𝑐 βŠ• π‘Ž)))
144143ralrimivva 3200 . . . . 5 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ βˆ€π‘ ∈ 𝑋 βˆ€π‘ ∈ 𝑋 ((𝑏 + 𝑐) βŠ• π‘Ž) = (𝑏 βŠ• (𝑐 βŠ• π‘Ž)))
14580, 144jca 512 . . . 4 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ (((0gβ€˜πΊ) βŠ• π‘Ž) = π‘Ž ∧ βˆ€π‘ ∈ 𝑋 βˆ€π‘ ∈ 𝑋 ((𝑏 + 𝑐) βŠ• π‘Ž) = (𝑏 βŠ• (𝑐 βŠ• π‘Ž))))
146145ralrimiva 3146 . . 3 (πœ‘ β†’ βˆ€π‘Ž ∈ 𝑆 (((0gβ€˜πΊ) βŠ• π‘Ž) = π‘Ž ∧ βˆ€π‘ ∈ 𝑋 βˆ€π‘ ∈ 𝑋 ((𝑏 + 𝑐) βŠ• π‘Ž) = (𝑏 βŠ• (𝑐 βŠ• π‘Ž))))
14752, 146jca 512 . 2 (πœ‘ β†’ ( βŠ• :(𝑋 Γ— 𝑆)βŸΆπ‘† ∧ βˆ€π‘Ž ∈ 𝑆 (((0gβ€˜πΊ) βŠ• π‘Ž) = π‘Ž ∧ βˆ€π‘ ∈ 𝑋 βˆ€π‘ ∈ 𝑋 ((𝑏 + 𝑐) βŠ• π‘Ž) = (𝑏 βŠ• (𝑐 βŠ• π‘Ž)))))
1483, 9, 54isga 19154 . 2 ( βŠ• ∈ (𝐺 GrpAct 𝑆) ↔ ((𝐺 ∈ Grp ∧ 𝑆 ∈ V) ∧ ( βŠ• :(𝑋 Γ— 𝑆)βŸΆπ‘† ∧ βˆ€π‘Ž ∈ 𝑆 (((0gβ€˜πΊ) βŠ• π‘Ž) = π‘Ž ∧ βˆ€π‘ ∈ 𝑋 βˆ€π‘ ∈ 𝑋 ((𝑏 + 𝑐) βŠ• π‘Ž) = (𝑏 βŠ• (𝑐 βŠ• π‘Ž))))))
1497, 147, 148sylanbrc 583 1 (πœ‘ β†’ βŠ• ∈ (𝐺 GrpAct 𝑆))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {cab 2709  βˆ€wral 3061  βˆƒwrex 3070  {crab 3432  Vcvv 3474   βŠ† wss 3948  π’« cpw 4602   class class class wbr 5148   ↦ cmpt 5231   I cid 5573   Γ— cxp 5674  ran crn 5677   β†Ύ cres 5678  βŸΆwf 6539  β€“1-1β†’wf1 6540  β€“1-1-ontoβ†’wf1o 6542  β€˜cfv 6543  (class class class)co 7408   ∈ cmpo 7410   β‰ˆ cen 8935  Fincfn 8938  β„•0cn0 12471  β†‘cexp 14026  β™―chash 14289   βˆ₯ cdvds 16196  β„™cprime 16607  Basecbs 17143  +gcplusg 17196  0gc0g 17384  Grpcgrp 18818   GrpAct cga 19152
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724  ax-cnex 11165  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185  ax-pre-mulgt0 11186
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7364  df-ov 7411  df-oprab 7412  df-mpo 7413  df-om 7855  df-1st 7974  df-2nd 7975  df-frecs 8265  df-wrecs 8296  df-recs 8370  df-rdg 8409  df-1o 8465  df-er 8702  df-map 8821  df-en 8939  df-dom 8940  df-sdom 8941  df-fin 8942  df-card 9933  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11445  df-neg 11446  df-nn 12212  df-n0 12472  df-z 12558  df-uz 12822  df-hash 14290  df-0g 17386  df-mgm 18560  df-sgrp 18609  df-mnd 18625  df-grp 18821  df-minusg 18822  df-ga 19153
This theorem is referenced by:  sylow1lem3  19467  sylow1lem5  19469
  Copyright terms: Public domain W3C validator