This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eqglact

Description: A left coset can be expressed as the image of a left action. (Contributed by Mario Carneiro, 20-Sep-2015)

Ref Expression
Hypotheses eqger.x 
|- X = ( Base ` G )
eqger.r 
|- .~ = ( G ~QG Y )
eqglact.3 
|- .+ = ( +g ` G )
Assertion eqglact 
|- ( ( G e. Grp /\ Y C_ X /\ A e. X ) -> [ A ] .~ = ( ( x e. X |-> ( A .+ x ) ) " Y ) )

Proof

Step Hyp Ref Expression
1 eqger.x 
 |-  X = ( Base ` G )
2 eqger.r 
 |-  .~ = ( G ~QG Y )
3 eqglact.3 
 |-  .+ = ( +g ` G )
4 eqid 
 |-  ( invg ` G ) = ( invg ` G )
5 1 4 3 2 eqgval 
 |-  ( ( G e. Grp /\ Y C_ X ) -> ( A .~ x <-> ( A e. X /\ x e. X /\ ( ( ( invg ` G ) ` A ) .+ x ) e. Y ) ) )
6 3anass 
 |-  ( ( A e. X /\ x e. X /\ ( ( ( invg ` G ) ` A ) .+ x ) e. Y ) <-> ( A e. X /\ ( x e. X /\ ( ( ( invg ` G ) ` A ) .+ x ) e. Y ) ) )
7 5 6 bitrdi 
 |-  ( ( G e. Grp /\ Y C_ X ) -> ( A .~ x <-> ( A e. X /\ ( x e. X /\ ( ( ( invg ` G ) ` A ) .+ x ) e. Y ) ) ) )
8 7 baibd 
 |-  ( ( ( G e. Grp /\ Y C_ X ) /\ A e. X ) -> ( A .~ x <-> ( x e. X /\ ( ( ( invg ` G ) ` A ) .+ x ) e. Y ) ) )
9 8 3impa 
 |-  ( ( G e. Grp /\ Y C_ X /\ A e. X ) -> ( A .~ x <-> ( x e. X /\ ( ( ( invg ` G ) ` A ) .+ x ) e. Y ) ) )
10 9 abbidv 
 |-  ( ( G e. Grp /\ Y C_ X /\ A e. X ) -> { x | A .~ x } = { x | ( x e. X /\ ( ( ( invg ` G ) ` A ) .+ x ) e. Y ) } )
11 dfec2 
 |-  ( A e. X -> [ A ] .~ = { x | A .~ x } )
12 11 3ad2ant3 
 |-  ( ( G e. Grp /\ Y C_ X /\ A e. X ) -> [ A ] .~ = { x | A .~ x } )
13 eqid 
 |-  ( g e. X |-> ( x e. X |-> ( g .+ x ) ) ) = ( g e. X |-> ( x e. X |-> ( g .+ x ) ) )
14 13 1 3 4 grplactcnv 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( ( g e. X |-> ( x e. X |-> ( g .+ x ) ) ) ` A ) : X -1-1-onto-> X /\ `' ( ( g e. X |-> ( x e. X |-> ( g .+ x ) ) ) ` A ) = ( ( g e. X |-> ( x e. X |-> ( g .+ x ) ) ) ` ( ( invg ` G ) ` A ) ) ) )
15 14 simprd 
 |-  ( ( G e. Grp /\ A e. X ) -> `' ( ( g e. X |-> ( x e. X |-> ( g .+ x ) ) ) ` A ) = ( ( g e. X |-> ( x e. X |-> ( g .+ x ) ) ) ` ( ( invg ` G ) ` A ) ) )
16 13 1 grplactfval 
 |-  ( A e. X -> ( ( g e. X |-> ( x e. X |-> ( g .+ x ) ) ) ` A ) = ( x e. X |-> ( A .+ x ) ) )
17 16 adantl 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( g e. X |-> ( x e. X |-> ( g .+ x ) ) ) ` A ) = ( x e. X |-> ( A .+ x ) ) )
18 17 cnveqd 
 |-  ( ( G e. Grp /\ A e. X ) -> `' ( ( g e. X |-> ( x e. X |-> ( g .+ x ) ) ) ` A ) = `' ( x e. X |-> ( A .+ x ) ) )
19 1 4 grpinvcl 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( invg ` G ) ` A ) e. X )
20 13 1 grplactfval 
 |-  ( ( ( invg ` G ) ` A ) e. X -> ( ( g e. X |-> ( x e. X |-> ( g .+ x ) ) ) ` ( ( invg ` G ) ` A ) ) = ( x e. X |-> ( ( ( invg ` G ) ` A ) .+ x ) ) )
21 19 20 syl 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( g e. X |-> ( x e. X |-> ( g .+ x ) ) ) ` ( ( invg ` G ) ` A ) ) = ( x e. X |-> ( ( ( invg ` G ) ` A ) .+ x ) ) )
22 15 18 21 3eqtr3d 
 |-  ( ( G e. Grp /\ A e. X ) -> `' ( x e. X |-> ( A .+ x ) ) = ( x e. X |-> ( ( ( invg ` G ) ` A ) .+ x ) ) )
23 22 cnveqd 
 |-  ( ( G e. Grp /\ A e. X ) -> `' `' ( x e. X |-> ( A .+ x ) ) = `' ( x e. X |-> ( ( ( invg ` G ) ` A ) .+ x ) ) )
24 23 3adant2 
 |-  ( ( G e. Grp /\ Y C_ X /\ A e. X ) -> `' `' ( x e. X |-> ( A .+ x ) ) = `' ( x e. X |-> ( ( ( invg ` G ) ` A ) .+ x ) ) )
25 24 imaeq1d 
 |-  ( ( G e. Grp /\ Y C_ X /\ A e. X ) -> ( `' `' ( x e. X |-> ( A .+ x ) ) " Y ) = ( `' ( x e. X |-> ( ( ( invg ` G ) ` A ) .+ x ) ) " Y ) )
26 imacnvcnv 
 |-  ( `' `' ( x e. X |-> ( A .+ x ) ) " Y ) = ( ( x e. X |-> ( A .+ x ) ) " Y )
27 eqid 
 |-  ( x e. X |-> ( ( ( invg ` G ) ` A ) .+ x ) ) = ( x e. X |-> ( ( ( invg ` G ) ` A ) .+ x ) )
28 27 mptpreima 
 |-  ( `' ( x e. X |-> ( ( ( invg ` G ) ` A ) .+ x ) ) " Y ) = { x e. X | ( ( ( invg ` G ) ` A ) .+ x ) e. Y }
29 df-rab 
 |-  { x e. X | ( ( ( invg ` G ) ` A ) .+ x ) e. Y } = { x | ( x e. X /\ ( ( ( invg ` G ) ` A ) .+ x ) e. Y ) }
30 28 29 eqtri 
 |-  ( `' ( x e. X |-> ( ( ( invg ` G ) ` A ) .+ x ) ) " Y ) = { x | ( x e. X /\ ( ( ( invg ` G ) ` A ) .+ x ) e. Y ) }
31 25 26 30 3eqtr3g 
 |-  ( ( G e. Grp /\ Y C_ X /\ A e. X ) -> ( ( x e. X |-> ( A .+ x ) ) " Y ) = { x | ( x e. X /\ ( ( ( invg ` G ) ` A ) .+ x ) e. Y ) } )
32 10 12 31 3eqtr4d 
 |-  ( ( G e. Grp /\ Y C_ X /\ A e. X ) -> [ A ] .~ = ( ( x e. X |-> ( A .+ x ) ) " Y ) )