Metamath Proof Explorer

Theorem sylow2alem1

Description: Lemma for sylow2a . An equivalence class of fixed points is a singleton. (Contributed by Mario Carneiro, 17-Jan-2015)

Ref Expression
Hypotheses sylow2a.x ⊢X=BaseG
sylow2a.m ⊢φ→⊕˙∈GGrpActY
sylow2a.p ⊢φ→PpGrpG
sylow2a.f ⊢φ→X∈Fin
sylow2a.y ⊢φ→Y∈Fin
sylow2a.z ⊢Z=u∈Y|∀h∈Xh⊕˙u=u
sylow2a.r ⊢∼˙=xy|xy⊆Y∧∃g∈Xg⊕˙x=y
Assertion sylow2alem1 ⊢φ∧A∈Z→A∼˙=A

Proof

Step Hyp Ref Expression
1 sylow2a.x ⊢X=BaseG
2 sylow2a.m ⊢φ→⊕˙∈GGrpActY
3 sylow2a.p ⊢φ→PpGrpG
4 sylow2a.f ⊢φ→X∈Fin
5 sylow2a.y ⊢φ→Y∈Fin
6 sylow2a.z ⊢Z=u∈Y|∀h∈Xh⊕˙u=u
7 sylow2a.r ⊢∼˙=xy|xy⊆Y∧∃g∈Xg⊕˙x=y
8 vex ⊢w∈V
9 simpr ⊢φ∧A∈Z→A∈Z
10 elecg ⊢w∈V∧A∈Z→w∈A∼˙↔A∼˙w
11 8 9 10 sylancr ⊢φ∧A∈Z→w∈A∼˙↔A∼˙w
12 7 gaorb ⊢A∼˙w↔A∈Y∧w∈Y∧∃k∈Xk⊕˙A=w
13 12 simp3bi ⊢A∼˙w→∃k∈Xk⊕˙A=w
14 oveq2 ⊢u=A→h⊕˙u=h⊕˙A
15 id ⊢u=A→u=A
16 14 15 eqeq12d ⊢u=A→h⊕˙u=u↔h⊕˙A=A
17 16 ralbidv ⊢u=A→∀h∈Xh⊕˙u=u↔∀h∈Xh⊕˙A=A
18 17 6 elrab2 ⊢A∈Z↔A∈Y∧∀h∈Xh⊕˙A=A
19 9 18 sylib ⊢φ∧A∈Z→A∈Y∧∀h∈Xh⊕˙A=A
20 19 simprd ⊢φ∧A∈Z→∀h∈Xh⊕˙A=A
21 oveq1 ⊢h=k→h⊕˙A=k⊕˙A
22 21 eqeq1d ⊢h=k→h⊕˙A=A↔k⊕˙A=A
23 22 rspccva ⊢∀h∈Xh⊕˙A=A∧k∈X→k⊕˙A=A
24 20 23 sylan ⊢φ∧A∈Z∧k∈X→k⊕˙A=A
25 eqeq1 ⊢k⊕˙A=w→k⊕˙A=A↔w=A
26 24 25 syl5ibcom ⊢φ∧A∈Z∧k∈X→k⊕˙A=w→w=A
27 26 rexlimdva ⊢φ∧A∈Z→∃k∈Xk⊕˙A=w→w=A
28 13 27 syl5 ⊢φ∧A∈Z→A∼˙w→w=A
29 11 28 sylbid ⊢φ∧A∈Z→w∈A∼˙→w=A
30 velsn ⊢w∈A↔w=A
31 29 30 syl6ibr ⊢φ∧A∈Z→w∈A∼˙→w∈A
32 31 ssrdv ⊢φ∧A∈Z→A∼˙⊆A
33 7 1 gaorber ⊢⊕˙∈GGrpActY→∼˙ErY
34 2 33 syl ⊢φ→∼˙ErY
35 34 adantr ⊢φ∧A∈Z→∼˙ErY
36 19 simpld ⊢φ∧A∈Z→A∈Y
37 35 36 erref ⊢φ∧A∈Z→A∼˙A
38 elecg ⊢A∈Z∧A∈Z→A∈A∼˙↔A∼˙A
39 9 38 sylancom ⊢φ∧A∈Z→A∈A∼˙↔A∼˙A
40 37 39 mpbird ⊢φ∧A∈Z→A∈A∼˙
41 40 snssd ⊢φ∧A∈Z→A⊆A∼˙
42 32 41 eqssd ⊢φ∧A∈Z→A∼˙=A