:: by Jan Popio{\l}ek

::

:: Received July 19, 1991

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

definition

attr c_{1} is strict ;

struct UNITSTR -> RLSStruct ;

aggr UNITSTR(# carrier, ZeroF, addF, Mult, scalar #) -> UNITSTR ;

sel scalar c_{1} -> Function of [: the carrier of c_{1}, the carrier of c_{1}:],REAL;

end;
struct UNITSTR -> RLSStruct ;

aggr UNITSTR(# carrier, ZeroF, addF, Mult, scalar #) -> UNITSTR ;

sel scalar c

registration
end;

registration

let D be non empty set ;

let Z be Element of D;

let a be BinOp of D;

let m be Function of [:REAL,D:],D;

let s be Function of [:D,D:],REAL;

coherence

not UNITSTR(# D,Z,a,m,s #) is empty ;

end;
let Z be Element of D;

let a be BinOp of D;

let m be Function of [:REAL,D:],D;

let s be Function of [:D,D:],REAL;

coherence

not UNITSTR(# D,Z,a,m,s #) is empty ;

deffunc H

definition

let X be non empty UNITSTR ;

let x, y be Point of X;

correctness

coherence

the scalar of X . [x,y] is Real;

;

end;
let x, y be Point of X;

correctness

coherence

the scalar of X . [x,y] is Real;

;

:: deftheorem defines .|. BHSP_1:def 1 :

for X being non empty UNITSTR

for x, y being Point of X holds x .|. y = the scalar of X . [x,y];

for X being non empty UNITSTR

for x, y being Point of X holds x .|. y = the scalar of X . [x,y];

set V0 = the RealLinearSpace;

Lm1: the carrier of ((0). the RealLinearSpace) = {(0. the RealLinearSpace)}

by RLSUB_1:def 3;

reconsider nilfunc = [: the carrier of ((0). the RealLinearSpace), the carrier of ((0). the RealLinearSpace):] --> (In (0,REAL)) as Function of [: the carrier of ((0). the RealLinearSpace), the carrier of ((0). the RealLinearSpace):],REAL ;

( ( for x, y being VECTOR of ((0). the RealLinearSpace) holds nilfunc . [x,y] = 0 ) & 0. the RealLinearSpace in the carrier of ((0). the RealLinearSpace) )

by Lm1, FUNCOP_1:7, TARSKI:def 1;

then Lm2: nilfunc . [(0. the RealLinearSpace),(0. the RealLinearSpace)] = 0

;

Lm3: for u, v being VECTOR of ((0). the RealLinearSpace) holds nilfunc . [u,v] = nilfunc . [v,u]

proof end;

Lm4: for u, v, w being VECTOR of ((0). the RealLinearSpace) holds nilfunc . [(u + v),w] = (nilfunc . [u,w]) + (nilfunc . [v,w])

proof end;

Lm5: for u, v being VECTOR of ((0). the RealLinearSpace)

for a being Real holds nilfunc . [(a * u),v] = a * (nilfunc . [u,v])

proof end;

set X0 = UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #);

Lm6: now :: thesis: for x, y, z being Point of UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)

for a being Real holds

( ( x .|. x = In (0,REAL) implies x = H_{1}( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) ) & ( x = H_{1}( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) implies x .|. x = In (0,REAL) ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )

for a being Real holds

( ( x .|. x = In (0,REAL) implies x = H

let x, y, z be Point of UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #); :: thesis: for a being Real holds

( ( x .|. x = In (0,REAL) implies x = H_{1}( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) ) & ( x = H_{1}( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) implies x .|. x = In (0,REAL) ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )

let a be Real; :: thesis: ( ( x .|. x = In (0,REAL) implies x = H_{1}( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) ) & ( x = H_{1}( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) implies x .|. x = In (0,REAL) ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )

H_{1}( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) = 0. the RealLinearSpace
by RLSUB_1:11;

hence ( x .|. x = In (0,REAL) iff x = H_{1}( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) )
by Lm1, FUNCOP_1:7, TARSKI:def 1; :: thesis: ( 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )

thus 0 <= x .|. x by FUNCOP_1:7; :: thesis: ( x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )

thus x .|. y = y .|. x by Lm3; :: thesis: ( (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )

thus (x + y) .|. z = (x .|. z) + (y .|. z) :: thesis: (a * x) .|. y = a * (x .|. y)

end;
( ( x .|. x = In (0,REAL) implies x = H

let a be Real; :: thesis: ( ( x .|. x = In (0,REAL) implies x = H

H

hence ( x .|. x = In (0,REAL) iff x = H

thus 0 <= x .|. x by FUNCOP_1:7; :: thesis: ( x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )

thus x .|. y = y .|. x by Lm3; :: thesis: ( (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )

thus (x + y) .|. z = (x .|. z) + (y .|. z) :: thesis: (a * x) .|. y = a * (x .|. y)

proof

thus
(a * x) .|. y = a * (x .|. y)
:: thesis: verum
reconsider u = x, v = y, w = z as VECTOR of ((0). the RealLinearSpace) ;

(x + y) .|. z = nilfunc . [(u + v),w] ;

hence (x + y) .|. z = (x .|. z) + (y .|. z) by Lm4; :: thesis: verum

end;
(x + y) .|. z = nilfunc . [(u + v),w] ;

hence (x + y) .|. z = (x .|. z) + (y .|. z) by Lm4; :: thesis: verum

:: deftheorem Def2 defines RealUnitarySpace-like BHSP_1:def 2 :

for IT being non empty UNITSTR holds

( IT is RealUnitarySpace-like iff for x, y, z being Point of IT

for a being Real holds

( ( x .|. x = 0 implies x = 0. IT ) & ( x = 0. IT implies x .|. x = 0 ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) ) );

for IT being non empty UNITSTR holds

( IT is RealUnitarySpace-like iff for x, y, z being Point of IT

for a being Real holds

( ( x .|. x = 0 implies x = 0. IT ) & ( x = 0. IT implies x .|. x = 0 ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) ) );

registration

ex b_{1} being non empty UNITSTR st

( b_{1} is RealUnitarySpace-like & b_{1} is vector-distributive & b_{1} is scalar-distributive & b_{1} is scalar-associative & b_{1} is scalar-unital & b_{1} is Abelian & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is strict )
end;

cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like for UNITSTR ;

existence ex b

( b

proof end;

definition

mode RealUnitarySpace is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR ;

end;
definition

let X be RealUnitarySpace;

let x, y be Point of X;

:: original: .|.

redefine func x .|. y -> Real;

commutativity

for x, y being Point of X holds x .|. y = y .|. x by Def2;

end;
let x, y be Point of X;

:: original: .|.

redefine func x .|. y -> Real;

commutativity

for x, y being Point of X holds x .|. y = y .|. x by Def2;

theorem :: BHSP_1:2

theorem :: BHSP_1:3

theorem :: BHSP_1:4

for a being Real

for X being RealUnitarySpace

for x, y being Point of X holds (a * x) .|. y = x .|. (a * y)

for X being RealUnitarySpace

for x, y being Point of X holds (a * x) .|. y = x .|. (a * y)

proof end;

theorem Th5: :: BHSP_1:5

for a, b being Real

for X being RealUnitarySpace

for x, y, z being Point of X holds ((a * x) + (b * y)) .|. z = (a * (x .|. z)) + (b * (y .|. z))

for X being RealUnitarySpace

for x, y, z being Point of X holds ((a * x) + (b * y)) .|. z = (a * (x .|. z)) + (b * (y .|. z))

proof end;

theorem :: BHSP_1:6

theorem :: BHSP_1:9

theorem Th11: :: BHSP_1:11

for X being RealUnitarySpace

for x, y, z being Point of X holds (x - y) .|. z = (x .|. z) - (y .|. z)

for x, y, z being Point of X holds (x - y) .|. z = (x .|. z) - (y .|. z)

proof end;

theorem Th12: :: BHSP_1:12

for X being RealUnitarySpace

for x, y, z being Point of X holds x .|. (y - z) = (x .|. y) - (x .|. z)

for x, y, z being Point of X holds x .|. (y - z) = (x .|. y) - (x .|. z)

proof end;

theorem :: BHSP_1:13

for X being RealUnitarySpace

for x, y, u, v being Point of X holds (x - y) .|. (u - v) = (((x .|. u) - (x .|. v)) - (y .|. u)) + (y .|. v)

for x, y, u, v being Point of X holds (x - y) .|. (u - v) = (((x .|. u) - (x .|. v)) - (y .|. u)) + (y .|. v)

proof end;

theorem :: BHSP_1:15

theorem Th16: :: BHSP_1:16

for X being RealUnitarySpace

for x, y being Point of X holds (x + y) .|. (x + y) = ((x .|. x) + (2 * (x .|. y))) + (y .|. y)

for x, y being Point of X holds (x + y) .|. (x + y) = ((x .|. x) + (2 * (x .|. y))) + (y .|. y)

proof end;

theorem :: BHSP_1:17

for X being RealUnitarySpace

for x, y being Point of X holds (x + y) .|. (x - y) = (x .|. x) - (y .|. y)

for x, y being Point of X holds (x + y) .|. (x - y) = (x .|. x) - (y .|. y)

proof end;

theorem Th18: :: BHSP_1:18

for X being RealUnitarySpace

for x, y being Point of X holds (x - y) .|. (x - y) = ((x .|. x) - (2 * (x .|. y))) + (y .|. y)

for x, y being Point of X holds (x - y) .|. (x - y) = ((x .|. x) - (2 * (x .|. y))) + (y .|. y)

proof end;

theorem Th19: :: BHSP_1:19

for X being RealUnitarySpace

for x, y being Point of X holds |.(x .|. y).| <= (sqrt (x .|. x)) * (sqrt (y .|. y))

for x, y being Point of X holds |.(x .|. y).| <= (sqrt (x .|. x)) * (sqrt (y .|. y))

proof end;

definition

let X be RealUnitarySpace;

let x, y be Point of X;

symmetry

for x, y being Point of X st x .|. y = 0 holds

y .|. x = 0 ;

end;
let x, y be Point of X;

symmetry

for x, y being Point of X st x .|. y = 0 holds

y .|. x = 0 ;

:: deftheorem defines are_orthogonal BHSP_1:def 3 :

for X being RealUnitarySpace

for x, y being Point of X holds

( x,y are_orthogonal iff x .|. y = 0 );

for X being RealUnitarySpace

for x, y being Point of X holds

( x,y are_orthogonal iff x .|. y = 0 );

theorem :: BHSP_1:20

for X being RealUnitarySpace

for x, y being Point of X st x,y are_orthogonal holds

x, - y are_orthogonal

for x, y being Point of X st x,y are_orthogonal holds

x, - y are_orthogonal

proof end;

theorem :: BHSP_1:21

for X being RealUnitarySpace

for x, y being Point of X st x,y are_orthogonal holds

- x,y are_orthogonal

for x, y being Point of X st x,y are_orthogonal holds

- x,y are_orthogonal

proof end;

theorem :: BHSP_1:22

for X being RealUnitarySpace

for x, y being Point of X st x,y are_orthogonal holds

- x, - y are_orthogonal by Th10;

for x, y being Point of X st x,y are_orthogonal holds

- x, - y are_orthogonal by Th10;

theorem :: BHSP_1:23

theorem :: BHSP_1:24

for X being RealUnitarySpace

for x, y being Point of X st x,y are_orthogonal holds

(x + y) .|. (x + y) = (x .|. x) + (y .|. y)

for x, y being Point of X st x,y are_orthogonal holds

(x + y) .|. (x + y) = (x .|. x) + (y .|. y)

proof end;

theorem :: BHSP_1:25

for X being RealUnitarySpace

for x, y being Point of X st x,y are_orthogonal holds

(x - y) .|. (x - y) = (x .|. x) + (y .|. y)

for x, y being Point of X st x,y are_orthogonal holds

(x - y) .|. (x - y) = (x .|. x) + (y .|. y)

proof end;

definition
end;

:: deftheorem defines ||. BHSP_1:def 4 :

for X being RealUnitarySpace

for x being Point of X holds ||.x.|| = sqrt (x .|. x);

for X being RealUnitarySpace

for x being Point of X holds ||.x.|| = sqrt (x .|. x);

theorem Th27: :: BHSP_1:27

for a being Real

for X being RealUnitarySpace

for x being Point of X holds ||.(a * x).|| = |.a.| * ||.x.||

for X being RealUnitarySpace

for x being Point of X holds ||.(a * x).|| = |.a.| * ||.x.||

proof end;

theorem :: BHSP_1:29

theorem :: BHSP_1:33

for X being RealUnitarySpace

for x, y being Point of X holds |.(||.x.|| - ||.y.||).| <= ||.(x - y).||

for x, y being Point of X holds |.(||.x.|| - ||.y.||).| <= ||.(x - y).||

proof end;

definition

let X be RealUnitarySpace;

let x, y be Point of X;

correctness

coherence

||.(x - y).|| is Real;

;

commutativity

for b_{1} being Real

for x, y being Point of X st b_{1} = ||.(x - y).|| holds

b_{1} = ||.(y - x).||

end;
let x, y be Point of X;

correctness

coherence

||.(x - y).|| is Real;

;

commutativity

for b

for x, y being Point of X st b

b

proof end;

:: deftheorem defines dist BHSP_1:def 5 :

for X being RealUnitarySpace

for x, y being Point of X holds dist (x,y) = ||.(x - y).||;

for X being RealUnitarySpace

for x, y being Point of X holds dist (x,y) = ||.(x - y).||;

theorem :: BHSP_1:35

for X being RealUnitarySpace

for x, y, z being Point of X holds dist (x,z) <= (dist (x,y)) + (dist (y,z))

for x, y, z being Point of X holds dist (x,z) <= (dist (x,y)) + (dist (y,z))

proof end;

theorem :: BHSP_1:37

theorem :: BHSP_1:39

theorem :: BHSP_1:40

for X being RealUnitarySpace

for x, y, u, v being Point of X holds dist ((x + y),(u + v)) <= (dist (x,u)) + (dist (y,v))

for x, y, u, v being Point of X holds dist ((x + y),(u + v)) <= (dist (x,u)) + (dist (y,v))

proof end;

theorem :: BHSP_1:41

for X being RealUnitarySpace

for x, y, u, v being Point of X holds dist ((x - y),(u - v)) <= (dist (x,u)) + (dist (y,v))

for x, y, u, v being Point of X holds dist ((x - y),(u - v)) <= (dist (x,u)) + (dist (y,v))

proof end;

theorem :: BHSP_1:43

for X being RealUnitarySpace

for x, y, z being Point of X holds dist ((x - z),(y - z)) <= (dist (z,x)) + (dist (z,y))

for x, y, z being Point of X holds dist ((x - z),(y - z)) <= (dist (z,x)) + (dist (z,y))

proof end;

definition

let X be non empty addLoopStr ;

let seq be sequence of X;

let x be Point of X;

ex b_{1} being sequence of X st

for n being Nat holds b_{1} . n = (seq . n) + x

for b_{1}, b_{2} being sequence of X st ( for n being Nat holds b_{1} . n = (seq . n) + x ) & ( for n being Nat holds b_{2} . n = (seq . n) + x ) holds

b_{1} = b_{2}

end;
let seq be sequence of X;

let x be Point of X;

func seq + x -> sequence of X means :Def6: :: BHSP_1:def 6

for n being Nat holds it . n = (seq . n) + x;

existence for n being Nat holds it . n = (seq . n) + x;

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines + BHSP_1:def 6 :

for X being non empty addLoopStr

for seq being sequence of X

for x being Point of X

for b_{4} being sequence of X holds

( b_{4} = seq + x iff for n being Nat holds b_{4} . n = (seq . n) + x );

for X being non empty addLoopStr

for seq being sequence of X

for x being Point of X

for b

( b

theorem Th44: :: BHSP_1:44

for n being Nat

for X being non empty addLoopStr

for seq being sequence of X holds (- seq) . n = - (seq . n)

for X being non empty addLoopStr

for seq being sequence of X holds (- seq) . n = - (seq . n)

proof end;

definition

let X be RealUnitarySpace;

let seq1, seq2 be sequence of X;

:: original: +

redefine func seq1 + seq2 -> Element of bool [:NAT, the carrier of X:];

commutativity

for seq1, seq2 being sequence of X holds seq1 + seq2 = seq2 + seq1

end;
let seq1, seq2 be sequence of X;

:: original: +

redefine func seq1 + seq2 -> Element of bool [:NAT, the carrier of X:];

commutativity

for seq1, seq2 being sequence of X holds seq1 + seq2 = seq2 + seq1

proof end;

theorem :: BHSP_1:45

for X being RealUnitarySpace

for seq1, seq2, seq3 being sequence of X holds seq1 + (seq2 + seq3) = (seq1 + seq2) + seq3

for seq1, seq2, seq3 being sequence of X holds seq1 + (seq2 + seq3) = (seq1 + seq2) + seq3

proof end;

theorem :: BHSP_1:46

for X being RealUnitarySpace

for seq1, seq2 being sequence of X st seq1 is constant & seq2 is constant holds

seq1 + seq2 is constant

for seq1, seq2 being sequence of X st seq1 is constant & seq2 is constant holds

seq1 + seq2 is constant

proof end;

theorem :: BHSP_1:47

for X being RealUnitarySpace

for seq1, seq2 being sequence of X st seq1 is constant & seq2 is constant holds

seq1 - seq2 is constant

for seq1, seq2 being sequence of X st seq1 is constant & seq2 is constant holds

seq1 - seq2 is constant

proof end;

theorem :: BHSP_1:48

for a being Real

for X being RealUnitarySpace

for seq1 being sequence of X st seq1 is constant holds

a * seq1 is constant

for X being RealUnitarySpace

for seq1 being sequence of X st seq1 is constant holds

a * seq1 is constant

proof end;

theorem :: BHSP_1:51

for a being Real

for X being RealUnitarySpace

for seq1, seq2 being sequence of X holds a * (seq1 + seq2) = (a * seq1) + (a * seq2)

for X being RealUnitarySpace

for seq1, seq2 being sequence of X holds a * (seq1 + seq2) = (a * seq1) + (a * seq2)

proof end;

theorem :: BHSP_1:52

for a, b being Real

for X being RealUnitarySpace

for seq being sequence of X holds (a + b) * seq = (a * seq) + (b * seq)

for X being RealUnitarySpace

for seq being sequence of X holds (a + b) * seq = (a * seq) + (b * seq)

proof end;

theorem :: BHSP_1:53

for a, b being Real

for X being RealUnitarySpace

for seq being sequence of X holds (a * b) * seq = a * (b * seq)

for X being RealUnitarySpace

for seq being sequence of X holds (a * b) * seq = a * (b * seq)

proof end;

theorem :: BHSP_1:56

for X being RealUnitarySpace

for x being Point of X

for seq being sequence of X holds seq - x = seq + (- x)

for x being Point of X

for seq being sequence of X holds seq - x = seq + (- x)

proof end;

theorem :: BHSP_1:60

for X being RealUnitarySpace

for seq1, seq2, seq3 being sequence of X holds seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3

for seq1, seq2, seq3 being sequence of X holds seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3

proof end;

theorem :: BHSP_1:61

for X being RealUnitarySpace

for seq1, seq2, seq3 being sequence of X holds (seq1 + seq2) - seq3 = seq1 + (seq2 - seq3)

for seq1, seq2, seq3 being sequence of X holds (seq1 + seq2) - seq3 = seq1 + (seq2 - seq3)

proof end;

theorem :: BHSP_1:62

for X being RealUnitarySpace

for seq1, seq2, seq3 being sequence of X holds seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3

for seq1, seq2, seq3 being sequence of X holds seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3

proof end;

theorem :: BHSP_1:63

for a being Real

for X being RealUnitarySpace

for seq1, seq2 being sequence of X holds a * (seq1 - seq2) = (a * seq1) - (a * seq2)

for X being RealUnitarySpace

for seq1, seq2 being sequence of X holds a * (seq1 - seq2) = (a * seq1) - (a * seq2)

proof end;