let x, x1, x2, y1, y2 be Surreal; :: thesis:
( ((x2 + (- x)) * y2) * x1 == ((x2 * y2) + ((- x) * y2)) * x1 & ((x2 * y2) + ((- x) * y2)) * x1 == ((x2 * y2) * x1) + (((- x) * y2) * x1) ) by SURREALR:51, SURREALR:67;
then ((x2 + (- x)) * y2) * x1 == ((x2 * y2) * x1) + (((- x) * y2) * x1) by SURREALO:4;
then ( (1_No + ((x2 + (- x)) * y2)) * x1 == (1_No * x1) + (((x2 + (- x)) * y2) * x1) & (1_No * x1) + (((x2 + (- x)) * y2) * x1) == x1 + (((x2 * y2) * x1) + (((- x) * y2) * x1)) ) by SURREALR:43, SURREALR:67;
then A1: (1_No + ((x2 + (- x)) * y2)) * x1 == x1 + (((x2 * y2) * x1) + (((- x) * y2) * x1)) by SURREALO:4;
( ((x1 + (- x)) * y1) * x2 == ((x1 * y1) + ((- x) * y1)) * x2 & ((x1 * y1) + ((- x) * y1)) * x2 == ((x1 * y1) * x2) + (((- x) * y1) * x2) ) by SURREALR:51, SURREALR:67;
then ((x1 + (- x)) * y1) * x2 == ((x1 * y1) * x2) + (((- x) * y1) * x2) by SURREALO:4;
then ( (1_No + ((x1 + (- x)) * y1)) * x2 == (1_No * x2) + (((x1 + (- x)) * y1) * x2) & (1_No * x2) + (((x1 + (- x)) * y1) * x2) == x2 + (((x1 * y1) * x2) + (((- x) * y1) * x2)) ) by SURREALR:43, SURREALR:67;
then (1_No + ((x1 + (- x)) * y1)) * x2 == x2 + (((x1 * y1) * x2) + (((- x) * y1) * x2)) by SURREALO:4;
then A2: - ((1_No + ((x1 + (- x)) * y1)) * x2) == - (x2 + (((x1 * y1) * x2) + (((- x) * y1) * x2))) by SURREALR:10;
A3: (x1 + (- x2)) * 1_No = x1 + (- x2) ;
(x1 + (- x2)) * (- (x * y1)) == (x1 * (- (x * y1))) + ((- x2) * (- (x * y1))) by SURREALR:67;
then ( (x1 + (- x2)) * (1_No + (- (x * y1))) == (x1 + (- x2)) + ((x1 + (- x2)) * (- (x * y1))) & (x1 + (- x2)) + ((x1 + (- x2)) * (- (x * y1))) == (x1 + (- x2)) + ((x1 * (- (x * y1))) + ((- x2) * (- (x * y1)))) ) by A3, SURREALR:43, SURREALR:67;
then A4: (x1 + (- x2)) * (1_No + (- (x * y1))) == (x1 + (- x2)) + ((x1 * (- (x * y1))) + ((- x2) * (- (x * y1)))) by SURREALO:4;
set X3 = x1 * (- (x * y1));
set X4 = (- x2) * (- (x * y1));
set Y3 = (y1 * x1) * x;
set X5 = ((- y2) * x1) * x;
set X6 = (y1 * x1) * (- x2);
set X7 = ((- y2) * x1) * (- x2);
A5: ( ((y1 * x1) + ((- y2) * x1)) * x == ((y1 * x1) * x) + (((- y2) * x1) * x) & ((y1 * x1) + ((- y2) * x1)) * (- x2) == ((y1 * x1) * (- x2)) + (((- y2) * x1) * (- x2)) ) by SURREALR:67;
( ((y1 + (- y2)) * x1) * (x + (- x2)) == ((y1 * x1) + ((- y2) * x1)) * (x + (- x2)) & ((y1 * x1) + ((- y2) * x1)) * (x + (- x2)) == (((y1 * x1) + ((- y2) * x1)) * x) + (((y1 * x1) + ((- y2) * x1)) * (- x2)) ) by SURREALR:51, SURREALR:67;
then ( ((y1 + (- y2)) * x1) * (x + (- x2)) == (((y1 * x1) + ((- y2) * x1)) * x) + (((y1 * x1) + ((- y2) * x1)) * (- x2)) & (((y1 * x1) + ((- y2) * x1)) * x) + (((y1 * x1) + ((- y2) * x1)) * (- x2)) == (((y1 * x1) * x) + (((- y2) * x1) * x)) + (((y1 * x1) * (- x2)) + (((- y2) * x1) * (- x2))) ) by A5, SURREALO:4, SURREALR:43;
then ((y1 + (- y2)) * x1) * (x + (- x2)) == (((y1 * x1) * x) + (((- y2) * x1) * x)) + (((y1 * x1) * (- x2)) + (((- y2) * x1) * (- x2))) by SURREALO:4;
then A6: ((x1 + (- x2)) * (1_No + (- (x * y1)))) + (((y1 + (- y2)) * x1) * (x + (- x2))) == ((x1 + (- x2)) + ((x1 * (- (x * y1))) + ((- x2) * (- (x * y1))))) + ((((y1 * x1) * x) + (((- y2) * x1) * x)) + (((y1 * x1) * (- x2)) + (((- y2) * x1) * (- x2)))) by A4, SURREALR:43;
A7: ((x1 * (- (x * y1))) + ((- x2) * (- (x * y1)))) + ((((y1 * x1) * x) + (((- y2) * x1) * x)) + (((y1 * x1) * (- x2)) + (((- y2) * x1) * (- x2)))) = ((- x2) * (- (x * y1))) + ((x1 * (- (x * y1))) + ((((y1 * x1) * x) + (((- y2) * x1) * x)) + (((y1 * x1) * (- x2)) + (((- y2) * x1) * (- x2))))) by SURREALR:37
.= (((x1 * (- (x * y1))) + (((y1 * x1) * x) + (((- y2) * x1) * x))) + ((((- y2) * x1) * (- x2)) + ((y1 * x1) * (- x2)))) + ((- x2) * (- (x * y1))) by SURREALR:37
.= ((((x1 * (- (x * y1))) + ((y1 * x1) * x)) + (((- y2) * x1) * x)) + ((((- y2) * x1) * (- x2)) + ((y1 * x1) * (- x2)))) + ((- x2) * (- (x * y1))) by SURREALR:37
.= (((((x1 * (- (x * y1))) + ((y1 * x1) * x)) + (((- y2) * x1) * x)) + (((- y2) * x1) * (- x2))) + ((y1 * x1) * (- x2))) + ((- x2) * (- (x * y1))) by SURREALR:37
.= ((((x1 * (- (x * y1))) + ((y1 * x1) * x)) + ((((- y2) * x1) * x) + (((- y2) * x1) * (- x2)))) + ((y1 * x1) * (- x2))) + ((- x2) * (- (x * y1))) by SURREALR:37
.= (((x1 * (- (x * y1))) + ((y1 * x1) * x)) + ((((- y2) * x1) * x) + (((- y2) * x1) * (- x2)))) + (((y1 * x1) * (- x2)) + ((- x2) * (- (x * y1)))) by SURREALR:37 ;
A8: ((x1 + (- x2)) + ((x1 * (- (x * y1))) + ((- x2) * (- (x * y1))))) + ((((y1 * x1) * x) + (((- y2) * x1) * x)) + (((y1 * x1) * (- x2)) + (((- y2) * x1) * (- x2)))) = (x1 + (- x2)) + (((x1 * (- (x * y1))) + ((- x2) * (- (x * y1)))) + ((((y1 * x1) * x) + (((- y2) * x1) * x)) + (((y1 * x1) * (- x2)) + (((- y2) * x1) * (- x2))))) by SURREALR:37
.= ((x1 + (- x2)) + (((x1 * (- (x * y1))) + ((y1 * x1) * x)) + ((((- y2) * x1) * x) + (((- y2) * x1) * (- x2))))) + (((y1 * x1) * (- x2)) + ((- x2) * (- (x * y1)))) by A7, SURREALR:37
.= (x1 + ((((x1 * (- (x * y1))) + ((y1 * x1) * x)) + ((((- y2) * x1) * x) + (((- y2) * x1) * (- x2)))) + (- x2))) + (((y1 * x1) * (- x2)) + ((- x2) * (- (x * y1)))) by SURREALR:37
.= x1 + (((((x1 * (- (x * y1))) + ((y1 * x1) * x)) + ((((- y2) * x1) * x) + (((- y2) * x1) * (- x2)))) + (- x2)) + (((y1 * x1) * (- x2)) + ((- x2) * (- (x * y1))))) by SURREALR:37
.= x1 + ((((x1 * (- (x * y1))) + ((y1 * x1) * x)) + ((((- y2) * x1) * x) + (((- y2) * x1) * (- x2)))) + ((- x2) + (((y1 * x1) * (- x2)) + ((- x2) * (- (x * y1)))))) by SURREALR:37
.= (x1 + (((x1 * (- (x * y1))) + ((y1 * x1) * x)) + ((((- y2) * x1) * x) + (((- y2) * x1) * (- x2))))) + ((- x2) + (((y1 * x1) * (- x2)) + ((- x2) * (- (x * y1))))) by SURREALR:37 ;
A9: - (x1 * (x * y1)) == - ((y1 * x1) * x) by SURREALR:65, SURREALR:69;
x1 * (- (x * y1)) == - ((y1 * x1) * x) by A9, SURREALR:58;
then ( (x1 * (- (x * y1))) + ((y1 * x1) * x) == (- ((y1 * x1) * x)) + ((y1 * x1) * x) & (- ((y1 * x1) * x)) + ((y1 * x1) * x) = ((y1 * x1) * x) - ((y1 * x1) * x) & ((y1 * x1) * x) - ((y1 * x1) * x) == 0_No ) by SURREALR:39, SURREALR:43;
then A10: (x1 * (- (x * y1))) + ((y1 * x1) * x) == 0_No by SURREALO:4;
((- y2) * x1) * x = (- (y2 * x1)) * x by SURREALR:58
.= - ((y2 * x1) * x) by SURREALR:58
.= (y2 * x1) * (- x) by SURREALR:58 ;
then A11: ((- y2) * x1) * x == ((- x) * y2) * x1 by SURREALR:69;
((- y2) * x1) * (- x2) = (- (y2 * x1)) * (- x2) by SURREALR:58
.= x2 * (y2 * x1) by SURREALR:58 ;
then ((- y2) * x1) * (- x2) == (x2 * y2) * x1 by SURREALR:69;
then (((- y2) * x1) * x) + (((- y2) * x1) * (- x2)) == ((x2 * y2) * x1) + (((- x) * y2) * x1) by A11, SURREALR:43;
then A12: ( ((x1 * (- (x * y1))) + ((y1 * x1) * x)) + ((((- y2) * x1) * x) + (((- y2) * x1) * (- x2))) == 0_No + (((x2 * y2) * x1) + (((- x) * y2) * x1)) & 0_No + (((x2 * y2) * x1) + (((- x) * y2) * x1)) = ((x2 * y2) * x1) + (((- x) * y2) * x1) ) by A10, SURREALR:43;
(- x2) * (- (x * y1)) = ((- x) * y1) * (- x2) by SURREALR:58
.= - (((- x) * y1) * x2) by SURREALR:58 ;
then A13: (- x2) + (((y1 * x1) * (- x2)) + ((- x2) * (- (x * y1)))) == (- x2) + ((- ((x1 * y1) * x2)) + (- (((- x) * y1) * x2))) by SURREALR:58;
x1 + (((x2 * y2) * x1) + (((- x) * y2) * x1)) == x1 + (((x1 * (- (x * y1))) + ((y1 * x1) * x)) + ((((- y2) * x1) * x) + (((- y2) * x1) * (- x2)))) by A12, SURREALR:43;
then A14: (x1 + (((x2 * y2) * x1) + (((- x) * y2) * x1))) + ((- x2) + ((- ((x1 * y1) * x2)) + (- (((- x) * y1) * x2)))) == (x1 + (((x1 * (- (x * y1))) + ((y1 * x1) * x)) + ((((- y2) * x1) * x) + (((- y2) * x1) * (- x2))))) + ((- x2) + (((y1 * x1) * (- x2)) + ((- x2) * (- (x * y1))))) by A13, SURREALR:43;
- (x2 + (((x1 * y1) * x2) + (((- x) * y1) * x2))) = (- x2) + (- (((x1 * y1) * x2) + (((- x) * y1) * x2))) by SURREALR:40
.= (- x2) + ((- ((x1 * y1) * x2)) + (- (((- x) * y1) * x2))) by SURREALR:40 ;
then A15: (x1 + (((x2 * y2) * x1) + (((- x) * y2) * x1))) + ((- x2) + ((- ((x1 * y1) * x2)) + (- (((- x) * y1) * x2)))) == ((1_No + ((x2 + (- x)) * y2)) * x1) + (- ((1_No + ((x1 + (- x)) * y1)) * x2)) by A1, A2, SURREALR:43;
then ((1_No + ((x2 + (- x)) * y2)) * x1) + (- ((1_No + ((x1 + (- x)) * y1)) * x2)) == (x1 + (((x1 * (- (x * y1))) + ((y1 * x1) * x)) + ((((- y2) * x1) * x) + (((- y2) * x1) * (- x2))))) + ((- x2) + (((y1 * x1) * (- x2)) + ((- x2) * (- (x * y1))))) by A14, SURREALO:4;
hence ((1_No + ((x2 - x) * y2)) * x1) + (- ((1_No + ((x1 - x) * y1)) * x2)) == ((x1 - x2) * (1_No - (x * y1))) + (((y1 - y2) * x1) * (x - x2)) by A6, A8, SURREALO:4; :: thesis:
A16: (x1 + (- x2)) * 1_No = x1 + (- x2) ;
(x1 + (- x2)) * (- (x * y2)) == (x1 * (- (x * y2))) + ((- x2) * (- (x * y2))) by SURREALR:67;
then ( (x1 + (- x2)) * (1_No + (- (x * y2))) == (x1 + (- x2)) + ((x1 + (- x2)) * (- (x * y2))) & (x1 + (- x2)) + ((x1 + (- x2)) * (- (x * y2))) == (x1 + (- x2)) + ((x1 * (- (x * y2))) + ((- x2) * (- (x * y2)))) ) by A16, SURREALR:43, SURREALR:67;
then A17: (x1 + (- x2)) * (1_No + (- (x * y2))) == (x1 + (- x2)) + ((x1 * (- (x * y2))) + ((- x2) * (- (x * y2)))) by SURREALO:4;
A18: ( ((y2 * x2) + ((- y1) * x2)) * x1 == ((y2 * x2) * x1) + (((- y1) * x2) * x1) & ((y2 * x2) + ((- y1) * x2)) * (- x) == ((y2 * x2) * (- x)) + (((- y1) * x2) * (- x)) ) by SURREALR:67;
( ((y2 + (- y1)) * x2) * (x1 + (- x)) == ((y2 * x2) + ((- y1) * x2)) * (x1 + (- x)) & ((y2 * x2) + ((- y1) * x2)) * (x1 + (- x)) == (((y2 * x2) + ((- y1) * x2)) * x1) + (((y2 * x2) + ((- y1) * x2)) * (- x)) ) by SURREALR:51, SURREALR:67;
then ( ((y2 + (- y1)) * x2) * (x1 + (- x)) == (((y2 * x2) + ((- y1) * x2)) * x1) + (((y2 * x2) + ((- y1) * x2)) * (- x)) & (((y2 * x2) + ((- y1) * x2)) * x1) + (((y2 * x2) + ((- y1) * x2)) * (- x)) == (((y2 * x2) * x1) + (((- y1) * x2) * x1)) + (((y2 * x2) * (- x)) + (((- y1) * x2) * (- x))) ) by A18, SURREALO:4, SURREALR:43;
then A19: ((y2 + (- y1)) * x2) * (x1 + (- x)) == (((y2 * x2) * x1) + (((- y1) * x2) * x1)) + (((y2 * x2) * (- x)) + (((- y1) * x2) * (- x))) by SURREALO:4;
set A2 = (y2 * x2) * x1;
set A3 = x1 * (- (x * y2));
set A4 = - x2;
set A5 = ((- y1) * x2) * x1;
set A6 = ((- y1) * x2) * (- x);
set A7 = (- x2) * (- (x * y2));
set B7 = (y2 * x2) * (- x);
A20: ((x1 + (- x2)) * (1_No + (- (x * y2)))) + (((y2 + (- y1)) * x2) * (x1 + (- x))) == ((x1 + (- x2)) + ((x1 * (- (x * y2))) + ((- x2) * (- (x * y2))))) + ((((y2 * x2) * x1) + (((- y1) * x2) * x1)) + (((y2 * x2) * (- x)) + (((- y1) * x2) * (- x)))) by A19, A17, SURREALR:43;
(((- x2) * (- (x * y2))) + (x1 * (- (x * y2)))) + (((y2 * x2) * (- x)) + ((y2 * x2) * x1)) = (((x1 * (- (x * y2))) + ((- x2) * (- (x * y2)))) + ((y2 * x2) * (- x))) + ((y2 * x2) * x1) by SURREALR:37
.= ((x1 * (- (x * y2))) + (((- x2) * (- (x * y2))) + ((y2 * x2) * (- x)))) + ((y2 * x2) * x1) by SURREALR:37
.= (((y2 * x2) * x1) + (x1 * (- (x * y2)))) + (((- x2) * (- (x * y2))) + ((y2 * x2) * (- x))) by SURREALR:37 ;
then ((x1 * (- (x * y2))) + ((- x2) * (- (x * y2)))) + ((((y2 * x2) * x1) + ((y2 * x2) * (- x))) + ((((- y1) * x2) * x1) + (((- y1) * x2) * (- x)))) = ((((y2 * x2) * x1) + (x1 * (- (x * y2)))) + (((- x2) * (- (x * y2))) + ((y2 * x2) * (- x)))) + ((((- y1) * x2) * x1) + (((- y1) * x2) * (- x))) by SURREALR:37;
then A21: (x1 + (- x2)) + (((x1 * (- (x * y2))) + ((- x2) * (- (x * y2)))) + ((((y2 * x2) * x1) + ((y2 * x2) * (- x))) + ((((- y1) * x2) * x1) + (((- y1) * x2) * (- x))))) = x1 + ((((((y2 * x2) * x1) + (x1 * (- (x * y2)))) + (((- x2) * (- (x * y2))) + ((y2 * x2) * (- x)))) + ((((- y1) * x2) * x1) + (((- y1) * x2) * (- x)))) + (- x2)) by SURREALR:37
.= x1 + (((((y2 * x2) * x1) + (x1 * (- (x * y2)))) + (((- x2) * (- (x * y2))) + ((y2 * x2) * (- x)))) + (((((- y1) * x2) * x1) + (((- y1) * x2) * (- x))) + (- x2))) by SURREALR:37
.= (x1 + ((((y2 * x2) * x1) + (x1 * (- (x * y2)))) + (((- x2) * (- (x * y2))) + ((y2 * x2) * (- x))))) + ((- x2) + ((((- y1) * x2) * x1) + (((- y1) * x2) * (- x)))) by SURREALR:37
.= ((x1 + (((y2 * x2) * x1) + (x1 * (- (x * y2))))) + (((- x2) * (- (x * y2))) + ((y2 * x2) * (- x)))) + ((- x2) + ((((- y1) * x2) * x1) + (((- y1) * x2) * (- x)))) by SURREALR:37 ;
A22: (((y2 * x2) * x1) + (((- y1) * x2) * x1)) + (((y2 * x2) * (- x)) + (((- y1) * x2) * (- x))) = ((((y2 * x2) * x1) + (((- y1) * x2) * x1)) + (((- y1) * x2) * (- x))) + ((y2 * x2) * (- x)) by SURREALR:37
.= (((y2 * x2) * x1) + ((((- y1) * x2) * x1) + (((- y1) * x2) * (- x)))) + ((y2 * x2) * (- x)) by SURREALR:37
.= (((y2 * x2) * x1) + ((y2 * x2) * (- x))) + ((((- y1) * x2) * x1) + (((- y1) * x2) * (- x))) by SURREALR:37 ;
A23: ((x1 + (- x2)) + ((x1 * (- (x * y2))) + ((- x2) * (- (x * y2))))) + ((((y2 * x2) * x1) + ((y2 * x2) * (- x))) + ((((- y1) * x2) * x1) + (((- y1) * x2) * (- x)))) = ((x1 + (((y2 * x2) * x1) + (x1 * (- (x * y2))))) + (((- x2) * (- (x * y2))) + ((y2 * x2) * (- x)))) + ((- x2) + ((((- y1) * x2) * x1) + (((- y1) * x2) * (- x)))) by A21, SURREALR:37;
A24: ((y2 * x2) * x1) + (x1 * (- (x * y2))) = ((x2 * y2) * x1) + (((- x) * y2) * x1) by SURREALR:58;
((- y1) * x2) * x1 = (- (y1 * x2)) * x1 by SURREALR:58
.= - ((y1 * x2) * x1) by SURREALR:58 ;
then A25: ((- y1) * x2) * x1 == - ((x1 * y1) * x2) by SURREALR:65, SURREALR:69;
A26: ((- y1) * x2) * (- x) = (- (y1 * x2)) * (- x) by SURREALR:58
.= - ((y1 * x2) * (- x)) by SURREALR:58 ;
((- y1) * x2) * (- x) == - (((- x) * y1) * x2) by A26, SURREALR:65, SURREALR:69;
then (((- y1) * x2) * x1) + (((- y1) * x2) * (- x)) == (- ((x1 * y1) * x2)) + (- (((- x) * y1) * x2)) by A25, SURREALR:43;
then A27: (- x2) + ((((- y1) * x2) * x1) + (((- y1) * x2) * (- x))) == (- x2) + ((- ((x1 * y1) * x2)) + (- (((- x) * y1) * x2))) by SURREALR:43;
A28: (- x2) * (- (x * y2)) = - (x2 * (- (x * y2))) by SURREALR:58;
- (x * y2) = (- x) * y2 by SURREALR:58;
then x2 * (- (x * y2)) == (y2 * x2) * (- x) by SURREALR:69;
then (- x2) * (- (x * y2)) == - ((y2 * x2) * (- x)) by A28, SURREALR:10;
then ( ((- x2) * (- (x * y2))) + ((y2 * x2) * (- x)) == (- ((y2 * x2) * (- x))) + ((y2 * x2) * (- x)) & (- ((y2 * x2) * (- x))) + ((y2 * x2) * (- x)) = ((y2 * x2) * (- x)) - ((y2 * x2) * (- x)) & ((y2 * x2) * (- x)) - ((y2 * x2) * (- x)) == 0_No ) by SURREALR:39, SURREALR:43;
then A29: ((- x2) * (- (x * y2))) + ((y2 * x2) * (- x)) == 0_No by SURREALO:4;
(x1 + (((y2 * x2) * x1) + (x1 * (- (x * y2))))) + (((- x2) * (- (x * y2))) + ((y2 * x2) * (- x))) == (x1 + (((x2 * y2) * x1) + (((- x) * y2) * x1))) + 0_No by A29, SURREALR:43, A24;
then ((x1 + (((y2 * x2) * x1) + (x1 * (- (x * y2))))) + (((- x2) * (- (x * y2))) + ((y2 * x2) * (- x)))) + ((- x2) + ((((- y1) * x2) * x1) + (((- y1) * x2) * (- x)))) == (x1 + (((x2 * y2) * x1) + (((- x) * y2) * x1))) + ((- x2) + ((- ((x1 * y1) * x2)) + (- (((- x) * y1) * x2)))) by A27, SURREALR:43;
then ((x1 + (- x2)) + ((x1 * (- (x * y2))) + ((- x2) * (- (x * y2))))) + ((((y2 * x2) * x1) + ((y2 * x2) * (- x))) + ((((- y1) * x2) * x1) + (((- y1) * x2) * (- x)))) == ((1_No + ((x2 + (- x)) * y2)) * x1) + (- ((1_No + ((x1 + (- x)) * y1)) * x2)) by A23, SURREALO:4, A15;
hence ((1_No + ((x2 - x) * y2)) * x1) - ((1_No + ((x1 - x) * y1)) * x2) == ((x1 - x2) * (1_No - (x * y2))) + (((y2 - y1) * x2) * (x1 - x)) by A22, A20, SURREALO:4; :: thesis: