Metamath Proof Explorer

Theorem gaorber

Description: The orbit equivalence relation is an equivalence relation on the target set of the group action. (Contributed by NM, 11-Aug-2009) (Revised by Mario Carneiro, 13-Jan-2015)

Ref Expression
Hypotheses gaorb.1 ⊢∼˙=xy|xy⊆Y∧∃g∈Xg⊕˙x=y
gaorber.2 ⊢X=BaseG
Assertion gaorber ⊢⊕˙∈GGrpActY→∼˙ErY

Proof

Step Hyp Ref Expression
1 gaorb.1 ⊢∼˙=xy|xy⊆Y∧∃g∈Xg⊕˙x=y
2 gaorber.2 ⊢X=BaseG
3 1 relopabiv ⊢Rel⁡∼˙
4 3 a1i ⊢⊕˙∈GGrpActY→Rel⁡∼˙
5 simpr ⊢⊕˙∈GGrpActY∧u∼˙v→u∼˙v
6 1 gaorb ⊢u∼˙v↔u∈Y∧v∈Y∧∃h∈Xh⊕˙u=v
7 5 6 sylib ⊢⊕˙∈GGrpActY∧u∼˙v→u∈Y∧v∈Y∧∃h∈Xh⊕˙u=v
8 7 simp2d ⊢⊕˙∈GGrpActY∧u∼˙v→v∈Y
9 7 simp1d ⊢⊕˙∈GGrpActY∧u∼˙v→u∈Y
10 7 simp3d ⊢⊕˙∈GGrpActY∧u∼˙v→∃h∈Xh⊕˙u=v
11 simpll ⊢⊕˙∈GGrpActY∧u∼˙v∧h∈X→⊕˙∈GGrpActY
12 simpr ⊢⊕˙∈GGrpActY∧u∼˙v∧h∈X→h∈X
13 9 adantr ⊢⊕˙∈GGrpActY∧u∼˙v∧h∈X→u∈Y
14 8 adantr ⊢⊕˙∈GGrpActY∧u∼˙v∧h∈X→v∈Y
15 eqid ⊢invg⁡G=invg⁡G
16 2 15 gacan ⊢⊕˙∈GGrpActY∧h∈X∧u∈Y∧v∈Y→h⊕˙u=v↔invg⁡G⁡h⊕˙v=u
17 11 12 13 14 16 syl13anc ⊢⊕˙∈GGrpActY∧u∼˙v∧h∈X→h⊕˙u=v↔invg⁡G⁡h⊕˙v=u
18 gagrp ⊢⊕˙∈GGrpActY→G∈Grp
19 18 adantr ⊢⊕˙∈GGrpActY∧u∼˙v→G∈Grp
20 2 15 grpinvcl ⊢G∈Grp∧h∈X→invg⁡G⁡h∈X
21 19 20 sylan ⊢⊕˙∈GGrpActY∧u∼˙v∧h∈X→invg⁡G⁡h∈X
22 oveq1 ⊢k=invg⁡G⁡h→k⊕˙v=invg⁡G⁡h⊕˙v
23 22 eqeq1d ⊢k=invg⁡G⁡h→k⊕˙v=u↔invg⁡G⁡h⊕˙v=u
24 23 rspcev ⊢invg⁡G⁡h∈X∧invg⁡G⁡h⊕˙v=u→∃k∈Xk⊕˙v=u
25 24 ex ⊢invg⁡G⁡h∈X→invg⁡G⁡h⊕˙v=u→∃k∈Xk⊕˙v=u
26 21 25 syl ⊢⊕˙∈GGrpActY∧u∼˙v∧h∈X→invg⁡G⁡h⊕˙v=u→∃k∈Xk⊕˙v=u
27 17 26 sylbid ⊢⊕˙∈GGrpActY∧u∼˙v∧h∈X→h⊕˙u=v→∃k∈Xk⊕˙v=u
28 27 rexlimdva ⊢⊕˙∈GGrpActY∧u∼˙v→∃h∈Xh⊕˙u=v→∃k∈Xk⊕˙v=u
29 10 28 mpd ⊢⊕˙∈GGrpActY∧u∼˙v→∃k∈Xk⊕˙v=u
30 1 gaorb ⊢v∼˙u↔v∈Y∧u∈Y∧∃k∈Xk⊕˙v=u
31 8 9 29 30 syl3anbrc ⊢⊕˙∈GGrpActY∧u∼˙v→v∼˙u
32 9 adantrr ⊢⊕˙∈GGrpActY∧u∼˙v∧v∼˙w→u∈Y
33 simprr ⊢⊕˙∈GGrpActY∧u∼˙v∧v∼˙w→v∼˙w
34 1 gaorb ⊢v∼˙w↔v∈Y∧w∈Y∧∃k∈Xk⊕˙v=w
35 33 34 sylib ⊢⊕˙∈GGrpActY∧u∼˙v∧v∼˙w→v∈Y∧w∈Y∧∃k∈Xk⊕˙v=w
36 35 simp2d ⊢⊕˙∈GGrpActY∧u∼˙v∧v∼˙w→w∈Y
37 10 adantrr ⊢⊕˙∈GGrpActY∧u∼˙v∧v∼˙w→∃h∈Xh⊕˙u=v
38 35 simp3d ⊢⊕˙∈GGrpActY∧u∼˙v∧v∼˙w→∃k∈Xk⊕˙v=w
39 reeanv ⊢∃h∈X∃k∈Xh⊕˙u=v∧k⊕˙v=w↔∃h∈Xh⊕˙u=v∧∃k∈Xk⊕˙v=w
40 18 ad2antrr ⊢⊕˙∈GGrpActY∧u∼˙v∧v∼˙w∧h∈X∧k∈X∧h⊕˙u=v∧k⊕˙v=w→G∈Grp
41 simprlr ⊢⊕˙∈GGrpActY∧u∼˙v∧v∼˙w∧h∈X∧k∈X∧h⊕˙u=v∧k⊕˙v=w→k∈X
42 simprll ⊢⊕˙∈GGrpActY∧u∼˙v∧v∼˙w∧h∈X∧k∈X∧h⊕˙u=v∧k⊕˙v=w→h∈X
43 eqid ⊢+G=+G
44 2 43 grpcl ⊢G∈Grp∧k∈X∧h∈X→k+Gh∈X
45 40 41 42 44 syl3anc ⊢⊕˙∈GGrpActY∧u∼˙v∧v∼˙w∧h∈X∧k∈X∧h⊕˙u=v∧k⊕˙v=w→k+Gh∈X
46 simpll ⊢⊕˙∈GGrpActY∧u∼˙v∧v∼˙w∧h∈X∧k∈X∧h⊕˙u=v∧k⊕˙v=w→⊕˙∈GGrpActY
47 32 adantr ⊢⊕˙∈GGrpActY∧u∼˙v∧v∼˙w∧h∈X∧k∈X∧h⊕˙u=v∧k⊕˙v=w→u∈Y
48 2 43 gaass ⊢⊕˙∈GGrpActY∧k∈X∧h∈X∧u∈Y→k+Gh⊕˙u=k⊕˙h⊕˙u
49 46 41 42 47 48 syl13anc ⊢⊕˙∈GGrpActY∧u∼˙v∧v∼˙w∧h∈X∧k∈X∧h⊕˙u=v∧k⊕˙v=w→k+Gh⊕˙u=k⊕˙h⊕˙u
50 simprrl ⊢⊕˙∈GGrpActY∧u∼˙v∧v∼˙w∧h∈X∧k∈X∧h⊕˙u=v∧k⊕˙v=w→h⊕˙u=v
51 50 oveq2d ⊢⊕˙∈GGrpActY∧u∼˙v∧v∼˙w∧h∈X∧k∈X∧h⊕˙u=v∧k⊕˙v=w→k⊕˙h⊕˙u=k⊕˙v
52 simprrr ⊢⊕˙∈GGrpActY∧u∼˙v∧v∼˙w∧h∈X∧k∈X∧h⊕˙u=v∧k⊕˙v=w→k⊕˙v=w
53 49 51 52 3eqtrd ⊢⊕˙∈GGrpActY∧u∼˙v∧v∼˙w∧h∈X∧k∈X∧h⊕˙u=v∧k⊕˙v=w→k+Gh⊕˙u=w
54 oveq1 ⊢f=k+Gh→f⊕˙u=k+Gh⊕˙u
55 54 eqeq1d ⊢f=k+Gh→f⊕˙u=w↔k+Gh⊕˙u=w
56 55 rspcev ⊢k+Gh∈X∧k+Gh⊕˙u=w→∃f∈Xf⊕˙u=w
57 45 53 56 syl2anc ⊢⊕˙∈GGrpActY∧u∼˙v∧v∼˙w∧h∈X∧k∈X∧h⊕˙u=v∧k⊕˙v=w→∃f∈Xf⊕˙u=w
58 57 expr ⊢⊕˙∈GGrpActY∧u∼˙v∧v∼˙w∧h∈X∧k∈X→h⊕˙u=v∧k⊕˙v=w→∃f∈Xf⊕˙u=w
59 58 rexlimdvva ⊢⊕˙∈GGrpActY∧u∼˙v∧v∼˙w→∃h∈X∃k∈Xh⊕˙u=v∧k⊕˙v=w→∃f∈Xf⊕˙u=w
60 39 59 biimtrrid ⊢⊕˙∈GGrpActY∧u∼˙v∧v∼˙w→∃h∈Xh⊕˙u=v∧∃k∈Xk⊕˙v=w→∃f∈Xf⊕˙u=w
61 37 38 60 mp2and ⊢⊕˙∈GGrpActY∧u∼˙v∧v∼˙w→∃f∈Xf⊕˙u=w
62 1 gaorb ⊢u∼˙w↔u∈Y∧w∈Y∧∃f∈Xf⊕˙u=w
63 32 36 61 62 syl3anbrc ⊢⊕˙∈GGrpActY∧u∼˙v∧v∼˙w→u∼˙w
64 18 adantr ⊢⊕˙∈GGrpActY∧u∈Y→G∈Grp
65 eqid ⊢0G=0G
66 2 65 grpidcl ⊢G∈Grp→0G∈X
67 64 66 syl ⊢⊕˙∈GGrpActY∧u∈Y→0G∈X
68 65 gagrpid ⊢⊕˙∈GGrpActY∧u∈Y→0G⊕˙u=u
69 oveq1 ⊢h=0G→h⊕˙u=0G⊕˙u
70 69 eqeq1d ⊢h=0G→h⊕˙u=u↔0G⊕˙u=u
71 70 rspcev ⊢0G∈X∧0G⊕˙u=u→∃h∈Xh⊕˙u=u
72 67 68 71 syl2anc ⊢⊕˙∈GGrpActY∧u∈Y→∃h∈Xh⊕˙u=u
73 72 ex ⊢⊕˙∈GGrpActY→u∈Y→∃h∈Xh⊕˙u=u
74 73 pm4.71rd ⊢⊕˙∈GGrpActY→u∈Y↔∃h∈Xh⊕˙u=u∧u∈Y
75 df-3an ⊢u∈Y∧u∈Y∧∃h∈Xh⊕˙u=u↔u∈Y∧u∈Y∧∃h∈Xh⊕˙u=u
76 anidm ⊢u∈Y∧u∈Y↔u∈Y
77 76 anbi2ci ⊢u∈Y∧u∈Y∧∃h∈Xh⊕˙u=u↔∃h∈Xh⊕˙u=u∧u∈Y
78 75 77 bitri ⊢u∈Y∧u∈Y∧∃h∈Xh⊕˙u=u↔∃h∈Xh⊕˙u=u∧u∈Y
79 74 78 bitr4di ⊢⊕˙∈GGrpActY→u∈Y↔u∈Y∧u∈Y∧∃h∈Xh⊕˙u=u
80 1 gaorb ⊢u∼˙u↔u∈Y∧u∈Y∧∃h∈Xh⊕˙u=u
81 79 80 bitr4di ⊢⊕˙∈GGrpActY→u∈Y↔u∼˙u
82 4 31 63 81 iserd ⊢⊕˙∈GGrpActY→∼˙ErY