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 ) } )