Metamath Proof Explorer

Theorem eqgval

Description: Value of the subgroup left coset equivalence relation. (Contributed by Mario Carneiro, 15-Jan-2015) (Revised by Mario Carneiro, 14-Jun-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 eqgval 
|- ( ( G e. V /\ S C_ X ) -> ( A R B <-> ( A e. X /\ B e. X /\ ( ( N ` A ) .+ B ) 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 1 2 3 4 eqgfval 
 |-  ( ( G e. V /\ S C_ X ) -> R = { <. x , y >. | ( { x , y } C_ X /\ ( ( N ` x ) .+ y ) e. S ) } )
6 5 breqd 
 |-  ( ( G e. V /\ S C_ X ) -> ( A R B <-> A { <. x , y >. | ( { x , y } C_ X /\ ( ( N ` x ) .+ y ) e. S ) } B ) )
7 brabv 
 |-  ( A { <. x , y >. | ( { x , y } C_ X /\ ( ( N ` x ) .+ y ) e. S ) } B -> ( A e. _V /\ B e. _V ) )
8 7 adantl 
 |-  ( ( ( G e. V /\ S C_ X ) /\ A { <. x , y >. | ( { x , y } C_ X /\ ( ( N ` x ) .+ y ) e. S ) } B ) -> ( A e. _V /\ B e. _V ) )
9 simpr1 
 |-  ( ( ( G e. V /\ S C_ X ) /\ ( A e. X /\ B e. X /\ ( ( N ` A ) .+ B ) e. S ) ) -> A e. X )
10 9 elexd 
 |-  ( ( ( G e. V /\ S C_ X ) /\ ( A e. X /\ B e. X /\ ( ( N ` A ) .+ B ) e. S ) ) -> A e. _V )
11 simpr2 
 |-  ( ( ( G e. V /\ S C_ X ) /\ ( A e. X /\ B e. X /\ ( ( N ` A ) .+ B ) e. S ) ) -> B e. X )
12 11 elexd 
 |-  ( ( ( G e. V /\ S C_ X ) /\ ( A e. X /\ B e. X /\ ( ( N ` A ) .+ B ) e. S ) ) -> B e. _V )
13 10 12 jca 
 |-  ( ( ( G e. V /\ S C_ X ) /\ ( A e. X /\ B e. X /\ ( ( N ` A ) .+ B ) e. S ) ) -> ( A e. _V /\ B e. _V ) )
14 vex 
 |-  x e. _V
15 vex 
 |-  y e. _V
16 14 15 prss 
 |-  ( ( x e. X /\ y e. X ) <-> { x , y } C_ X )
17 eleq1 
 |-  ( x = A -> ( x e. X <-> A e. X ) )
18 eleq1 
 |-  ( y = B -> ( y e. X <-> B e. X ) )
19 17 18 bi2anan9 
 |-  ( ( x = A /\ y = B ) -> ( ( x e. X /\ y e. X ) <-> ( A e. X /\ B e. X ) ) )
20 16 19 bitr3id 
 |-  ( ( x = A /\ y = B ) -> ( { x , y } C_ X <-> ( A e. X /\ B e. X ) ) )
21 fveq2 
 |-  ( x = A -> ( N ` x ) = ( N ` A ) )
22 id 
 |-  ( y = B -> y = B )
23 21 22 oveqan12d 
 |-  ( ( x = A /\ y = B ) -> ( ( N ` x ) .+ y ) = ( ( N ` A ) .+ B ) )
24 23 eleq1d 
 |-  ( ( x = A /\ y = B ) -> ( ( ( N ` x ) .+ y ) e. S <-> ( ( N ` A ) .+ B ) e. S ) )
25 20 24 anbi12d 
 |-  ( ( x = A /\ y = B ) -> ( ( { x , y } C_ X /\ ( ( N ` x ) .+ y ) e. S ) <-> ( ( A e. X /\ B e. X ) /\ ( ( N ` A ) .+ B ) e. S ) ) )
26 df-3an 
 |-  ( ( A e. X /\ B e. X /\ ( ( N ` A ) .+ B ) e. S ) <-> ( ( A e. X /\ B e. X ) /\ ( ( N ` A ) .+ B ) e. S ) )
27 25 26 bitr4di 
 |-  ( ( x = A /\ y = B ) -> ( ( { x , y } C_ X /\ ( ( N ` x ) .+ y ) e. S ) <-> ( A e. X /\ B e. X /\ ( ( N ` A ) .+ B ) e. S ) ) )
28 eqid 
 |-  { <. x , y >. | ( { x , y } C_ X /\ ( ( N ` x ) .+ y ) e. S ) } = { <. x , y >. | ( { x , y } C_ X /\ ( ( N ` x ) .+ y ) e. S ) }
29 27 28 brabga 
 |-  ( ( A e. _V /\ B e. _V ) -> ( A { <. x , y >. | ( { x , y } C_ X /\ ( ( N ` x ) .+ y ) e. S ) } B <-> ( A e. X /\ B e. X /\ ( ( N ` A ) .+ B ) e. S ) ) )
30 8 13 29 pm5.21nd 
 |-  ( ( G e. V /\ S C_ X ) -> ( A { <. x , y >. | ( { x , y } C_ X /\ ( ( N ` x ) .+ y ) e. S ) } B <-> ( A e. X /\ B e. X /\ ( ( N ` A ) .+ B ) e. S ) ) )
31 6 30 bitrd 
 |-  ( ( G e. V /\ S C_ X ) -> ( A R B <-> ( A e. X /\ B e. X /\ ( ( N ` A ) .+ B ) e. S ) ) )