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

Theorem sylow1lem2 19617
Description: Lemma for sylow1 19621. 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 6920 . . . . 5 𝑋 ∈ V
54pwex 5380 . . . 4 𝒫 𝑋 ∈ V
62, 5rabex2 5341 . . 3 𝑆 ∈ V
71, 6jctir 520 . 2 (𝜑 → (𝐺 ∈ Grp ∧ 𝑆 ∈ V))
8 simprl 771 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → 𝑥𝑋)
9 sylow1lem.a . . . . . . . . . . . . 13 + = (+g𝐺)
10 eqid 2737 . . . . . . . . . . . . 13 (𝑧𝑋 ↦ (𝑥 + 𝑧)) = (𝑧𝑋 ↦ (𝑥 + 𝑧))
113, 9, 10grplmulf1o 19031 . . . . . . . . . . . 12 ((𝐺 ∈ Grp ∧ 𝑥𝑋) → (𝑧𝑋 ↦ (𝑥 + 𝑧)):𝑋1-1-onto𝑋)
121, 8, 11syl2an2r 685 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (𝑧𝑋 ↦ (𝑥 + 𝑧)):𝑋1-1-onto𝑋)
13 f1of1 6847 . . . . . . . . . . 11 ((𝑧𝑋 ↦ (𝑥 + 𝑧)):𝑋1-1-onto𝑋 → (𝑧𝑋 ↦ (𝑥 + 𝑧)):𝑋1-1𝑋)
1412, 13syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (𝑧𝑋 ↦ (𝑥 + 𝑧)):𝑋1-1𝑋)
15 simprr 773 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → 𝑦𝑆)
16 fveqeq2 6915 . . . . . . . . . . . . . 14 (𝑠 = 𝑦 → ((♯‘𝑠) = (𝑃𝑁) ↔ (♯‘𝑦) = (𝑃𝑁)))
1716, 2elrab2 3695 . . . . . . . . . . . . 13 (𝑦𝑆 ↔ (𝑦 ∈ 𝒫 𝑋 ∧ (♯‘𝑦) = (𝑃𝑁)))
1815, 17sylib 218 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (𝑦 ∈ 𝒫 𝑋 ∧ (♯‘𝑦) = (𝑃𝑁)))
1918simpld 494 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → 𝑦 ∈ 𝒫 𝑋)
2019elpwid 4609 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → 𝑦𝑋)
21 f1ssres 6811 . . . . . . . . . 10 (((𝑧𝑋 ↦ (𝑥 + 𝑧)):𝑋1-1𝑋𝑦𝑋) → ((𝑧𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦):𝑦1-1𝑋)
2214, 20, 21syl2anc 584 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → ((𝑧𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦):𝑦1-1𝑋)
23 resmpt 6055 . . . . . . . . . 10 (𝑦𝑋 → ((𝑧𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦) = (𝑧𝑦 ↦ (𝑥 + 𝑧)))
24 f1eq1 6799 . . . . . . . . . 10 (((𝑧𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦) = (𝑧𝑦 ↦ (𝑥 + 𝑧)) → (((𝑧𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦):𝑦1-1𝑋 ↔ (𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1𝑋))
2520, 23, 243syl 18 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (((𝑧𝑋 ↦ (𝑥 + 𝑧)) ↾ 𝑦):𝑦1-1𝑋 ↔ (𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1𝑋))
2622, 25mpbid 232 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1𝑋)
27 f1f 6804 . . . . . . . 8 ((𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1𝑋 → (𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦𝑋)
28 frn 6743 . . . . . . . 8 ((𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦𝑋 → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ⊆ 𝑋)
2926, 27, 283syl 18 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ⊆ 𝑋)
304elpw2 5334 . . . . . . 7 (ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝒫 𝑋 ↔ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ⊆ 𝑋)
3129, 30sylibr 234 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝒫 𝑋)
32 f1f1orn 6859 . . . . . . . . 9 ((𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1𝑋 → (𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1-onto→ran (𝑧𝑦 ↦ (𝑥 + 𝑧)))
33 vex 3484 . . . . . . . . . 10 𝑦 ∈ V
3433f1oen 9013 . . . . . . . . 9 ((𝑧𝑦 ↦ (𝑥 + 𝑧)):𝑦1-1-onto→ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) → 𝑦 ≈ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)))
3526, 32, 343syl 18 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → 𝑦 ≈ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)))
36 sylow1.f . . . . . . . . . 10 (𝜑𝑋 ∈ Fin)
37 ssfi 9213 . . . . . . . . . 10 ((𝑋 ∈ Fin ∧ 𝑦𝑋) → 𝑦 ∈ Fin)
3836, 20, 37syl2an2r 685 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → 𝑦 ∈ Fin)
39 ssfi 9213 . . . . . . . . . 10 ((𝑋 ∈ Fin ∧ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ⊆ 𝑋) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ Fin)
4036, 29, 39syl2an2r 685 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ Fin)
41 hashen 14386 . . . . . . . . 9 ((𝑦 ∈ Fin ∧ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ Fin) → ((♯‘𝑦) = (♯‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))) ↔ 𝑦 ≈ ran (𝑧𝑦 ↦ (𝑥 + 𝑧))))
4238, 40, 41syl2anc 584 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → ((♯‘𝑦) = (♯‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))) ↔ 𝑦 ≈ ran (𝑧𝑦 ↦ (𝑥 + 𝑧))))
4335, 42mpbird 257 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (♯‘𝑦) = (♯‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))))
4418simprd 495 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (♯‘𝑦) = (𝑃𝑁))
4543, 44eqtr3d 2779 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → (♯‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))) = (𝑃𝑁))
46 fveqeq2 6915 . . . . . . 7 (𝑠 = ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) → ((♯‘𝑠) = (𝑃𝑁) ↔ (♯‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))) = (𝑃𝑁)))
4746, 2elrab2 3695 . . . . . 6 (ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝑆 ↔ (ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝒫 𝑋 ∧ (♯‘ran (𝑧𝑦 ↦ (𝑥 + 𝑧))) = (𝑃𝑁)))
4831, 45, 47sylanbrc 583 . . . . 5 ((𝜑 ∧ (𝑥𝑋𝑦𝑆)) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝑆)
4948ralrimivva 3202 . . . 4 (𝜑 → ∀𝑥𝑋𝑦𝑆 ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝑆)
50 sylow1lem.m . . . . 5 = (𝑥𝑋, 𝑦𝑆 ↦ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)))
5150fmpo 8093 . . . 4 (∀𝑥𝑋𝑦𝑆 ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) ∈ 𝑆 :(𝑋 × 𝑆)⟶𝑆)
5249, 51sylib 218 . . 3 (𝜑 :(𝑋 × 𝑆)⟶𝑆)
531adantr 480 . . . . . . . 8 ((𝜑𝑎𝑆) → 𝐺 ∈ Grp)
54 eqid 2737 . . . . . . . . 9 (0g𝐺) = (0g𝐺)
553, 54grpidcl 18983 . . . . . . . 8 (𝐺 ∈ Grp → (0g𝐺) ∈ 𝑋)
5653, 55syl 17 . . . . . . 7 ((𝜑𝑎𝑆) → (0g𝐺) ∈ 𝑋)
57 simpr 484 . . . . . . 7 ((𝜑𝑎𝑆) → 𝑎𝑆)
58 simpr 484 . . . . . . . . . 10 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → 𝑦 = 𝑎)
59 simpl 482 . . . . . . . . . . 11 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → 𝑥 = (0g𝐺))
6059oveq1d 7446 . . . . . . . . . 10 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → (𝑥 + 𝑧) = ((0g𝐺) + 𝑧))
6158, 60mpteq12dv 5233 . . . . . . . . 9 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → (𝑧𝑦 ↦ (𝑥 + 𝑧)) = (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)))
6261rneqd 5949 . . . . . . . 8 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)))
63 vex 3484 . . . . . . . . . 10 𝑎 ∈ V
6463mptex 7243 . . . . . . . . 9 (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)) ∈ V
6564rnex 7932 . . . . . . . 8 ran (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)) ∈ V
6662, 50, 65ovmpoa 7588 . . . . . . 7 (((0g𝐺) ∈ 𝑋𝑎𝑆) → ((0g𝐺) 𝑎) = ran (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)))
6756, 57, 66syl2anc 584 . . . . . 6 ((𝜑𝑎𝑆) → ((0g𝐺) 𝑎) = ran (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)))
682ssrab3 4082 . . . . . . . . . . . . . 14 𝑆 ⊆ 𝒫 𝑋
6968, 57sselid 3981 . . . . . . . . . . . . 13 ((𝜑𝑎𝑆) → 𝑎 ∈ 𝒫 𝑋)
7069elpwid 4609 . . . . . . . . . . . 12 ((𝜑𝑎𝑆) → 𝑎𝑋)
7170sselda 3983 . . . . . . . . . . 11 (((𝜑𝑎𝑆) ∧ 𝑧𝑎) → 𝑧𝑋)
723, 9, 54grplid 18985 . . . . . . . . . . 11 ((𝐺 ∈ Grp ∧ 𝑧𝑋) → ((0g𝐺) + 𝑧) = 𝑧)
7353, 71, 72syl2an2r 685 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ 𝑧𝑎) → ((0g𝐺) + 𝑧) = 𝑧)
7473mpteq2dva 5242 . . . . . . . . 9 ((𝜑𝑎𝑆) → (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)) = (𝑧𝑎𝑧))
75 mptresid 6069 . . . . . . . . 9 ( I ↾ 𝑎) = (𝑧𝑎𝑧)
7674, 75eqtr4di 2795 . . . . . . . 8 ((𝜑𝑎𝑆) → (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)) = ( I ↾ 𝑎))
7776rneqd 5949 . . . . . . 7 ((𝜑𝑎𝑆) → ran (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)) = ran ( I ↾ 𝑎))
78 rnresi 6093 . . . . . . 7 ran ( I ↾ 𝑎) = 𝑎
7977, 78eqtrdi 2793 . . . . . 6 ((𝜑𝑎𝑆) → ran (𝑧𝑎 ↦ ((0g𝐺) + 𝑧)) = 𝑎)
8067, 79eqtrd 2777 . . . . 5 ((𝜑𝑎𝑆) → ((0g𝐺) 𝑎) = 𝑎)
81 ovex 7464 . . . . . . . . . 10 (𝑐 + 𝑧) ∈ V
82 oveq2 7439 . . . . . . . . . 10 (𝑤 = (𝑐 + 𝑧) → (𝑏 + 𝑤) = (𝑏 + (𝑐 + 𝑧)))
8381, 82abrexco 7264 . . . . . . . . 9 {𝑢 ∣ ∃𝑤 ∈ {𝑣 ∣ ∃𝑧𝑎 𝑣 = (𝑐 + 𝑧)}𝑢 = (𝑏 + 𝑤)} = {𝑢 ∣ ∃𝑧𝑎 𝑢 = (𝑏 + (𝑐 + 𝑧))}
84 simprr 773 . . . . . . . . . . . . 13 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → 𝑐𝑋)
8557adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → 𝑎𝑆)
86 simpr 484 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑐𝑦 = 𝑎) → 𝑦 = 𝑎)
87 simpl 482 . . . . . . . . . . . . . . . . 17 ((𝑥 = 𝑐𝑦 = 𝑎) → 𝑥 = 𝑐)
8887oveq1d 7446 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑐𝑦 = 𝑎) → (𝑥 + 𝑧) = (𝑐 + 𝑧))
8986, 88mpteq12dv 5233 . . . . . . . . . . . . . . 15 ((𝑥 = 𝑐𝑦 = 𝑎) → (𝑧𝑦 ↦ (𝑥 + 𝑧)) = (𝑧𝑎 ↦ (𝑐 + 𝑧)))
9089rneqd 5949 . . . . . . . . . . . . . 14 ((𝑥 = 𝑐𝑦 = 𝑎) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑧𝑎 ↦ (𝑐 + 𝑧)))
9163mptex 7243 . . . . . . . . . . . . . . 15 (𝑧𝑎 ↦ (𝑐 + 𝑧)) ∈ V
9291rnex 7932 . . . . . . . . . . . . . 14 ran (𝑧𝑎 ↦ (𝑐 + 𝑧)) ∈ V
9390, 50, 92ovmpoa 7588 . . . . . . . . . . . . 13 ((𝑐𝑋𝑎𝑆) → (𝑐 𝑎) = ran (𝑧𝑎 ↦ (𝑐 + 𝑧)))
9484, 85, 93syl2anc 584 . . . . . . . . . . . 12 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (𝑐 𝑎) = ran (𝑧𝑎 ↦ (𝑐 + 𝑧)))
95 eqid 2737 . . . . . . . . . . . . 13 (𝑧𝑎 ↦ (𝑐 + 𝑧)) = (𝑧𝑎 ↦ (𝑐 + 𝑧))
9695rnmpt 5968 . . . . . . . . . . . 12 ran (𝑧𝑎 ↦ (𝑐 + 𝑧)) = {𝑣 ∣ ∃𝑧𝑎 𝑣 = (𝑐 + 𝑧)}
9794, 96eqtrdi 2793 . . . . . . . . . . 11 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (𝑐 𝑎) = {𝑣 ∣ ∃𝑧𝑎 𝑣 = (𝑐 + 𝑧)})
9897rexeqdv 3327 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (∃𝑤 ∈ (𝑐 𝑎)𝑢 = (𝑏 + 𝑤) ↔ ∃𝑤 ∈ {𝑣 ∣ ∃𝑧𝑎 𝑣 = (𝑐 + 𝑧)}𝑢 = (𝑏 + 𝑤)))
9998abbidv 2808 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → {𝑢 ∣ ∃𝑤 ∈ (𝑐 𝑎)𝑢 = (𝑏 + 𝑤)} = {𝑢 ∣ ∃𝑤 ∈ {𝑣 ∣ ∃𝑧𝑎 𝑣 = (𝑐 + 𝑧)}𝑢 = (𝑏 + 𝑤)})
10053ad2antrr 726 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → 𝐺 ∈ Grp)
101 simprl 771 . . . . . . . . . . . . . 14 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → 𝑏𝑋)
102101adantr 480 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → 𝑏𝑋)
10384adantr 480 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → 𝑐𝑋)
10471adantlr 715 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → 𝑧𝑋)
1053, 9grpass 18960 . . . . . . . . . . . . 13 ((𝐺 ∈ Grp ∧ (𝑏𝑋𝑐𝑋𝑧𝑋)) → ((𝑏 + 𝑐) + 𝑧) = (𝑏 + (𝑐 + 𝑧)))
106100, 102, 103, 104, 105syl13anc 1374 . . . . . . . . . . . 12 ((((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → ((𝑏 + 𝑐) + 𝑧) = (𝑏 + (𝑐 + 𝑧)))
107106eqeq2d 2748 . . . . . . . . . . 11 ((((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → (𝑢 = ((𝑏 + 𝑐) + 𝑧) ↔ 𝑢 = (𝑏 + (𝑐 + 𝑧))))
108107rexbidva 3177 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (∃𝑧𝑎 𝑢 = ((𝑏 + 𝑐) + 𝑧) ↔ ∃𝑧𝑎 𝑢 = (𝑏 + (𝑐 + 𝑧))))
109108abbidv 2808 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → {𝑢 ∣ ∃𝑧𝑎 𝑢 = ((𝑏 + 𝑐) + 𝑧)} = {𝑢 ∣ ∃𝑧𝑎 𝑢 = (𝑏 + (𝑐 + 𝑧))})
11083, 99, 1093eqtr4a 2803 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → {𝑢 ∣ ∃𝑤 ∈ (𝑐 𝑎)𝑢 = (𝑏 + 𝑤)} = {𝑢 ∣ ∃𝑧𝑎 𝑢 = ((𝑏 + 𝑐) + 𝑧)})
111 eqid 2737 . . . . . . . . 9 (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)) = (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤))
112111rnmpt 5968 . . . . . . . 8 ran (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)) = {𝑢 ∣ ∃𝑤 ∈ (𝑐 𝑎)𝑢 = (𝑏 + 𝑤)}
113 eqid 2737 . . . . . . . . 9 (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)) = (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧))
114113rnmpt 5968 . . . . . . . 8 ran (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)) = {𝑢 ∣ ∃𝑧𝑎 𝑢 = ((𝑏 + 𝑐) + 𝑧)}
115110, 112, 1143eqtr4g 2802 . . . . . . 7 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → ran (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)) = ran (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)))
11652ad2antrr 726 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → :(𝑋 × 𝑆)⟶𝑆)
117116, 84, 85fovcdmd 7605 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (𝑐 𝑎) ∈ 𝑆)
118 simpr 484 . . . . . . . . . . . 12 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → 𝑦 = (𝑐 𝑎))
119 simpl 482 . . . . . . . . . . . . 13 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → 𝑥 = 𝑏)
120119oveq1d 7446 . . . . . . . . . . . 12 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → (𝑥 + 𝑧) = (𝑏 + 𝑧))
121118, 120mpteq12dv 5233 . . . . . . . . . . 11 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → (𝑧𝑦 ↦ (𝑥 + 𝑧)) = (𝑧 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑧)))
122 oveq2 7439 . . . . . . . . . . . 12 (𝑧 = 𝑤 → (𝑏 + 𝑧) = (𝑏 + 𝑤))
123122cbvmptv 5255 . . . . . . . . . . 11 (𝑧 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑧)) = (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤))
124121, 123eqtrdi 2793 . . . . . . . . . 10 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → (𝑧𝑦 ↦ (𝑥 + 𝑧)) = (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)))
125124rneqd 5949 . . . . . . . . 9 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)))
126 ovex 7464 . . . . . . . . . . 11 (𝑐 𝑎) ∈ V
127126mptex 7243 . . . . . . . . . 10 (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)) ∈ V
128127rnex 7932 . . . . . . . . 9 ran (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)) ∈ V
129125, 50, 128ovmpoa 7588 . . . . . . . 8 ((𝑏𝑋 ∧ (𝑐 𝑎) ∈ 𝑆) → (𝑏 (𝑐 𝑎)) = ran (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)))
130101, 117, 129syl2anc 584 . . . . . . 7 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (𝑏 (𝑐 𝑎)) = ran (𝑤 ∈ (𝑐 𝑎) ↦ (𝑏 + 𝑤)))
1311ad2antrr 726 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → 𝐺 ∈ Grp)
1323, 9grpcl 18959 . . . . . . . . 9 ((𝐺 ∈ Grp ∧ 𝑏𝑋𝑐𝑋) → (𝑏 + 𝑐) ∈ 𝑋)
133131, 101, 84, 132syl3anc 1373 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → (𝑏 + 𝑐) ∈ 𝑋)
134 simpr 484 . . . . . . . . . . 11 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → 𝑦 = 𝑎)
135 simpl 482 . . . . . . . . . . . 12 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → 𝑥 = (𝑏 + 𝑐))
136135oveq1d 7446 . . . . . . . . . . 11 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → (𝑥 + 𝑧) = ((𝑏 + 𝑐) + 𝑧))
137134, 136mpteq12dv 5233 . . . . . . . . . 10 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → (𝑧𝑦 ↦ (𝑥 + 𝑧)) = (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)))
138137rneqd 5949 . . . . . . . . 9 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)))
13963mptex 7243 . . . . . . . . . 10 (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)) ∈ V
140139rnex 7932 . . . . . . . . 9 ran (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)) ∈ V
141138, 50, 140ovmpoa 7588 . . . . . . . 8 (((𝑏 + 𝑐) ∈ 𝑋𝑎𝑆) → ((𝑏 + 𝑐) 𝑎) = ran (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)))
142133, 85, 141syl2anc 584 . . . . . . 7 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → ((𝑏 + 𝑐) 𝑎) = ran (𝑧𝑎 ↦ ((𝑏 + 𝑐) + 𝑧)))
143115, 130, 1423eqtr4rd 2788 . . . . . 6 (((𝜑𝑎𝑆) ∧ (𝑏𝑋𝑐𝑋)) → ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎)))
144143ralrimivva 3202 . . . . 5 ((𝜑𝑎𝑆) → ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎)))
14580, 144jca 511 . . . 4 ((𝜑𝑎𝑆) → (((0g𝐺) 𝑎) = 𝑎 ∧ ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎))))
146145ralrimiva 3146 . . 3 (𝜑 → ∀𝑎𝑆 (((0g𝐺) 𝑎) = 𝑎 ∧ ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎))))
14752, 146jca 511 . 2 (𝜑 → ( :(𝑋 × 𝑆)⟶𝑆 ∧ ∀𝑎𝑆 (((0g𝐺) 𝑎) = 𝑎 ∧ ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎)))))
1483, 9, 54isga 19309 . 2 ( ∈ (𝐺 GrpAct 𝑆) ↔ ((𝐺 ∈ Grp ∧ 𝑆 ∈ V) ∧ ( :(𝑋 × 𝑆)⟶𝑆 ∧ ∀𝑎𝑆 (((0g𝐺) 𝑎) = 𝑎 ∧ ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎))))))
1497, 147, 148sylanbrc 583 1 (𝜑 ∈ (𝐺 GrpAct 𝑆))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wcel 2108  {cab 2714  wral 3061  wrex 3070  {crab 3436  Vcvv 3480  wss 3951  𝒫 cpw 4600   class class class wbr 5143  cmpt 5225   I cid 5577   × cxp 5683  ran crn 5686  cres 5687  wf 6557  1-1wf1 6558  1-1-ontowf1o 6560  cfv 6561  (class class class)co 7431  cmpo 7433  cen 8982  Fincfn 8985  0cn0 12526  cexp 14102  chash 14369  cdvds 16290  cprime 16708  Basecbs 17247  +gcplusg 17297  0gc0g 17484  Grpcgrp 18951   GrpAct cga 19307
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-er 8745  df-map 8868  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-n0 12527  df-z 12614  df-uz 12879  df-hash 14370  df-0g 17486  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-grp 18954  df-minusg 18955  df-ga 19308
This theorem is referenced by:  sylow1lem3  19618  sylow1lem5  19620
  Copyright terms: Public domain W3C validator