Step |
Hyp |
Ref |
Expression |
1 |
|
opex |
|- <. ( A +R C ) , ( B +R D ) >. e. _V |
2 |
|
oveq1 |
|- ( w = A -> ( w +R u ) = ( A +R u ) ) |
3 |
|
oveq1 |
|- ( v = B -> ( v +R f ) = ( B +R f ) ) |
4 |
|
opeq12 |
|- ( ( ( w +R u ) = ( A +R u ) /\ ( v +R f ) = ( B +R f ) ) -> <. ( w +R u ) , ( v +R f ) >. = <. ( A +R u ) , ( B +R f ) >. ) |
5 |
2 3 4
|
syl2an |
|- ( ( w = A /\ v = B ) -> <. ( w +R u ) , ( v +R f ) >. = <. ( A +R u ) , ( B +R f ) >. ) |
6 |
|
oveq2 |
|- ( u = C -> ( A +R u ) = ( A +R C ) ) |
7 |
|
oveq2 |
|- ( f = D -> ( B +R f ) = ( B +R D ) ) |
8 |
|
opeq12 |
|- ( ( ( A +R u ) = ( A +R C ) /\ ( B +R f ) = ( B +R D ) ) -> <. ( A +R u ) , ( B +R f ) >. = <. ( A +R C ) , ( B +R D ) >. ) |
9 |
6 7 8
|
syl2an |
|- ( ( u = C /\ f = D ) -> <. ( A +R u ) , ( B +R f ) >. = <. ( A +R C ) , ( B +R D ) >. ) |
10 |
5 9
|
sylan9eq |
|- ( ( ( w = A /\ v = B ) /\ ( u = C /\ f = D ) ) -> <. ( w +R u ) , ( v +R f ) >. = <. ( A +R C ) , ( B +R D ) >. ) |
11 |
|
df-add |
|- + = { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +R u ) , ( v +R f ) >. ) ) } |
12 |
|
df-c |
|- CC = ( R. X. R. ) |
13 |
12
|
eleq2i |
|- ( x e. CC <-> x e. ( R. X. R. ) ) |
14 |
12
|
eleq2i |
|- ( y e. CC <-> y e. ( R. X. R. ) ) |
15 |
13 14
|
anbi12i |
|- ( ( x e. CC /\ y e. CC ) <-> ( x e. ( R. X. R. ) /\ y e. ( R. X. R. ) ) ) |
16 |
15
|
anbi1i |
|- ( ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +R u ) , ( v +R f ) >. ) ) <-> ( ( x e. ( R. X. R. ) /\ y e. ( R. X. R. ) ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +R u ) , ( v +R f ) >. ) ) ) |
17 |
16
|
oprabbii |
|- { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +R u ) , ( v +R f ) >. ) ) } = { <. <. x , y >. , z >. | ( ( x e. ( R. X. R. ) /\ y e. ( R. X. R. ) ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +R u ) , ( v +R f ) >. ) ) } |
18 |
11 17
|
eqtri |
|- + = { <. <. x , y >. , z >. | ( ( x e. ( R. X. R. ) /\ y e. ( R. X. R. ) ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +R u ) , ( v +R f ) >. ) ) } |
19 |
1 10 18
|
ov3 |
|- ( ( ( A e. R. /\ B e. R. ) /\ ( C e. R. /\ D e. R. ) ) -> ( <. A , B >. + <. C , D >. ) = <. ( A +R C ) , ( B +R D ) >. ) |