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