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 ˙ = x y | x y Y g X g ˙ x = y
gaorber.2 X = Base G
Assertion gaorber ˙ G GrpAct Y ˙ Er Y

Proof

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