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