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

Theorem sylow1lem2 19381
Description: Lemma for sylow1 19385. 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 6856 . . . . 5 𝑋 ∈ V
54pwex 5335 . . . 4 𝒫 𝑋 ∈ V
62, 5rabex2 5291 . . 3 𝑆 ∈ V
71, 6jctir 521 . 2 (𝜑 → (𝐺 ∈ Grp ∧ 𝑆 ∈ V))
8 simprl 769 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → 𝑥𝑋)
9 sylow1lem.a . . . . . . . . . . . . 13 + = (+g𝐺)
10 eqid 2736 . . . . . . . . . . . . 13 (𝑧𝑋 ↦ (𝑥 + 𝑧)) = (𝑧𝑋 ↦ (𝑥 + 𝑧))
113, 9, 10grplmulf1o 18821 . . . . . . . . . . . 12 ((𝐺 ∈ Grp ∧ 𝑥𝑋) → (𝑧𝑋 ↦ (𝑥 + 𝑧)):𝑋1-1-onto𝑋)
121, 8, 11syl2an2r 683 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (𝑧𝑋 ↦ (𝑥 + 𝑧)):𝑋1-1-onto𝑋)
13 f1of1 6783 . . . . . . . . . . 11 ((𝑧𝑋 ↦ (𝑥 + 𝑧)):𝑋1-1-onto𝑋 → (𝑧𝑋 ↦ (𝑥 + 𝑧)):𝑋1-1𝑋)
1412, 13syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (𝑧𝑋 ↦ (𝑥 + 𝑧)):𝑋1-1𝑋)
15 simprr 771 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → 𝑦𝑆)
16 fveqeq2 6851 . . . . . . . . . . . . . 14 (𝑠 = 𝑦 → ((♯‘𝑠) = (𝑃𝑁) ↔ (♯‘𝑦) = (𝑃𝑁)))
1716, 2elrab2 3648 . . . . . . . . . . . . 13 (𝑦𝑆 ↔ (𝑦 ∈ 𝒫 𝑋 ∧ (♯‘𝑦) = (𝑃𝑁)))
1815, 17sylib 217 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (𝑦 ∈ 𝒫 𝑋 ∧ (♯‘𝑦) = (𝑃𝑁)))
1918simpld 495 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → 𝑦 ∈ 𝒫 𝑋)
2019elpwid 4569 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → 𝑦𝑋)
21 f1ssres 6746 . . . . . . . . . 10 (((𝑧𝑋 ↦ (𝑥 + 𝑧)):𝑋1-1𝑋𝑦𝑋) → ((𝑧𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦):𝑦1-1𝑋)
2214, 20, 21syl2anc 584 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → ((𝑧𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦):𝑦1-1𝑋)
23 resmpt 5991 . . . . . . . . . 10 (𝑦𝑋 → ((𝑧𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦) = (𝑧𝑦 ↦ (𝑥 + 𝑧)))
24 f1eq1 6733 . . . . . . . . . 10 (((𝑧𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦) = (𝑧𝑦 ↦ (𝑥 + 𝑧)) → (((𝑧𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦):𝑦1-1𝑋 ↔ (𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1𝑋))
2520, 23, 243syl 18 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (((𝑧𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦):𝑦1-1𝑋 ↔ (𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1𝑋))
2622, 25mpbid 231 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1𝑋)
27 f1f 6738 . . . . . . . 8 ((𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1𝑋 → (𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦𝑋)
28 frn 6675 . . . . . . . 8 ((𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦𝑋 → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ⊆ 𝑋)
2926, 27, 283syl 18 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ⊆ 𝑋)
304elpw2 5302 . . . . . . 7 (ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝒫 𝑋 ↔ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ⊆ 𝑋)
3129, 30sylibr 233 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝒫 𝑋)
32 f1f1orn 6795 . . . . . . . . 9 ((𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1𝑋 → (𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1-onto→ran (𝑧𝑦 ↦ (𝑥 + 𝑧)))
33 vex 3449 . . . . . . . . . 10 𝑦 ∈ V
3433f1oen 8913 . . . . . . . . 9 ((𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1-onto→ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) → 𝑦 ≈ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)))
3526, 32, 343syl 18 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → 𝑦 ≈ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)))
36 sylow1.f . . . . . . . . . 10 (𝜑𝑋 ∈ Fin)
37 ssfi 9117 . . . . . . . . . 10 ((𝑋 ∈ Fin ∧ 𝑦𝑋) → 𝑦 ∈ Fin)
3836, 20, 37syl2an2r 683 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → 𝑦 ∈ Fin)
39 ssfi 9117 . . . . . . . . . 10 ((𝑋 ∈ Fin ∧ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ⊆ 𝑋) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ Fin)
4036, 29, 39syl2an2r 683 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ Fin)
41 hashen 14247 . . . . . . . . 9 ((𝑦 ∈ Fin ∧ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ Fin) → ((♯‘𝑦) = (♯‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))) ↔ 𝑦 ≈ ran (𝑧𝑦 ↦ (𝑥 + 𝑧))))
4238, 40, 41syl2anc 584 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → ((♯‘𝑦) = (♯‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))) ↔ 𝑦 ≈ ran (𝑧𝑦 ↦ (𝑥 + 𝑧))))
4335, 42mpbird 256 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (♯‘𝑦) = (♯‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))))
4418simprd 496 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (♯‘𝑦) = (𝑃𝑁))
4543, 44eqtr3d 2778 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (♯‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))) = (𝑃𝑁))
46 fveqeq2 6851 . . . . . . 7 (𝑠 = ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) → ((♯‘𝑠) = (𝑃𝑁) ↔ (♯‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))) = (𝑃𝑁)))
4746, 2elrab2 3648 . . . . . 6 (ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝑆 ↔ (ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝒫 𝑋 ∧ (♯‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))) = (𝑃𝑁)))
4831, 45, 47sylanbrc 583 . . . . 5 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝑆)
4948ralrimivva 3197 . . . 4 (𝜑 → ∀𝑥𝑋𝑦𝑆 ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝑆)
50 sylow1lem.m . . . . 5 = (𝑥𝑋, 𝑦𝑆 ↦ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)))
5150fmpo 8000 . . . 4 (∀𝑥𝑋𝑦𝑆 ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝑆 :(𝑋 × 𝑆)⟶𝑆)
5249, 51sylib 217 . . 3 (𝜑 :(𝑋 × 𝑆)⟶𝑆)
531adantr 481 . . . . . . . 8 ((𝜑𝑎𝑆) → 𝐺 ∈ Grp)
54 eqid 2736 . . . . . . . . 9 (0g𝐺) = (0g𝐺)
553, 54grpidcl 18778 . . . . . . . 8 (𝐺 ∈ Grp → (0g𝐺) ∈ 𝑋)
5653, 55syl 17 . . . . . . 7 ((𝜑𝑎𝑆) → (0g𝐺) ∈ 𝑋)
57 simpr 485 . . . . . . 7 ((𝜑𝑎𝑆) → 𝑎𝑆)
58 simpr 485 . . . . . . . . . 10 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → 𝑦 = 𝑎)
59 simpl 483 . . . . . . . . . . 11 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → 𝑥 = (0g𝐺))
6059oveq1d 7372 . . . . . . . . . 10 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → (𝑥 + 𝑧) = ((0g𝐺) + 𝑧))
6158, 60mpteq12dv 5196 . . . . . . . . 9 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → (𝑧𝑦 ↦ (𝑥 + 𝑧)) = (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)))
6261rneqd 5893 . . . . . . . 8 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)))
63 vex 3449 . . . . . . . . . 10 𝑎 ∈ V
6463mptex 7173 . . . . . . . . 9 (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)) ∈ V
6564rnex 7849 . . . . . . . 8 ran (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)) ∈ V
6662, 50, 65ovmpoa 7510 . . . . . . 7 (((0g𝐺) ∈ 𝑋𝑎𝑆) → ((0g𝐺) 𝑎) = ran (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)))
6756, 57, 66syl2anc 584 . . . . . 6 ((𝜑𝑎𝑆) → ((0g𝐺) 𝑎) = ran (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)))
682ssrab3 4040 . . . . . . . . . . . . . 14 𝑆 ⊆ 𝒫 𝑋
6968, 57sselid 3942 . . . . . . . . . . . . 13 ((𝜑𝑎𝑆) → 𝑎 ∈ 𝒫 𝑋)
7069elpwid 4569 . . . . . . . . . . . 12 ((𝜑𝑎𝑆) → 𝑎𝑋)
7170sselda 3944 . . . . . . . . . . 11 (((𝜑𝑎𝑆) ∧ 𝑧𝑎) → 𝑧𝑋)
723, 9, 54grplid 18780 . . . . . . . . . . 11 ((𝐺 ∈ Grp ∧ 𝑧𝑋) → ((0g𝐺) + 𝑧) = 𝑧)
7353, 71, 72syl2an2r 683 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ 𝑧𝑎) → ((0g𝐺) + 𝑧) = 𝑧)
7473mpteq2dva 5205 . . . . . . . . 9 ((𝜑𝑎𝑆) → (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)) = (𝑧𝑎𝑧))
75 mptresid 6004 . . . . . . . . 9 ( I ↾ 𝑎) = (𝑧𝑎𝑧)
7674, 75eqtr4di 2794 . . . . . . . 8 ((𝜑𝑎𝑆) → (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)) = ( I ↾ 𝑎))
7776rneqd 5893 . . . . . . 7 ((𝜑𝑎𝑆) → ran (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)) = ran ( I ↾ 𝑎))
78 rnresi 6027 . . . . . . 7 ran ( I ↾ 𝑎) = 𝑎
7977, 78eqtrdi 2792 . . . . . 6 ((𝜑𝑎𝑆) → ran (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)) = 𝑎)
8067, 79eqtrd 2776 . . . . 5 ((𝜑𝑎𝑆) → ((0g𝐺) 𝑎) = 𝑎)
81 ovex 7390 . . . . . . . . . 10 (𝑐 + 𝑧) ∈ V
82 oveq2 7365 . . . . . . . . . 10 (𝑤 = (𝑐 + 𝑧) → (𝑏 + 𝑤) = (𝑏 + (𝑐 + 𝑧)))
8381, 82abrexco 7191 . . . . . . . . 9 {𝑢 ∣ ∃𝑤 ∈ {𝑣 ∣ ∃𝑧𝑎 𝑣 = (𝑐 + 𝑧)}𝑢 = (𝑏 + 𝑤)} = {𝑢 ∣ ∃𝑧𝑎 𝑢 = (𝑏 + (𝑐 + 𝑧))}
84 simprr 771 . . . . . . . . . . . . 13 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → 𝑐𝑋)
8557adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → 𝑎𝑆)
86 simpr 485 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑐𝑦 = 𝑎) → 𝑦 = 𝑎)
87 simpl 483 . . . . . . . . . . . . . . . . 17 ((𝑥 = 𝑐𝑦 = 𝑎) → 𝑥 = 𝑐)
8887oveq1d 7372 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑐𝑦 = 𝑎) → (𝑥 + 𝑧) = (𝑐 + 𝑧))
8986, 88mpteq12dv 5196 . . . . . . . . . . . . . . 15 ((𝑥 = 𝑐𝑦 = 𝑎) → (𝑧𝑦 ↦ (𝑥 + 𝑧)) = (𝑧𝑎 ↦ (𝑐 + 𝑧)))
9089rneqd 5893 . . . . . . . . . . . . . 14 ((𝑥 = 𝑐𝑦 = 𝑎) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑧𝑎 ↦ (𝑐 + 𝑧)))
9163mptex 7173 . . . . . . . . . . . . . . 15 (𝑧𝑎 ↦ (𝑐 + 𝑧)) ∈ V
9291rnex 7849 . . . . . . . . . . . . . 14 ran (𝑧𝑎 ↦ (𝑐 + 𝑧)) ∈ V
9390, 50, 92ovmpoa 7510 . . . . . . . . . . . . 13 ((𝑐𝑋𝑎𝑆) → (𝑐 𝑎) = ran (𝑧𝑎 ↦ (𝑐 + 𝑧)))
9484, 85, 93syl2anc 584 . . . . . . . . . . . 12 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (𝑐 𝑎) = ran (𝑧𝑎 ↦ (𝑐 + 𝑧)))
95 eqid 2736 . . . . . . . . . . . . 13 (𝑧𝑎 ↦ (𝑐 + 𝑧)) = (𝑧𝑎 ↦ (𝑐 + 𝑧))
9695rnmpt 5910 . . . . . . . . . . . 12 ran (𝑧𝑎 ↦ (𝑐 + 𝑧)) = {𝑣 ∣ ∃𝑧𝑎 𝑣 = (𝑐 + 𝑧)}
9794, 96eqtrdi 2792 . . . . . . . . . . 11 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (𝑐 𝑎) = {𝑣 ∣ ∃𝑧𝑎 𝑣 = (𝑐 + 𝑧)})
9897rexeqdv 3314 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (∃𝑤 ∈ (𝑐 𝑎)𝑢 = (𝑏 + 𝑤) ↔ ∃𝑤 ∈ {𝑣 ∣ ∃𝑧𝑎 𝑣 = (𝑐 + 𝑧)}𝑢 = (𝑏 + 𝑤)))
9998abbidv 2805 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → {𝑢 ∣ ∃𝑤 ∈ (𝑐 𝑎)𝑢 = (𝑏 + 𝑤)} = {𝑢 ∣ ∃𝑤 ∈ {𝑣 ∣ ∃𝑧𝑎 𝑣 = (𝑐 + 𝑧)}𝑢 = (𝑏 + 𝑤)})
10053ad2antrr 724 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → 𝐺 ∈ Grp)
101 simprl 769 . . . . . . . . . . . . . 14 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → 𝑏𝑋)
102101adantr 481 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → 𝑏𝑋)
10384adantr 481 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → 𝑐𝑋)
10471adantlr 713 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → 𝑧𝑋)
1053, 9grpass 18757 . . . . . . . . . . . . 13 ((𝐺 ∈ Grp ∧ (𝑏𝑋𝑐𝑋𝑧𝑋)) → ((𝑏 + 𝑐) + 𝑧) = (𝑏 + (𝑐 + 𝑧)))
106100, 102, 103, 104, 105syl13anc 1372 . . . . . . . . . . . 12 ((((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → ((𝑏 + 𝑐) + 𝑧) = (𝑏 + (𝑐 + 𝑧)))
107106eqeq2d 2747 . . . . . . . . . . 11 ((((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → (𝑢 = ((𝑏 + 𝑐) + 𝑧) ↔ 𝑢 = (𝑏 + (𝑐 + 𝑧))))
108107rexbidva 3173 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (∃𝑧𝑎 𝑢 = ((𝑏 + 𝑐) + 𝑧) ↔ ∃𝑧𝑎 𝑢 = (𝑏 + (𝑐 + 𝑧))))
109108abbidv 2805 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → {𝑢 ∣ ∃𝑧𝑎 𝑢 = ((𝑏 + 𝑐) + 𝑧)} = {𝑢 ∣ ∃𝑧𝑎 𝑢 = (𝑏 + (𝑐 + 𝑧))})
11083, 99, 1093eqtr4a 2802 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → {𝑢 ∣ ∃𝑤 ∈ (𝑐 𝑎)𝑢 = (𝑏 + 𝑤)} = {𝑢 ∣ ∃𝑧𝑎 𝑢 = ((𝑏 + 𝑐) + 𝑧)})
111 eqid 2736 . . . . . . . . 9 (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)) = (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤))
112111rnmpt 5910 . . . . . . . 8 ran (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)) = {𝑢 ∣ ∃𝑤 ∈ (𝑐 𝑎)𝑢 = (𝑏 + 𝑤)}
113 eqid 2736 . . . . . . . . 9 (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)) = (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧))
114113rnmpt 5910 . . . . . . . 8 ran (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)) = {𝑢 ∣ ∃𝑧𝑎 𝑢 = ((𝑏 + 𝑐) + 𝑧)}
115110, 112, 1143eqtr4g 2801 . . . . . . 7 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → ran (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)) = ran (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)))
11652ad2antrr 724 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → :(𝑋 × 𝑆)⟶𝑆)
117116, 84, 85fovcdmd 7526 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (𝑐 𝑎) ∈ 𝑆)
118 simpr 485 . . . . . . . . . . . 12 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → 𝑦 = (𝑐 𝑎))
119 simpl 483 . . . . . . . . . . . . 13 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → 𝑥 = 𝑏)
120119oveq1d 7372 . . . . . . . . . . . 12 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → (𝑥 + 𝑧) = (𝑏 + 𝑧))
121118, 120mpteq12dv 5196 . . . . . . . . . . 11 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → (𝑧𝑦 ↦ (𝑥 + 𝑧)) = (𝑧 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑧)))
122 oveq2 7365 . . . . . . . . . . . 12 (𝑧 = 𝑤 → (𝑏 + 𝑧) = (𝑏 + 𝑤))
123122cbvmptv 5218 . . . . . . . . . . 11 (𝑧 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑧)) = (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤))
124121, 123eqtrdi 2792 . . . . . . . . . 10 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → (𝑧𝑦 ↦ (𝑥 + 𝑧)) = (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)))
125124rneqd 5893 . . . . . . . . 9 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)))
126 ovex 7390 . . . . . . . . . . 11 (𝑐 𝑎) ∈ V
127126mptex 7173 . . . . . . . . . 10 (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)) ∈ V
128127rnex 7849 . . . . . . . . 9 ran (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)) ∈ V
129125, 50, 128ovmpoa 7510 . . . . . . . 8 ((𝑏𝑋 ∧ (𝑐 𝑎) ∈ 𝑆) → (𝑏 (𝑐 𝑎)) = ran (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)))
130101, 117, 129syl2anc 584 . . . . . . 7 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (𝑏 (𝑐 𝑎)) = ran (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)))
1311ad2antrr 724 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → 𝐺 ∈ Grp)
1323, 9grpcl 18756 . . . . . . . . 9 ((𝐺 ∈ Grp ∧ 𝑏𝑋𝑐𝑋) → (𝑏 + 𝑐) ∈ 𝑋)
133131, 101, 84, 132syl3anc 1371 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (𝑏 + 𝑐) ∈ 𝑋)
134 simpr 485 . . . . . . . . . . 11 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → 𝑦 = 𝑎)
135 simpl 483 . . . . . . . . . . . 12 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → 𝑥 = (𝑏 + 𝑐))
136135oveq1d 7372 . . . . . . . . . . 11 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → (𝑥 + 𝑧) = ((𝑏 + 𝑐) + 𝑧))
137134, 136mpteq12dv 5196 . . . . . . . . . 10 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → (𝑧𝑦 ↦ (𝑥 + 𝑧)) = (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)))
138137rneqd 5893 . . . . . . . . 9 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)))
13963mptex 7173 . . . . . . . . . 10 (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)) ∈ V
140139rnex 7849 . . . . . . . . 9 ran (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)) ∈ V
141138, 50, 140ovmpoa 7510 . . . . . . . 8 (((𝑏 + 𝑐) ∈ 𝑋𝑎𝑆) → ((𝑏 + 𝑐) 𝑎) = ran (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)))
142133, 85, 141syl2anc 584 . . . . . . 7 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → ((𝑏 + 𝑐) 𝑎) = ran (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)))
143115, 130, 1423eqtr4rd 2787 . . . . . 6 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎)))
144143ralrimivva 3197 . . . . 5 ((𝜑𝑎𝑆) → ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎)))
14580, 144jca 512 . . . 4 ((𝜑𝑎𝑆) → (((0g𝐺) 𝑎) = 𝑎 ∧ ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎))))
146145ralrimiva 3143 . . 3 (𝜑 → ∀𝑎𝑆 (((0g𝐺) 𝑎) = 𝑎 ∧ ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎))))
14752, 146jca 512 . 2 (𝜑 → ( :(𝑋 × 𝑆)⟶𝑆 ∧ ∀𝑎𝑆 (((0g𝐺) 𝑎) = 𝑎 ∧ ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎)))))
1483, 9, 54isga 19071 . 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 2713  wral 3064  wrex 3073  {crab 3407  Vcvv 3445  wss 3910  𝒫 cpw 4560   class class class wbr 5105  cmpt 5188   I cid 5530   × cxp 5631  ran crn 5634  cres 5635  wf 6492  1-1wf1 6493  1-1-ontowf1o 6495  cfv 6496  (class class class)co 7357  cmpo 7359  cen 8880  Fincfn 8883  0cn0 12413  cexp 13967  chash 14230  cdvds 16136  cprime 16547  Basecbs 17083  +gcplusg 17133  0gc0g 17321  Grpcgrp 18748   GrpAct cga 19069
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 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
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 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-map 8767  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-n0 12414  df-z 12500  df-uz 12764  df-hash 14231  df-0g 17323  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-grp 18751  df-minusg 18752  df-ga 19070
This theorem is referenced by:  sylow1lem3  19382  sylow1lem5  19384
  Copyright terms: Public domain W3C validator