Metamath Proof Explorer


Theorem eqgfval

Description: Value of the subgroup left coset equivalence relation. (Contributed by Mario Carneiro, 15-Jan-2015)

Ref Expression
Hypotheses eqgval.x
|- X = ( Base ` G )
eqgval.n
|- N = ( invg ` G )
eqgval.p
|- .+ = ( +g ` G )
eqgval.r
|- R = ( G ~QG S )
Assertion eqgfval
|- ( ( G e. V /\ S C_ X ) -> R = { <. x , y >. | ( { x , y } C_ X /\ ( ( N ` x ) .+ y ) e. S ) } )

Proof

Step Hyp Ref Expression
1 eqgval.x
 |-  X = ( Base ` G )
2 eqgval.n
 |-  N = ( invg ` G )
3 eqgval.p
 |-  .+ = ( +g ` G )
4 eqgval.r
 |-  R = ( G ~QG S )
5 elex
 |-  ( G e. V -> G e. _V )
6 1 fvexi
 |-  X e. _V
7 6 ssex
 |-  ( S C_ X -> S e. _V )
8 simpl
 |-  ( ( g = G /\ s = S ) -> g = G )
9 8 fveq2d
 |-  ( ( g = G /\ s = S ) -> ( Base ` g ) = ( Base ` G ) )
10 9 1 eqtr4di
 |-  ( ( g = G /\ s = S ) -> ( Base ` g ) = X )
11 10 sseq2d
 |-  ( ( g = G /\ s = S ) -> ( { x , y } C_ ( Base ` g ) <-> { x , y } C_ X ) )
12 8 fveq2d
 |-  ( ( g = G /\ s = S ) -> ( +g ` g ) = ( +g ` G ) )
13 12 3 eqtr4di
 |-  ( ( g = G /\ s = S ) -> ( +g ` g ) = .+ )
14 8 fveq2d
 |-  ( ( g = G /\ s = S ) -> ( invg ` g ) = ( invg ` G ) )
15 14 2 eqtr4di
 |-  ( ( g = G /\ s = S ) -> ( invg ` g ) = N )
16 15 fveq1d
 |-  ( ( g = G /\ s = S ) -> ( ( invg ` g ) ` x ) = ( N ` x ) )
17 eqidd
 |-  ( ( g = G /\ s = S ) -> y = y )
18 13 16 17 oveq123d
 |-  ( ( g = G /\ s = S ) -> ( ( ( invg ` g ) ` x ) ( +g ` g ) y ) = ( ( N ` x ) .+ y ) )
19 simpr
 |-  ( ( g = G /\ s = S ) -> s = S )
20 18 19 eleq12d
 |-  ( ( g = G /\ s = S ) -> ( ( ( ( invg ` g ) ` x ) ( +g ` g ) y ) e. s <-> ( ( N ` x ) .+ y ) e. S ) )
21 11 20 anbi12d
 |-  ( ( g = G /\ s = S ) -> ( ( { x , y } C_ ( Base ` g ) /\ ( ( ( invg ` g ) ` x ) ( +g ` g ) y ) e. s ) <-> ( { x , y } C_ X /\ ( ( N ` x ) .+ y ) e. S ) ) )
22 21 opabbidv
 |-  ( ( g = G /\ s = S ) -> { <. x , y >. | ( { x , y } C_ ( Base ` g ) /\ ( ( ( invg ` g ) ` x ) ( +g ` g ) y ) e. s ) } = { <. x , y >. | ( { x , y } C_ X /\ ( ( N ` x ) .+ y ) e. S ) } )
23 df-eqg
 |-  ~QG = ( g e. _V , s e. _V |-> { <. x , y >. | ( { x , y } C_ ( Base ` g ) /\ ( ( ( invg ` g ) ` x ) ( +g ` g ) y ) e. s ) } )
24 6 6 xpex
 |-  ( X X. X ) e. _V
25 simpl
 |-  ( ( { x , y } C_ X /\ ( ( N ` x ) .+ y ) e. S ) -> { x , y } C_ X )
26 vex
 |-  x e. _V
27 vex
 |-  y e. _V
28 26 27 prss
 |-  ( ( x e. X /\ y e. X ) <-> { x , y } C_ X )
29 25 28 sylibr
 |-  ( ( { x , y } C_ X /\ ( ( N ` x ) .+ y ) e. S ) -> ( x e. X /\ y e. X ) )
30 29 ssopab2i
 |-  { <. x , y >. | ( { x , y } C_ X /\ ( ( N ` x ) .+ y ) e. S ) } C_ { <. x , y >. | ( x e. X /\ y e. X ) }
31 df-xp
 |-  ( X X. X ) = { <. x , y >. | ( x e. X /\ y e. X ) }
32 30 31 sseqtrri
 |-  { <. x , y >. | ( { x , y } C_ X /\ ( ( N ` x ) .+ y ) e. S ) } C_ ( X X. X )
33 24 32 ssexi
 |-  { <. x , y >. | ( { x , y } C_ X /\ ( ( N ` x ) .+ y ) e. S ) } e. _V
34 22 23 33 ovmpoa
 |-  ( ( G e. _V /\ S e. _V ) -> ( G ~QG S ) = { <. x , y >. | ( { x , y } C_ X /\ ( ( N ` x ) .+ y ) e. S ) } )
35 4 34 syl5eq
 |-  ( ( G e. _V /\ S e. _V ) -> R = { <. x , y >. | ( { x , y } C_ X /\ ( ( N ` x ) .+ y ) e. S ) } )
36 5 7 35 syl2an
 |-  ( ( G e. V /\ S C_ X ) -> R = { <. x , y >. | ( { x , y } C_ X /\ ( ( N ` x ) .+ y ) e. S ) } )