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 } C_ Y /\ E. g e. X ( g .(+) x ) = y ) }
gaorber.2 
|- X = ( Base ` G )
Assertion gaorber 
|- ( .(+) e. ( G GrpAct Y ) -> .~ Er Y )

Proof

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