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

Theorem sylow1lem2 17930
Description: Lemma for sylow1 17934. 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 6160 . . . . . 6 (Base‘𝐺) ∈ V
53, 4eqeltri 2700 . . . . 5 𝑋 ∈ V
65pwex 4813 . . . 4 𝒫 𝑋 ∈ V
72, 6rabex2 4780 . . 3 𝑆 ∈ V
81, 7jctir 560 . 2 (𝜑 → (𝐺 ∈ Grp ∧ 𝑆 ∈ V))
9 simprl 793 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → 𝑥𝑋)
10 sylow1lem.a . . . . . . . . . . . . 13 + = (+g𝐺)
11 eqid 2626 . . . . . . . . . . . . 13 (𝑧𝑋 ↦ (𝑥 + 𝑧)) = (𝑧𝑋 ↦ (𝑥 + 𝑧))
123, 10, 11grplmulf1o 17405 . . . . . . . . . . . 12 ((𝐺 ∈ Grp ∧ 𝑥𝑋) → (𝑧𝑋 ↦ (𝑥 + 𝑧)):𝑋1-1-onto𝑋)
131, 9, 12syl2an2r 875 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (𝑧𝑋 ↦ (𝑥 + 𝑧)):𝑋1-1-onto𝑋)
14 f1of1 6095 . . . . . . . . . . 11 ((𝑧𝑋 ↦ (𝑥 + 𝑧)):𝑋1-1-onto𝑋 → (𝑧𝑋 ↦ (𝑥 + 𝑧)):𝑋1-1𝑋)
1513, 14syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (𝑧𝑋 ↦ (𝑥 + 𝑧)):𝑋1-1𝑋)
16 simprr 795 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → 𝑦𝑆)
17 fveq2 6150 . . . . . . . . . . . . . . 15 (𝑠 = 𝑦 → (#‘𝑠) = (#‘𝑦))
1817eqeq1d 2628 . . . . . . . . . . . . . 14 (𝑠 = 𝑦 → ((#‘𝑠) = (𝑃𝑁) ↔ (#‘𝑦) = (𝑃𝑁)))
1918, 2elrab2 3353 . . . . . . . . . . . . 13 (𝑦𝑆 ↔ (𝑦 ∈ 𝒫 𝑋 ∧ (#‘𝑦) = (𝑃𝑁)))
2016, 19sylib 208 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (𝑦 ∈ 𝒫 𝑋 ∧ (#‘𝑦) = (𝑃𝑁)))
2120simpld 475 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → 𝑦 ∈ 𝒫 𝑋)
2221elpwid 4146 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → 𝑦𝑋)
23 f1ssres 6067 . . . . . . . . . 10 (((𝑧𝑋 ↦ (𝑥 + 𝑧)):𝑋1-1𝑋𝑦𝑋) → ((𝑧𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦):𝑦1-1𝑋)
2415, 22, 23syl2anc 692 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → ((𝑧𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦):𝑦1-1𝑋)
25 resmpt 5412 . . . . . . . . . 10 (𝑦𝑋 → ((𝑧𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦) = (𝑧𝑦 ↦ (𝑥 + 𝑧)))
26 f1eq1 6055 . . . . . . . . . 10 (((𝑧𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦) = (𝑧𝑦 ↦ (𝑥 + 𝑧)) → (((𝑧𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦):𝑦1-1𝑋 ↔ (𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1𝑋))
2722, 25, 263syl 18 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (((𝑧𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦):𝑦1-1𝑋 ↔ (𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1𝑋))
2824, 27mpbid 222 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1𝑋)
29 f1f 6060 . . . . . . . 8 ((𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1𝑋 → (𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦𝑋)
30 frn 6012 . . . . . . . 8 ((𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦𝑋 → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ⊆ 𝑋)
3128, 29, 303syl 18 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ⊆ 𝑋)
325elpw2 4793 . . . . . . 7 (ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝒫 𝑋 ↔ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ⊆ 𝑋)
3331, 32sylibr 224 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝒫 𝑋)
34 f1f1orn 6107 . . . . . . . . 9 ((𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1𝑋 → (𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1-onto→ran (𝑧𝑦 ↦ (𝑥 + 𝑧)))
35 vex 3194 . . . . . . . . . 10 𝑦 ∈ V
3635f1oen 7921 . . . . . . . . 9 ((𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1-onto→ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) → 𝑦 ≈ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)))
3728, 34, 363syl 18 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → 𝑦 ≈ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)))
38 sylow1.f . . . . . . . . . 10 (𝜑𝑋 ∈ Fin)
39 ssfi 8125 . . . . . . . . . 10 ((𝑋 ∈ Fin ∧ 𝑦𝑋) → 𝑦 ∈ Fin)
4038, 22, 39syl2an2r 875 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → 𝑦 ∈ Fin)
41 ssfi 8125 . . . . . . . . . 10 ((𝑋 ∈ Fin ∧ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ⊆ 𝑋) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ Fin)
4238, 31, 41syl2an2r 875 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ Fin)
43 hashen 13072 . . . . . . . . 9 ((𝑦 ∈ Fin ∧ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ Fin) → ((#‘𝑦) = (#‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))) ↔ 𝑦 ≈ ran (𝑧𝑦 ↦ (𝑥 + 𝑧))))
4440, 42, 43syl2anc 692 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → ((#‘𝑦) = (#‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))) ↔ 𝑦 ≈ ran (𝑧𝑦 ↦ (𝑥 + 𝑧))))
4537, 44mpbird 247 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (#‘𝑦) = (#‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))))
4620simprd 479 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (#‘𝑦) = (𝑃𝑁))
4745, 46eqtr3d 2662 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (#‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))) = (𝑃𝑁))
48 fveq2 6150 . . . . . . . 8 (𝑠 = ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) → (#‘𝑠) = (#‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))))
4948eqeq1d 2628 . . . . . . 7 (𝑠 = ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) → ((#‘𝑠) = (𝑃𝑁) ↔ (#‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))) = (𝑃𝑁)))
5049, 2elrab2 3353 . . . . . 6 (ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝑆 ↔ (ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝒫 𝑋 ∧ (#‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))) = (𝑃𝑁)))
5133, 47, 50sylanbrc 697 . . . . 5 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝑆)
5251ralrimivva 2970 . . . 4 (𝜑 → ∀𝑥𝑋𝑦𝑆 ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝑆)
53 sylow1lem.m . . . . 5 = (𝑥𝑋, 𝑦𝑆 ↦ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)))
5453fmpt2 7183 . . . 4 (∀𝑥𝑋𝑦𝑆 ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝑆 :(𝑋 × 𝑆)⟶𝑆)
5552, 54sylib 208 . . 3 (𝜑 :(𝑋 × 𝑆)⟶𝑆)
561adantr 481 . . . . . . . 8 ((𝜑𝑎𝑆) → 𝐺 ∈ Grp)
57 eqid 2626 . . . . . . . . 9 (0g𝐺) = (0g𝐺)
583, 57grpidcl 17366 . . . . . . . 8 (𝐺 ∈ Grp → (0g𝐺) ∈ 𝑋)
5956, 58syl 17 . . . . . . 7 ((𝜑𝑎𝑆) → (0g𝐺) ∈ 𝑋)
60 simpr 477 . . . . . . 7 ((𝜑𝑎𝑆) → 𝑎𝑆)
61 simpr 477 . . . . . . . . . 10 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → 𝑦 = 𝑎)
62 simpl 473 . . . . . . . . . . 11 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → 𝑥 = (0g𝐺))
6362oveq1d 6620 . . . . . . . . . 10 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → (𝑥 + 𝑧) = ((0g𝐺) + 𝑧))
6461, 63mpteq12dv 4698 . . . . . . . . 9 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → (𝑧𝑦 ↦ (𝑥 + 𝑧)) = (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)))
6564rneqd 5317 . . . . . . . 8 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)))
66 vex 3194 . . . . . . . . . 10 𝑎 ∈ V
6766mptex 6441 . . . . . . . . 9 (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)) ∈ V
6867rnex 7048 . . . . . . . 8 ran (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)) ∈ V
6965, 53, 68ovmpt2a 6745 . . . . . . 7 (((0g𝐺) ∈ 𝑋𝑎𝑆) → ((0g𝐺) 𝑎) = ran (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)))
7059, 60, 69syl2anc 692 . . . . . 6 ((𝜑𝑎𝑆) → ((0g𝐺) 𝑎) = ran (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)))
71 ssrab2 3671 . . . . . . . . . . . . . . 15 {𝑠 ∈ 𝒫 𝑋 ∣ (#‘𝑠) = (𝑃𝑁)} ⊆ 𝒫 𝑋
722, 71eqsstri 3619 . . . . . . . . . . . . . 14 𝑆 ⊆ 𝒫 𝑋
7372, 60sseldi 3586 . . . . . . . . . . . . 13 ((𝜑𝑎𝑆) → 𝑎 ∈ 𝒫 𝑋)
7473elpwid 4146 . . . . . . . . . . . 12 ((𝜑𝑎𝑆) → 𝑎𝑋)
7574sselda 3588 . . . . . . . . . . 11 (((𝜑𝑎𝑆) ∧ 𝑧𝑎) → 𝑧𝑋)
763, 10, 57grplid 17368 . . . . . . . . . . 11 ((𝐺 ∈ Grp ∧ 𝑧𝑋) → ((0g𝐺) + 𝑧) = 𝑧)
7756, 75, 76syl2an2r 875 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ 𝑧𝑎) → ((0g𝐺) + 𝑧) = 𝑧)
7877mpteq2dva 4709 . . . . . . . . 9 ((𝜑𝑎𝑆) → (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)) = (𝑧𝑎𝑧))
79 mptresid 5419 . . . . . . . . 9 (𝑧𝑎𝑧) = ( I ↾ 𝑎)
8078, 79syl6eq 2676 . . . . . . . 8 ((𝜑𝑎𝑆) → (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)) = ( I ↾ 𝑎))
8180rneqd 5317 . . . . . . 7 ((𝜑𝑎𝑆) → ran (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)) = ran ( I ↾ 𝑎))
82 rnresi 5442 . . . . . . 7 ran ( I ↾ 𝑎) = 𝑎
8381, 82syl6eq 2676 . . . . . 6 ((𝜑𝑎𝑆) → ran (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)) = 𝑎)
8470, 83eqtrd 2660 . . . . 5 ((𝜑𝑎𝑆) → ((0g𝐺) 𝑎) = 𝑎)
85 ovex 6633 . . . . . . . . . 10 (𝑐 + 𝑧) ∈ V
86 oveq2 6613 . . . . . . . . . 10 (𝑤 = (𝑐 + 𝑧) → (𝑏 + 𝑤) = (𝑏 + (𝑐 + 𝑧)))
8785, 86abrexco 6457 . . . . . . . . 9 {𝑢 ∣ ∃𝑤 ∈ {𝑣 ∣ ∃𝑧𝑎 𝑣 = (𝑐 + 𝑧)}𝑢 = (𝑏 + 𝑤)} = {𝑢 ∣ ∃𝑧𝑎 𝑢 = (𝑏 + (𝑐 + 𝑧))}
88 simprr 795 . . . . . . . . . . . . 13 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → 𝑐𝑋)
8960adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → 𝑎𝑆)
90 simpr 477 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑐𝑦 = 𝑎) → 𝑦 = 𝑎)
91 simpl 473 . . . . . . . . . . . . . . . . 17 ((𝑥 = 𝑐𝑦 = 𝑎) → 𝑥 = 𝑐)
9291oveq1d 6620 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑐𝑦 = 𝑎) → (𝑥 + 𝑧) = (𝑐 + 𝑧))
9390, 92mpteq12dv 4698 . . . . . . . . . . . . . . 15 ((𝑥 = 𝑐𝑦 = 𝑎) → (𝑧𝑦 ↦ (𝑥 + 𝑧)) = (𝑧𝑎 ↦ (𝑐 + 𝑧)))
9493rneqd 5317 . . . . . . . . . . . . . 14 ((𝑥 = 𝑐𝑦 = 𝑎) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑧𝑎 ↦ (𝑐 + 𝑧)))
9566mptex 6441 . . . . . . . . . . . . . . 15 (𝑧𝑎 ↦ (𝑐 + 𝑧)) ∈ V
9695rnex 7048 . . . . . . . . . . . . . 14 ran (𝑧𝑎 ↦ (𝑐 + 𝑧)) ∈ V
9794, 53, 96ovmpt2a 6745 . . . . . . . . . . . . 13 ((𝑐𝑋𝑎𝑆) → (𝑐 𝑎) = ran (𝑧𝑎 ↦ (𝑐 + 𝑧)))
9888, 89, 97syl2anc 692 . . . . . . . . . . . 12 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (𝑐 𝑎) = ran (𝑧𝑎 ↦ (𝑐 + 𝑧)))
99 eqid 2626 . . . . . . . . . . . . 13 (𝑧𝑎 ↦ (𝑐 + 𝑧)) = (𝑧𝑎 ↦ (𝑐 + 𝑧))
10099rnmpt 5335 . . . . . . . . . . . 12 ran (𝑧𝑎 ↦ (𝑐 + 𝑧)) = {𝑣 ∣ ∃𝑧𝑎 𝑣 = (𝑐 + 𝑧)}
10198, 100syl6eq 2676 . . . . . . . . . . 11 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (𝑐 𝑎) = {𝑣 ∣ ∃𝑧𝑎 𝑣 = (𝑐 + 𝑧)})
102101rexeqdv 3139 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (∃𝑤 ∈ (𝑐 𝑎)𝑢 = (𝑏 + 𝑤) ↔ ∃𝑤 ∈ {𝑣 ∣ ∃𝑧𝑎 𝑣 = (𝑐 + 𝑧)}𝑢 = (𝑏 + 𝑤)))
103102abbidv 2744 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → {𝑢 ∣ ∃𝑤 ∈ (𝑐 𝑎)𝑢 = (𝑏 + 𝑤)} = {𝑢 ∣ ∃𝑤 ∈ {𝑣 ∣ ∃𝑧𝑎 𝑣 = (𝑐 + 𝑧)}𝑢 = (𝑏 + 𝑤)})
10456ad2antrr 761 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → 𝐺 ∈ Grp)
105 simprl 793 . . . . . . . . . . . . . 14 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → 𝑏𝑋)
106105adantr 481 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → 𝑏𝑋)
10788adantr 481 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → 𝑐𝑋)
10875adantlr 750 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → 𝑧𝑋)
1093, 10grpass 17347 . . . . . . . . . . . . 13 ((𝐺 ∈ Grp ∧ (𝑏𝑋𝑐𝑋𝑧𝑋)) → ((𝑏 + 𝑐) + 𝑧) = (𝑏 + (𝑐 + 𝑧)))
110104, 106, 107, 108, 109syl13anc 1325 . . . . . . . . . . . 12 ((((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → ((𝑏 + 𝑐) + 𝑧) = (𝑏 + (𝑐 + 𝑧)))
111110eqeq2d 2636 . . . . . . . . . . 11 ((((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → (𝑢 = ((𝑏 + 𝑐) + 𝑧) ↔ 𝑢 = (𝑏 + (𝑐 + 𝑧))))
112111rexbidva 3047 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (∃𝑧𝑎 𝑢 = ((𝑏 + 𝑐) + 𝑧) ↔ ∃𝑧𝑎 𝑢 = (𝑏 + (𝑐 + 𝑧))))
113112abbidv 2744 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → {𝑢 ∣ ∃𝑧𝑎 𝑢 = ((𝑏 + 𝑐) + 𝑧)} = {𝑢 ∣ ∃𝑧𝑎 𝑢 = (𝑏 + (𝑐 + 𝑧))})
11487, 103, 1133eqtr4a 2686 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → {𝑢 ∣ ∃𝑤 ∈ (𝑐 𝑎)𝑢 = (𝑏 + 𝑤)} = {𝑢 ∣ ∃𝑧𝑎 𝑢 = ((𝑏 + 𝑐) + 𝑧)})
115 eqid 2626 . . . . . . . . 9 (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)) = (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤))
116115rnmpt 5335 . . . . . . . 8 ran (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)) = {𝑢 ∣ ∃𝑤 ∈ (𝑐 𝑎)𝑢 = (𝑏 + 𝑤)}
117 eqid 2626 . . . . . . . . 9 (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)) = (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧))
118117rnmpt 5335 . . . . . . . 8 ran (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)) = {𝑢 ∣ ∃𝑧𝑎 𝑢 = ((𝑏 + 𝑐) + 𝑧)}
119114, 116, 1183eqtr4g 2685 . . . . . . 7 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → ran (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)) = ran (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)))
12055ad2antrr 761 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → :(𝑋 × 𝑆)⟶𝑆)
121120, 88, 89fovrnd 6760 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (𝑐 𝑎) ∈ 𝑆)
122 simpr 477 . . . . . . . . . . . 12 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → 𝑦 = (𝑐 𝑎))
123 simpl 473 . . . . . . . . . . . . 13 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → 𝑥 = 𝑏)
124123oveq1d 6620 . . . . . . . . . . . 12 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → (𝑥 + 𝑧) = (𝑏 + 𝑧))
125122, 124mpteq12dv 4698 . . . . . . . . . . 11 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → (𝑧𝑦 ↦ (𝑥 + 𝑧)) = (𝑧 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑧)))
126 oveq2 6613 . . . . . . . . . . . 12 (𝑧 = 𝑤 → (𝑏 + 𝑧) = (𝑏 + 𝑤))
127126cbvmptv 4715 . . . . . . . . . . 11 (𝑧 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑧)) = (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤))
128125, 127syl6eq 2676 . . . . . . . . . 10 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → (𝑧𝑦 ↦ (𝑥 + 𝑧)) = (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)))
129128rneqd 5317 . . . . . . . . 9 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)))
130 ovex 6633 . . . . . . . . . . 11 (𝑐 𝑎) ∈ V
131130mptex 6441 . . . . . . . . . 10 (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)) ∈ V
132131rnex 7048 . . . . . . . . 9 ran (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)) ∈ V
133129, 53, 132ovmpt2a 6745 . . . . . . . 8 ((𝑏𝑋 ∧ (𝑐 𝑎) ∈ 𝑆) → (𝑏 (𝑐 𝑎)) = ran (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)))
134105, 121, 133syl2anc 692 . . . . . . 7 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (𝑏 (𝑐 𝑎)) = ran (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)))
1351ad2antrr 761 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → 𝐺 ∈ Grp)
1363, 10grpcl 17346 . . . . . . . . 9 ((𝐺 ∈ Grp ∧ 𝑏𝑋𝑐𝑋) → (𝑏 + 𝑐) ∈ 𝑋)
137135, 105, 88, 136syl3anc 1323 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (𝑏 + 𝑐) ∈ 𝑋)
138 simpr 477 . . . . . . . . . . 11 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → 𝑦 = 𝑎)
139 simpl 473 . . . . . . . . . . . 12 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → 𝑥 = (𝑏 + 𝑐))
140139oveq1d 6620 . . . . . . . . . . 11 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → (𝑥 + 𝑧) = ((𝑏 + 𝑐) + 𝑧))
141138, 140mpteq12dv 4698 . . . . . . . . . 10 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → (𝑧𝑦 ↦ (𝑥 + 𝑧)) = (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)))
142141rneqd 5317 . . . . . . . . 9 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)))
14366mptex 6441 . . . . . . . . . 10 (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)) ∈ V
144143rnex 7048 . . . . . . . . 9 ran (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)) ∈ V
145142, 53, 144ovmpt2a 6745 . . . . . . . 8 (((𝑏 + 𝑐) ∈ 𝑋𝑎𝑆) → ((𝑏 + 𝑐) 𝑎) = ran (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)))
146137, 89, 145syl2anc 692 . . . . . . 7 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → ((𝑏 + 𝑐) 𝑎) = ran (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)))
147119, 134, 1463eqtr4rd 2671 . . . . . 6 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎)))
148147ralrimivva 2970 . . . . 5 ((𝜑𝑎𝑆) → ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎)))
14984, 148jca 554 . . . 4 ((𝜑𝑎𝑆) → (((0g𝐺) 𝑎) = 𝑎 ∧ ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎))))
150149ralrimiva 2965 . . 3 (𝜑 → ∀𝑎𝑆 (((0g𝐺) 𝑎) = 𝑎 ∧ ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎))))
15155, 150jca 554 . 2 (𝜑 → ( :(𝑋 × 𝑆)⟶𝑆 ∧ ∀𝑎𝑆 (((0g𝐺) 𝑎) = 𝑎 ∧ ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎)))))
1523, 10, 57isga 17640 . 2 ( ∈ (𝐺 GrpAct 𝑆) ↔ ((𝐺 ∈ Grp ∧ 𝑆 ∈ V) ∧ ( :(𝑋 × 𝑆)⟶𝑆 ∧ ∀𝑎𝑆 (((0g𝐺) 𝑎) = 𝑎 ∧ ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎))))))
1538, 151, 152sylanbrc 697 1 (𝜑 ∈ (𝐺 GrpAct 𝑆))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1992  {cab 2612  wral 2912  wrex 2913  {crab 2916  Vcvv 3191  wss 3560  𝒫 cpw 4135   class class class wbr 4618  cmpt 4678   I cid 4989   × cxp 5077  ran crn 5080  cres 5081  wf 5846  1-1wf1 5847  1-1-ontowf1o 5849  cfv 5850  (class class class)co 6605  cmpt2 6607  cen 7897  Fincfn 7900  0cn0 11237  cexp 12797  #chash 13054  cdvds 14902  cprime 15304  Basecbs 15776  +gcplusg 15857  0gc0g 16016  Grpcgrp 17338   GrpAct cga 17638
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903  ax-cnex 9937  ax-resscn 9938  ax-1cn 9939  ax-icn 9940  ax-addcl 9941  ax-addrcl 9942  ax-mulcl 9943  ax-mulrcl 9944  ax-mulcom 9945  ax-addass 9946  ax-mulass 9947  ax-distr 9948  ax-i2m1 9949  ax-1ne0 9950  ax-1rid 9951  ax-rnegex 9952  ax-rrecex 9953  ax-cnre 9954  ax-pre-lttri 9955  ax-pre-lttrn 9956  ax-pre-ltadd 9957  ax-pre-mulgt0 9958
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-nel 2900  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5642  df-ord 5688  df-on 5689  df-lim 5690  df-suc 5691  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-riota 6566  df-ov 6608  df-oprab 6609  df-mpt2 6610  df-om 7014  df-1st 7116  df-2nd 7117  df-wrecs 7353  df-recs 7414  df-rdg 7452  df-er 7688  df-map 7805  df-en 7901  df-dom 7902  df-sdom 7903  df-fin 7904  df-card 8710  df-pnf 10021  df-mnf 10022  df-xr 10023  df-ltxr 10024  df-le 10025  df-sub 10213  df-neg 10214  df-nn 10966  df-n0 11238  df-z 11323  df-uz 11632  df-hash 13055  df-0g 16018  df-mgm 17158  df-sgrp 17200  df-mnd 17211  df-grp 17341  df-minusg 17342  df-ga 17639
This theorem is referenced by:  sylow1lem3  17931  sylow1lem5  17933
  Copyright terms: Public domain W3C validator