Metamath Proof Explorer

Theorem eqger

Description: The subgroup coset equivalence relation is an equivalence relation. (Contributed by Mario Carneiro, 13-Jan-2015)

Ref Expression
Hypotheses eqger.x 
|- X = ( Base ` G )
eqger.r 
|- .~ = ( G ~QG Y )
Assertion eqger 
|- ( Y e. ( SubGrp ` G ) -> .~ Er X )

Proof

Step Hyp Ref Expression
1 eqger.x 
 |-  X = ( Base ` G )
2 eqger.r 
 |-  .~ = ( G ~QG Y )
3 2 releqg 
 |-  Rel .~
4 3 a1i 
 |-  ( Y e. ( SubGrp ` G ) -> Rel .~ )
5 subgrcl 
 |-  ( Y e. ( SubGrp ` G ) -> G e. Grp )
6 1 subgss 
 |-  ( Y e. ( SubGrp ` G ) -> Y C_ X )
7 eqid 
 |-  ( invg ` G ) = ( invg ` G )
8 eqid 
 |-  ( +g ` G ) = ( +g ` G )
9 1 7 8 2 eqgval 
 |-  ( ( G e. Grp /\ Y C_ X ) -> ( x .~ y <-> ( x e. X /\ y e. X /\ ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) e. Y ) ) )
10 5 6 9 syl2anc 
 |-  ( Y e. ( SubGrp ` G ) -> ( x .~ y <-> ( x e. X /\ y e. X /\ ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) e. Y ) ) )
11 10 biimpa 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x .~ y ) -> ( x e. X /\ y e. X /\ ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) e. Y ) )
12 11 simp2d 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x .~ y ) -> y e. X )
13 11 simp1d 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x .~ y ) -> x e. X )
14 5 adantr 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x .~ y ) -> G e. Grp )
15 1 7 14 13 grpinvcld 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x .~ y ) -> ( ( invg ` G ) ` x ) e. X )
16 1 8 7 grpinvadd 
 |-  ( ( G e. Grp /\ ( ( invg ` G ) ` x ) e. X /\ y e. X ) -> ( ( invg ` G ) ` ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) ) = ( ( ( invg ` G ) ` y ) ( +g ` G ) ( ( invg ` G ) ` ( ( invg ` G ) ` x ) ) ) )
17 14 15 12 16 syl3anc 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x .~ y ) -> ( ( invg ` G ) ` ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) ) = ( ( ( invg ` G ) ` y ) ( +g ` G ) ( ( invg ` G ) ` ( ( invg ` G ) ` x ) ) ) )
18 1 7 grpinvinv 
 |-  ( ( G e. Grp /\ x e. X ) -> ( ( invg ` G ) ` ( ( invg ` G ) ` x ) ) = x )
19 14 13 18 syl2anc 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x .~ y ) -> ( ( invg ` G ) ` ( ( invg ` G ) ` x ) ) = x )
20 19 oveq2d 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x .~ y ) -> ( ( ( invg ` G ) ` y ) ( +g ` G ) ( ( invg ` G ) ` ( ( invg ` G ) ` x ) ) ) = ( ( ( invg ` G ) ` y ) ( +g ` G ) x ) )
21 17 20 eqtrd 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x .~ y ) -> ( ( invg ` G ) ` ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) ) = ( ( ( invg ` G ) ` y ) ( +g ` G ) x ) )
22 11 simp3d 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x .~ y ) -> ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) e. Y )
23 7 subginvcl 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) e. Y ) -> ( ( invg ` G ) ` ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) ) e. Y )
24 22 23 syldan 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x .~ y ) -> ( ( invg ` G ) ` ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) ) e. Y )
25 21 24 eqeltrrd 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x .~ y ) -> ( ( ( invg ` G ) ` y ) ( +g ` G ) x ) e. Y )
26 6 adantr 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x .~ y ) -> Y C_ X )
27 1 7 8 2 eqgval 
 |-  ( ( G e. Grp /\ Y C_ X ) -> ( y .~ x <-> ( y e. X /\ x e. X /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) x ) e. Y ) ) )
28 14 26 27 syl2anc 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x .~ y ) -> ( y .~ x <-> ( y e. X /\ x e. X /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) x ) e. Y ) ) )
29 12 13 25 28 mpbir3and 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x .~ y ) -> y .~ x )
30 13 adantrr 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> x e. X )
31 1 7 8 2 eqgval 
 |-  ( ( G e. Grp /\ Y C_ X ) -> ( y .~ z <-> ( y e. X /\ z e. X /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) ) )
32 5 6 31 syl2anc 
 |-  ( Y e. ( SubGrp ` G ) -> ( y .~ z <-> ( y e. X /\ z e. X /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) ) )
33 32 biimpa 
 |-  ( ( Y e. ( SubGrp ` G ) /\ y .~ z ) -> ( y e. X /\ z e. X /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) )
34 33 adantrl 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> ( y e. X /\ z e. X /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) )
35 34 simp2d 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> z e. X )
36 5 adantr 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> G e. Grp )
37 1 7 36 30 grpinvcld 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> ( ( invg ` G ) ` x ) e. X )
38 12 adantrr 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> y e. X )
39 1 7 36 38 grpinvcld 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> ( ( invg ` G ) ` y ) e. X )
40 1 8 36 39 35 grpcld 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. X )
41 1 8 36 37 38 40 grpassd 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> ( ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) = ( ( ( invg ` G ) ` x ) ( +g ` G ) ( y ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) )
42 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
43 1 8 42 7 grprinv 
 |-  ( ( G e. Grp /\ y e. X ) -> ( y ( +g ` G ) ( ( invg ` G ) ` y ) ) = ( 0g ` G ) )
44 36 38 43 syl2anc 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> ( y ( +g ` G ) ( ( invg ` G ) ` y ) ) = ( 0g ` G ) )
45 44 oveq1d 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> ( ( y ( +g ` G ) ( ( invg ` G ) ` y ) ) ( +g ` G ) z ) = ( ( 0g ` G ) ( +g ` G ) z ) )
46 1 8 36 38 39 35 grpassd 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> ( ( y ( +g ` G ) ( ( invg ` G ) ` y ) ) ( +g ` G ) z ) = ( y ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) )
47 1 8 42 36 35 grplidd 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> ( ( 0g ` G ) ( +g ` G ) z ) = z )
48 45 46 47 3eqtr3d 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> ( y ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) = z )
49 48 oveq2d 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> ( ( ( invg ` G ) ` x ) ( +g ` G ) ( y ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) ) = ( ( ( invg ` G ) ` x ) ( +g ` G ) z ) )
50 41 49 eqtrd 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> ( ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) = ( ( ( invg ` G ) ` x ) ( +g ` G ) z ) )
51 simpl 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> Y e. ( SubGrp ` G ) )
52 22 adantrr 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) e. Y )
53 34 simp3d 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y )
54 8 subgcl 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) e. Y /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) -> ( ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) e. Y )
55 51 52 53 54 syl3anc 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> ( ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) e. Y )
56 50 55 eqeltrrd 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> ( ( ( invg ` G ) ` x ) ( +g ` G ) z ) e. Y )
57 6 adantr 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> Y C_ X )
58 1 7 8 2 eqgval 
 |-  ( ( G e. Grp /\ Y C_ X ) -> ( x .~ z <-> ( x e. X /\ z e. X /\ ( ( ( invg ` G ) ` x ) ( +g ` G ) z ) e. Y ) ) )
59 36 57 58 syl2anc 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> ( x .~ z <-> ( x e. X /\ z e. X /\ ( ( ( invg ` G ) ` x ) ( +g ` G ) z ) e. Y ) ) )
60 30 35 56 59 mpbir3and 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> x .~ z )
61 1 8 42 7 grplinv 
 |-  ( ( G e. Grp /\ x e. X ) -> ( ( ( invg ` G ) ` x ) ( +g ` G ) x ) = ( 0g ` G ) )
62 5 61 sylan 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x e. X ) -> ( ( ( invg ` G ) ` x ) ( +g ` G ) x ) = ( 0g ` G ) )
63 42 subg0cl 
 |-  ( Y e. ( SubGrp ` G ) -> ( 0g ` G ) e. Y )
64 63 adantr 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x e. X ) -> ( 0g ` G ) e. Y )
65 62 64 eqeltrd 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x e. X ) -> ( ( ( invg ` G ) ` x ) ( +g ` G ) x ) e. Y )
66 65 ex 
 |-  ( Y e. ( SubGrp ` G ) -> ( x e. X -> ( ( ( invg ` G ) ` x ) ( +g ` G ) x ) e. Y ) )
67 66 pm4.71rd 
 |-  ( Y e. ( SubGrp ` G ) -> ( x e. X <-> ( ( ( ( invg ` G ) ` x ) ( +g ` G ) x ) e. Y /\ x e. X ) ) )
68 1 7 8 2 eqgval 
 |-  ( ( G e. Grp /\ Y C_ X ) -> ( x .~ x <-> ( x e. X /\ x e. X /\ ( ( ( invg ` G ) ` x ) ( +g ` G ) x ) e. Y ) ) )
69 5 6 68 syl2anc 
 |-  ( Y e. ( SubGrp ` G ) -> ( x .~ x <-> ( x e. X /\ x e. X /\ ( ( ( invg ` G ) ` x ) ( +g ` G ) x ) e. Y ) ) )
70 df-3an 
 |-  ( ( x e. X /\ x e. X /\ ( ( ( invg ` G ) ` x ) ( +g ` G ) x ) e. Y ) <-> ( ( x e. X /\ x e. X ) /\ ( ( ( invg ` G ) ` x ) ( +g ` G ) x ) e. Y ) )
71 anidm 
 |-  ( ( x e. X /\ x e. X ) <-> x e. X )
72 71 anbi2ci 
 |-  ( ( ( x e. X /\ x e. X ) /\ ( ( ( invg ` G ) ` x ) ( +g ` G ) x ) e. Y ) <-> ( ( ( ( invg ` G ) ` x ) ( +g ` G ) x ) e. Y /\ x e. X ) )
73 70 72 bitri 
 |-  ( ( x e. X /\ x e. X /\ ( ( ( invg ` G ) ` x ) ( +g ` G ) x ) e. Y ) <-> ( ( ( ( invg ` G ) ` x ) ( +g ` G ) x ) e. Y /\ x e. X ) )
74 69 73 bitrdi 
 |-  ( Y e. ( SubGrp ` G ) -> ( x .~ x <-> ( ( ( ( invg ` G ) ` x ) ( +g ` G ) x ) e. Y /\ x e. X ) ) )
75 67 74 bitr4d 
 |-  ( Y e. ( SubGrp ` G ) -> ( x e. X <-> x .~ x ) )
76 4 29 60 75 iserd 
 |-  ( Y e. ( SubGrp ` G ) -> .~ Er X )