:: ANALORT semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let V be non empty Abelian LoopStr ;
let v, w be Element of V;
:: original: +
redefine func v + w -> M3(the carrier of V);
commutativity
for v, w being Element of V holds v + w = w + v
by RLVECT_1:def 5;
end;

Lm1: for V being RealLinearSpace
for v1, x, y, v2 being VECTOR of V
for b1, b2, c1, c2 being Real st v1 = (b1 * x) + (b2 * y) & v2 = (c1 * x) + (c2 * y) holds
( v1 + v2 = ((b1 + c1) * x) + ((b2 + c2) * y) & v1 - v2 = ((b1 - c1) * x) + ((b2 - c2) * y) )
proof end;

Lm2: for V being RealLinearSpace
for v, x, y being VECTOR of V
for b1, b2, a being Real st v = (b1 * x) + (b2 * y) holds
a * v = ((a * b1) * x) + ((a * b2) * y)
proof end;

Lm3: for V being RealLinearSpace
for x, y being VECTOR of V
for a1, a2, b1, b2 being Real st Gen x,y & (a1 * x) + (a2 * y) = (b1 * x) + (b2 * y) holds
( a1 = b1 & a2 = b2 )
proof end;

Lm4: for V being RealLinearSpace
for x, y being VECTOR of V st Gen x,y holds
( x <> 0. V & y <> 0. V )
proof end;

Lm5: for V being RealLinearSpace
for x, y, u being VECTOR of V st Gen x,y holds
u = ((pr1 x,y,u) * x) + ((pr2 x,y,u) * y)
proof end;

Lm6: for V being RealLinearSpace
for x, y, u being VECTOR of V
for k1, k2 being Real st Gen x,y & u = (k1 * x) + (k2 * y) holds
( k1 = pr1 x,y,u & k2 = pr2 x,y,u )
proof end;

Lm7: for V being RealLinearSpace
for x, y, u, v being VECTOR of V
for a being Real st Gen x,y holds
( pr1 x,y,(u + v) = (pr1 x,y,u) + (pr1 x,y,v) & pr2 x,y,(u + v) = (pr2 x,y,u) + (pr2 x,y,v) & pr1 x,y,(u - v) = (pr1 x,y,u) - (pr1 x,y,v) & pr2 x,y,(u - v) = (pr2 x,y,u) - (pr2 x,y,v) & pr1 x,y,(a * u) = a * (pr1 x,y,u) & pr2 x,y,(a * u) = a * (pr2 x,y,u) )
proof end;

definition
let V be RealLinearSpace;
let x, y, u be VECTOR of V;
func Ortm x,y,u -> VECTOR of V equals :: ANALORT:def 1
((pr1 x,y,u) * x) + ((- (pr2 x,y,u)) * y);
correctness
coherence
((pr1 x,y,u) * x) + ((- (pr2 x,y,u)) * y) is VECTOR of V
;
;
end;

:: deftheorem defines Ortm ANALORT:def 1 :
for V being RealLinearSpace
for x, y, u being VECTOR of V holds Ortm x,y,u = ((pr1 x,y,u) * x) + ((- (pr2 x,y,u)) * y);

theorem Th1: :: ANALORT:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u, v being VECTOR of V st Gen x,y holds
Ortm x,y,(u + v) = (Ortm x,y,u) + (Ortm x,y,v)
proof end;

theorem Th2: :: ANALORT:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u being VECTOR of V
for n being Real st Gen x,y holds
Ortm x,y,(n * u) = n * (Ortm x,y,u)
proof end;

theorem :: ANALORT:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y being VECTOR of V st Gen x,y holds
Ortm x,y,(0. V) = 0. V
proof end;

theorem Th4: :: ANALORT:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u being VECTOR of V st Gen x,y holds
Ortm x,y,(- u) = - (Ortm x,y,u)
proof end;

theorem Th5: :: ANALORT:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u, v being VECTOR of V st Gen x,y holds
Ortm x,y,(u - v) = (Ortm x,y,u) - (Ortm x,y,v)
proof end;

theorem Th6: :: ANALORT:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u, v being VECTOR of V st Gen x,y & Ortm x,y,u = Ortm x,y,v holds
u = v
proof end;

theorem Th7: :: ANALORT:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u being VECTOR of V st Gen x,y holds
Ortm x,y,(Ortm x,y,u) = u
proof end;

theorem Th8: :: ANALORT:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u being VECTOR of V st Gen x,y holds
ex v being VECTOR of V st u = Ortm x,y,v
proof end;

definition
let V be RealLinearSpace;
let x, y, u be VECTOR of V;
func Orte x,y,u -> VECTOR of V equals :: ANALORT:def 2
((pr2 x,y,u) * x) + ((- (pr1 x,y,u)) * y);
correctness
coherence
((pr2 x,y,u) * x) + ((- (pr1 x,y,u)) * y) is VECTOR of V
;
;
end;

:: deftheorem defines Orte ANALORT:def 2 :
for V being RealLinearSpace
for x, y, u being VECTOR of V holds Orte x,y,u = ((pr2 x,y,u) * x) + ((- (pr1 x,y,u)) * y);

theorem Th9: :: ANALORT:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, v being VECTOR of V st Gen x,y holds
Orte x,y,(- v) = - (Orte x,y,v)
proof end;

theorem Th10: :: ANALORT:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u, v being VECTOR of V st Gen x,y holds
Orte x,y,(u + v) = (Orte x,y,u) + (Orte x,y,v)
proof end;

theorem Th11: :: ANALORT:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u, v being VECTOR of V st Gen x,y holds
Orte x,y,(u - v) = (Orte x,y,u) - (Orte x,y,v)
proof end;

theorem Th12: :: ANALORT:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u being VECTOR of V
for n being Real st Gen x,y holds
Orte x,y,(n * u) = n * (Orte x,y,u)
proof end;

theorem Th13: :: ANALORT:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u, v being VECTOR of V st Gen x,y & Orte x,y,u = Orte x,y,v holds
u = v
proof end;

theorem Th14: :: ANALORT:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u being VECTOR of V st Gen x,y holds
Orte x,y,(Orte x,y,u) = - u
proof end;

theorem Th15: :: ANALORT:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u being VECTOR of V st Gen x,y holds
ex v being VECTOR of V st Orte x,y,v = u
proof end;

definition
let V be RealLinearSpace;
let x, y, u, v, u1, v1 be VECTOR of V;
pred u,v,u1,v1 are_COrte_wrt x,y means :Def3: :: ANALORT:def 3
Orte x,y,u, Orte x,y,v // u1,v1;
pred u,v,u1,v1 are_COrtm_wrt x,y means :Def4: :: ANALORT:def 4
Ortm x,y,u, Ortm x,y,v // u1,v1;
end;

:: deftheorem Def3 defines are_COrte_wrt ANALORT:def 3 :
for V being RealLinearSpace
for x, y, u, v, u1, v1 being VECTOR of V holds
( u,v,u1,v1 are_COrte_wrt x,y iff Orte x,y,u, Orte x,y,v // u1,v1 );

:: deftheorem Def4 defines are_COrtm_wrt ANALORT:def 4 :
for V being RealLinearSpace
for x, y, u, v, u1, v1 being VECTOR of V holds
( u,v,u1,v1 are_COrtm_wrt x,y iff Ortm x,y,u, Ortm x,y,v // u1,v1 );

theorem Th16: :: ANALORT:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u, v, u1, v1 being VECTOR of V st Gen x,y & u,v // u1,v1 holds
Orte x,y,u, Orte x,y,v // Orte x,y,u1, Orte x,y,v1
proof end;

theorem Th17: :: ANALORT:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u, v, u1, v1 being VECTOR of V st Gen x,y & u,v // u1,v1 holds
Ortm x,y,u, Ortm x,y,v // Ortm x,y,u1, Ortm x,y,v1
proof end;

theorem Th18: :: ANALORT:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u, u1, v, v1 being VECTOR of V st Gen x,y & u,u1,v,v1 are_COrte_wrt x,y holds
v,v1,u1,u are_COrte_wrt x,y
proof end;

theorem Th19: :: ANALORT:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u, u1, v, v1 being VECTOR of V st Gen x,y & u,u1,v,v1 are_COrtm_wrt x,y holds
v,v1,u,u1 are_COrtm_wrt x,y
proof end;

theorem Th20: :: ANALORT:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for u, v, w, x, y being VECTOR of V holds u,u,v,w are_COrte_wrt x,y
proof end;

theorem :: ANALORT:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for u, v, w, x, y being VECTOR of V holds u,u,v,w are_COrtm_wrt x,y
proof end;

theorem :: ANALORT:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for u, v, w, x, y being VECTOR of V holds u,v,w,w are_COrte_wrt x,y
proof end;

theorem :: ANALORT:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for u, v, w, x, y being VECTOR of V holds u,v,w,w are_COrtm_wrt x,y
proof end;

theorem Th24: :: ANALORT:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u, v being VECTOR of V st Gen x,y holds
u,v, Orte x,y,u, Orte x,y,v are_Ort_wrt x,y
proof end;

theorem :: ANALORT:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for u, v, x, y being VECTOR of V holds u,v, Orte x,y,u, Orte x,y,v are_COrte_wrt x,y
proof end;

theorem :: ANALORT:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for u, v, x, y being VECTOR of V holds u,v, Ortm x,y,u, Ortm x,y,v are_COrtm_wrt x,y
proof end;

theorem :: ANALORT:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u, v, u1, v1 being VECTOR of V st Gen x,y holds
( u,v // u1,v1 iff ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y ) )
proof end;

theorem :: ANALORT:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u, v, u1, v1 being VECTOR of V st Gen x,y holds
( u,v // u1,v1 iff ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y ) )
proof end;

theorem :: ANALORT:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u, v, u1, v1 being VECTOR of V st Gen x,y holds
( u,v,u1,v1 are_Ort_wrt x,y iff ( u,v,u1,v1 are_COrte_wrt x,y or u,v,v1,u1 are_COrte_wrt x,y ) )
proof end;

theorem :: ANALORT:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u, v, u1, v1 being VECTOR of V st Gen x,y & u,v,u1,v1 are_COrte_wrt x,y & u,v,v1,u1 are_COrte_wrt x,y & not u = v holds
u1 = v1
proof end;

theorem :: ANALORT:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u, v, u1, v1 being VECTOR of V st Gen x,y & u,v,u1,v1 are_COrtm_wrt x,y & u,v,v1,u1 are_COrtm_wrt x,y & not u = v holds
u1 = v1
proof end;

theorem :: ANALORT:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u, v, u1, v1, w being VECTOR of V st Gen x,y & u,v,u1,v1 are_COrte_wrt x,y & u,v,u1,w are_COrte_wrt x,y & not u,v,v1,w are_COrte_wrt x,y holds
u,v,w,v1 are_COrte_wrt x,y
proof end;

theorem :: ANALORT:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u, v, u1, v1, w being VECTOR of V st Gen x,y & u,v,u1,v1 are_COrtm_wrt x,y & u,v,u1,w are_COrtm_wrt x,y & not u,v,v1,w are_COrtm_wrt x,y holds
u,v,w,v1 are_COrtm_wrt x,y
proof end;

theorem :: ANALORT:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for u, v, u1, v1, x, y being VECTOR of V st u,v,u1,v1 are_COrte_wrt x,y holds
v,u,v1,u1 are_COrte_wrt x,y
proof end;

theorem :: ANALORT:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for u, v, u1, v1, x, y being VECTOR of V st u,v,u1,v1 are_COrtm_wrt x,y holds
v,u,v1,u1 are_COrtm_wrt x,y
proof end;

theorem :: ANALORT:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u, v, u1, v1, w being VECTOR of V st Gen x,y & u,v,u1,v1 are_COrte_wrt x,y & u,v,v1,w are_COrte_wrt x,y holds
u,v,u1,w are_COrte_wrt x,y
proof end;

theorem :: ANALORT:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u, v, u1, v1, w being VECTOR of V st Gen x,y & u,v,u1,v1 are_COrtm_wrt x,y & u,v,v1,w are_COrtm_wrt x,y holds
u,v,u1,w are_COrtm_wrt x,y
proof end;

theorem :: ANALORT:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y being VECTOR of V st Gen x,y holds
for u, v, w being VECTOR of V ex u1 being VECTOR of V st
( w <> u1 & w,u1,u,v are_COrte_wrt x,y )
proof end;

theorem :: ANALORT:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y being VECTOR of V st Gen x,y holds
for u, v, w being VECTOR of V ex u1 being VECTOR of V st
( w <> u1 & w,u1,u,v are_COrtm_wrt x,y )
proof end;

theorem Th40: :: ANALORT:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y being VECTOR of V st Gen x,y holds
for u, v, w being VECTOR of V ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y )
proof end;

theorem Th41: :: ANALORT:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y being VECTOR of V st Gen x,y holds
for u, v, w being VECTOR of V ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrtm_wrt x,y )
proof end;

theorem :: ANALORT:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u, u1, v, v1, w, w1, u2, v2 being VECTOR of V st Gen x,y & u,u1,v,v1 are_COrte_wrt x,y & w,w1,v,v1 are_COrte_wrt x,y & w,w1,u2,v2 are_COrte_wrt x,y & not w = w1 & not v = v1 holds
u,u1,u2,v2 are_COrte_wrt x,y
proof end;

theorem :: ANALORT:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u, u1, v, v1, w, w1, u2, v2 being VECTOR of V st Gen x,y & u,u1,v,v1 are_COrtm_wrt x,y & w,w1,v,v1 are_COrtm_wrt x,y & w,w1,u2,v2 are_COrtm_wrt x,y & not w = w1 & not v = v1 holds
u,u1,u2,v2 are_COrtm_wrt x,y
proof end;

theorem :: ANALORT:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ANALORT:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ANALORT:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u, u1, v, v1, w, w1, u2, v2 being VECTOR of V st Gen x,y & u,u1,v,v1 are_COrte_wrt x,y & v,v1,w,w1 are_COrte_wrt x,y & u2,v2,w,w1 are_COrte_wrt x,y & not u,u1,u2,v2 are_COrte_wrt x,y & not v = v1 holds
w = w1
proof end;

theorem :: ANALORT:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u, u1, v, v1, w, w1, u2, v2 being VECTOR of V st Gen x,y & u,u1,v,v1 are_COrtm_wrt x,y & v,v1,w,w1 are_COrtm_wrt x,y & u2,v2,w,w1 are_COrtm_wrt x,y & not u,u1,u2,v2 are_COrtm_wrt x,y & not v = v1 holds
w = w1
proof end;

theorem :: ANALORT:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u, u1, v, v1, w, w1, u2, v2 being VECTOR of V st Gen x,y & u,u1,v,v1 are_COrte_wrt x,y & v,v1,w,w1 are_COrte_wrt x,y & u,u1,u2,v2 are_COrte_wrt x,y & not u2,v2,w,w1 are_COrte_wrt x,y & not v = v1 holds
u = u1
proof end;

theorem :: ANALORT:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y, u, u1, v, v1, w, w1, u2, v2 being VECTOR of V st Gen x,y & u,u1,v,v1 are_COrtm_wrt x,y & v,v1,w,w1 are_COrtm_wrt x,y & u,u1,u2,v2 are_COrtm_wrt x,y & not u2,v2,w,w1 are_COrtm_wrt x,y & not v = v1 holds
u = u1
proof end;

theorem :: ANALORT:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y being VECTOR of V st Gen x,y holds
for v, w, u1, v1, w1 being VECTOR of V st not v,v1,w,u1 are_COrte_wrt x,y & not v,v1,u1,w are_COrte_wrt x,y & u1,w1,u1,w are_COrte_wrt x,y holds
ex u2 being VECTOR of V st
( ( v,v1,v,u2 are_COrte_wrt x,y or v,v1,u2,v are_COrte_wrt x,y ) & ( u1,w1,u1,u2 are_COrte_wrt x,y or u1,w1,u2,u1 are_COrte_wrt x,y ) )
proof end;

theorem :: ANALORT:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y being VECTOR of V st Gen x,y holds
ex u, v, w being VECTOR of V st
( u,v,u,w are_COrte_wrt x,y & ( for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrte_wrt x,y or ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) ) )
proof end;

theorem :: ANALORT:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y being VECTOR of V st Gen x,y holds
for v, w, u1, v1, w1 being VECTOR of V st not v,v1,w,u1 are_COrtm_wrt x,y & not v,v1,u1,w are_COrtm_wrt x,y & u1,w1,u1,w are_COrtm_wrt x,y holds
ex u2 being VECTOR of V st
( ( v,v1,v,u2 are_COrtm_wrt x,y or v,v1,u2,v are_COrtm_wrt x,y ) & ( u1,w1,u1,u2 are_COrtm_wrt x,y or u1,w1,u2,u1 are_COrtm_wrt x,y ) )
proof end;

theorem :: ANALORT:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y being VECTOR of V st Gen x,y holds
ex u, v, w being VECTOR of V st
( u,v,u,w are_COrtm_wrt x,y & ( for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrtm_wrt x,y or ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) ) )
proof end;

definition
let V be RealLinearSpace;
let x, y be VECTOR of V;
func CORTE V,x,y -> Relation of [:the carrier of V,the carrier of V:] means :Def5: :: ANALORT:def 5
for uu, vv being set holds
( [uu,vv] in it iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) );
existence
ex b1 being Relation of [:the carrier of V,the carrier of V:] st
for uu, vv being set holds
( [uu,vv] in b1 iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) )
proof end;
uniqueness
for b1, b2 being Relation of [:the carrier of V,the carrier of V:] st ( for uu, vv being set holds
( [uu,vv] in b1 iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) ) ) & ( for uu, vv being set holds
( [uu,vv] in b2 iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines CORTE ANALORT:def 5 :
for V being RealLinearSpace
for x, y being VECTOR of V
for b4 being Relation of [:the carrier of V,the carrier of V:] holds
( b4 = CORTE V,x,y iff for uu, vv being set holds
( [uu,vv] in b4 iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) ) );

definition
let V be RealLinearSpace;
let x, y be VECTOR of V;
func CORTM V,x,y -> Relation of [:the carrier of V,the carrier of V:] means :Def6: :: ANALORT:def 6
for uu, vv being set holds
( [uu,vv] in it iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y ) );
existence
ex b1 being Relation of [:the carrier of V,the carrier of V:] st
for uu, vv being set holds
( [uu,vv] in b1 iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y ) )
proof end;
uniqueness
for b1, b2 being Relation of [:the carrier of V,the carrier of V:] st ( for uu, vv being set holds
( [uu,vv] in b1 iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y ) ) ) & ( for uu, vv being set holds
( [uu,vv] in b2 iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines CORTM ANALORT:def 6 :
for V being RealLinearSpace
for x, y being VECTOR of V
for b4 being Relation of [:the carrier of V,the carrier of V:] holds
( b4 = CORTM V,x,y iff for uu, vv being set holds
( [uu,vv] in b4 iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y ) ) );

definition
let V be RealLinearSpace;
let x, y be VECTOR of V;
func CESpace V,x,y -> strict AffinStruct equals :: ANALORT:def 7
AffinStruct(# the carrier of V,(CORTE V,x,y) #);
correctness
coherence
AffinStruct(# the carrier of V,(CORTE V,x,y) #) is strict AffinStruct
;
;
end;

:: deftheorem defines CESpace ANALORT:def 7 :
for V being RealLinearSpace
for x, y being VECTOR of V holds CESpace V,x,y = AffinStruct(# the carrier of V,(CORTE V,x,y) #);

registration
let V be RealLinearSpace;
let x, y be VECTOR of V;
cluster CESpace V,x,y -> non empty strict ;
coherence
not CESpace V,x,y is empty
proof end;
end;

definition
let V be RealLinearSpace;
let x, y be VECTOR of V;
func CMSpace V,x,y -> strict AffinStruct equals :: ANALORT:def 8
AffinStruct(# the carrier of V,(CORTM V,x,y) #);
correctness
coherence
AffinStruct(# the carrier of V,(CORTM V,x,y) #) is strict AffinStruct
;
;
end;

:: deftheorem defines CMSpace ANALORT:def 8 :
for V being RealLinearSpace
for x, y being VECTOR of V holds CMSpace V,x,y = AffinStruct(# the carrier of V,(CORTM V,x,y) #);

registration
let V be RealLinearSpace;
let x, y be VECTOR of V;
cluster CMSpace V,x,y -> non empty strict ;
coherence
not CMSpace V,x,y is empty
proof end;
end;

theorem :: ANALORT:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y being VECTOR of V
for uu being set holds
( uu is Element of (CESpace V,x,y) iff uu is VECTOR of V ) ;

theorem :: ANALORT:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for x, y being VECTOR of V
for uu being set holds
( uu is Element of (CMSpace V,x,y) iff uu is VECTOR of V ) ;

theorem :: ANALORT:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for u, v, u1, v1, x, y being VECTOR of V
for p, q, r, s being Element of (CESpace V,x,y) st u = p & v = q & u1 = r & v1 = s holds
( p,q // r,s iff u,v,u1,v1 are_COrte_wrt x,y )
proof end;

theorem :: ANALORT:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for u, v, u1, v1, x, y being VECTOR of V
for p, q, r, s being Element of (CMSpace V,x,y) st u = p & v = q & u1 = r & v1 = s holds
( p,q // r,s iff u,v,u1,v1 are_COrtm_wrt x,y )
proof end;