begin
Lm1:
for V being RealLinearSpace
for v1, x, y, v2 being VECTOR of
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) )
Lm2:
for V being RealLinearSpace
for v, x, y being VECTOR of
for b1, b2, a being Real st v = (b1 * x) + (b2 * y) holds
a * v = ((a * b1) * x) + ((a * b2) * y)
Lm3:
for V being RealLinearSpace
for x, y being VECTOR of
for a1, a2, b1, b2 being Real st Gen x,y & (a1 * x) + (a2 * y) = (b1 * x) + (b2 * y) holds
( a1 = b1 & a2 = b2 )
Lm4:
for V being RealLinearSpace
for x, y being VECTOR of st Gen x,y holds
( x <> 0. V & y <> 0. V )
Lm5:
for V being RealLinearSpace
for x, y, u being VECTOR of st Gen x,y holds
u = ((pr1 x,y,u) * x) + ((pr2 x,y,u) * y)
Lm6:
for V being RealLinearSpace
for x, y, u being VECTOR of
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 )
Lm7:
for V being RealLinearSpace
for x, y, u, v being VECTOR of
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) )
definition
let V be
RealLinearSpace;
let x,
y,
u be
VECTOR of ;
func Ortm x,
y,
u -> VECTOR of
equals
((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 ;
;
end;
:: deftheorem defines Ortm ANALORT:def 1 :
theorem Th1:
for
V being
RealLinearSpace for
x,
y,
u,
v being
VECTOR of st
Gen x,
y holds
Ortm x,
y,
(u + v) = (Ortm x,y,u) + (Ortm x,y,v)
theorem Th2:
theorem
theorem Th4:
theorem Th5:
for
V being
RealLinearSpace for
x,
y,
u,
v being
VECTOR of st
Gen x,
y holds
Ortm x,
y,
(u - v) = (Ortm x,y,u) - (Ortm x,y,v)
theorem Th6:
theorem Th7:
theorem Th8:
definition
let V be
RealLinearSpace;
let x,
y,
u be
VECTOR of ;
func Orte x,
y,
u -> VECTOR of
equals
((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 ;
;
end;
:: deftheorem defines Orte ANALORT:def 2 :
theorem Th9:
theorem Th10:
for
V being
RealLinearSpace for
x,
y,
u,
v being
VECTOR of st
Gen x,
y holds
Orte x,
y,
(u + v) = (Orte x,y,u) + (Orte x,y,v)
theorem Th11:
for
V being
RealLinearSpace for
x,
y,
u,
v being
VECTOR of st
Gen x,
y holds
Orte x,
y,
(u - v) = (Orte x,y,u) - (Orte x,y,v)
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
definition
let V be
RealLinearSpace;
let x,
y,
u,
v,
u1,
v1 be
VECTOR of ;
pred u,
v,
u1,
v1 are_COrte_wrt x,
y means :
Def3:
Orte x,
y,
u,
Orte x,
y,
v // u1,
v1;
pred u,
v,
u1,
v1 are_COrtm_wrt x,
y means :
Def4:
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 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 holds
(
u,
v,
u1,
v1 are_COrtm_wrt x,
y iff
Ortm x,
y,
u,
Ortm x,
y,
v // u1,
v1 );
theorem Th16:
for
V being
RealLinearSpace for
x,
y,
u,
v,
u1,
v1 being
VECTOR of 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
theorem Th17:
for
V being
RealLinearSpace for
x,
y,
u,
v,
u1,
v1 being
VECTOR of 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
theorem Th18:
for
V being
RealLinearSpace for
x,
y,
u,
u1,
v,
v1 being
VECTOR of st
Gen x,
y &
u,
u1,
v,
v1 are_COrte_wrt x,
y holds
v,
v1,
u1,
u are_COrte_wrt x,
y
theorem Th19:
for
V being
RealLinearSpace for
x,
y,
u,
u1,
v,
v1 being
VECTOR of st
Gen x,
y &
u,
u1,
v,
v1 are_COrtm_wrt x,
y holds
v,
v1,
u,
u1 are_COrtm_wrt x,
y
theorem Th20:
theorem
theorem
theorem
theorem Th24:
for
V being
RealLinearSpace for
x,
y,
u,
v being
VECTOR of st
Gen x,
y holds
u,
v,
Orte x,
y,
u,
Orte x,
y,
v are_Ort_wrt x,
y
theorem
for
V being
RealLinearSpace for
u,
v,
x,
y being
VECTOR of holds
u,
v,
Orte x,
y,
u,
Orte x,
y,
v are_COrte_wrt x,
y
theorem
for
V being
RealLinearSpace for
u,
v,
x,
y being
VECTOR of holds
u,
v,
Ortm x,
y,
u,
Ortm x,
y,
v are_COrtm_wrt x,
y
theorem
for
V being
RealLinearSpace for
x,
y,
u,
v,
u1,
v1 being
VECTOR of st
Gen x,
y holds
(
u,
v // u1,
v1 iff ex
u2,
v2 being
VECTOR of st
(
u2 <> v2 &
u2,
v2,
u,
v are_COrte_wrt x,
y &
u2,
v2,
u1,
v1 are_COrte_wrt x,
y ) )
theorem
for
V being
RealLinearSpace for
x,
y,
u,
v,
u1,
v1 being
VECTOR of st
Gen x,
y holds
(
u,
v // u1,
v1 iff ex
u2,
v2 being
VECTOR of st
(
u2 <> v2 &
u2,
v2,
u,
v are_COrtm_wrt x,
y &
u2,
v2,
u1,
v1 are_COrtm_wrt x,
y ) )
theorem
for
V being
RealLinearSpace for
x,
y,
u,
v,
u1,
v1 being
VECTOR of 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 ) )
theorem
for
V being
RealLinearSpace for
x,
y,
u,
v,
u1,
v1 being
VECTOR of 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
theorem
for
V being
RealLinearSpace for
x,
y,
u,
v,
u1,
v1 being
VECTOR of 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
theorem
for
V being
RealLinearSpace for
x,
y,
u,
v,
u1,
v1,
w being
VECTOR of 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
theorem
for
V being
RealLinearSpace for
x,
y,
u,
v,
u1,
v1,
w being
VECTOR of 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
theorem
for
V being
RealLinearSpace for
u,
v,
u1,
v1,
x,
y being
VECTOR of st
u,
v,
u1,
v1 are_COrte_wrt x,
y holds
v,
u,
v1,
u1 are_COrte_wrt x,
y
theorem
for
V being
RealLinearSpace for
u,
v,
u1,
v1,
x,
y being
VECTOR of st
u,
v,
u1,
v1 are_COrtm_wrt x,
y holds
v,
u,
v1,
u1 are_COrtm_wrt x,
y
theorem
for
V being
RealLinearSpace for
x,
y,
u,
v,
u1,
v1,
w being
VECTOR of 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
theorem
for
V being
RealLinearSpace for
x,
y,
u,
v,
u1,
v1,
w being
VECTOR of 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
theorem
theorem
theorem Th40:
theorem Th41:
theorem
for
V being
RealLinearSpace for
x,
y,
u,
u1,
v,
v1,
w,
w1,
u2,
v2 being
VECTOR of 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
theorem
for
V being
RealLinearSpace for
x,
y,
u,
u1,
v,
v1,
w,
w1,
u2,
v2 being
VECTOR of 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
theorem
canceled;
theorem
canceled;
theorem
for
V being
RealLinearSpace for
x,
y,
u,
u1,
v,
v1,
w,
w1,
u2,
v2 being
VECTOR of 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
theorem
for
V being
RealLinearSpace for
x,
y,
u,
u1,
v,
v1,
w,
w1,
u2,
v2 being
VECTOR of 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
theorem
for
V being
RealLinearSpace for
x,
y,
u,
u1,
v,
v1,
w,
w1,
u2,
v2 being
VECTOR of 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
theorem
for
V being
RealLinearSpace for
x,
y,
u,
u1,
v,
v1,
w,
w1,
u2,
v2 being
VECTOR of 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
theorem
for
V being
RealLinearSpace for
x,
y being
VECTOR of st
Gen x,
y holds
for
v,
w,
u1,
v1,
w1 being
VECTOR of 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 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 ) )
theorem
for
V being
RealLinearSpace for
x,
y being
VECTOR of st
Gen x,
y holds
ex
u,
v,
w being
VECTOR of st
(
u,
v,
u,
w are_COrte_wrt x,
y & ( for
v1,
w1 being
VECTOR of 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 ) ) )
theorem
for
V being
RealLinearSpace for
x,
y being
VECTOR of st
Gen x,
y holds
for
v,
w,
u1,
v1,
w1 being
VECTOR of 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 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 ) )
theorem
for
V being
RealLinearSpace for
x,
y being
VECTOR of st
Gen x,
y holds
ex
u,
v,
w being
VECTOR of st
(
u,
v,
u,
w are_COrtm_wrt x,
y & ( for
v1,
w1 being
VECTOR of 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 ) ) )
definition
let V be
RealLinearSpace;
let x,
y be
VECTOR of ;
func CORTE V,
x,
y -> Relation of
means :
Def5:
for
uu,
vv being
set holds
(
[uu,vv] in it iff ex
u1,
u2,
v1,
v2 being
VECTOR of st
(
uu = [u1,u2] &
vv = [v1,v2] &
u1,
u2,
v1,
v2 are_COrte_wrt x,
y ) );
existence
ex b1 being Relation of st
for uu, vv being set holds
( [uu,vv] in b1 iff ex u1, u2, v1, v2 being VECTOR of st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) )
uniqueness
for b1, b2 being Relation of st ( for uu, vv being set holds
( [uu,vv] in b1 iff ex u1, u2, v1, v2 being VECTOR of 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 st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) ) ) holds
b1 = b2
end;
:: deftheorem Def5 defines CORTE ANALORT:def 5 :
for
V being
RealLinearSpace for
x,
y being
VECTOR of
for
b4 being
Relation of 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 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 ;
func CORTM V,
x,
y -> Relation of
means :
Def6:
for
uu,
vv being
set holds
(
[uu,vv] in it iff ex
u1,
u2,
v1,
v2 being
VECTOR of st
(
uu = [u1,u2] &
vv = [v1,v2] &
u1,
u2,
v1,
v2 are_COrtm_wrt x,
y ) );
existence
ex b1 being Relation of st
for uu, vv being set holds
( [uu,vv] in b1 iff ex u1, u2, v1, v2 being VECTOR of st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y ) )
uniqueness
for b1, b2 being Relation of st ( for uu, vv being set holds
( [uu,vv] in b1 iff ex u1, u2, v1, v2 being VECTOR of 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 st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y ) ) ) holds
b1 = b2
end;
:: deftheorem Def6 defines CORTM ANALORT:def 6 :
for
V being
RealLinearSpace for
x,
y being
VECTOR of
for
b4 being
Relation of 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 st
(
uu = [u1,u2] &
vv = [v1,v2] &
u1,
u2,
v1,
v2 are_COrtm_wrt x,
y ) ) );
:: deftheorem defines CESpace ANALORT:def 7 :
:: deftheorem defines CMSpace ANALORT:def 8 :
theorem
theorem
theorem
for
V being
RealLinearSpace for
u,
v,
u1,
v1,
x,
y being
VECTOR of
for
p,
q,
r,
s being
Element of st
u = p &
v = q &
u1 = r &
v1 = s holds
(
p,
q // r,
s iff
u,
v,
u1,
v1 are_COrte_wrt x,
y )
theorem
for
V being
RealLinearSpace for
u,
v,
u1,
v1,
x,
y being
VECTOR of
for
p,
q,
r,
s being
Element of st
u = p &
v = q &
u1 = r &
v1 = s holds
(
p,
q // r,
s iff
u,
v,
u1,
v1 are_COrtm_wrt x,
y )