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 grpinvcl 
 |-  ( ( G e. Grp /\ x e. X ) -> ( ( invg ` G ) ` x ) e. X )
16 14 13 15 syl2anc 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x .~ y ) -> ( ( invg ` G ) ` x ) e. X )
17 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 ) ) ) )
18 14 16 12 17 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 ) ) ) )
19 1 7 grpinvinv 
 |-  ( ( G e. Grp /\ x e. X ) -> ( ( invg ` G ) ` ( ( invg ` G ) ` x ) ) = x )
20 14 13 19 syl2anc 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x .~ y ) -> ( ( invg ` G ) ` ( ( invg ` G ) ` x ) ) = x )
21 20 oveq2d 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x .~ y ) -> ( ( ( invg ` G ) ` y ) ( +g ` G ) ( ( invg ` G ) ` ( ( invg ` G ) ` x ) ) ) = ( ( ( invg ` G ) ` y ) ( +g ` G ) x ) )
22 18 21 eqtrd 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x .~ y ) -> ( ( invg ` G ) ` ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) ) = ( ( ( invg ` G ) ` y ) ( +g ` G ) x ) )
23 11 simp3d 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x .~ y ) -> ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) e. Y )
24 7 subginvcl 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) e. Y ) -> ( ( invg ` G ) ` ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) ) e. Y )
25 23 24 syldan 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x .~ y ) -> ( ( invg ` G ) ` ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) ) e. Y )
26 22 25 eqeltrrd 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x .~ y ) -> ( ( ( invg ` G ) ` y ) ( +g ` G ) x ) e. Y )
27 6 adantr 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x .~ y ) -> Y C_ X )
28 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 ) ) )
29 14 27 28 syl2anc 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x .~ y ) -> ( y .~ x <-> ( y e. X /\ x e. X /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) x ) e. Y ) ) )
30 12 13 26 29 mpbir3and 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x .~ y ) -> y .~ x )
31 13 adantrr 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> x e. X )
32 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 ) ) )
33 5 6 32 syl2anc 
 |-  ( Y e. ( SubGrp ` G ) -> ( y .~ z <-> ( y e. X /\ z e. X /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) ) )
34 33 biimpa 
 |-  ( ( Y e. ( SubGrp ` G ) /\ y .~ z ) -> ( y e. X /\ z e. X /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) )
35 34 adantrl 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> ( y e. X /\ z e. X /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y ) )
36 35 simp2d 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> z e. X )
37 5 adantr 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> G e. Grp )
38 37 31 15 syl2anc 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> ( ( invg ` G ) ` x ) e. X )
39 12 adantrr 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> y e. X )
40 1 7 grpinvcl 
 |-  ( ( G e. Grp /\ y e. X ) -> ( ( invg ` G ) ` y ) e. X )
41 37 39 40 syl2anc 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> ( ( invg ` G ) ` y ) e. X )
42 1 8 grpcl 
 |-  ( ( G e. Grp /\ ( ( invg ` G ) ` y ) e. X /\ z e. X ) -> ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. X )
43 37 41 36 42 syl3anc 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. X )
44 1 8 grpass 
 |-  ( ( G e. Grp /\ ( ( ( invg ` G ) ` x ) e. X /\ y e. X /\ ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. X ) ) -> ( ( ( ( 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 ) ) ) )
45 37 38 39 43 44 syl13anc 
 |-  ( ( 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 ) ) ) )
46 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
47 1 8 46 7 grprinv 
 |-  ( ( G e. Grp /\ y e. X ) -> ( y ( +g ` G ) ( ( invg ` G ) ` y ) ) = ( 0g ` G ) )
48 37 39 47 syl2anc 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> ( y ( +g ` G ) ( ( invg ` G ) ` y ) ) = ( 0g ` G ) )
49 48 oveq1d 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> ( ( y ( +g ` G ) ( ( invg ` G ) ` y ) ) ( +g ` G ) z ) = ( ( 0g ` G ) ( +g ` G ) z ) )
50 1 8 grpass 
 |-  ( ( G e. Grp /\ ( y e. X /\ ( ( invg ` G ) ` y ) e. X /\ z e. X ) ) -> ( ( y ( +g ` G ) ( ( invg ` G ) ` y ) ) ( +g ` G ) z ) = ( y ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) )
51 37 39 41 36 50 syl13anc 
 |-  ( ( 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 ) ) )
52 1 8 46 grplid 
 |-  ( ( G e. Grp /\ z e. X ) -> ( ( 0g ` G ) ( +g ` G ) z ) = z )
53 37 36 52 syl2anc 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> ( ( 0g ` G ) ( +g ` G ) z ) = z )
54 49 51 53 3eqtr3d 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> ( y ( +g ` G ) ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) ) = z )
55 54 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 ) )
56 45 55 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 ) )
57 simpl 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> Y e. ( SubGrp ` G ) )
58 23 adantrr 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) e. Y )
59 35 simp3d 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> ( ( ( invg ` G ) ` y ) ( +g ` G ) z ) e. Y )
60 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 )
61 57 58 59 60 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 )
62 56 61 eqeltrrd 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> ( ( ( invg ` G ) ` x ) ( +g ` G ) z ) e. Y )
63 6 adantr 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> Y C_ X )
64 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 ) ) )
65 37 63 64 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 ) ) )
66 31 36 62 65 mpbir3and 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x .~ y /\ y .~ z ) ) -> x .~ z )
67 1 8 46 7 grplinv 
 |-  ( ( G e. Grp /\ x e. X ) -> ( ( ( invg ` G ) ` x ) ( +g ` G ) x ) = ( 0g ` G ) )
68 5 67 sylan 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x e. X ) -> ( ( ( invg ` G ) ` x ) ( +g ` G ) x ) = ( 0g ` G ) )
69 46 subg0cl 
 |-  ( Y e. ( SubGrp ` G ) -> ( 0g ` G ) e. Y )
70 69 adantr 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x e. X ) -> ( 0g ` G ) e. Y )
71 68 70 eqeltrd 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x e. X ) -> ( ( ( invg ` G ) ` x ) ( +g ` G ) x ) e. Y )
72 71 ex 
 |-  ( Y e. ( SubGrp ` G ) -> ( x e. X -> ( ( ( invg ` G ) ` x ) ( +g ` G ) x ) e. Y ) )
73 72 pm4.71rd 
 |-  ( Y e. ( SubGrp ` G ) -> ( x e. X <-> ( ( ( ( invg ` G ) ` x ) ( +g ` G ) x ) e. Y /\ x e. X ) ) )
74 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 ) ) )
75 5 6 74 syl2anc 
 |-  ( Y e. ( SubGrp ` G ) -> ( x .~ x <-> ( x e. X /\ x e. X /\ ( ( ( invg ` G ) ` x ) ( +g ` G ) x ) e. Y ) ) )
76 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 ) )
77 anidm 
 |-  ( ( x e. X /\ x e. X ) <-> x e. X )
78 77 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 ) )
79 76 78 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 ) )
80 75 79 bitrdi 
 |-  ( Y e. ( SubGrp ` G ) -> ( x .~ x <-> ( ( ( ( invg ` G ) ` x ) ( +g ` G ) x ) e. Y /\ x e. X ) ) )
81 73 80 bitr4d 
 |-  ( Y e. ( SubGrp ` G ) -> ( x e. X <-> x .~ x ) )
82 4 30 66 81 iserd 
 |-  ( Y e. ( SubGrp ` G ) -> .~ Er X )