:: by Agata Darmochwa{\l}

::

:: Received November 21, 1991

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

registration
end;

definition

ex b_{1} being Function of REAL,REAL st

for r being Real holds b_{1} . r = |.r.|

for b_{1}, b_{2} being Function of REAL,REAL st ( for r being Real holds b_{1} . r = |.r.| ) & ( for r being Real holds b_{2} . r = |.r.| ) holds

b_{1} = b_{2}
end;

func absreal -> Function of REAL,REAL means :Def2: :: EUCLID:def 2

for r being Real holds it . r = |.r.|;

existence for r being Real holds it . r = |.r.|;

ex b

for r being Real holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines absreal EUCLID:def 2 :

for b_{1} being Function of REAL,REAL holds

( b_{1} = absreal iff for r being Real holds b_{1} . r = |.r.| );

for b

( b

definition

let x be real-valued FinSequence;

coherence

|.x.| is FinSequence of REAL

for b_{1} being FinSequence of REAL holds

( b_{1} = |.x.| iff b_{1} = absreal * x )

end;
coherence

|.x.| is FinSequence of REAL

proof end;

compatibility for b

( b

proof end;

:: deftheorem defines abs EUCLID:def 3 :

for x being real-valued FinSequence holds abs x = absreal * x;

for x being real-valued FinSequence holds abs x = absreal * x;

definition

let n be Nat;

:: original: 0*

redefine func 0* n -> Element of REAL n;

coherence

0* n is Element of REAL n ;

end;
:: original: 0*

redefine func 0* n -> Element of REAL n;

coherence

0* n is Element of REAL n ;

definition

let n be Nat;

let x be Element of REAL n;

:: original: -

redefine func - x -> Element of REAL n;

coherence

- x is Element of REAL n

end;
let x be Element of REAL n;

:: original: -

redefine func - x -> Element of REAL n;

coherence

- x is Element of REAL n

proof end;

definition

let n be Nat;

let x, y be Element of REAL n;

:: original: +

redefine func x + y -> Element of REAL n;

coherence

x + y is Element of REAL n

redefine func x - y -> Element of REAL n;

coherence

x - y is Element of REAL n

end;
let x, y be Element of REAL n;

:: original: +

redefine func x + y -> Element of REAL n;

coherence

x + y is Element of REAL n

proof end;

:: original: -redefine func x - y -> Element of REAL n;

coherence

x - y is Element of REAL n

proof end;

definition

let n be Nat;

let x be Element of REAL n;

let r be Real;

:: original: (#)

redefine func r * x -> Element of REAL n;

coherence

r (#) x is Element of REAL n

end;
let x be Element of REAL n;

let r be Real;

:: original: (#)

redefine func r * x -> Element of REAL n;

coherence

r (#) x is Element of REAL n

proof end;

definition

let n be Nat;

let x be Element of REAL n;

:: original: |.

redefine func abs x -> Element of n -tuples_on REAL;

coherence

|.x.| is Element of n -tuples_on REAL by FINSEQ_2:113;

end;
let x be Element of REAL n;

:: original: |.

redefine func abs x -> Element of n -tuples_on REAL;

coherence

|.x.| is Element of n -tuples_on REAL by FINSEQ_2:113;

definition

let n be Nat;

let x be Element of REAL n;

:: original: ^2

redefine func sqr x -> Element of n -tuples_on REAL;

coherence

x ^2 is Element of n -tuples_on REAL by FINSEQ_2:113;

end;
let x be Element of REAL n;

:: original: ^2

redefine func sqr x -> Element of n -tuples_on REAL;

coherence

x ^2 is Element of n -tuples_on REAL by FINSEQ_2:113;

:: deftheorem defines |. EUCLID:def 5 :

for f being real-valued FinSequence holds |.f.| = sqrt (Sum (sqr f));

for f being real-valued FinSequence holds |.f.| = sqrt (Sum (sqr f));

Lm1: for f being real-valued FinSequence holds f is Element of REAL (len f)

proof end;

::$CT 3

theorem Th3: :: EUCLID:6

for r being Real

for f being real-valued FinSequence holds abs (r * f) = |.r.| * (abs f) by RFUNCT_1:25;

for f being real-valued FinSequence holds abs (r * f) = |.r.| * (abs f) by RFUNCT_1:25;

Lm2: for f being real-valued FinSequence holds sqr (abs f) = sqr f

proof end;

registration
end;

theorem Th16: :: EUCLID:19

for n being Nat

for x, x1, x2 being Element of REAL n holds |.(x1 - x2).| <= |.(x1 - x).| + |.(x - x2).|

for x, x1, x2 being Element of REAL n holds |.(x1 - x2).| <= |.(x1 - x).| + |.(x - x2).|

proof end;

definition

let n be Nat;

ex b_{1} being Function of [:(REAL n),(REAL n):],REAL st

for x, y being Element of REAL n holds b_{1} . (x,y) = |.(x - y).|

for b_{1}, b_{2} being Function of [:(REAL n),(REAL n):],REAL st ( for x, y being Element of REAL n holds b_{1} . (x,y) = |.(x - y).| ) & ( for x, y being Element of REAL n holds b_{2} . (x,y) = |.(x - y).| ) holds

b_{1} = b_{2}

end;
func Pitag_dist n -> Function of [:(REAL n),(REAL n):],REAL means :Def6: :: EUCLID:def 6

for x, y being Element of REAL n holds it . (x,y) = |.(x - y).|;

existence for x, y being Element of REAL n holds it . (x,y) = |.(x - y).|;

ex b

for x, y being Element of REAL n holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines Pitag_dist EUCLID:def 6 :

for n being Nat

for b_{2} being Function of [:(REAL n),(REAL n):],REAL holds

( b_{2} = Pitag_dist n iff for x, y being Element of REAL n holds b_{2} . (x,y) = |.(x - y).| );

for n being Nat

for b

( b

definition
end;

:: deftheorem defines Euclid EUCLID:def 7 :

for n being Nat holds Euclid n = MetrStruct(# (REAL n),(Pitag_dist n) #);

for n being Nat holds Euclid n = MetrStruct(# (REAL n),(Pitag_dist n) #);

registration
end;

definition

let n be Nat;

ex b_{1} being strict RLTopStruct st

( TopStruct(# the carrier of b_{1}, the topology of b_{1} #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of b_{1}, the ZeroF of b_{1}, the addF of b_{1}, the Mult of b_{1} #) = RealVectSpace (Seg n) )

for b_{1}, b_{2} being strict RLTopStruct st TopStruct(# the carrier of b_{1}, the topology of b_{1} #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of b_{1}, the ZeroF of b_{1}, the addF of b_{1}, the Mult of b_{1} #) = RealVectSpace (Seg n) & TopStruct(# the carrier of b_{2}, the topology of b_{2} #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of b_{2}, the ZeroF of b_{2}, the addF of b_{2}, the Mult of b_{2} #) = RealVectSpace (Seg n) holds

b_{1} = b_{2}
;

end;
func TOP-REAL n -> strict RLTopStruct means :Def8: :: EUCLID:def 8

( TopStruct(# the carrier of it, the topology of it #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of it, the ZeroF of it, the addF of it, the Mult of it #) = RealVectSpace (Seg n) );

existence ( TopStruct(# the carrier of it, the topology of it #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of it, the ZeroF of it, the addF of it, the Mult of it #) = RealVectSpace (Seg n) );

ex b

( TopStruct(# the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def8 defines TOP-REAL EUCLID:def 8 :

for n being Nat

for b_{2} being strict RLTopStruct holds

( b_{2} = TOP-REAL n iff ( TopStruct(# the carrier of b_{2}, the topology of b_{2} #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of b_{2}, the ZeroF of b_{2}, the addF of b_{2}, the Mult of b_{2} #) = RealVectSpace (Seg n) ) );

for n being Nat

for b

( b

registration
end;

registration

let n be Nat;

( TOP-REAL n is TopSpace-like & TOP-REAL n is Abelian & TOP-REAL n is add-associative & TOP-REAL n is right_zeroed & TOP-REAL n is right_complementable & TOP-REAL n is vector-distributive & TOP-REAL n is scalar-distributive & TOP-REAL n is scalar-associative & TOP-REAL n is scalar-unital )

end;
cluster TOP-REAL n -> TopSpace-like right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ;

coherence ( TOP-REAL n is TopSpace-like & TOP-REAL n is Abelian & TOP-REAL n is add-associative & TOP-REAL n is right_zeroed & TOP-REAL n is right_complementable & TOP-REAL n is vector-distributive & TOP-REAL n is scalar-distributive & TOP-REAL n is scalar-associative & TOP-REAL n is scalar-unital )

proof end;

registration
end;

registration
end;

Lm3: for n being Nat

for p1, p2 being Point of (TOP-REAL n)

for r1, r2 being real-valued Function st p1 = r1 & p2 = r2 holds

p1 + p2 = r1 + r2

proof end;

Lm4: for n being Nat

for p being Point of (TOP-REAL n)

for x being Real

for r being real-valued Function st p = r holds

x * p = x (#) r

proof end;

registration

let r, s be Real;

let n be Nat;

let p be Element of (TOP-REAL n);

let f be real-valued FinSequence;

compatibility

( r = s & p = f implies r * p = s * f ) by Lm4;

end;
let n be Nat;

let p be Element of (TOP-REAL n);

let f be real-valued FinSequence;

compatibility

( r = s & p = f implies r * p = s * f ) by Lm4;

registration

let n be Nat;

let p, q be Element of (TOP-REAL n);

let f, g be real-valued FinSequence;

compatibility

( p = f & q = g implies p + q = f + g ) by Lm3;

end;
let p, q be Element of (TOP-REAL n);

let f, g be real-valued FinSequence;

compatibility

( p = f & q = g implies p + q = f + g ) by Lm3;

registration

let n be Nat;

let p be Element of (TOP-REAL n);

let f be real-valued FinSequence;

compatibility

( p = f implies - p = - f )

end;
let p be Element of (TOP-REAL n);

let f be real-valued FinSequence;

compatibility

( p = f implies - p = - f )

proof end;

registration

let n be Nat;

let p, q be Element of (TOP-REAL n);

let f, g be real-valued FinSequence;

compatibility

( p = f & q = g implies p - q = f - g ) ;

end;
let p, q be Element of (TOP-REAL n);

let f, g be real-valued FinSequence;

compatibility

( p = f & q = g implies p - q = f - g ) ;

registration
end;

definition

let n be Nat;

:: original: 0*

redefine func 0.REAL n -> Point of (TOP-REAL n);

coherence

0* n is Point of (TOP-REAL n)

end;
:: original: 0*

redefine func 0.REAL n -> Point of (TOP-REAL n);

coherence

0* n is Point of (TOP-REAL n)

proof end;

theorem :: EUCLID:25

definition

let x, y be Real;

:: original: |[

redefine func |[x,y]| -> Point of (TOP-REAL 2);

coherence

|[x,y]| is Point of (TOP-REAL 2)

end;
:: original: |[

redefine func |[x,y]| -> Point of (TOP-REAL 2);

coherence

|[x,y]| is Point of (TOP-REAL 2)

proof end;

theorem :: EUCLID:63

for n being Nat

for P being Subset of (TOP-REAL n)

for Q being non empty Subset of (Euclid n) st P = Q holds

(TOP-REAL n) | P = TopSpaceMetr ((Euclid n) | Q)

for P being Subset of (TOP-REAL n)

for Q being non empty Subset of (Euclid n) st P = Q holds

(TOP-REAL n) | P = TopSpaceMetr ((Euclid n) | Q)

proof end;

:: to enable the 03.2009. revision A.T.

theorem :: EUCLID:64

theorem :: EUCLID:65

theorem :: EUCLID:68

theorem :: EUCLID:69

theorem :: EUCLID:71

registration
end;

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

definition

let n be Nat;

:: original: 1*

redefine func 1* n -> Element of REAL n;

coherence

1* n is Element of REAL n

end;
:: original: 1*

redefine func 1* n -> Element of REAL n;

coherence

1* n is Element of REAL n

proof end;

theorem :: EUCLID:76

for f being FinSequence of REAL holds

( f is Element of REAL (len f) & f is Point of (TOP-REAL (len f)) )

( f is Element of REAL (len f) & f is Point of (TOP-REAL (len f)) )

proof end;