Metamath Proof Explorer

Theorem eqgid

Description: The left coset containing the identity is the original subgroup. (Contributed by Mario Carneiro, 20-Sep-2015)

Ref Expression
Hypotheses eqger.x 
|- X = ( Base ` G )
eqger.r 
|- .~ = ( G ~QG Y )
eqgid.3 
|- .0. = ( 0g ` G )
Assertion eqgid 
|- ( Y e. ( SubGrp ` G ) -> [ .0. ] .~ = Y )

Proof

Step Hyp Ref Expression
1 eqger.x 
 |-  X = ( Base ` G )
2 eqger.r 
 |-  .~ = ( G ~QG Y )
3 eqgid.3 
 |-  .0. = ( 0g ` G )
4 2 releqg 
 |-  Rel .~
5 relelec 
 |-  ( Rel .~ -> ( x e. [ .0. ] .~ <-> .0. .~ x ) )
6 4 5 ax-mp 
 |-  ( x e. [ .0. ] .~ <-> .0. .~ x )
7 subgrcl 
 |-  ( Y e. ( SubGrp ` G ) -> G e. Grp )
8 7 adantr 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x e. X ) -> G e. Grp )
9 eqid 
 |-  ( invg ` G ) = ( invg ` G )
10 3 9 grpinvid 
 |-  ( G e. Grp -> ( ( invg ` G ) ` .0. ) = .0. )
11 8 10 syl 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x e. X ) -> ( ( invg ` G ) ` .0. ) = .0. )
12 11 oveq1d 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x e. X ) -> ( ( ( invg ` G ) ` .0. ) ( +g ` G ) x ) = ( .0. ( +g ` G ) x ) )
13 eqid 
 |-  ( +g ` G ) = ( +g ` G )
14 1 13 3 grplid 
 |-  ( ( G e. Grp /\ x e. X ) -> ( .0. ( +g ` G ) x ) = x )
15 7 14 sylan 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x e. X ) -> ( .0. ( +g ` G ) x ) = x )
16 12 15 eqtrd 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x e. X ) -> ( ( ( invg ` G ) ` .0. ) ( +g ` G ) x ) = x )
17 16 eleq1d 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x e. X ) -> ( ( ( ( invg ` G ) ` .0. ) ( +g ` G ) x ) e. Y <-> x e. Y ) )
18 17 pm5.32da 
 |-  ( Y e. ( SubGrp ` G ) -> ( ( x e. X /\ ( ( ( invg ` G ) ` .0. ) ( +g ` G ) x ) e. Y ) <-> ( x e. X /\ x e. Y ) ) )
19 1 subgss 
 |-  ( Y e. ( SubGrp ` G ) -> Y C_ X )
20 1 3 grpidcl 
 |-  ( G e. Grp -> .0. e. X )
21 7 20 syl 
 |-  ( Y e. ( SubGrp ` G ) -> .0. e. X )
22 1 9 13 2 eqgval 
 |-  ( ( G e. Grp /\ Y C_ X ) -> ( .0. .~ x <-> ( .0. e. X /\ x e. X /\ ( ( ( invg ` G ) ` .0. ) ( +g ` G ) x ) e. Y ) ) )
23 3anass 
 |-  ( ( .0. e. X /\ x e. X /\ ( ( ( invg ` G ) ` .0. ) ( +g ` G ) x ) e. Y ) <-> ( .0. e. X /\ ( x e. X /\ ( ( ( invg ` G ) ` .0. ) ( +g ` G ) x ) e. Y ) ) )
24 22 23 bitrdi 
 |-  ( ( G e. Grp /\ Y C_ X ) -> ( .0. .~ x <-> ( .0. e. X /\ ( x e. X /\ ( ( ( invg ` G ) ` .0. ) ( +g ` G ) x ) e. Y ) ) ) )
25 24 baibd 
 |-  ( ( ( G e. Grp /\ Y C_ X ) /\ .0. e. X ) -> ( .0. .~ x <-> ( x e. X /\ ( ( ( invg ` G ) ` .0. ) ( +g ` G ) x ) e. Y ) ) )
26 7 19 21 25 syl21anc 
 |-  ( Y e. ( SubGrp ` G ) -> ( .0. .~ x <-> ( x e. X /\ ( ( ( invg ` G ) ` .0. ) ( +g ` G ) x ) e. Y ) ) )
27 19 sseld 
 |-  ( Y e. ( SubGrp ` G ) -> ( x e. Y -> x e. X ) )
28 27 pm4.71rd 
 |-  ( Y e. ( SubGrp ` G ) -> ( x e. Y <-> ( x e. X /\ x e. Y ) ) )
29 18 26 28 3bitr4d 
 |-  ( Y e. ( SubGrp ` G ) -> ( .0. .~ x <-> x e. Y ) )
30 6 29 syl5bb 
 |-  ( Y e. ( SubGrp ` G ) -> ( x e. [ .0. ] .~ <-> x e. Y ) )
31 30 eqrdv 
 |-  ( Y e. ( SubGrp ` G ) -> [ .0. ] .~ = Y )