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

Theorem sylow1lem2 17837
Description: Lemma for sylow1 17841. 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 6113 . . . . . 6 (Base‘𝐺) ∈ V
53, 4eqeltri 2684 . . . . 5 𝑋 ∈ V
65pwex 4774 . . . 4 𝒫 𝑋 ∈ V
72, 6rabex2 4742 . . 3 𝑆 ∈ V
81, 7jctir 559 . 2 (𝜑 → (𝐺 ∈ Grp ∧ 𝑆 ∈ V))
9 simprl 790 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → 𝑥𝑋)
10 sylow1lem.a . . . . . . . . . . . . 13 + = (+g𝐺)
11 eqid 2610 . . . . . . . . . . . . 13 (𝑧𝑋 ↦ (𝑥 + 𝑧)) = (𝑧𝑋 ↦ (𝑥 + 𝑧))
123, 10, 11grplmulf1o 17312 . . . . . . . . . . . 12 ((𝐺 ∈ Grp ∧ 𝑥𝑋) → (𝑧𝑋 ↦ (𝑥 + 𝑧)):𝑋1-1-onto𝑋)
131, 9, 12syl2an2r 872 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (𝑧𝑋 ↦ (𝑥 + 𝑧)):𝑋1-1-onto𝑋)
14 f1of1 6049 . . . . . . . . . . 11 ((𝑧𝑋 ↦ (𝑥 + 𝑧)):𝑋1-1-onto𝑋 → (𝑧𝑋 ↦ (𝑥 + 𝑧)):𝑋1-1𝑋)
1513, 14syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (𝑧𝑋 ↦ (𝑥 + 𝑧)):𝑋1-1𝑋)
16 simprr 792 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → 𝑦𝑆)
17 fveq2 6103 . . . . . . . . . . . . . . 15 (𝑠 = 𝑦 → (#‘𝑠) = (#‘𝑦))
1817eqeq1d 2612 . . . . . . . . . . . . . 14 (𝑠 = 𝑦 → ((#‘𝑠) = (𝑃𝑁) ↔ (#‘𝑦) = (𝑃𝑁)))
1918, 2elrab2 3333 . . . . . . . . . . . . 13 (𝑦𝑆 ↔ (𝑦 ∈ 𝒫 𝑋 ∧ (#‘𝑦) = (𝑃𝑁)))
2016, 19sylib 207 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (𝑦 ∈ 𝒫 𝑋 ∧ (#‘𝑦) = (𝑃𝑁)))
2120simpld 474 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → 𝑦 ∈ 𝒫 𝑋)
2221elpwid 4118 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → 𝑦𝑋)
23 f1ssres 6021 . . . . . . . . . 10 (((𝑧𝑋 ↦ (𝑥 + 𝑧)):𝑋1-1𝑋𝑦𝑋) → ((𝑧𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦):𝑦1-1𝑋)
2415, 22, 23syl2anc 691 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → ((𝑧𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦):𝑦1-1𝑋)
25 resmpt 5369 . . . . . . . . . 10 (𝑦𝑋 → ((𝑧𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦) = (𝑧𝑦 ↦ (𝑥 + 𝑧)))
26 f1eq1 6009 . . . . . . . . . 10 (((𝑧𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦) = (𝑧𝑦 ↦ (𝑥 + 𝑧)) → (((𝑧𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦):𝑦1-1𝑋 ↔ (𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1𝑋))
2722, 25, 263syl 18 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (((𝑧𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦):𝑦1-1𝑋 ↔ (𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1𝑋))
2824, 27mpbid 221 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1𝑋)
29 f1f 6014 . . . . . . . 8 ((𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1𝑋 → (𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦𝑋)
30 frn 5966 . . . . . . . 8 ((𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦𝑋 → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ⊆ 𝑋)
3128, 29, 303syl 18 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ⊆ 𝑋)
325elpw2 4755 . . . . . . 7 (ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝒫 𝑋 ↔ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ⊆ 𝑋)
3331, 32sylibr 223 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝒫 𝑋)
34 f1f1orn 6061 . . . . . . . . 9 ((𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1𝑋 → (𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1-onto→ran (𝑧𝑦 ↦ (𝑥 + 𝑧)))
35 vex 3176 . . . . . . . . . 10 𝑦 ∈ V
3635f1oen 7862 . . . . . . . . 9 ((𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1-onto→ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) → 𝑦 ≈ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)))
3728, 34, 363syl 18 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → 𝑦 ≈ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)))
38 sylow1.f . . . . . . . . . 10 (𝜑𝑋 ∈ Fin)
39 ssfi 8065 . . . . . . . . . 10 ((𝑋 ∈ Fin ∧ 𝑦𝑋) → 𝑦 ∈ Fin)
4038, 22, 39syl2an2r 872 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → 𝑦 ∈ Fin)
41 ssfi 8065 . . . . . . . . . 10 ((𝑋 ∈ Fin ∧ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ⊆ 𝑋) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ Fin)
4238, 31, 41syl2an2r 872 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ Fin)
43 hashen 12997 . . . . . . . . 9 ((𝑦 ∈ Fin ∧ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ Fin) → ((#‘𝑦) = (#‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))) ↔ 𝑦 ≈ ran (𝑧𝑦 ↦ (𝑥 + 𝑧))))
4440, 42, 43syl2anc 691 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → ((#‘𝑦) = (#‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))) ↔ 𝑦 ≈ ran (𝑧𝑦 ↦ (𝑥 + 𝑧))))
4537, 44mpbird 246 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (#‘𝑦) = (#‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))))
4620simprd 478 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (#‘𝑦) = (𝑃𝑁))
4745, 46eqtr3d 2646 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (#‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))) = (𝑃𝑁))
48 fveq2 6103 . . . . . . . 8 (𝑠 = ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) → (#‘𝑠) = (#‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))))
4948eqeq1d 2612 . . . . . . 7 (𝑠 = ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) → ((#‘𝑠) = (𝑃𝑁) ↔ (#‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))) = (𝑃𝑁)))
5049, 2elrab2 3333 . . . . . 6 (ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝑆 ↔ (ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝒫 𝑋 ∧ (#‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))) = (𝑃𝑁)))
5133, 47, 50sylanbrc 695 . . . . 5 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝑆)
5251ralrimivva 2954 . . . 4 (𝜑 → ∀𝑥𝑋𝑦𝑆 ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝑆)
53 sylow1lem.m . . . . 5 = (𝑥𝑋, 𝑦𝑆 ↦ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)))
5453fmpt2 7126 . . . 4 (∀𝑥𝑋𝑦𝑆 ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝑆 :(𝑋 × 𝑆)⟶𝑆)
5552, 54sylib 207 . . 3 (𝜑 :(𝑋 × 𝑆)⟶𝑆)
561adantr 480 . . . . . . . 8 ((𝜑𝑎𝑆) → 𝐺 ∈ Grp)
57 eqid 2610 . . . . . . . . 9 (0g𝐺) = (0g𝐺)
583, 57grpidcl 17273 . . . . . . . 8 (𝐺 ∈ Grp → (0g𝐺) ∈ 𝑋)
5956, 58syl 17 . . . . . . 7 ((𝜑𝑎𝑆) → (0g𝐺) ∈ 𝑋)
60 simpr 476 . . . . . . 7 ((𝜑𝑎𝑆) → 𝑎𝑆)
61 simpr 476 . . . . . . . . . 10 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → 𝑦 = 𝑎)
62 simpl 472 . . . . . . . . . . 11 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → 𝑥 = (0g𝐺))
6362oveq1d 6564 . . . . . . . . . 10 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → (𝑥 + 𝑧) = ((0g𝐺) + 𝑧))
6461, 63mpteq12dv 4663 . . . . . . . . 9 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → (𝑧𝑦 ↦ (𝑥 + 𝑧)) = (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)))
6564rneqd 5274 . . . . . . . 8 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)))
66 vex 3176 . . . . . . . . . 10 𝑎 ∈ V
6766mptex 6390 . . . . . . . . 9 (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)) ∈ V
6867rnex 6992 . . . . . . . 8 ran (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)) ∈ V
6965, 53, 68ovmpt2a 6689 . . . . . . 7 (((0g𝐺) ∈ 𝑋𝑎𝑆) → ((0g𝐺) 𝑎) = ran (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)))
7059, 60, 69syl2anc 691 . . . . . 6 ((𝜑𝑎𝑆) → ((0g𝐺) 𝑎) = ran (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)))
71 ssrab2 3650 . . . . . . . . . . . . . . 15 {𝑠 ∈ 𝒫 𝑋 ∣ (#‘𝑠) = (𝑃𝑁)} ⊆ 𝒫 𝑋
722, 71eqsstri 3598 . . . . . . . . . . . . . 14 𝑆 ⊆ 𝒫 𝑋
7372, 60sseldi 3566 . . . . . . . . . . . . 13 ((𝜑𝑎𝑆) → 𝑎 ∈ 𝒫 𝑋)
7473elpwid 4118 . . . . . . . . . . . 12 ((𝜑𝑎𝑆) → 𝑎𝑋)
7574sselda 3568 . . . . . . . . . . 11 (((𝜑𝑎𝑆) ∧ 𝑧𝑎) → 𝑧𝑋)
763, 10, 57grplid 17275 . . . . . . . . . . 11 ((𝐺 ∈ Grp ∧ 𝑧𝑋) → ((0g𝐺) + 𝑧) = 𝑧)
7756, 75, 76syl2an2r 872 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ 𝑧𝑎) → ((0g𝐺) + 𝑧) = 𝑧)
7877mpteq2dva 4672 . . . . . . . . 9 ((𝜑𝑎𝑆) → (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)) = (𝑧𝑎𝑧))
79 mptresid 5375 . . . . . . . . 9 (𝑧𝑎𝑧) = ( I ↾ 𝑎)
8078, 79syl6eq 2660 . . . . . . . 8 ((𝜑𝑎𝑆) → (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)) = ( I ↾ 𝑎))
8180rneqd 5274 . . . . . . 7 ((𝜑𝑎𝑆) → ran (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)) = ran ( I ↾ 𝑎))
82 rnresi 5398 . . . . . . 7 ran ( I ↾ 𝑎) = 𝑎
8381, 82syl6eq 2660 . . . . . 6 ((𝜑𝑎𝑆) → ran (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)) = 𝑎)
8470, 83eqtrd 2644 . . . . 5 ((𝜑𝑎𝑆) → ((0g𝐺) 𝑎) = 𝑎)
85 ovex 6577 . . . . . . . . . 10 (𝑐 + 𝑧) ∈ V
86 oveq2 6557 . . . . . . . . . 10 (𝑤 = (𝑐 + 𝑧) → (𝑏 + 𝑤) = (𝑏 + (𝑐 + 𝑧)))
8785, 86abrexco 6406 . . . . . . . . 9 {𝑢 ∣ ∃𝑤 ∈ {𝑣 ∣ ∃𝑧𝑎 𝑣 = (𝑐 + 𝑧)}𝑢 = (𝑏 + 𝑤)} = {𝑢 ∣ ∃𝑧𝑎 𝑢 = (𝑏 + (𝑐 + 𝑧))}
88 simprr 792 . . . . . . . . . . . . 13 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → 𝑐𝑋)
8960adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → 𝑎𝑆)
90 simpr 476 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑐𝑦 = 𝑎) → 𝑦 = 𝑎)
91 simpl 472 . . . . . . . . . . . . . . . . 17 ((𝑥 = 𝑐𝑦 = 𝑎) → 𝑥 = 𝑐)
9291oveq1d 6564 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑐𝑦 = 𝑎) → (𝑥 + 𝑧) = (𝑐 + 𝑧))
9390, 92mpteq12dv 4663 . . . . . . . . . . . . . . 15 ((𝑥 = 𝑐𝑦 = 𝑎) → (𝑧𝑦 ↦ (𝑥 + 𝑧)) = (𝑧𝑎 ↦ (𝑐 + 𝑧)))
9493rneqd 5274 . . . . . . . . . . . . . 14 ((𝑥 = 𝑐𝑦 = 𝑎) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑧𝑎 ↦ (𝑐 + 𝑧)))
9566mptex 6390 . . . . . . . . . . . . . . 15 (𝑧𝑎 ↦ (𝑐 + 𝑧)) ∈ V
9695rnex 6992 . . . . . . . . . . . . . 14 ran (𝑧𝑎 ↦ (𝑐 + 𝑧)) ∈ V
9794, 53, 96ovmpt2a 6689 . . . . . . . . . . . . 13 ((𝑐𝑋𝑎𝑆) → (𝑐 𝑎) = ran (𝑧𝑎 ↦ (𝑐 + 𝑧)))
9888, 89, 97syl2anc 691 . . . . . . . . . . . 12 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (𝑐 𝑎) = ran (𝑧𝑎 ↦ (𝑐 + 𝑧)))
99 eqid 2610 . . . . . . . . . . . . 13 (𝑧𝑎 ↦ (𝑐 + 𝑧)) = (𝑧𝑎 ↦ (𝑐 + 𝑧))
10099rnmpt 5292 . . . . . . . . . . . 12 ran (𝑧𝑎 ↦ (𝑐 + 𝑧)) = {𝑣 ∣ ∃𝑧𝑎 𝑣 = (𝑐 + 𝑧)}
10198, 100syl6eq 2660 . . . . . . . . . . 11 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (𝑐 𝑎) = {𝑣 ∣ ∃𝑧𝑎 𝑣 = (𝑐 + 𝑧)})
102101rexeqdv 3122 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (∃𝑤 ∈ (𝑐 𝑎)𝑢 = (𝑏 + 𝑤) ↔ ∃𝑤 ∈ {𝑣 ∣ ∃𝑧𝑎 𝑣 = (𝑐 + 𝑧)}𝑢 = (𝑏 + 𝑤)))
103102abbidv 2728 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → {𝑢 ∣ ∃𝑤 ∈ (𝑐 𝑎)𝑢 = (𝑏 + 𝑤)} = {𝑢 ∣ ∃𝑤 ∈ {𝑣 ∣ ∃𝑧𝑎 𝑣 = (𝑐 + 𝑧)}𝑢 = (𝑏 + 𝑤)})
10456ad2antrr 758 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → 𝐺 ∈ Grp)
105 simprl 790 . . . . . . . . . . . . . 14 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → 𝑏𝑋)
106105adantr 480 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → 𝑏𝑋)
10788adantr 480 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → 𝑐𝑋)
10875adantlr 747 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → 𝑧𝑋)
1093, 10grpass 17254 . . . . . . . . . . . . 13 ((𝐺 ∈ Grp ∧ (𝑏𝑋𝑐𝑋𝑧𝑋)) → ((𝑏 + 𝑐) + 𝑧) = (𝑏 + (𝑐 + 𝑧)))
110104, 106, 107, 108, 109syl13anc 1320 . . . . . . . . . . . 12 ((((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → ((𝑏 + 𝑐) + 𝑧) = (𝑏 + (𝑐 + 𝑧)))
111110eqeq2d 2620 . . . . . . . . . . 11 ((((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → (𝑢 = ((𝑏 + 𝑐) + 𝑧) ↔ 𝑢 = (𝑏 + (𝑐 + 𝑧))))
112111rexbidva 3031 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (∃𝑧𝑎 𝑢 = ((𝑏 + 𝑐) + 𝑧) ↔ ∃𝑧𝑎 𝑢 = (𝑏 + (𝑐 + 𝑧))))
113112abbidv 2728 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → {𝑢 ∣ ∃𝑧𝑎 𝑢 = ((𝑏 + 𝑐) + 𝑧)} = {𝑢 ∣ ∃𝑧𝑎 𝑢 = (𝑏 + (𝑐 + 𝑧))})
11487, 103, 1133eqtr4a 2670 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → {𝑢 ∣ ∃𝑤 ∈ (𝑐 𝑎)𝑢 = (𝑏 + 𝑤)} = {𝑢 ∣ ∃𝑧𝑎 𝑢 = ((𝑏 + 𝑐) + 𝑧)})
115 eqid 2610 . . . . . . . . 9 (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)) = (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤))
116115rnmpt 5292 . . . . . . . 8 ran (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)) = {𝑢 ∣ ∃𝑤 ∈ (𝑐 𝑎)𝑢 = (𝑏 + 𝑤)}
117 eqid 2610 . . . . . . . . 9 (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)) = (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧))
118117rnmpt 5292 . . . . . . . 8 ran (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)) = {𝑢 ∣ ∃𝑧𝑎 𝑢 = ((𝑏 + 𝑐) + 𝑧)}
119114, 116, 1183eqtr4g 2669 . . . . . . 7 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → ran (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)) = ran (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)))
12055ad2antrr 758 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → :(𝑋 × 𝑆)⟶𝑆)
121120, 88, 89fovrnd 6704 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (𝑐 𝑎) ∈ 𝑆)
122 simpr 476 . . . . . . . . . . . 12 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → 𝑦 = (𝑐 𝑎))
123 simpl 472 . . . . . . . . . . . . 13 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → 𝑥 = 𝑏)
124123oveq1d 6564 . . . . . . . . . . . 12 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → (𝑥 + 𝑧) = (𝑏 + 𝑧))
125122, 124mpteq12dv 4663 . . . . . . . . . . 11 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → (𝑧𝑦 ↦ (𝑥 + 𝑧)) = (𝑧 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑧)))
126 oveq2 6557 . . . . . . . . . . . 12 (𝑧 = 𝑤 → (𝑏 + 𝑧) = (𝑏 + 𝑤))
127126cbvmptv 4678 . . . . . . . . . . 11 (𝑧 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑧)) = (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤))
128125, 127syl6eq 2660 . . . . . . . . . 10 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → (𝑧𝑦 ↦ (𝑥 + 𝑧)) = (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)))
129128rneqd 5274 . . . . . . . . 9 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)))
130 ovex 6577 . . . . . . . . . . 11 (𝑐 𝑎) ∈ V
131130mptex 6390 . . . . . . . . . 10 (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)) ∈ V
132131rnex 6992 . . . . . . . . 9 ran (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)) ∈ V
133129, 53, 132ovmpt2a 6689 . . . . . . . 8 ((𝑏𝑋 ∧ (𝑐 𝑎) ∈ 𝑆) → (𝑏 (𝑐 𝑎)) = ran (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)))
134105, 121, 133syl2anc 691 . . . . . . 7 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (𝑏 (𝑐 𝑎)) = ran (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)))
1351ad2antrr 758 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → 𝐺 ∈ Grp)
1363, 10grpcl 17253 . . . . . . . . 9 ((𝐺 ∈ Grp ∧ 𝑏𝑋𝑐𝑋) → (𝑏 + 𝑐) ∈ 𝑋)
137135, 105, 88, 136syl3anc 1318 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (𝑏 + 𝑐) ∈ 𝑋)
138 simpr 476 . . . . . . . . . . 11 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → 𝑦 = 𝑎)
139 simpl 472 . . . . . . . . . . . 12 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → 𝑥 = (𝑏 + 𝑐))
140139oveq1d 6564 . . . . . . . . . . 11 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → (𝑥 + 𝑧) = ((𝑏 + 𝑐) + 𝑧))
141138, 140mpteq12dv 4663 . . . . . . . . . 10 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → (𝑧𝑦 ↦ (𝑥 + 𝑧)) = (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)))
142141rneqd 5274 . . . . . . . . 9 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)))
14366mptex 6390 . . . . . . . . . 10 (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)) ∈ V
144143rnex 6992 . . . . . . . . 9 ran (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)) ∈ V
145142, 53, 144ovmpt2a 6689 . . . . . . . 8 (((𝑏 + 𝑐) ∈ 𝑋𝑎𝑆) → ((𝑏 + 𝑐) 𝑎) = ran (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)))
146137, 89, 145syl2anc 691 . . . . . . 7 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → ((𝑏 + 𝑐) 𝑎) = ran (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)))
147119, 134, 1463eqtr4rd 2655 . . . . . 6 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎)))
148147ralrimivva 2954 . . . . 5 ((𝜑𝑎𝑆) → ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎)))
14984, 148jca 553 . . . 4 ((𝜑𝑎𝑆) → (((0g𝐺) 𝑎) = 𝑎 ∧ ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎))))
150149ralrimiva 2949 . . 3 (𝜑 → ∀𝑎𝑆 (((0g𝐺) 𝑎) = 𝑎 ∧ ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎))))
15155, 150jca 553 . 2 (𝜑 → ( :(𝑋 × 𝑆)⟶𝑆 ∧ ∀𝑎𝑆 (((0g𝐺) 𝑎) = 𝑎 ∧ ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎)))))
1523, 10, 57isga 17547 . 2 ( ∈ (𝐺 GrpAct 𝑆) ↔ ((𝐺 ∈ Grp ∧ 𝑆 ∈ V) ∧ ( :(𝑋 × 𝑆)⟶𝑆 ∧ ∀𝑎𝑆 (((0g𝐺) 𝑎) = 𝑎 ∧ ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎))))))
1538, 151, 152sylanbrc 695 1 (𝜑 ∈ (𝐺 GrpAct 𝑆))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383   = wceq 1475  wcel 1977  {cab 2596  wral 2896  wrex 2897  {crab 2900  Vcvv 3173  wss 3540  𝒫 cpw 4108   class class class wbr 4583  cmpt 4643   I cid 4948   × cxp 5036  ran crn 5039  cres 5040  wf 5800  1-1wf1 5801  1-1-ontowf1o 5803  cfv 5804  (class class class)co 6549  cmpt2 6551  cen 7838  Fincfn 7841  0cn0 11169  cexp 12722  #chash 12979  cdvds 14821  cprime 15223  Basecbs 15695  +gcplusg 15768  0gc0g 15923  Grpcgrp 17245   GrpAct cga 17545
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-n0 11170  df-z 11255  df-uz 11564  df-hash 12980  df-0g 15925  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-grp 17248  df-minusg 17249  df-ga 17546
This theorem is referenced by:  sylow1lem3  17838  sylow1lem5  17840
  Copyright terms: Public domain W3C validator