:: The Euclidean Space :: by Agata Darmochwa{\l} :: :: Received November 21, 1991 :: Copyright (c) 1991-2012 Association of Mizar Users begin definition let n be Nat; func REAL n -> FinSequenceSet of REAL equals :: EUCLID:def 1 n -tuples_on REAL; coherence n -tuples_on REAL is FinSequenceSet of REAL ; end; :: deftheorem defines REAL EUCLID:def_1_:_ for n being Nat holds REAL n = n -tuples_on REAL; registration let n be Nat; cluster REAL n -> non empty ; coherence not REAL n is empty ; end; registration let n be Nat; cluster -> n -element for Element of REAL n; coherence for b1 being Element of REAL n holds b1 is n -element ; end; definition func absreal -> Function of REAL,REAL means :Def2: :: EUCLID:def 2 for r being real number holds it . r = abs r; existence ex b1 being Function of REAL,REAL st for r being real number holds b1 . r = abs r proofend; uniqueness for b1, b2 being Function of REAL,REAL st ( for r being real number holds b1 . r = abs r ) & ( for r being real number holds b2 . r = abs r ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines absreal EUCLID:def_2_:_ for b1 being Function of REAL,REAL holds ( b1 = absreal iff for r being real number holds b1 . r = abs r ); definition let x be real-valued FinSequence; :: original:|. redefine func abs x -> FinSequence of REAL equals :: EUCLID:def 3 absreal * x; coherence |.x.| is FinSequence of REAL proofend; compatibility for b1 being FinSequence of REAL holds ( b1 = |.x.| iff b1 = absreal * x ) proofend; end; :: deftheorem defines abs EUCLID:def_3_:_ for x being real-valued FinSequence holds abs x = absreal * x; definition let n be Nat; func 0* n -> real-valued FinSequence equals :: EUCLID:def 4 n |-> 0; coherence n |-> 0 is real-valued FinSequence ; end; :: deftheorem defines 0* EUCLID:def_4_:_ for n being Nat holds 0* n = n |-> 0; definition let n be Nat; :: original:0* redefine func 0* n -> Element of REAL n; coherence 0* n is Element of REAL n ; end; 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 proofend; end; definition let n be Nat; let x, y be Element of REAL n; :: original:+ redefine funcx + y -> Element of REAL n; coherence x + y is Element of REAL n proofend; :: original:- redefine funcx - y -> Element of REAL n; coherence x - y is Element of REAL n proofend; end; definition let n be Nat; let x be Element of REAL n; let r be real number ; :: original:(#) redefine funcr * x -> Element of REAL n; coherence r (#) x is Element of REAL n proofend; 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; 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; definition let f be real-valued FinSequence; func|.f.| -> Real equals :: EUCLID:def 5 sqrt (Sum (sqr f)); coherence sqrt (Sum (sqr f)) is Real ; end; :: deftheorem defines |. EUCLID:def_5_:_ 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) proofend; theorem :: EUCLID:1 canceled; theorem :: EUCLID:2 canceled; theorem :: EUCLID:3 canceled; theorem :: EUCLID:4 for n being Nat holds abs (0* n) = n |-> 0 proofend; theorem Th5: :: EUCLID:5 for f being complex-valued Function holds abs (- f) = abs f proofend; theorem Th6: :: EUCLID:6 for r being real number for f being real-valued FinSequence holds abs (r * f) = (abs r) * (abs f) by RFUNCT_1:25; theorem Th7: :: EUCLID:7 for n being Nat holds |.(0* n).| = 0 proofend; Lm2: for f being real-valued FinSequence holds sqr (abs f) = sqr f proofend; theorem Th8: :: EUCLID:8 for n being Nat for x being Element of REAL n st |.x.| = 0 holds x = 0* n proofend; theorem Th9: :: EUCLID:9 for f being real-valued FinSequence holds |.f.| >= 0 proofend; registration let f be real-valued FinSequence; cluster|.f.| -> non negative ; coherence not |.f.| is negative by Th9; end; theorem Th10: :: EUCLID:10 for f being real-valued FinSequence holds |.(- f).| = |.f.| proofend; theorem :: EUCLID:11 for r being real number for f being real-valued FinSequence holds |.(r * f).| = (abs r) * |.f.| proofend; theorem Th12: :: EUCLID:12 for n being Nat for x1, x2 being Element of REAL n holds |.(x1 + x2).| <= |.x1.| + |.x2.| proofend; theorem Th13: :: EUCLID:13 for n being Nat for x1, x2 being Element of REAL n holds |.(x1 - x2).| <= |.x1.| + |.x2.| proofend; theorem :: EUCLID:14 for n being Nat for x1, x2 being Element of REAL n holds |.x1.| - |.x2.| <= |.(x1 + x2).| proofend; theorem :: EUCLID:15 for n being Nat for x1, x2 being Element of REAL n holds |.x1.| - |.x2.| <= |.(x1 - x2).| proofend; theorem Th16: :: EUCLID:16 for n being Nat for x1, x2 being Element of REAL n holds ( |.(x1 - x2).| = 0 iff x1 = x2 ) proofend; registration let n be Nat; let x1 be Element of REAL n; cluster|.(x1 - x1).| -> zero ; coherence |.(x1 - x1).| is empty by Th16; end; theorem :: EUCLID:17 for n being Nat for x1, x2 being Element of REAL n st x1 <> x2 holds |.(x1 - x2).| > 0 proofend; theorem Th18: :: EUCLID:18 for n being Nat for x1, x2 being Element of REAL n holds |.(x1 - x2).| = |.(x2 - x1).| proofend; theorem Th19: :: EUCLID:19 for n being Nat for x1, x2, x being Element of REAL n holds |.(x1 - x2).| <= |.(x1 - x).| + |.(x - x2).| proofend; definition let n be Nat; 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 ex b1 being Function of [:(REAL n),(REAL n):],REAL st for x, y being Element of REAL n holds b1 . (x,y) = |.(x - y).| proofend; uniqueness for b1, b2 being Function of [:(REAL n),(REAL n):],REAL st ( for x, y being Element of REAL n holds b1 . (x,y) = |.(x - y).| ) & ( for x, y being Element of REAL n holds b2 . (x,y) = |.(x - y).| ) holds b1 = b2 proofend; end; :: deftheorem Def6 defines Pitag_dist EUCLID:def_6_:_ for n being Nat for b2 being Function of [:(REAL n),(REAL n):],REAL holds ( b2 = Pitag_dist n iff for x, y being Element of REAL n holds b2 . (x,y) = |.(x - y).| ); theorem :: EUCLID:20 for x, y being real-valued FinSequence holds sqr (x - y) = sqr (y - x) proofend; theorem Th21: :: EUCLID:21 for n being Nat holds Pitag_dist n is_metric_of REAL n proofend; definition let n be Nat; func Euclid n -> strict MetrSpace equals :: EUCLID:def 7 MetrStruct(# (REAL n),(Pitag_dist n) #); coherence MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrSpace proofend; end; :: deftheorem defines Euclid EUCLID:def_7_:_ for n being Nat holds Euclid n = MetrStruct(# (REAL n),(Pitag_dist n) #); registration let n be Nat; cluster Euclid n -> non empty strict ; coherence not Euclid n is empty ; end; definition let n be Nat; 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 ex b1 being strict RLTopStruct st ( TopStruct(# the carrier of b1, the topology of b1 #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of b1, the ZeroF of b1, the addF of b1, the Mult of b1 #) = RealVectSpace (Seg n) ) proofend; uniqueness for b1, b2 being strict RLTopStruct st TopStruct(# the carrier of b1, the topology of b1 #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of b1, the ZeroF of b1, the addF of b1, the Mult of b1 #) = RealVectSpace (Seg n) & TopStruct(# the carrier of b2, the topology of b2 #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of b2, the ZeroF of b2, the addF of b2, the Mult of b2 #) = RealVectSpace (Seg n) holds b1 = b2 ; end; :: deftheorem Def8 defines TOP-REAL EUCLID:def_8_:_ for n being Nat for b2 being strict RLTopStruct holds ( b2 = TOP-REAL n iff ( TopStruct(# the carrier of b2, the topology of b2 #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of b2, the ZeroF of b2, the addF of b2, the Mult of b2 #) = RealVectSpace (Seg n) ) ); registration let n be Nat; cluster TOP-REAL n -> non empty strict ; coherence not TOP-REAL n is empty proofend; end; registration let n be Nat; 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 ) proofend; end; theorem Th22: :: EUCLID:22 for n being Nat holds the carrier of (TOP-REAL n) = REAL n proofend; theorem Th23: :: EUCLID:23 for n being Nat for p being Point of (TOP-REAL n) holds p is Function of (Seg n),REAL proofend; theorem Th24: :: EUCLID:24 for n being Nat for p being Point of (TOP-REAL n) holds p is FinSequence of REAL proofend; registration let n be Nat; cluster TOP-REAL n -> constituted-FinSeqs strict ; coherence TOP-REAL n is constituted-FinSeqs proofend; end; registration let n be Nat; cluster -> FinSequence-like for Element of the carrier of (TOP-REAL n); coherence for b1 being Point of (TOP-REAL n) holds b1 is FinSequence-like ; end; registration let n be Nat; cluster -> real-valued for Element of the carrier of (TOP-REAL n); coherence for b1 being Point of (TOP-REAL n) holds b1 is real-valued by Th24; 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 proofend; Lm4: for n being Nat for p being Point of (TOP-REAL n) for x being real number for r being real-valued Function st p = r holds x * p = x (#) r proofend; registration let r, s be real number ; let n be Nat; let p be Element of (TOP-REAL n); let f be real-valued FinSequence; identifyr * p with s * f when r = s, p = f; compatibility ( r = s & p = f implies r * p = s * f ) by Lm4; end; registration let n be Nat; let p, q be Element of (TOP-REAL n); let f, g be real-valued FinSequence; identifyp + q with f + g when p = f, q = g; compatibility ( p = f & q = g implies p + q = f + g ) by Lm3; end; registration let n be Nat; let p be Element of (TOP-REAL n); let f be real-valued FinSequence; identify - p with - f when p = f; compatibility ( p = f implies - p = - f ) proofend; end; registration let n be Nat; let p, q be Element of (TOP-REAL n); let f, g be real-valued FinSequence; identifyp - q with f - g when p = f, q = g; compatibility ( p = f & q = g implies p - q = f - g ) ; end; registration let n be Nat; cluster -> n -element for Element of the carrier of (TOP-REAL n); coherence for b1 being Point of (TOP-REAL n) holds b1 is n -element proofend; end; notation let n be Nat; synonym 0.REAL n for 0* n; 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) proofend; end; theorem :: EUCLID:25 for n being Nat for x being Element of REAL n holds sqr (abs x) = sqr x by Lm2; theorem :: EUCLID:26 for n being Nat for p1, p2, p3 being Point of (TOP-REAL n) holds (p1 + p2) + p3 = p1 + (p2 + p3) by RLVECT_1:def_3; theorem :: EUCLID:27 for n being Nat for p being Point of (TOP-REAL n) holds ( (0. (TOP-REAL n)) + p = p & p + (0. (TOP-REAL n)) = p ) by RLVECT_1:4; theorem :: EUCLID:28 for n being Nat for x being real number holds x * (0. (TOP-REAL n)) = 0. (TOP-REAL n) by RLVECT_1:10; theorem :: EUCLID:29 for n being Nat for p being Point of (TOP-REAL n) holds ( 1 * p = p & 0 * p = 0. (TOP-REAL n) ) by RLVECT_1:10, RLVECT_1:def_8; theorem :: EUCLID:30 for n being Nat for p being Point of (TOP-REAL n) for x, y being real number holds (x * y) * p = x * (y * p) by RLVECT_1:def_7; theorem :: EUCLID:31 for n being Nat for p being Point of (TOP-REAL n) for x being real number holds ( not x * p = 0. (TOP-REAL n) or x = 0 or p = 0. (TOP-REAL n) ) by RLVECT_1:11; theorem :: EUCLID:32 for n being Nat for p1, p2 being Point of (TOP-REAL n) for x being real number holds x * (p1 + p2) = (x * p1) + (x * p2) by RLVECT_1:def_5; theorem :: EUCLID:33 for n being Nat for p being Point of (TOP-REAL n) for x, y being real number holds (x + y) * p = (x * p) + (y * p) by RLVECT_1:def_6; theorem :: EUCLID:34 for n being Nat for p1, p2 being Point of (TOP-REAL n) for x being real number holds ( not x * p1 = x * p2 or x = 0 or p1 = p2 ) by RLVECT_1:36; theorem :: EUCLID:35 canceled; theorem :: EUCLID:36 for n being Nat for p being Point of (TOP-REAL n) holds p + (- p) = 0. (TOP-REAL n) by RLVECT_1:5; theorem :: EUCLID:37 for n being Nat for p1, p2 being Point of (TOP-REAL n) st p1 + p2 = 0. (TOP-REAL n) holds p1 = - p2 by RLVECT_1:6; theorem :: EUCLID:38 for n being Nat for p1, p2 being Point of (TOP-REAL n) holds - (p1 + p2) = (- p1) - p2 by RLVECT_1:30; theorem :: EUCLID:39 for n being Nat for p being Point of (TOP-REAL n) holds - p = (- 1) * p ; theorem :: EUCLID:40 for n being Nat for p being Point of (TOP-REAL n) for x being real number holds ( - (x * p) = (- x) * p & - (x * p) = x * (- p) ) by RLVECT_1:25, RLVECT_1:79; theorem :: EUCLID:41 for n being Nat for p1, p2 being Point of (TOP-REAL n) holds p1 - p2 = p1 + (- p2) ; theorem :: EUCLID:42 for n being Nat for p being Point of (TOP-REAL n) holds p - p = 0. (TOP-REAL n) by RLVECT_1:5; theorem :: EUCLID:43 for n being Nat for p1, p2 being Point of (TOP-REAL n) st p1 - p2 = 0. (TOP-REAL n) holds p1 = p2 by RLVECT_1:21; theorem :: EUCLID:44 for n being Nat for p1, p2 being Point of (TOP-REAL n) holds ( - (p1 - p2) = p2 - p1 & - (p1 - p2) = (- p1) + p2 ) by RLVECT_1:33; theorem :: EUCLID:45 for n being Nat for p1, p2, p3 being Point of (TOP-REAL n) holds p1 + (p2 - p3) = (p1 + p2) - p3 by RLVECT_1:def_3; theorem :: EUCLID:46 for n being Nat for p1, p2, p3 being Point of (TOP-REAL n) holds p1 - (p2 + p3) = (p1 - p2) - p3 by RLVECT_1:27; theorem :: EUCLID:47 for n being Nat for p1, p2, p3 being Point of (TOP-REAL n) holds p1 - (p2 - p3) = (p1 - p2) + p3 by RLVECT_1:29; theorem :: EUCLID:48 for n being Nat for p, p1 being Point of (TOP-REAL n) holds ( p = (p + p1) - p1 & p = (p - p1) + p1 ) by RLVECT_4:1; theorem :: EUCLID:49 for n being Nat for p1, p2 being Point of (TOP-REAL n) for x being real number holds x * (p1 - p2) = (x * p1) - (x * p2) by RLVECT_1:34; theorem :: EUCLID:50 for n being Nat for p being Point of (TOP-REAL n) for x, y being real number holds (x - y) * p = (x * p) - (y * p) by RLVECT_1:35; theorem :: EUCLID:51 for p being Point of (TOP-REAL 2) ex x, y being Real st p = <*x,y*> proofend; definition let p be Point of (TOP-REAL 2); funcp `1 -> Real equals :: EUCLID:def 9 p . 1; coherence p . 1 is Real ; funcp `2 -> Real equals :: EUCLID:def 10 p . 2; coherence p . 2 is Real ; end; :: deftheorem defines `1 EUCLID:def_9_:_ for p being Point of (TOP-REAL 2) holds p `1 = p . 1; :: deftheorem defines `2 EUCLID:def_10_:_ for p being Point of (TOP-REAL 2) holds p `2 = p . 2; notation let x, y be real number ; synonym |[x,y]| for <*x,y*>; end; definition let x, y be real number ; :: original:|[ redefine func|[x,y]| -> Point of (TOP-REAL 2); coherence |[x,y]| is Point of (TOP-REAL 2) proofend; end; theorem :: EUCLID:52 for x, y being real number holds ( |[x,y]| `1 = x & |[x,y]| `2 = y ) by FINSEQ_1:44; theorem Th53: :: EUCLID:53 for p being Point of (TOP-REAL 2) holds p = |[(p `1),(p `2)]| proofend; theorem :: EUCLID:54 0. (TOP-REAL 2) = |[0,0]| proofend; theorem Th55: :: EUCLID:55 for p1, p2 being Point of (TOP-REAL 2) holds p1 + p2 = |[((p1 `1) + (p2 `1)),((p1 `2) + (p2 `2))]| proofend; theorem :: EUCLID:56 for x1, y1, x2, y2 being real number holds |[x1,y1]| + |[x2,y2]| = |[(x1 + x2),(y1 + y2)]| proofend; theorem Th57: :: EUCLID:57 for x being real number for p being Point of (TOP-REAL 2) holds x * p = |[(x * (p `1)),(x * (p `2))]| proofend; theorem :: EUCLID:58 for x, x1, y1 being real number holds x * |[x1,y1]| = |[(x * x1),(x * y1)]| proofend; theorem Th59: :: EUCLID:59 for p being Point of (TOP-REAL 2) holds - p = |[(- (p `1)),(- (p `2))]| proofend; theorem :: EUCLID:60 for x1, y1 being real number holds - |[x1,y1]| = |[(- x1),(- y1)]| proofend; theorem Th61: :: EUCLID:61 for p1, p2 being Point of (TOP-REAL 2) holds p1 - p2 = |[((p1 `1) - (p2 `1)),((p1 `2) - (p2 `2))]| proofend; theorem :: EUCLID:62 for x1, y1, x2, y2 being real number holds |[x1,y1]| - |[x2,y2]| = |[(x1 - x2),(y1 - y2)]| proofend; 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) proofend; :: to enable the 03.2009. revision A.T. theorem :: EUCLID:64 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 ; theorem :: EUCLID:65 for n being Nat for x being real number for p being Point of (TOP-REAL n) for r being real-valued Function st p = r holds x * p = x (#) r ; theorem Th66: :: EUCLID:66 for n being Nat holds 0.REAL n = 0. (TOP-REAL n) proofend; theorem Th67: :: EUCLID:67 for n being Nat holds the carrier of (Euclid n) = the carrier of (TOP-REAL n) proofend; theorem :: EUCLID:68 for n being Nat for p1 being Point of (TOP-REAL n) for r1 being real-valued Function st p1 = r1 holds - p1 = - r1 ; theorem :: EUCLID:69 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 ; theorem :: EUCLID:70 for n being Nat holds 0. (TOP-REAL n) = 0* n by Th66; theorem :: EUCLID:71 for n being Nat for p being Point of (TOP-REAL n) holds |.(- p).| = |.p.| by Th10; registration let n be Nat; let D be set ; clustern -tuples_on D -> FinSequence-membered ; coherence n -tuples_on D is FinSequence-membered ; end; registration let n be Nat; cluster REAL n -> FinSequence-membered ; coherence REAL n is FinSequence-membered ; end; registration let n be Nat; cluster REAL n -> real-functions-membered ; coherence REAL n is real-functions-membered proofend; end; :: from JORDAN2C, 2011.07.28, A.T. definition let n be Nat; func 1* n -> FinSequence of REAL equals :: EUCLID:def 11 n |-> 1; coherence n |-> 1 is FinSequence of REAL ; end; :: deftheorem defines 1* EUCLID:def_11_:_ for n being Nat holds 1* n = n |-> 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; definition let n be Nat; func 1.REAL n -> Point of (TOP-REAL n) equals :: EUCLID:def 12 1* n; coherence 1* n is Point of (TOP-REAL n) by Th22; end; :: deftheorem defines 1.REAL EUCLID:def_12_:_ for n being Nat holds 1.REAL n = 1* n; theorem :: EUCLID:72 for n being Nat holds abs (1* n) = n |-> 1 proofend; theorem Th73: :: EUCLID:73 for n being Nat holds |.(1* n).| = sqrt n proofend; theorem :: EUCLID:74 for n being Nat holds |.(1.REAL n).| = sqrt n by Th73; theorem :: EUCLID:75 for n being Nat st 1 <= n holds 1 <= |.(1.REAL n).| proofend; 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)) ) proofend; theorem :: EUCLID:77 REAL 0 = {(0. (TOP-REAL 0))} proofend;