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

Theorem sylow1lem2 19389
Description: Lemma for sylow1 19393. 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 6860 . . . . 5 𝑋 ∈ V
54pwex 5339 . . . 4 𝒫 𝑋 ∈ V
62, 5rabex2 5295 . . 3 𝑆 ∈ V
71, 6jctir 522 . 2 (πœ‘ β†’ (𝐺 ∈ Grp ∧ 𝑆 ∈ V))
8 simprl 770 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ π‘₯ ∈ 𝑋)
9 sylow1lem.a . . . . . . . . . . . . 13 + = (+gβ€˜πΊ)
10 eqid 2733 . . . . . . . . . . . . 13 (𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)) = (𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧))
113, 9, 10grplmulf1o 18829 . . . . . . . . . . . 12 ((𝐺 ∈ Grp ∧ π‘₯ ∈ 𝑋) β†’ (𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)):𝑋–1-1-onto→𝑋)
121, 8, 11syl2an2r 684 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ (𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)):𝑋–1-1-onto→𝑋)
13 f1of1 6787 . . . . . . . . . . 11 ((𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)):𝑋–1-1-onto→𝑋 β†’ (𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)):𝑋–1-1→𝑋)
1412, 13syl 17 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ (𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)):𝑋–1-1→𝑋)
15 simprr 772 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ 𝑦 ∈ 𝑆)
16 fveqeq2 6855 . . . . . . . . . . . . . 14 (𝑠 = 𝑦 β†’ ((β™―β€˜π‘ ) = (𝑃↑𝑁) ↔ (β™―β€˜π‘¦) = (𝑃↑𝑁)))
1716, 2elrab2 3652 . . . . . . . . . . . . 13 (𝑦 ∈ 𝑆 ↔ (𝑦 ∈ 𝒫 𝑋 ∧ (β™―β€˜π‘¦) = (𝑃↑𝑁)))
1815, 17sylib 217 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ (𝑦 ∈ 𝒫 𝑋 ∧ (β™―β€˜π‘¦) = (𝑃↑𝑁)))
1918simpld 496 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ 𝑦 ∈ 𝒫 𝑋)
2019elpwid 4573 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ 𝑦 βŠ† 𝑋)
21 f1ssres 6750 . . . . . . . . . 10 (((𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)):𝑋–1-1→𝑋 ∧ 𝑦 βŠ† 𝑋) β†’ ((𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)) β†Ύ 𝑦):𝑦–1-1→𝑋)
2214, 20, 21syl2anc 585 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ ((𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)) β†Ύ 𝑦):𝑦–1-1→𝑋)
23 resmpt 5995 . . . . . . . . . 10 (𝑦 βŠ† 𝑋 β†’ ((𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)) β†Ύ 𝑦) = (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)))
24 f1eq1 6737 . . . . . . . . . 10 (((𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)) β†Ύ 𝑦) = (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) β†’ (((𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)) β†Ύ 𝑦):𝑦–1-1→𝑋 ↔ (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)):𝑦–1-1→𝑋))
2520, 23, 243syl 18 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ (((𝑧 ∈ 𝑋 ↦ (π‘₯ + 𝑧)) β†Ύ 𝑦):𝑦–1-1→𝑋 ↔ (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)):𝑦–1-1→𝑋))
2622, 25mpbid 231 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)):𝑦–1-1→𝑋)
27 f1f 6742 . . . . . . . 8 ((𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)):𝑦–1-1→𝑋 β†’ (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)):π‘¦βŸΆπ‘‹)
28 frn 6679 . . . . . . . 8 ((𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)):π‘¦βŸΆπ‘‹ β†’ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) βŠ† 𝑋)
2926, 27, 283syl 18 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) βŠ† 𝑋)
304elpw2 5306 . . . . . . 7 (ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) ∈ 𝒫 𝑋 ↔ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) βŠ† 𝑋)
3129, 30sylibr 233 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) ∈ 𝒫 𝑋)
32 f1f1orn 6799 . . . . . . . . 9 ((𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)):𝑦–1-1→𝑋 β†’ (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)):𝑦–1-1-ontoβ†’ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)))
33 vex 3451 . . . . . . . . . 10 𝑦 ∈ V
3433f1oen 8919 . . . . . . . . 9 ((𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)):𝑦–1-1-ontoβ†’ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) β†’ 𝑦 β‰ˆ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)))
3526, 32, 343syl 18 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ 𝑦 β‰ˆ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)))
36 sylow1.f . . . . . . . . . 10 (πœ‘ β†’ 𝑋 ∈ Fin)
37 ssfi 9123 . . . . . . . . . 10 ((𝑋 ∈ Fin ∧ 𝑦 βŠ† 𝑋) β†’ 𝑦 ∈ Fin)
3836, 20, 37syl2an2r 684 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ 𝑦 ∈ Fin)
39 ssfi 9123 . . . . . . . . . 10 ((𝑋 ∈ Fin ∧ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) βŠ† 𝑋) β†’ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) ∈ Fin)
4036, 29, 39syl2an2r 684 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) ∈ Fin)
41 hashen 14256 . . . . . . . . 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 6855 . . . . . . 7 (𝑠 = ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) β†’ ((β™―β€˜π‘ ) = (𝑃↑𝑁) ↔ (β™―β€˜ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧))) = (𝑃↑𝑁)))
4746, 2elrab2 3652 . . . . . 6 (ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) ∈ 𝑆 ↔ (ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) ∈ 𝒫 𝑋 ∧ (β™―β€˜ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧))) = (𝑃↑𝑁)))
4831, 45, 47sylanbrc 584 . . . . 5 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑆)) β†’ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) ∈ 𝑆)
4948ralrimivva 3194 . . . 4 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ 𝑆 ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) ∈ 𝑆)
50 sylow1lem.m . . . . 5 βŠ• = (π‘₯ ∈ 𝑋, 𝑦 ∈ 𝑆 ↦ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)))
5150fmpo 8004 . . . 4 (βˆ€π‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ 𝑆 ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) ∈ 𝑆 ↔ βŠ• :(𝑋 Γ— 𝑆)βŸΆπ‘†)
5249, 51sylib 217 . . 3 (πœ‘ β†’ βŠ• :(𝑋 Γ— 𝑆)βŸΆπ‘†)
531adantr 482 . . . . . . . 8 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ 𝐺 ∈ Grp)
54 eqid 2733 . . . . . . . . 9 (0gβ€˜πΊ) = (0gβ€˜πΊ)
553, 54grpidcl 18786 . . . . . . . 8 (𝐺 ∈ Grp β†’ (0gβ€˜πΊ) ∈ 𝑋)
5653, 55syl 17 . . . . . . 7 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ (0gβ€˜πΊ) ∈ 𝑋)
57 simpr 486 . . . . . . 7 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ π‘Ž ∈ 𝑆)
58 simpr 486 . . . . . . . . . 10 ((π‘₯ = (0gβ€˜πΊ) ∧ 𝑦 = π‘Ž) β†’ 𝑦 = π‘Ž)
59 simpl 484 . . . . . . . . . . 11 ((π‘₯ = (0gβ€˜πΊ) ∧ 𝑦 = π‘Ž) β†’ π‘₯ = (0gβ€˜πΊ))
6059oveq1d 7376 . . . . . . . . . 10 ((π‘₯ = (0gβ€˜πΊ) ∧ 𝑦 = π‘Ž) β†’ (π‘₯ + 𝑧) = ((0gβ€˜πΊ) + 𝑧))
6158, 60mpteq12dv 5200 . . . . . . . . 9 ((π‘₯ = (0gβ€˜πΊ) ∧ 𝑦 = π‘Ž) β†’ (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) = (𝑧 ∈ π‘Ž ↦ ((0gβ€˜πΊ) + 𝑧)))
6261rneqd 5897 . . . . . . . 8 ((π‘₯ = (0gβ€˜πΊ) ∧ 𝑦 = π‘Ž) β†’ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) = ran (𝑧 ∈ π‘Ž ↦ ((0gβ€˜πΊ) + 𝑧)))
63 vex 3451 . . . . . . . . . 10 π‘Ž ∈ V
6463mptex 7177 . . . . . . . . 9 (𝑧 ∈ π‘Ž ↦ ((0gβ€˜πΊ) + 𝑧)) ∈ V
6564rnex 7853 . . . . . . . 8 ran (𝑧 ∈ π‘Ž ↦ ((0gβ€˜πΊ) + 𝑧)) ∈ V
6662, 50, 65ovmpoa 7514 . . . . . . 7 (((0gβ€˜πΊ) ∈ 𝑋 ∧ π‘Ž ∈ 𝑆) β†’ ((0gβ€˜πΊ) βŠ• π‘Ž) = ran (𝑧 ∈ π‘Ž ↦ ((0gβ€˜πΊ) + 𝑧)))
6756, 57, 66syl2anc 585 . . . . . 6 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ ((0gβ€˜πΊ) βŠ• π‘Ž) = ran (𝑧 ∈ π‘Ž ↦ ((0gβ€˜πΊ) + 𝑧)))
682ssrab3 4044 . . . . . . . . . . . . . 14 𝑆 βŠ† 𝒫 𝑋
6968, 57sselid 3946 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ π‘Ž ∈ 𝒫 𝑋)
7069elpwid 4573 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ π‘Ž βŠ† 𝑋)
7170sselda 3948 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ 𝑧 ∈ π‘Ž) β†’ 𝑧 ∈ 𝑋)
723, 9, 54grplid 18788 . . . . . . . . . . 11 ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋) β†’ ((0gβ€˜πΊ) + 𝑧) = 𝑧)
7353, 71, 72syl2an2r 684 . . . . . . . . . 10 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ 𝑧 ∈ π‘Ž) β†’ ((0gβ€˜πΊ) + 𝑧) = 𝑧)
7473mpteq2dva 5209 . . . . . . . . 9 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ (𝑧 ∈ π‘Ž ↦ ((0gβ€˜πΊ) + 𝑧)) = (𝑧 ∈ π‘Ž ↦ 𝑧))
75 mptresid 6008 . . . . . . . . 9 ( I β†Ύ π‘Ž) = (𝑧 ∈ π‘Ž ↦ 𝑧)
7674, 75eqtr4di 2791 . . . . . . . 8 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ (𝑧 ∈ π‘Ž ↦ ((0gβ€˜πΊ) + 𝑧)) = ( I β†Ύ π‘Ž))
7776rneqd 5897 . . . . . . 7 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ ran (𝑧 ∈ π‘Ž ↦ ((0gβ€˜πΊ) + 𝑧)) = ran ( I β†Ύ π‘Ž))
78 rnresi 6031 . . . . . . 7 ran ( I β†Ύ π‘Ž) = π‘Ž
7977, 78eqtrdi 2789 . . . . . 6 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ ran (𝑧 ∈ π‘Ž ↦ ((0gβ€˜πΊ) + 𝑧)) = π‘Ž)
8067, 79eqtrd 2773 . . . . 5 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ ((0gβ€˜πΊ) βŠ• π‘Ž) = π‘Ž)
81 ovex 7394 . . . . . . . . . 10 (𝑐 + 𝑧) ∈ V
82 oveq2 7369 . . . . . . . . . 10 (𝑀 = (𝑐 + 𝑧) β†’ (𝑏 + 𝑀) = (𝑏 + (𝑐 + 𝑧)))
8381, 82abrexco 7195 . . . . . . . . 9 {𝑒 ∣ βˆƒπ‘€ ∈ {𝑣 ∣ βˆƒπ‘§ ∈ π‘Ž 𝑣 = (𝑐 + 𝑧)}𝑒 = (𝑏 + 𝑀)} = {𝑒 ∣ βˆƒπ‘§ ∈ π‘Ž 𝑒 = (𝑏 + (𝑐 + 𝑧))}
84 simprr 772 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ 𝑐 ∈ 𝑋)
8557adantr 482 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ π‘Ž ∈ 𝑆)
86 simpr 486 . . . . . . . . . . . . . . . 16 ((π‘₯ = 𝑐 ∧ 𝑦 = π‘Ž) β†’ 𝑦 = π‘Ž)
87 simpl 484 . . . . . . . . . . . . . . . . 17 ((π‘₯ = 𝑐 ∧ 𝑦 = π‘Ž) β†’ π‘₯ = 𝑐)
8887oveq1d 7376 . . . . . . . . . . . . . . . 16 ((π‘₯ = 𝑐 ∧ 𝑦 = π‘Ž) β†’ (π‘₯ + 𝑧) = (𝑐 + 𝑧))
8986, 88mpteq12dv 5200 . . . . . . . . . . . . . . 15 ((π‘₯ = 𝑐 ∧ 𝑦 = π‘Ž) β†’ (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) = (𝑧 ∈ π‘Ž ↦ (𝑐 + 𝑧)))
9089rneqd 5897 . . . . . . . . . . . . . 14 ((π‘₯ = 𝑐 ∧ 𝑦 = π‘Ž) β†’ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) = ran (𝑧 ∈ π‘Ž ↦ (𝑐 + 𝑧)))
9163mptex 7177 . . . . . . . . . . . . . . 15 (𝑧 ∈ π‘Ž ↦ (𝑐 + 𝑧)) ∈ V
9291rnex 7853 . . . . . . . . . . . . . 14 ran (𝑧 ∈ π‘Ž ↦ (𝑐 + 𝑧)) ∈ V
9390, 50, 92ovmpoa 7514 . . . . . . . . . . . . 13 ((𝑐 ∈ 𝑋 ∧ π‘Ž ∈ 𝑆) β†’ (𝑐 βŠ• π‘Ž) = ran (𝑧 ∈ π‘Ž ↦ (𝑐 + 𝑧)))
9484, 85, 93syl2anc 585 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ (𝑐 βŠ• π‘Ž) = ran (𝑧 ∈ π‘Ž ↦ (𝑐 + 𝑧)))
95 eqid 2733 . . . . . . . . . . . . 13 (𝑧 ∈ π‘Ž ↦ (𝑐 + 𝑧)) = (𝑧 ∈ π‘Ž ↦ (𝑐 + 𝑧))
9695rnmpt 5914 . . . . . . . . . . . 12 ran (𝑧 ∈ π‘Ž ↦ (𝑐 + 𝑧)) = {𝑣 ∣ βˆƒπ‘§ ∈ π‘Ž 𝑣 = (𝑐 + 𝑧)}
9794, 96eqtrdi 2789 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ (𝑐 βŠ• π‘Ž) = {𝑣 ∣ βˆƒπ‘§ ∈ π‘Ž 𝑣 = (𝑐 + 𝑧)})
9897rexeqdv 3313 . . . . . . . . . 10 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ (βˆƒπ‘€ ∈ (𝑐 βŠ• π‘Ž)𝑒 = (𝑏 + 𝑀) ↔ βˆƒπ‘€ ∈ {𝑣 ∣ βˆƒπ‘§ ∈ π‘Ž 𝑣 = (𝑐 + 𝑧)}𝑒 = (𝑏 + 𝑀)))
9998abbidv 2802 . . . . . . . . 9 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ {𝑒 ∣ βˆƒπ‘€ ∈ (𝑐 βŠ• π‘Ž)𝑒 = (𝑏 + 𝑀)} = {𝑒 ∣ βˆƒπ‘€ ∈ {𝑣 ∣ βˆƒπ‘§ ∈ π‘Ž 𝑣 = (𝑐 + 𝑧)}𝑒 = (𝑏 + 𝑀)})
10053ad2antrr 725 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ π‘Ž) β†’ 𝐺 ∈ Grp)
101 simprl 770 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ 𝑏 ∈ 𝑋)
102101adantr 482 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ π‘Ž) β†’ 𝑏 ∈ 𝑋)
10384adantr 482 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ π‘Ž) β†’ 𝑐 ∈ 𝑋)
10471adantlr 714 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ π‘Ž) β†’ 𝑧 ∈ 𝑋)
1053, 9grpass 18765 . . . . . . . . . . . . 13 ((𝐺 ∈ Grp ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) β†’ ((𝑏 + 𝑐) + 𝑧) = (𝑏 + (𝑐 + 𝑧)))
106100, 102, 103, 104, 105syl13anc 1373 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ π‘Ž) β†’ ((𝑏 + 𝑐) + 𝑧) = (𝑏 + (𝑐 + 𝑧)))
107106eqeq2d 2744 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ π‘Ž) β†’ (𝑒 = ((𝑏 + 𝑐) + 𝑧) ↔ 𝑒 = (𝑏 + (𝑐 + 𝑧))))
108107rexbidva 3170 . . . . . . . . . 10 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ (βˆƒπ‘§ ∈ π‘Ž 𝑒 = ((𝑏 + 𝑐) + 𝑧) ↔ βˆƒπ‘§ ∈ π‘Ž 𝑒 = (𝑏 + (𝑐 + 𝑧))))
109108abbidv 2802 . . . . . . . . 9 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ {𝑒 ∣ βˆƒπ‘§ ∈ π‘Ž 𝑒 = ((𝑏 + 𝑐) + 𝑧)} = {𝑒 ∣ βˆƒπ‘§ ∈ π‘Ž 𝑒 = (𝑏 + (𝑐 + 𝑧))})
11083, 99, 1093eqtr4a 2799 . . . . . . . 8 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ {𝑒 ∣ βˆƒπ‘€ ∈ (𝑐 βŠ• π‘Ž)𝑒 = (𝑏 + 𝑀)} = {𝑒 ∣ βˆƒπ‘§ ∈ π‘Ž 𝑒 = ((𝑏 + 𝑐) + 𝑧)})
111 eqid 2733 . . . . . . . . 9 (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀)) = (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀))
112111rnmpt 5914 . . . . . . . 8 ran (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀)) = {𝑒 ∣ βˆƒπ‘€ ∈ (𝑐 βŠ• π‘Ž)𝑒 = (𝑏 + 𝑀)}
113 eqid 2733 . . . . . . . . 9 (𝑧 ∈ π‘Ž ↦ ((𝑏 + 𝑐) + 𝑧)) = (𝑧 ∈ π‘Ž ↦ ((𝑏 + 𝑐) + 𝑧))
114113rnmpt 5914 . . . . . . . 8 ran (𝑧 ∈ π‘Ž ↦ ((𝑏 + 𝑐) + 𝑧)) = {𝑒 ∣ βˆƒπ‘§ ∈ π‘Ž 𝑒 = ((𝑏 + 𝑐) + 𝑧)}
115110, 112, 1143eqtr4g 2798 . . . . . . 7 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ ran (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀)) = ran (𝑧 ∈ π‘Ž ↦ ((𝑏 + 𝑐) + 𝑧)))
11652ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ βŠ• :(𝑋 Γ— 𝑆)βŸΆπ‘†)
117116, 84, 85fovcdmd 7530 . . . . . . . 8 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ (𝑐 βŠ• π‘Ž) ∈ 𝑆)
118 simpr 486 . . . . . . . . . . . 12 ((π‘₯ = 𝑏 ∧ 𝑦 = (𝑐 βŠ• π‘Ž)) β†’ 𝑦 = (𝑐 βŠ• π‘Ž))
119 simpl 484 . . . . . . . . . . . . 13 ((π‘₯ = 𝑏 ∧ 𝑦 = (𝑐 βŠ• π‘Ž)) β†’ π‘₯ = 𝑏)
120119oveq1d 7376 . . . . . . . . . . . 12 ((π‘₯ = 𝑏 ∧ 𝑦 = (𝑐 βŠ• π‘Ž)) β†’ (π‘₯ + 𝑧) = (𝑏 + 𝑧))
121118, 120mpteq12dv 5200 . . . . . . . . . . 11 ((π‘₯ = 𝑏 ∧ 𝑦 = (𝑐 βŠ• π‘Ž)) β†’ (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) = (𝑧 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑧)))
122 oveq2 7369 . . . . . . . . . . . 12 (𝑧 = 𝑀 β†’ (𝑏 + 𝑧) = (𝑏 + 𝑀))
123122cbvmptv 5222 . . . . . . . . . . 11 (𝑧 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑧)) = (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀))
124121, 123eqtrdi 2789 . . . . . . . . . 10 ((π‘₯ = 𝑏 ∧ 𝑦 = (𝑐 βŠ• π‘Ž)) β†’ (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) = (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀)))
125124rneqd 5897 . . . . . . . . 9 ((π‘₯ = 𝑏 ∧ 𝑦 = (𝑐 βŠ• π‘Ž)) β†’ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) = ran (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀)))
126 ovex 7394 . . . . . . . . . . 11 (𝑐 βŠ• π‘Ž) ∈ V
127126mptex 7177 . . . . . . . . . 10 (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀)) ∈ V
128127rnex 7853 . . . . . . . . 9 ran (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀)) ∈ V
129125, 50, 128ovmpoa 7514 . . . . . . . 8 ((𝑏 ∈ 𝑋 ∧ (𝑐 βŠ• π‘Ž) ∈ 𝑆) β†’ (𝑏 βŠ• (𝑐 βŠ• π‘Ž)) = ran (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀)))
130101, 117, 129syl2anc 585 . . . . . . 7 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ (𝑏 βŠ• (𝑐 βŠ• π‘Ž)) = ran (𝑀 ∈ (𝑐 βŠ• π‘Ž) ↦ (𝑏 + 𝑀)))
1311ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ 𝐺 ∈ Grp)
1323, 9grpcl 18764 . . . . . . . . 9 ((𝐺 ∈ Grp ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋) β†’ (𝑏 + 𝑐) ∈ 𝑋)
133131, 101, 84, 132syl3anc 1372 . . . . . . . 8 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ (𝑏 + 𝑐) ∈ 𝑋)
134 simpr 486 . . . . . . . . . . 11 ((π‘₯ = (𝑏 + 𝑐) ∧ 𝑦 = π‘Ž) β†’ 𝑦 = π‘Ž)
135 simpl 484 . . . . . . . . . . . 12 ((π‘₯ = (𝑏 + 𝑐) ∧ 𝑦 = π‘Ž) β†’ π‘₯ = (𝑏 + 𝑐))
136135oveq1d 7376 . . . . . . . . . . 11 ((π‘₯ = (𝑏 + 𝑐) ∧ 𝑦 = π‘Ž) β†’ (π‘₯ + 𝑧) = ((𝑏 + 𝑐) + 𝑧))
137134, 136mpteq12dv 5200 . . . . . . . . . 10 ((π‘₯ = (𝑏 + 𝑐) ∧ 𝑦 = π‘Ž) β†’ (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) = (𝑧 ∈ π‘Ž ↦ ((𝑏 + 𝑐) + 𝑧)))
138137rneqd 5897 . . . . . . . . 9 ((π‘₯ = (𝑏 + 𝑐) ∧ 𝑦 = π‘Ž) β†’ ran (𝑧 ∈ 𝑦 ↦ (π‘₯ + 𝑧)) = ran (𝑧 ∈ π‘Ž ↦ ((𝑏 + 𝑐) + 𝑧)))
13963mptex 7177 . . . . . . . . . 10 (𝑧 ∈ π‘Ž ↦ ((𝑏 + 𝑐) + 𝑧)) ∈ V
140139rnex 7853 . . . . . . . . 9 ran (𝑧 ∈ π‘Ž ↦ ((𝑏 + 𝑐) + 𝑧)) ∈ V
141138, 50, 140ovmpoa 7514 . . . . . . . 8 (((𝑏 + 𝑐) ∈ 𝑋 ∧ π‘Ž ∈ 𝑆) β†’ ((𝑏 + 𝑐) βŠ• π‘Ž) = ran (𝑧 ∈ π‘Ž ↦ ((𝑏 + 𝑐) + 𝑧)))
142133, 85, 141syl2anc 585 . . . . . . 7 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ ((𝑏 + 𝑐) βŠ• π‘Ž) = ran (𝑧 ∈ π‘Ž ↦ ((𝑏 + 𝑐) + 𝑧)))
143115, 130, 1423eqtr4rd 2784 . . . . . 6 (((πœ‘ ∧ π‘Ž ∈ 𝑆) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) β†’ ((𝑏 + 𝑐) βŠ• π‘Ž) = (𝑏 βŠ• (𝑐 βŠ• π‘Ž)))
144143ralrimivva 3194 . . . . 5 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ βˆ€π‘ ∈ 𝑋 βˆ€π‘ ∈ 𝑋 ((𝑏 + 𝑐) βŠ• π‘Ž) = (𝑏 βŠ• (𝑐 βŠ• π‘Ž)))
14580, 144jca 513 . . . 4 ((πœ‘ ∧ π‘Ž ∈ 𝑆) β†’ (((0gβ€˜πΊ) βŠ• π‘Ž) = π‘Ž ∧ βˆ€π‘ ∈ 𝑋 βˆ€π‘ ∈ 𝑋 ((𝑏 + 𝑐) βŠ• π‘Ž) = (𝑏 βŠ• (𝑐 βŠ• π‘Ž))))
146145ralrimiva 3140 . . 3 (πœ‘ β†’ βˆ€π‘Ž ∈ 𝑆 (((0gβ€˜πΊ) βŠ• π‘Ž) = π‘Ž ∧ βˆ€π‘ ∈ 𝑋 βˆ€π‘ ∈ 𝑋 ((𝑏 + 𝑐) βŠ• π‘Ž) = (𝑏 βŠ• (𝑐 βŠ• π‘Ž))))
14752, 146jca 513 . 2 (πœ‘ β†’ ( βŠ• :(𝑋 Γ— 𝑆)βŸΆπ‘† ∧ βˆ€π‘Ž ∈ 𝑆 (((0gβ€˜πΊ) βŠ• π‘Ž) = π‘Ž ∧ βˆ€π‘ ∈ 𝑋 βˆ€π‘ ∈ 𝑋 ((𝑏 + 𝑐) βŠ• π‘Ž) = (𝑏 βŠ• (𝑐 βŠ• π‘Ž)))))
1483, 9, 54isga 19079 . 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 3061  βˆƒwrex 3070  {crab 3406  Vcvv 3447   βŠ† wss 3914  π’« cpw 4564   class class class wbr 5109   ↦ cmpt 5192   I cid 5534   Γ— cxp 5635  ran crn 5638   β†Ύ cres 5639  βŸΆwf 6496  β€“1-1β†’wf1 6497  β€“1-1-ontoβ†’wf1o 6499  β€˜cfv 6500  (class class class)co 7361   ∈ cmpo 7363   β‰ˆ cen 8886  Fincfn 8889  β„•0cn0 12421  β†‘cexp 13976  β™―chash 14239   βˆ₯ cdvds 16144  β„™cprime 16555  Basecbs 17091  +gcplusg 17141  0gc0g 17329  Grpcgrp 18756   GrpAct cga 19077
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 5246  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676  ax-cnex 11115  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-mulcom 11123  ax-addass 11124  ax-mulass 11125  ax-distr 11126  ax-i2m1 11127  ax-1ne0 11128  ax-1rid 11129  ax-rnegex 11130  ax-rrecex 11131  ax-cnre 11132  ax-pre-lttri 11133  ax-pre-lttrn 11134  ax-pre-ltadd 11135  ax-pre-mulgt0 11136
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 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3933  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-int 4912  df-iun 4960  df-br 5110  df-opab 5172  df-mpt 5193  df-tr 5227  df-id 5535  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5592  df-we 5594  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-pred 6257  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7317  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7807  df-1st 7925  df-2nd 7926  df-frecs 8216  df-wrecs 8247  df-recs 8321  df-rdg 8360  df-1o 8416  df-er 8654  df-map 8773  df-en 8890  df-dom 8891  df-sdom 8892  df-fin 8893  df-card 9883  df-pnf 11199  df-mnf 11200  df-xr 11201  df-ltxr 11202  df-le 11203  df-sub 11395  df-neg 11396  df-nn 12162  df-n0 12422  df-z 12508  df-uz 12772  df-hash 14240  df-0g 17331  df-mgm 18505  df-sgrp 18554  df-mnd 18565  df-grp 18759  df-minusg 18760  df-ga 19078
This theorem is referenced by:  sylow1lem3  19390  sylow1lem5  19392
  Copyright terms: Public domain W3C validator