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

Theorem sylow1lem2 18220
Description: Lemma for sylow1 18224. 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‘𝐺)
4 fvex 6342 . . . . . 6 (Base‘𝐺) ∈ V
53, 4eqeltri 2846 . . . . 5 𝑋 ∈ V
65pwex 4979 . . . 4 𝒫 𝑋 ∈ V
72, 6rabex2 4948 . . 3 𝑆 ∈ V
81, 7jctir 504 . 2 (𝜑 → (𝐺 ∈ Grp ∧ 𝑆 ∈ V))
9 simprl 746 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → 𝑥𝑋)
10 sylow1lem.a . . . . . . . . . . . . 13 + = (+g𝐺)
11 eqid 2771 . . . . . . . . . . . . 13 (𝑧𝑋 ↦ (𝑥 + 𝑧)) = (𝑧𝑋 ↦ (𝑥 + 𝑧))
123, 10, 11grplmulf1o 17696 . . . . . . . . . . . 12 ((𝐺 ∈ Grp ∧ 𝑥𝑋) → (𝑧𝑋 ↦ (𝑥 + 𝑧)):𝑋1-1-onto𝑋)
131, 9, 12syl2an2r 656 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (𝑧𝑋 ↦ (𝑥 + 𝑧)):𝑋1-1-onto𝑋)
14 f1of1 6277 . . . . . . . . . . 11 ((𝑧𝑋 ↦ (𝑥 + 𝑧)):𝑋1-1-onto𝑋 → (𝑧𝑋 ↦ (𝑥 + 𝑧)):𝑋1-1𝑋)
1513, 14syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (𝑧𝑋 ↦ (𝑥 + 𝑧)):𝑋1-1𝑋)
16 simprr 748 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → 𝑦𝑆)
17 fveq2 6332 . . . . . . . . . . . . . . 15 (𝑠 = 𝑦 → (♯‘𝑠) = (♯‘𝑦))
1817eqeq1d 2773 . . . . . . . . . . . . . 14 (𝑠 = 𝑦 → ((♯‘𝑠) = (𝑃𝑁) ↔ (♯‘𝑦) = (𝑃𝑁)))
1918, 2elrab2 3518 . . . . . . . . . . . . 13 (𝑦𝑆 ↔ (𝑦 ∈ 𝒫 𝑋 ∧ (♯‘𝑦) = (𝑃𝑁)))
2016, 19sylib 208 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (𝑦 ∈ 𝒫 𝑋 ∧ (♯‘𝑦) = (𝑃𝑁)))
2120simpld 476 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → 𝑦 ∈ 𝒫 𝑋)
2221elpwid 4309 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → 𝑦𝑋)
23 f1ssres 6248 . . . . . . . . . 10 (((𝑧𝑋 ↦ (𝑥 + 𝑧)):𝑋1-1𝑋𝑦𝑋) → ((𝑧𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦):𝑦1-1𝑋)
2415, 22, 23syl2anc 565 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → ((𝑧𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦):𝑦1-1𝑋)
25 resmpt 5590 . . . . . . . . . 10 (𝑦𝑋 → ((𝑧𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦) = (𝑧𝑦 ↦ (𝑥 + 𝑧)))
26 f1eq1 6236 . . . . . . . . . 10 (((𝑧𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦) = (𝑧𝑦 ↦ (𝑥 + 𝑧)) → (((𝑧𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦):𝑦1-1𝑋 ↔ (𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1𝑋))
2722, 25, 263syl 18 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (((𝑧𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦):𝑦1-1𝑋 ↔ (𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1𝑋))
2824, 27mpbid 222 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1𝑋)
29 f1f 6241 . . . . . . . 8 ((𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1𝑋 → (𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦𝑋)
30 frn 6193 . . . . . . . 8 ((𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦𝑋 → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ⊆ 𝑋)
3128, 29, 303syl 18 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ⊆ 𝑋)
325elpw2 4959 . . . . . . 7 (ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝒫 𝑋 ↔ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ⊆ 𝑋)
3331, 32sylibr 224 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝒫 𝑋)
34 f1f1orn 6289 . . . . . . . . 9 ((𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1𝑋 → (𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1-onto→ran (𝑧𝑦 ↦ (𝑥 + 𝑧)))
35 vex 3354 . . . . . . . . . 10 𝑦 ∈ V
3635f1oen 8129 . . . . . . . . 9 ((𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1-onto→ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) → 𝑦 ≈ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)))
3728, 34, 363syl 18 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → 𝑦 ≈ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)))
38 sylow1.f . . . . . . . . . 10 (𝜑𝑋 ∈ Fin)
39 ssfi 8335 . . . . . . . . . 10 ((𝑋 ∈ Fin ∧ 𝑦𝑋) → 𝑦 ∈ Fin)
4038, 22, 39syl2an2r 656 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → 𝑦 ∈ Fin)
41 ssfi 8335 . . . . . . . . . 10 ((𝑋 ∈ Fin ∧ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ⊆ 𝑋) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ Fin)
4238, 31, 41syl2an2r 656 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ Fin)
43 hashen 13338 . . . . . . . . 9 ((𝑦 ∈ Fin ∧ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ Fin) → ((♯‘𝑦) = (♯‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))) ↔ 𝑦 ≈ ran (𝑧𝑦 ↦ (𝑥 + 𝑧))))
4440, 42, 43syl2anc 565 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → ((♯‘𝑦) = (♯‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))) ↔ 𝑦 ≈ ran (𝑧𝑦 ↦ (𝑥 + 𝑧))))
4537, 44mpbird 247 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (♯‘𝑦) = (♯‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))))
4620simprd 477 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (♯‘𝑦) = (𝑃𝑁))
4745, 46eqtr3d 2807 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (♯‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))) = (𝑃𝑁))
48 fveq2 6332 . . . . . . . 8 (𝑠 = ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) → (♯‘𝑠) = (♯‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))))
4948eqeq1d 2773 . . . . . . 7 (𝑠 = ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) → ((♯‘𝑠) = (𝑃𝑁) ↔ (♯‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))) = (𝑃𝑁)))
5049, 2elrab2 3518 . . . . . 6 (ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝑆 ↔ (ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝒫 𝑋 ∧ (♯‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))) = (𝑃𝑁)))
5133, 47, 50sylanbrc 564 . . . . 5 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝑆)
5251ralrimivva 3120 . . . 4 (𝜑 → ∀𝑥𝑋𝑦𝑆 ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝑆)
53 sylow1lem.m . . . . 5 = (𝑥𝑋, 𝑦𝑆 ↦ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)))
5453fmpt2 7386 . . . 4 (∀𝑥𝑋𝑦𝑆 ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝑆 :(𝑋 × 𝑆)⟶𝑆)
5552, 54sylib 208 . . 3 (𝜑 :(𝑋 × 𝑆)⟶𝑆)
561adantr 466 . . . . . . . 8 ((𝜑𝑎𝑆) → 𝐺 ∈ Grp)
57 eqid 2771 . . . . . . . . 9 (0g𝐺) = (0g𝐺)
583, 57grpidcl 17657 . . . . . . . 8 (𝐺 ∈ Grp → (0g𝐺) ∈ 𝑋)
5956, 58syl 17 . . . . . . 7 ((𝜑𝑎𝑆) → (0g𝐺) ∈ 𝑋)
60 simpr 471 . . . . . . 7 ((𝜑𝑎𝑆) → 𝑎𝑆)
61 simpr 471 . . . . . . . . . 10 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → 𝑦 = 𝑎)
62 simpl 468 . . . . . . . . . . 11 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → 𝑥 = (0g𝐺))
6362oveq1d 6807 . . . . . . . . . 10 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → (𝑥 + 𝑧) = ((0g𝐺) + 𝑧))
6461, 63mpteq12dv 4867 . . . . . . . . 9 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → (𝑧𝑦 ↦ (𝑥 + 𝑧)) = (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)))
6564rneqd 5491 . . . . . . . 8 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)))
66 vex 3354 . . . . . . . . . 10 𝑎 ∈ V
6766mptex 6629 . . . . . . . . 9 (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)) ∈ V
6867rnex 7246 . . . . . . . 8 ran (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)) ∈ V
6965, 53, 68ovmpt2a 6937 . . . . . . 7 (((0g𝐺) ∈ 𝑋𝑎𝑆) → ((0g𝐺) 𝑎) = ran (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)))
7059, 60, 69syl2anc 565 . . . . . 6 ((𝜑𝑎𝑆) → ((0g𝐺) 𝑎) = ran (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)))
71 ssrab2 3836 . . . . . . . . . . . . . . 15 {𝑠 ∈ 𝒫 𝑋 ∣ (♯‘𝑠) = (𝑃𝑁)} ⊆ 𝒫 𝑋
722, 71eqsstri 3784 . . . . . . . . . . . . . 14 𝑆 ⊆ 𝒫 𝑋
7372, 60sseldi 3750 . . . . . . . . . . . . 13 ((𝜑𝑎𝑆) → 𝑎 ∈ 𝒫 𝑋)
7473elpwid 4309 . . . . . . . . . . . 12 ((𝜑𝑎𝑆) → 𝑎𝑋)
7574sselda 3752 . . . . . . . . . . 11 (((𝜑𝑎𝑆) ∧ 𝑧𝑎) → 𝑧𝑋)
763, 10, 57grplid 17659 . . . . . . . . . . 11 ((𝐺 ∈ Grp ∧ 𝑧𝑋) → ((0g𝐺) + 𝑧) = 𝑧)
7756, 75, 76syl2an2r 656 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ 𝑧𝑎) → ((0g𝐺) + 𝑧) = 𝑧)
7877mpteq2dva 4878 . . . . . . . . 9 ((𝜑𝑎𝑆) → (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)) = (𝑧𝑎𝑧))
79 mptresid 5597 . . . . . . . . 9 (𝑧𝑎𝑧) = ( I ↾ 𝑎)
8078, 79syl6eq 2821 . . . . . . . 8 ((𝜑𝑎𝑆) → (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)) = ( I ↾ 𝑎))
8180rneqd 5491 . . . . . . 7 ((𝜑𝑎𝑆) → ran (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)) = ran ( I ↾ 𝑎))
82 rnresi 5620 . . . . . . 7 ran ( I ↾ 𝑎) = 𝑎
8381, 82syl6eq 2821 . . . . . 6 ((𝜑𝑎𝑆) → ran (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)) = 𝑎)
8470, 83eqtrd 2805 . . . . 5 ((𝜑𝑎𝑆) → ((0g𝐺) 𝑎) = 𝑎)
85 ovex 6822 . . . . . . . . . 10 (𝑐 + 𝑧) ∈ V
86 oveq2 6800 . . . . . . . . . 10 (𝑤 = (𝑐 + 𝑧) → (𝑏 + 𝑤) = (𝑏 + (𝑐 + 𝑧)))
8785, 86abrexco 6644 . . . . . . . . 9 {𝑢 ∣ ∃𝑤 ∈ {𝑣 ∣ ∃𝑧𝑎 𝑣 = (𝑐 + 𝑧)}𝑢 = (𝑏 + 𝑤)} = {𝑢 ∣ ∃𝑧𝑎 𝑢 = (𝑏 + (𝑐 + 𝑧))}
88 simprr 748 . . . . . . . . . . . . 13 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → 𝑐𝑋)
8960adantr 466 . . . . . . . . . . . . 13 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → 𝑎𝑆)
90 simpr 471 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑐𝑦 = 𝑎) → 𝑦 = 𝑎)
91 simpl 468 . . . . . . . . . . . . . . . . 17 ((𝑥 = 𝑐𝑦 = 𝑎) → 𝑥 = 𝑐)
9291oveq1d 6807 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑐𝑦 = 𝑎) → (𝑥 + 𝑧) = (𝑐 + 𝑧))
9390, 92mpteq12dv 4867 . . . . . . . . . . . . . . 15 ((𝑥 = 𝑐𝑦 = 𝑎) → (𝑧𝑦 ↦ (𝑥 + 𝑧)) = (𝑧𝑎 ↦ (𝑐 + 𝑧)))
9493rneqd 5491 . . . . . . . . . . . . . 14 ((𝑥 = 𝑐𝑦 = 𝑎) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑧𝑎 ↦ (𝑐 + 𝑧)))
9566mptex 6629 . . . . . . . . . . . . . . 15 (𝑧𝑎 ↦ (𝑐 + 𝑧)) ∈ V
9695rnex 7246 . . . . . . . . . . . . . 14 ran (𝑧𝑎 ↦ (𝑐 + 𝑧)) ∈ V
9794, 53, 96ovmpt2a 6937 . . . . . . . . . . . . 13 ((𝑐𝑋𝑎𝑆) → (𝑐 𝑎) = ran (𝑧𝑎 ↦ (𝑐 + 𝑧)))
9888, 89, 97syl2anc 565 . . . . . . . . . . . 12 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (𝑐 𝑎) = ran (𝑧𝑎 ↦ (𝑐 + 𝑧)))
99 eqid 2771 . . . . . . . . . . . . 13 (𝑧𝑎 ↦ (𝑐 + 𝑧)) = (𝑧𝑎 ↦ (𝑐 + 𝑧))
10099rnmpt 5509 . . . . . . . . . . . 12 ran (𝑧𝑎 ↦ (𝑐 + 𝑧)) = {𝑣 ∣ ∃𝑧𝑎 𝑣 = (𝑐 + 𝑧)}
10198, 100syl6eq 2821 . . . . . . . . . . 11 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (𝑐 𝑎) = {𝑣 ∣ ∃𝑧𝑎 𝑣 = (𝑐 + 𝑧)})
102101rexeqdv 3294 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (∃𝑤 ∈ (𝑐 𝑎)𝑢 = (𝑏 + 𝑤) ↔ ∃𝑤 ∈ {𝑣 ∣ ∃𝑧𝑎 𝑣 = (𝑐 + 𝑧)}𝑢 = (𝑏 + 𝑤)))
103102abbidv 2890 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → {𝑢 ∣ ∃𝑤 ∈ (𝑐 𝑎)𝑢 = (𝑏 + 𝑤)} = {𝑢 ∣ ∃𝑤 ∈ {𝑣 ∣ ∃𝑧𝑎 𝑣 = (𝑐 + 𝑧)}𝑢 = (𝑏 + 𝑤)})
10456ad2antrr 697 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → 𝐺 ∈ Grp)
105 simprl 746 . . . . . . . . . . . . . 14 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → 𝑏𝑋)
106105adantr 466 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → 𝑏𝑋)
10788adantr 466 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → 𝑐𝑋)
10875adantlr 686 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → 𝑧𝑋)
1093, 10grpass 17638 . . . . . . . . . . . . 13 ((𝐺 ∈ Grp ∧ (𝑏𝑋𝑐𝑋𝑧𝑋)) → ((𝑏 + 𝑐) + 𝑧) = (𝑏 + (𝑐 + 𝑧)))
110104, 106, 107, 108, 109syl13anc 1478 . . . . . . . . . . . 12 ((((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → ((𝑏 + 𝑐) + 𝑧) = (𝑏 + (𝑐 + 𝑧)))
111110eqeq2d 2781 . . . . . . . . . . 11 ((((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → (𝑢 = ((𝑏 + 𝑐) + 𝑧) ↔ 𝑢 = (𝑏 + (𝑐 + 𝑧))))
112111rexbidva 3197 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (∃𝑧𝑎 𝑢 = ((𝑏 + 𝑐) + 𝑧) ↔ ∃𝑧𝑎 𝑢 = (𝑏 + (𝑐 + 𝑧))))
113112abbidv 2890 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → {𝑢 ∣ ∃𝑧𝑎 𝑢 = ((𝑏 + 𝑐) + 𝑧)} = {𝑢 ∣ ∃𝑧𝑎 𝑢 = (𝑏 + (𝑐 + 𝑧))})
11487, 103, 1133eqtr4a 2831 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → {𝑢 ∣ ∃𝑤 ∈ (𝑐 𝑎)𝑢 = (𝑏 + 𝑤)} = {𝑢 ∣ ∃𝑧𝑎 𝑢 = ((𝑏 + 𝑐) + 𝑧)})
115 eqid 2771 . . . . . . . . 9 (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)) = (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤))
116115rnmpt 5509 . . . . . . . 8 ran (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)) = {𝑢 ∣ ∃𝑤 ∈ (𝑐 𝑎)𝑢 = (𝑏 + 𝑤)}
117 eqid 2771 . . . . . . . . 9 (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)) = (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧))
118117rnmpt 5509 . . . . . . . 8 ran (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)) = {𝑢 ∣ ∃𝑧𝑎 𝑢 = ((𝑏 + 𝑐) + 𝑧)}
119114, 116, 1183eqtr4g 2830 . . . . . . 7 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → ran (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)) = ran (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)))
12055ad2antrr 697 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → :(𝑋 × 𝑆)⟶𝑆)
121120, 88, 89fovrnd 6952 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (𝑐 𝑎) ∈ 𝑆)
122 simpr 471 . . . . . . . . . . . 12 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → 𝑦 = (𝑐 𝑎))
123 simpl 468 . . . . . . . . . . . . 13 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → 𝑥 = 𝑏)
124123oveq1d 6807 . . . . . . . . . . . 12 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → (𝑥 + 𝑧) = (𝑏 + 𝑧))
125122, 124mpteq12dv 4867 . . . . . . . . . . 11 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → (𝑧𝑦 ↦ (𝑥 + 𝑧)) = (𝑧 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑧)))
126 oveq2 6800 . . . . . . . . . . . 12 (𝑧 = 𝑤 → (𝑏 + 𝑧) = (𝑏 + 𝑤))
127126cbvmptv 4884 . . . . . . . . . . 11 (𝑧 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑧)) = (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤))
128125, 127syl6eq 2821 . . . . . . . . . 10 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → (𝑧𝑦 ↦ (𝑥 + 𝑧)) = (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)))
129128rneqd 5491 . . . . . . . . 9 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)))
130 ovex 6822 . . . . . . . . . . 11 (𝑐 𝑎) ∈ V
131130mptex 6629 . . . . . . . . . 10 (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)) ∈ V
132131rnex 7246 . . . . . . . . 9 ran (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)) ∈ V
133129, 53, 132ovmpt2a 6937 . . . . . . . 8 ((𝑏𝑋 ∧ (𝑐 𝑎) ∈ 𝑆) → (𝑏 (𝑐 𝑎)) = ran (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)))
134105, 121, 133syl2anc 565 . . . . . . 7 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (𝑏 (𝑐 𝑎)) = ran (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)))
1351ad2antrr 697 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → 𝐺 ∈ Grp)
1363, 10grpcl 17637 . . . . . . . . 9 ((𝐺 ∈ Grp ∧ 𝑏𝑋𝑐𝑋) → (𝑏 + 𝑐) ∈ 𝑋)
137135, 105, 88, 136syl3anc 1476 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (𝑏 + 𝑐) ∈ 𝑋)
138 simpr 471 . . . . . . . . . . 11 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → 𝑦 = 𝑎)
139 simpl 468 . . . . . . . . . . . 12 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → 𝑥 = (𝑏 + 𝑐))
140139oveq1d 6807 . . . . . . . . . . 11 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → (𝑥 + 𝑧) = ((𝑏 + 𝑐) + 𝑧))
141138, 140mpteq12dv 4867 . . . . . . . . . 10 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → (𝑧𝑦 ↦ (𝑥 + 𝑧)) = (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)))
142141rneqd 5491 . . . . . . . . 9 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)))
14366mptex 6629 . . . . . . . . . 10 (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)) ∈ V
144143rnex 7246 . . . . . . . . 9 ran (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)) ∈ V
145142, 53, 144ovmpt2a 6937 . . . . . . . 8 (((𝑏 + 𝑐) ∈ 𝑋𝑎𝑆) → ((𝑏 + 𝑐) 𝑎) = ran (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)))
146137, 89, 145syl2anc 565 . . . . . . 7 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → ((𝑏 + 𝑐) 𝑎) = ran (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)))
147119, 134, 1463eqtr4rd 2816 . . . . . 6 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎)))
148147ralrimivva 3120 . . . . 5 ((𝜑𝑎𝑆) → ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎)))
14984, 148jca 495 . . . 4 ((𝜑𝑎𝑆) → (((0g𝐺) 𝑎) = 𝑎 ∧ ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎))))
150149ralrimiva 3115 . . 3 (𝜑 → ∀𝑎𝑆 (((0g𝐺) 𝑎) = 𝑎 ∧ ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎))))
15155, 150jca 495 . 2 (𝜑 → ( :(𝑋 × 𝑆)⟶𝑆 ∧ ∀𝑎𝑆 (((0g𝐺) 𝑎) = 𝑎 ∧ ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎)))))
1523, 10, 57isga 17930 . 2 ( ∈ (𝐺 GrpAct 𝑆) ↔ ((𝐺 ∈ Grp ∧ 𝑆 ∈ V) ∧ ( :(𝑋 × 𝑆)⟶𝑆 ∧ ∀𝑎𝑆 (((0g𝐺) 𝑎) = 𝑎 ∧ ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎))))))
1538, 151, 152sylanbrc 564 1 (𝜑 ∈ (𝐺 GrpAct 𝑆))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382   = wceq 1631  wcel 2145  {cab 2757  wral 3061  wrex 3062  {crab 3065  Vcvv 3351  wss 3723  𝒫 cpw 4297   class class class wbr 4786  cmpt 4863   I cid 5156   × cxp 5247  ran crn 5250  cres 5251  wf 6027  1-1wf1 6028  1-1-ontowf1o 6030  cfv 6031  (class class class)co 6792  cmpt2 6794  cen 8105  Fincfn 8108  0cn0 11493  cexp 13066  chash 13320  cdvds 15188  cprime 15591  Basecbs 16063  +gcplusg 16148  0gc0g 16307  Grpcgrp 17629   GrpAct cga 17928
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7095  ax-cnex 10193  ax-resscn 10194  ax-1cn 10195  ax-icn 10196  ax-addcl 10197  ax-addrcl 10198  ax-mulcl 10199  ax-mulrcl 10200  ax-mulcom 10201  ax-addass 10202  ax-mulass 10203  ax-distr 10204  ax-i2m1 10205  ax-1ne0 10206  ax-1rid 10207  ax-rnegex 10208  ax-rrecex 10209  ax-cnre 10210  ax-pre-lttri 10211  ax-pre-lttrn 10212  ax-pre-ltadd 10213  ax-pre-mulgt0 10214
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6753  df-ov 6795  df-oprab 6796  df-mpt2 6797  df-om 7212  df-1st 7314  df-2nd 7315  df-wrecs 7558  df-recs 7620  df-rdg 7658  df-er 7895  df-map 8010  df-en 8109  df-dom 8110  df-sdom 8111  df-fin 8112  df-card 8964  df-pnf 10277  df-mnf 10278  df-xr 10279  df-ltxr 10280  df-le 10281  df-sub 10469  df-neg 10470  df-nn 11222  df-n0 11494  df-z 11579  df-uz 11888  df-hash 13321  df-0g 16309  df-mgm 17449  df-sgrp 17491  df-mnd 17502  df-grp 17632  df-minusg 17633  df-ga 17929
This theorem is referenced by:  sylow1lem3  18221  sylow1lem5  18223
  Copyright terms: Public domain W3C validator