Metamath Proof Explorer

Theorem eqgen

Description: Each coset is equipotent to the subgroup itself (which is also the coset containing the identity). (Contributed by Mario Carneiro, 20-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 eqger.x 
 |-  X = ( Base ` G )
2 eqger.r 
 |-  .~ = ( G ~QG Y )
3 eqid 
 |-  ( X /. .~ ) = ( X /. .~ )
4 breq2 
 |-  ( [ x ] .~ = A -> ( Y ~~ [ x ] .~ <-> Y ~~ A ) )
5 simpl 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x e. X ) -> Y e. ( SubGrp ` G ) )
6 subgrcl 
 |-  ( Y e. ( SubGrp ` G ) -> G e. Grp )
7 1 subgss 
 |-  ( Y e. ( SubGrp ` G ) -> Y C_ X )
8 6 7 jca 
 |-  ( Y e. ( SubGrp ` G ) -> ( G e. Grp /\ Y C_ X ) )
9 eqid 
 |-  ( +g ` G ) = ( +g ` G )
10 1 2 9 eqglact 
 |-  ( ( G e. Grp /\ Y C_ X /\ x e. X ) -> [ x ] .~ = ( ( z e. X |-> ( x ( +g ` G ) z ) ) " Y ) )
11 10 3expa 
 |-  ( ( ( G e. Grp /\ Y C_ X ) /\ x e. X ) -> [ x ] .~ = ( ( z e. X |-> ( x ( +g ` G ) z ) ) " Y ) )
12 8 11 sylan 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x e. X ) -> [ x ] .~ = ( ( z e. X |-> ( x ( +g ` G ) z ) ) " Y ) )
13 2 ovexi 
 |-  .~ e. _V
14 ecexg 
 |-  ( .~ e. _V -> [ x ] .~ e. _V )
15 13 14 ax-mp 
 |-  [ x ] .~ e. _V
16 12 15 eqeltrrdi 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x e. X ) -> ( ( z e. X |-> ( x ( +g ` G ) z ) ) " Y ) e. _V )
17 eqid 
 |-  ( y e. X |-> ( z e. X |-> ( y ( +g ` G ) z ) ) ) = ( y e. X |-> ( z e. X |-> ( y ( +g ` G ) z ) ) )
18 17 1 9 grplactf1o 
 |-  ( ( G e. Grp /\ x e. X ) -> ( ( y e. X |-> ( z e. X |-> ( y ( +g ` G ) z ) ) ) ` x ) : X -1-1-onto-> X )
19 17 1 grplactfval 
 |-  ( x e. X -> ( ( y e. X |-> ( z e. X |-> ( y ( +g ` G ) z ) ) ) ` x ) = ( z e. X |-> ( x ( +g ` G ) z ) ) )
20 19 adantl 
 |-  ( ( G e. Grp /\ x e. X ) -> ( ( y e. X |-> ( z e. X |-> ( y ( +g ` G ) z ) ) ) ` x ) = ( z e. X |-> ( x ( +g ` G ) z ) ) )
21 f1oeq1 
 |-  ( ( ( y e. X |-> ( z e. X |-> ( y ( +g ` G ) z ) ) ) ` x ) = ( z e. X |-> ( x ( +g ` G ) z ) ) -> ( ( ( y e. X |-> ( z e. X |-> ( y ( +g ` G ) z ) ) ) ` x ) : X -1-1-onto-> X <-> ( z e. X |-> ( x ( +g ` G ) z ) ) : X -1-1-onto-> X ) )
22 20 21 syl 
 |-  ( ( G e. Grp /\ x e. X ) -> ( ( ( y e. X |-> ( z e. X |-> ( y ( +g ` G ) z ) ) ) ` x ) : X -1-1-onto-> X <-> ( z e. X |-> ( x ( +g ` G ) z ) ) : X -1-1-onto-> X ) )
23 18 22 mpbid 
 |-  ( ( G e. Grp /\ x e. X ) -> ( z e. X |-> ( x ( +g ` G ) z ) ) : X -1-1-onto-> X )
24 6 23 sylan 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x e. X ) -> ( z e. X |-> ( x ( +g ` G ) z ) ) : X -1-1-onto-> X )
25 f1of1 
 |-  ( ( z e. X |-> ( x ( +g ` G ) z ) ) : X -1-1-onto-> X -> ( z e. X |-> ( x ( +g ` G ) z ) ) : X -1-1-> X )
26 24 25 syl 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x e. X ) -> ( z e. X |-> ( x ( +g ` G ) z ) ) : X -1-1-> X )
27 7 adantr 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x e. X ) -> Y C_ X )
28 f1ores 
 |-  ( ( ( z e. X |-> ( x ( +g ` G ) z ) ) : X -1-1-> X /\ Y C_ X ) -> ( ( z e. X |-> ( x ( +g ` G ) z ) ) |` Y ) : Y -1-1-onto-> ( ( z e. X |-> ( x ( +g ` G ) z ) ) " Y ) )
29 26 27 28 syl2anc 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x e. X ) -> ( ( z e. X |-> ( x ( +g ` G ) z ) ) |` Y ) : Y -1-1-onto-> ( ( z e. X |-> ( x ( +g ` G ) z ) ) " Y ) )
30 f1oen2g 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( ( z e. X |-> ( x ( +g ` G ) z ) ) " Y ) e. _V /\ ( ( z e. X |-> ( x ( +g ` G ) z ) ) |` Y ) : Y -1-1-onto-> ( ( z e. X |-> ( x ( +g ` G ) z ) ) " Y ) ) -> Y ~~ ( ( z e. X |-> ( x ( +g ` G ) z ) ) " Y ) )
31 5 16 29 30 syl3anc 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x e. X ) -> Y ~~ ( ( z e. X |-> ( x ( +g ` G ) z ) ) " Y ) )
32 31 12 breqtrrd 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x e. X ) -> Y ~~ [ x ] .~ )
33 3 4 32 ectocld 
 |-  ( ( Y e. ( SubGrp ` G ) /\ A e. ( X /. .~ ) ) -> Y ~~ A )