:: by Jaroslaw Zajkowski

::

:: Received October 24, 1991

:: Copyright (c) 1991-2019 Association of Mizar Users

Lm1: for V being RealLinearSpace

for v1, v2, x, y 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 a, b1, b2 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 u, x, y 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 u, x, y 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 u, v, x, y 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;

coherence

((pr1 (x,y,u)) * x) + ((- (pr2 (x,y,u))) * y) is VECTOR of V;

;

end;
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 ((pr1 (x,y,u)) * x) + ((- (pr2 (x,y,u))) * y);

coherence

((pr1 (x,y,u)) * x) + ((- (pr2 (x,y,u))) * y) is VECTOR of V;

;

:: 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);

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

for V being RealLinearSpace

for u, v, x, y being VECTOR of V st Gen x,y holds

Ortm (x,y,(u + v)) = (Ortm (x,y,u)) + (Ortm (x,y,v))

for u, v, x, y 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

for V being RealLinearSpace

for u, x, y being VECTOR of V

for n being Real st Gen x,y holds

Ortm (x,y,(n * u)) = n * (Ortm (x,y,u))

for u, x, y 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 Th4: :: ANALORT:4

for V being RealLinearSpace

for u, x, y being VECTOR of V st Gen x,y holds

Ortm (x,y,(- u)) = - (Ortm (x,y,u))

for u, x, y being VECTOR of V st Gen x,y holds

Ortm (x,y,(- u)) = - (Ortm (x,y,u))

proof end;

theorem Th5: :: ANALORT:5

for V being RealLinearSpace

for u, v, x, y being VECTOR of V st Gen x,y holds

Ortm (x,y,(u - v)) = (Ortm (x,y,u)) - (Ortm (x,y,v))

for u, v, x, y 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

for V being RealLinearSpace

for u, v, x, y being VECTOR of V st Gen x,y & Ortm (x,y,u) = Ortm (x,y,v) holds

u = v

for u, v, x, y 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

for V being RealLinearSpace

for u, x, y being VECTOR of V st Gen x,y holds

Ortm (x,y,(Ortm (x,y,u))) = u

for u, x, y being VECTOR of V st Gen x,y holds

Ortm (x,y,(Ortm (x,y,u))) = u

proof end;

theorem Th8: :: ANALORT:8

for V being RealLinearSpace

for u, x, y being VECTOR of V st Gen x,y holds

ex v being VECTOR of V st u = Ortm (x,y,v)

for u, x, y 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;

coherence

((pr2 (x,y,u)) * x) + ((- (pr1 (x,y,u))) * y) is VECTOR of V;

;

end;
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 ((pr2 (x,y,u)) * x) + ((- (pr1 (x,y,u))) * y);

coherence

((pr2 (x,y,u)) * x) + ((- (pr1 (x,y,u))) * y) is VECTOR of V;

;

:: 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);

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

for V being RealLinearSpace

for v, x, y being VECTOR of V st Gen x,y holds

Orte (x,y,(- v)) = - (Orte (x,y,v))

for v, x, y being VECTOR of V st Gen x,y holds

Orte (x,y,(- v)) = - (Orte (x,y,v))

proof end;

theorem Th10: :: ANALORT:10

for V being RealLinearSpace

for u, v, x, y being VECTOR of V st Gen x,y holds

Orte (x,y,(u + v)) = (Orte (x,y,u)) + (Orte (x,y,v))

for u, v, x, y 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

for V being RealLinearSpace

for u, v, x, y being VECTOR of V st Gen x,y holds

Orte (x,y,(u - v)) = (Orte (x,y,u)) - (Orte (x,y,v))

for u, v, x, y 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

for V being RealLinearSpace

for u, x, y being VECTOR of V

for n being Real st Gen x,y holds

Orte (x,y,(n * u)) = n * (Orte (x,y,u))

for u, x, y 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

for V being RealLinearSpace

for u, v, x, y being VECTOR of V st Gen x,y & Orte (x,y,u) = Orte (x,y,v) holds

u = v

for u, v, x, y 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

for V being RealLinearSpace

for u, x, y being VECTOR of V st Gen x,y holds

Orte (x,y,(Orte (x,y,u))) = - u

for u, x, y being VECTOR of V st Gen x,y holds

Orte (x,y,(Orte (x,y,u))) = - u

proof end;

theorem Th15: :: ANALORT:15

for V being RealLinearSpace

for u, x, y being VECTOR of V st Gen x,y holds

ex v being VECTOR of V st Orte (x,y,v) = u

for u, x, y being VECTOR of V st Gen x,y holds

ex v being VECTOR of V st Orte (x,y,v) = u

proof end;

:: deftheorem 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 );

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 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 );

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

for V being RealLinearSpace

for u, u1, v, v1, x, y 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)

for u, u1, v, v1, x, y 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

for V being RealLinearSpace

for u, u1, v, v1, x, y 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)

for u, u1, v, v1, x, y 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

for V being RealLinearSpace

for u, u1, v, v1, x, y 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

for u, u1, v, v1, x, y 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

for V being RealLinearSpace

for u, u1, v, v1, x, y 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

for u, u1, v, v1, x, y 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

for V being RealLinearSpace

for u, v, w, x, y being VECTOR of V holds u,u,v,w are_COrte_wrt x,y by ANALOAF:9;

for u, v, w, x, y being VECTOR of V holds u,u,v,w are_COrte_wrt x,y by ANALOAF:9;

theorem :: ANALORT:21

for V being RealLinearSpace

for u, v, w, x, y being VECTOR of V holds u,u,v,w are_COrtm_wrt x,y by ANALOAF:9;

for u, v, w, x, y being VECTOR of V holds u,u,v,w are_COrtm_wrt x,y by ANALOAF:9;

theorem :: ANALORT:22

for V being RealLinearSpace

for u, v, w, x, y being VECTOR of V holds u,v,w,w are_COrte_wrt x,y by ANALOAF:9;

for u, v, w, x, y being VECTOR of V holds u,v,w,w are_COrte_wrt x,y by ANALOAF:9;

theorem :: ANALORT:23

for V being RealLinearSpace

for u, v, w, x, y being VECTOR of V holds u,v,w,w are_COrtm_wrt x,y by ANALOAF:9;

for u, v, w, x, y being VECTOR of V holds u,v,w,w are_COrtm_wrt x,y by ANALOAF:9;

theorem Th24: :: ANALORT:24

for V being RealLinearSpace

for u, v, x, y being VECTOR of V st Gen x,y holds

u,v, Orte (x,y,u), Orte (x,y,v) are_Ort_wrt x,y

for u, v, x, y 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

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 by ANALOAF:8;

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 by ANALOAF:8;

theorem :: ANALORT:26

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 by ANALOAF:8;

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 by ANALOAF:8;

theorem :: ANALORT:27

for V being RealLinearSpace

for u, u1, v, v1, x, y 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 ) )

for u, u1, v, v1, x, y 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

for V being RealLinearSpace

for u, u1, v, v1, x, y 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 ) )

for u, u1, v, v1, x, y 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

for V being RealLinearSpace

for u, u1, v, v1, x, y 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 ) )

for u, u1, v, v1, x, y 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

for V being RealLinearSpace

for u, u1, v, v1, x, y 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

for u, u1, v, v1, x, y 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

for V being RealLinearSpace

for u, u1, v, v1, x, y 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

for u, u1, v, v1, x, y 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

for V being RealLinearSpace

for u, u1, v, v1, w, x, y 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

for u, u1, v, v1, w, x, y 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

for V being RealLinearSpace

for u, u1, v, v1, w, x, y 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

for u, u1, v, v1, w, x, y 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

for V being RealLinearSpace

for u, u1, v, 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 by ANALOAF:12;

for u, u1, v, 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 by ANALOAF:12;

theorem :: ANALORT:35

for V being RealLinearSpace

for u, u1, v, 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 by ANALOAF:12;

for u, u1, v, 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 by ANALOAF:12;

theorem :: ANALORT:36

for V being RealLinearSpace

for u, u1, v, v1, w, x, y 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

for u, u1, v, v1, w, x, y 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

for V being RealLinearSpace

for u, u1, v, v1, w, x, y 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

for u, u1, v, v1, w, x, y 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

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 )

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

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 )

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

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 )

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

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 )

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

for V being RealLinearSpace

for u, u1, u2, v, v1, v2, w, w1, x, y 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

for u, u1, u2, v, v1, v2, w, w1, x, y 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

for V being RealLinearSpace

for u, u1, u2, v, v1, v2, w, w1, x, y 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

for u, u1, u2, v, v1, v2, w, w1, x, y 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

for V being RealLinearSpace

for u, u1, u2, v, v1, v2, w, w1, x, y 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

for u, u1, u2, v, v1, v2, w, w1, x, y 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:45

for V being RealLinearSpace

for u, u1, u2, v, v1, v2, w, w1, x, y 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

for u, u1, u2, v, v1, v2, w, w1, x, y 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:46

for V being RealLinearSpace

for u, u1, u2, v, v1, v2, w, w1, x, y 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

for u, u1, u2, v, v1, v2, w, w1, x, y 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:47

for V being RealLinearSpace

for u, u1, u2, v, v1, v2, w, w1, x, y 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

for u, u1, u2, v, v1, v2, w, w1, x, y 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:48

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 ) )

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:49

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 ) ) )

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:50

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 ) )

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:51

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 ) ) )

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;

ex b_{1} being Relation of [: the carrier of V, the carrier of V:] st

for uu, vv being object holds

( [uu,vv] in b_{1} 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 b_{1}, b_{2} being Relation of [: the carrier of V, the carrier of V:] st ( for uu, vv being object holds

( [uu,vv] in b_{1} 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 object holds

( [uu,vv] in b_{2} 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

b_{1} = b_{2}

end;
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 object 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 for uu, vv being object 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 ) );

ex b

for uu, vv being object holds

( [uu,vv] in b

( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) )

proof end;

uniqueness for b

( [uu,vv] in b

( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) ) ) & ( for uu, vv being object holds

( [uu,vv] in b

( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) ) ) holds

b

proof end;

:: deftheorem Def5 defines CORTE ANALORT:def 5 :

for V being RealLinearSpace

for x, y being VECTOR of V

for b_{4} being Relation of [: the carrier of V, the carrier of V:] holds

( b_{4} = CORTE (V,x,y) iff for uu, vv being object holds

( [uu,vv] in b_{4} 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 V being RealLinearSpace

for x, y being VECTOR of V

for b

( b

( [uu,vv] in b

( 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;

ex b_{1} being Relation of [: the carrier of V, the carrier of V:] st

for uu, vv being object holds

( [uu,vv] in b_{1} 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 b_{1}, b_{2} being Relation of [: the carrier of V, the carrier of V:] st ( for uu, vv being object holds

( [uu,vv] in b_{1} 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 object holds

( [uu,vv] in b_{2} 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

b_{1} = b_{2}

end;
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 object 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 for uu, vv being object 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 ) );

ex b

for uu, vv being object holds

( [uu,vv] in b

( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y ) )

proof end;

uniqueness for b

( [uu,vv] in b

( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y ) ) ) & ( for uu, vv being object holds

( [uu,vv] in b

( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y ) ) ) holds

b

proof end;

:: deftheorem Def6 defines CORTM ANALORT:def 6 :

for V being RealLinearSpace

for x, y being VECTOR of V

for b_{4} being Relation of [: the carrier of V, the carrier of V:] holds

( b_{4} = CORTM (V,x,y) iff for uu, vv being object holds

( [uu,vv] in b_{4} 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 V being RealLinearSpace

for x, y being VECTOR of V

for b

( b

( [uu,vv] in b

( 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;

coherence

OrtStr(# the carrier of V,(CORTE (V,x,y)) #) is strict OrtStr ;

;

end;
let x, y be VECTOR of V;

func CESpace (V,x,y) -> strict OrtStr equals :: ANALORT:def 7

OrtStr(# the carrier of V,(CORTE (V,x,y)) #);

correctness OrtStr(# the carrier of V,(CORTE (V,x,y)) #);

coherence

OrtStr(# the carrier of V,(CORTE (V,x,y)) #) is strict OrtStr ;

;

:: deftheorem defines CESpace ANALORT:def 7 :

for V being RealLinearSpace

for x, y being VECTOR of V holds CESpace (V,x,y) = OrtStr(# the carrier of V,(CORTE (V,x,y)) #);

for V being RealLinearSpace

for x, y being VECTOR of V holds CESpace (V,x,y) = OrtStr(# the carrier of V,(CORTE (V,x,y)) #);

registration
end;

definition

let V be RealLinearSpace;

let x, y be VECTOR of V;

coherence

OrtStr(# the carrier of V,(CORTM (V,x,y)) #) is strict OrtStr ;

;

end;
let x, y be VECTOR of V;

func CMSpace (V,x,y) -> strict OrtStr equals :: ANALORT:def 8

OrtStr(# the carrier of V,(CORTM (V,x,y)) #);

correctness OrtStr(# the carrier of V,(CORTM (V,x,y)) #);

coherence

OrtStr(# the carrier of V,(CORTM (V,x,y)) #) is strict OrtStr ;

;

:: deftheorem defines CMSpace ANALORT:def 8 :

for V being RealLinearSpace

for x, y being VECTOR of V holds CMSpace (V,x,y) = OrtStr(# the carrier of V,(CORTM (V,x,y)) #);

for V being RealLinearSpace

for x, y being VECTOR of V holds CMSpace (V,x,y) = OrtStr(# the carrier of V,(CORTM (V,x,y)) #);

registration
end;

theorem :: ANALORT:52

theorem :: ANALORT:53

theorem :: ANALORT:54

for V being RealLinearSpace

for u, u1, v, 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 )

for u, u1, v, 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:55

for V being RealLinearSpace

for u, u1, v, 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 )

for u, u1, v, 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;