Step |
Hyp |
Ref |
Expression |
0 |
|
cqg |
|- ~QG |
1 |
|
vr |
|- r |
2 |
|
cvv |
|- _V |
3 |
|
vi |
|- i |
4 |
|
vx |
|- x |
5 |
|
vy |
|- y |
6 |
4
|
cv |
|- x |
7 |
5
|
cv |
|- y |
8 |
6 7
|
cpr |
|- { x , y } |
9 |
|
cbs |
|- Base |
10 |
1
|
cv |
|- r |
11 |
10 9
|
cfv |
|- ( Base ` r ) |
12 |
8 11
|
wss |
|- { x , y } C_ ( Base ` r ) |
13 |
|
cminusg |
|- invg |
14 |
10 13
|
cfv |
|- ( invg ` r ) |
15 |
6 14
|
cfv |
|- ( ( invg ` r ) ` x ) |
16 |
|
cplusg |
|- +g |
17 |
10 16
|
cfv |
|- ( +g ` r ) |
18 |
15 7 17
|
co |
|- ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) |
19 |
3
|
cv |
|- i |
20 |
18 19
|
wcel |
|- ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i |
21 |
12 20
|
wa |
|- ( { x , y } C_ ( Base ` r ) /\ ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i ) |
22 |
21 4 5
|
copab |
|- { <. x , y >. | ( { x , y } C_ ( Base ` r ) /\ ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i ) } |
23 |
1 3 2 2 22
|
cmpo |
|- ( r e. _V , i e. _V |-> { <. x , y >. | ( { x , y } C_ ( Base ` r ) /\ ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i ) } ) |
24 |
0 23
|
wceq |
|- ~QG = ( r e. _V , i e. _V |-> { <. x , y >. | ( { x , y } C_ ( Base ` r ) /\ ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i ) } ) |