:: EUCLID_2 semantic presentation begin theorem Th1: :: EUCLID_2:1 for n, i being Nat for v being Element of n -tuples_on REAL holds (mlt (v,(0* n))) . i = 0 proof let n, i be Nat; ::_thesis: for v being Element of n -tuples_on REAL holds (mlt (v,(0* n))) . i = 0 let v be Element of n -tuples_on REAL; ::_thesis: (mlt (v,(0* n))) . i = 0 A1: 0* n = n |-> 0 by EUCLID:def_4; set v0 = (0* n) . i; A2: dom (0* n) = Seg n by FINSEQ_2:124; ( i in Seg n or not i in Seg n ) ; then A3: (0* n) . i = 0 by A1, A2, FUNCOP_1:7, FUNCT_1:def_2; (mlt (v,(0* n))) . i = (v . i) * ((0* n) . i) by RVSUM_1:60 .= 0 by A3 ; hence (mlt (v,(0* n))) . i = 0 ; ::_thesis: verum end; theorem Th2: :: EUCLID_2:2 for n being Nat for v being Element of n -tuples_on REAL holds mlt (v,(0* n)) = 0* n proof let n be Nat; ::_thesis: for v being Element of n -tuples_on REAL holds mlt (v,(0* n)) = 0* n let v be Element of n -tuples_on REAL; ::_thesis: mlt (v,(0* n)) = 0* n len (0* n) = n by CARD_1:def_7; then reconsider z = 0* n as Element of n -tuples_on REAL by FINSEQ_2:92; A1: len (0* n) = n by CARD_1:def_7; A2: for j being Nat st j in dom (0* n) holds (mlt (v,(0* n))) . j = (0* n) . j proof let j be Nat; ::_thesis: ( j in dom (0* n) implies (mlt (v,(0* n))) . j = (0* n) . j ) assume j in dom (0* n) ; ::_thesis: (mlt (v,(0* n))) . j = (0* n) . j thus (mlt (v,(0* n))) . j = 0 by Th1 .= (n |-> 0) . j .= (0* n) . j by EUCLID:def_4 ; ::_thesis: verum end; len (mlt (v,z)) = n by CARD_1:def_7; then dom (mlt (v,(0* n))) = dom (0* n) by A1, FINSEQ_3:29; hence mlt (v,(0* n)) = 0* n by A2, FINSEQ_1:13; ::_thesis: verum end; begin theorem Th3: :: EUCLID_2:3 for n being Nat for y1, y2 being real-valued FinSequence for x1, x2 being Element of REAL n st x1 = y1 & x2 = y2 holds |(y1,y2)| = (1 / 4) * ((|.(x1 + x2).| ^2) - (|.(x1 - x2).| ^2)) proof let n be Nat; ::_thesis: for y1, y2 being real-valued FinSequence for x1, x2 being Element of REAL n st x1 = y1 & x2 = y2 holds |(y1,y2)| = (1 / 4) * ((|.(x1 + x2).| ^2) - (|.(x1 - x2).| ^2)) let y1, y2 be real-valued FinSequence; ::_thesis: for x1, x2 being Element of REAL n st x1 = y1 & x2 = y2 holds |(y1,y2)| = (1 / 4) * ((|.(x1 + x2).| ^2) - (|.(x1 - x2).| ^2)) let x1, x2 be Element of REAL n; ::_thesis: ( x1 = y1 & x2 = y2 implies |(y1,y2)| = (1 / 4) * ((|.(x1 + x2).| ^2) - (|.(x1 - x2).| ^2)) ) assume A1: ( x1 = y1 & x2 = y2 ) ; ::_thesis: |(y1,y2)| = (1 / 4) * ((|.(x1 + x2).| ^2) - (|.(x1 - x2).| ^2)) reconsider w1 = x1, w2 = x2 as Element of n -tuples_on REAL by EUCLID:def_1; set v1 = sqr (x1 + x2); set v2 = sqr (x1 - x2); set z1 = x1 + x2; set z2 = x1 - x2; A2: (1 / 4) * ((|.(x1 + x2).| ^2) - (|.(x1 - x2).| ^2)) = (1 / 4) * (((sqrt (Sum (sqr (x1 + x2)))) ^2) - (|.(x1 - x2).| ^2)) by EUCLID:def_5 .= (1 / 4) * (((sqrt (Sum (sqr (x1 + x2)))) ^2) - ((sqrt (Sum (sqr (x1 - x2)))) ^2)) by EUCLID:def_5 ; Sum (sqr (x1 + x2)) >= 0 by RVSUM_1:86; then A3: (sqrt (Sum (sqr (x1 + x2)))) ^2 = Sum (sqr (x1 + x2)) by SQUARE_1:def_2; A4: (Sum (sqr (x1 + x2))) - (Sum (sqr (x1 - x2))) = Sum ((sqr (x1 + x2)) - (sqr (x1 - x2))) by RVSUM_1:90; Sum (sqr (x1 - x2)) >= 0 by RVSUM_1:86; then A5: (sqrt (Sum (sqr (x1 - x2)))) ^2 = Sum (sqr (x1 - x2)) by SQUARE_1:def_2; A6: ((2 * (mlt (w1,w2))) + (sqr w2)) + (2 * (mlt (w1,w2))) = (2 * (mlt (w1,w2))) + ((2 * (mlt (w1,w2))) + (sqr w2)) .= ((2 * (mlt (w1,w2))) + (2 * (mlt (w1,w2)))) + (sqr w2) by FINSEQOP:28 ; A7: (sqr w1) + ((2 * (mlt (w1,w2))) + (sqr w2)) = ((2 * (mlt (w1,w2))) + (sqr w2)) + (sqr w1) ; (sqr (x1 + x2)) - (sqr (x1 - x2)) = (((sqr w1) + (2 * (mlt (w1,w2)))) + (sqr w2)) - (sqr (w1 - w2)) by RVSUM_1:68 .= (((sqr w1) + (2 * (mlt (w1,w2)))) + (sqr w2)) - (((sqr w1) - (2 * (mlt (w1,w2)))) + (sqr w2)) by RVSUM_1:69 .= (((2 * (mlt (w1,w2))) + (sqr w2)) + (sqr w1)) - (((sqr w1) - (2 * (mlt (w1,w2)))) + (sqr w2)) by A7, FINSEQOP:28 .= ((((2 * (mlt (w1,w2))) + (sqr w2)) + (sqr w1)) - ((sqr w1) - (2 * (mlt (w1,w2))))) - (sqr w2) by RVSUM_1:39 .= (((((2 * (mlt (w1,w2))) + (sqr w2)) + (sqr w1)) - (sqr w1)) + (2 * (mlt (w1,w2)))) - (sqr w2) by RVSUM_1:41 .= (((2 * (mlt (w1,w2))) + (sqr w2)) + (2 * (mlt (w1,w2)))) - (sqr w2) by RVSUM_1:42 .= (2 * (mlt (w1,w2))) + (2 * (mlt (w1,w2))) by A6, RVSUM_1:42 .= (2 + 2) * (mlt (w1,w2)) by RVSUM_1:50 .= 4 * (mlt (w1,w2)) ; then (1 / 4) * ((|.(x1 + x2).| ^2) - (|.(x1 - x2).| ^2)) = (1 / 4) * (4 * (Sum (mlt (w1,w2)))) by A2, A3, A5, A4, RVSUM_1:87 .= Sum (mlt (w1,w2)) ; hence |(y1,y2)| = (1 / 4) * ((|.(x1 + x2).| ^2) - (|.(x1 - x2).| ^2)) by A1; ::_thesis: verum end; Lm1: now__::_thesis:_for_x_being_real-valued_FinSequence_holds_x_is_FinSequence_of_REAL let x be real-valued FinSequence; ::_thesis: x is FinSequence of REAL rng x c= REAL ; hence x is FinSequence of REAL by FINSEQ_1:def_4; ::_thesis: verum end; theorem Th4: :: EUCLID_2:4 for x being real-valued FinSequence holds |.x.| ^2 = |(x,x)| proof let x be real-valued FinSequence; ::_thesis: |.x.| ^2 = |(x,x)| A1: 0 <= |(x,x)| by RVSUM_1:119; |.x.| ^2 = (sqrt (Sum (sqr x))) ^2 by EUCLID:def_5 .= |(x,x)| by A1, SQUARE_1:def_2 ; hence |.x.| ^2 = |(x,x)| ; ::_thesis: verum end; theorem Th5: :: EUCLID_2:5 for x being real-valued FinSequence holds |.x.| = sqrt |(x,x)| proof let x be real-valued FinSequence; ::_thesis: |.x.| = sqrt |(x,x)| |.x.| = sqrt (|.x.| ^2) by EUCLID:9, SQUARE_1:22 .= sqrt |(x,x)| by Th4 ; hence |.x.| = sqrt |(x,x)| ; ::_thesis: verum end; theorem Th6: :: EUCLID_2:6 for x being real-valued FinSequence holds 0 <= |.x.| proof let x be real-valued FinSequence; ::_thesis: 0 <= |.x.| ( |.x.| = sqrt |(x,x)| & 0 <= |(x,x)| ) by Th5, RVSUM_1:119; hence 0 <= |.x.| by SQUARE_1:def_2; ::_thesis: verum end; theorem Th7: :: EUCLID_2:7 for x being real-valued FinSequence holds ( |(x,x)| = 0 iff x = 0* (len x) ) proof let x be real-valued FinSequence; ::_thesis: ( |(x,x)| = 0 iff x = 0* (len x) ) thus ( |(x,x)| = 0 implies x = 0* (len x) ) ::_thesis: ( x = 0* (len x) implies |(x,x)| = 0 ) proof x is FinSequence of REAL by Lm1; then reconsider y = x as Element of REAL (len x) by EUCLID:76; assume |(x,x)| = 0 ; ::_thesis: x = 0* (len x) then |.x.| ^2 = 0 by Th4; then |.x.| = 0 by XCMPLX_1:6; then y = 0* (len x) by EUCLID:8; hence x = 0* (len x) ; ::_thesis: verum end; assume x = 0* (len x) ; ::_thesis: |(x,x)| = 0 then |.x.| = 0 by EUCLID:7; then |(x,x)| = 0 ^2 by Th4; hence |(x,x)| = 0 ; ::_thesis: verum end; theorem :: EUCLID_2:8 for x being real-valued FinSequence holds ( |(x,x)| = 0 iff |.x.| = 0 ) proof let x be real-valued FinSequence; ::_thesis: ( |(x,x)| = 0 iff |.x.| = 0 ) A1: ( |(x,x)| = 0 ^2 implies |.x.| = 0 ) proof assume |(x,x)| = 0 ^2 ; ::_thesis: |.x.| = 0 then x = 0* (len x) by Th7; hence |.x.| = 0 by EUCLID:7; ::_thesis: verum end; ( |.x.| = 0 implies |(x,x)| = 0 ^2 ) by Th4; hence ( |(x,x)| = 0 iff |.x.| = 0 ) by A1; ::_thesis: verum end; theorem Th9: :: EUCLID_2:9 for x being real-valued FinSequence holds |(x,(0* (len x)))| = 0 proof let x be real-valued FinSequence; ::_thesis: |(x,(0* (len x)))| = 0 set n = len x; x is FinSequence of REAL by Lm1; then reconsider p1 = x as Element of (len x) -tuples_on REAL by FINSEQ_2:92; A1: 0* (len x) = (len x) |-> 0 by EUCLID:def_4; |(x,(0* (len x)))| = Sum (mlt (p1,(0* (len x)))) .= Sum (0* (len x)) by Th2 .= 0 by A1, RVSUM_1:81 ; hence |(x,(0* (len x)))| = 0 ; ::_thesis: verum end; theorem :: EUCLID_2:10 for x being real-valued FinSequence holds |((0* (len x)),x)| = 0 by Th9; theorem Th11: :: EUCLID_2:11 for x, y being real-valued FinSequence st len x = len y holds |.(x + y).| ^2 = ((|.x.| ^2) + (2 * |(y,x)|)) + (|.y.| ^2) proof let x, y be real-valued FinSequence; ::_thesis: ( len x = len y implies |.(x + y).| ^2 = ((|.x.| ^2) + (2 * |(y,x)|)) + (|.y.| ^2) ) assume A1: len x = len y ; ::_thesis: |.(x + y).| ^2 = ((|.x.| ^2) + (2 * |(y,x)|)) + (|.y.| ^2) |.(x + y).| ^2 = |((x + y),(x + y))| by Th4 .= (|(x,x)| + (2 * |(x,y)|)) + |(y,y)| by A1, RVSUM_1:128 .= ((|.x.| ^2) + (2 * |(y,x)|)) + |(y,y)| by Th4 .= ((|.x.| ^2) + (2 * |(y,x)|)) + (|.y.| ^2) by Th4 ; hence |.(x + y).| ^2 = ((|.x.| ^2) + (2 * |(y,x)|)) + (|.y.| ^2) ; ::_thesis: verum end; theorem Th12: :: EUCLID_2:12 for x, y being real-valued FinSequence st len x = len y holds |.(x - y).| ^2 = ((|.x.| ^2) - (2 * |(y,x)|)) + (|.y.| ^2) proof let x, y be real-valued FinSequence; ::_thesis: ( len x = len y implies |.(x - y).| ^2 = ((|.x.| ^2) - (2 * |(y,x)|)) + (|.y.| ^2) ) assume A1: len x = len y ; ::_thesis: |.(x - y).| ^2 = ((|.x.| ^2) - (2 * |(y,x)|)) + (|.y.| ^2) |.(x - y).| ^2 = |((x - y),(x - y))| by Th4 .= (|(x,x)| - (2 * |(x,y)|)) + |(y,y)| by A1, RVSUM_1:129 .= ((|.x.| ^2) - (2 * |(y,x)|)) + |(y,y)| by Th4 .= ((|.x.| ^2) - (2 * |(y,x)|)) + (|.y.| ^2) by Th4 ; hence |.(x - y).| ^2 = ((|.x.| ^2) - (2 * |(y,x)|)) + (|.y.| ^2) ; ::_thesis: verum end; theorem :: EUCLID_2:13 for x, y being real-valued FinSequence st len x = len y holds (|.(x + y).| ^2) + (|.(x - y).| ^2) = 2 * ((|.x.| ^2) + (|.y.| ^2)) proof let x, y be real-valued FinSequence; ::_thesis: ( len x = len y implies (|.(x + y).| ^2) + (|.(x - y).| ^2) = 2 * ((|.x.| ^2) + (|.y.| ^2)) ) assume A1: len x = len y ; ::_thesis: (|.(x + y).| ^2) + (|.(x - y).| ^2) = 2 * ((|.x.| ^2) + (|.y.| ^2)) then (|.(x + y).| ^2) + (|.(x - y).| ^2) = (((|.x.| ^2) + (2 * |(y,x)|)) + (|.y.| ^2)) + (|.(x - y).| ^2) by Th11 .= (((|.x.| ^2) + (2 * |(x,y)|)) + (|.y.| ^2)) + (((|.x.| ^2) - (2 * |(y,x)|)) + (|.y.| ^2)) by A1, Th12 .= 2 * ((|.x.| ^2) + (|.y.| ^2)) ; hence (|.(x + y).| ^2) + (|.(x - y).| ^2) = 2 * ((|.x.| ^2) + (|.y.| ^2)) ; ::_thesis: verum end; theorem :: EUCLID_2:14 for x, y being real-valued FinSequence st len x = len y holds (|.(x + y).| ^2) - (|.(x - y).| ^2) = 4 * |(x,y)| proof let x, y be real-valued FinSequence; ::_thesis: ( len x = len y implies (|.(x + y).| ^2) - (|.(x - y).| ^2) = 4 * |(x,y)| ) assume A1: len x = len y ; ::_thesis: (|.(x + y).| ^2) - (|.(x - y).| ^2) = 4 * |(x,y)| then (|.(x + y).| ^2) - (|.(x - y).| ^2) = (((|.x.| ^2) + (2 * |(y,x)|)) + (|.y.| ^2)) - (|.(x - y).| ^2) by Th11 .= (((|.x.| ^2) + (2 * |(x,y)|)) + (|.y.| ^2)) - (((|.x.| ^2) - (2 * |(y,x)|)) + (|.y.| ^2)) by A1, Th12 .= 4 * |(x,y)| ; hence (|.(x + y).| ^2) - (|.(x - y).| ^2) = 4 * |(x,y)| ; ::_thesis: verum end; theorem Th15: :: EUCLID_2:15 for x, y being real-valued FinSequence st len x = len y holds abs |(x,y)| <= |.x.| * |.y.| proof let x, y be real-valued FinSequence; ::_thesis: ( len x = len y implies abs |(x,y)| <= |.x.| * |.y.| ) assume A1: len x = len y ; ::_thesis: abs |(x,y)| <= |.x.| * |.y.| A2: ( x = 0* (len x) implies abs |(x,y)| <= (sqrt |(x,x)|) * (sqrt |(y,y)|) ) proof assume x = 0* (len x) ; ::_thesis: abs |(x,y)| <= (sqrt |(x,x)|) * (sqrt |(y,y)|) then ( |(x,y)| = 0 & |(x,x)| = 0 ) by A1, Th9; hence abs |(x,y)| <= (sqrt |(x,x)|) * (sqrt |(y,y)|) by ABSVALUE:2, SQUARE_1:17; ::_thesis: verum end; A3: ( x <> 0* (len x) implies abs |(x,y)| <= (sqrt |(x,x)|) * (sqrt |(y,y)|) ) proof A4: for t being real number holds ((|(x,x)| * (t ^2)) + ((2 * |(x,y)|) * t)) + |(y,y)| >= 0 proof let t be real number ; ::_thesis: ((|(x,x)| * (t ^2)) + ((2 * |(x,y)|) * t)) + |(y,y)| >= 0 set s = t ^2 ; A5: len (t * x) = len x by RVSUM_1:117; |(((t * x) + y),((t * x) + y))| >= 0 by RVSUM_1:119; then (|((t * x),(t * x))| + (2 * |((t * x),y)|)) + |(y,y)| >= 0 by A1, A5, RVSUM_1:128; then ((t * |((t * x),x)|) + (2 * |((t * x),y)|)) + |(y,y)| >= 0 by A5, RVSUM_1:121; then ((t * (t * |(x,x)|)) + (2 * |((t * x),y)|)) + |(y,y)| >= 0 by A1, RVSUM_1:121; then ((|(x,x)| * (t ^2)) + (2 * (|(x,y)| * t))) + |(y,y)| >= 0 by A1, RVSUM_1:121; hence ((|(x,x)| * (t ^2)) + ((2 * |(x,y)|) * t)) + |(y,y)| >= 0 ; ::_thesis: verum end; set w = abs |(x,y)|; set u = |(x,y)|; A6: |(x,x)| >= 0 by RVSUM_1:119; assume x <> 0* (len x) ; ::_thesis: abs |(x,y)| <= (sqrt |(x,x)|) * (sqrt |(y,y)|) then |(x,x)| <> 0 by Th7; then |(x,x)| > 0 by A6, XXREAL_0:1; then delta (|(x,x)|,(2 * |(x,y)|),|(y,y)|) <= 0 by A4, QUIN_1:10; then ((2 * |(x,y)|) ^2) - ((4 * |(x,x)|) * |(y,y)|) <= 0 by QUIN_1:def_1; then 4 * ((|(x,y)| ^2) - (|(x,x)| * |(y,y)|)) <= 0 ; then (|(x,y)| ^2) - (|(x,x)| * |(y,y)|) <= 0 / 4 by XREAL_1:77; then |(x,y)| ^2 <= |(x,x)| * |(y,y)| by XREAL_1:50; then ( 0 <= (abs |(x,y)|) ^2 & (abs |(x,y)|) ^2 <= |(x,x)| * |(y,y)| ) by COMPLEX1:75, XREAL_1:63; then sqrt ((abs |(x,y)|) ^2) <= sqrt (|(x,x)| * |(y,y)|) by SQUARE_1:26; then A7: abs |(x,y)| <= sqrt (|(x,x)| * |(y,y)|) by COMPLEX1:46, SQUARE_1:22; |(y,y)| >= 0 by RVSUM_1:119; hence abs |(x,y)| <= (sqrt |(x,x)|) * (sqrt |(y,y)|) by A6, A7, SQUARE_1:29; ::_thesis: verum end; sqrt |(x,x)| = |.x.| by Th5; hence abs |(x,y)| <= |.x.| * |.y.| by A2, A3, Th5; ::_thesis: verum end; theorem Th16: :: EUCLID_2:16 for x, y being real-valued FinSequence st len x = len y holds |.(x + y).| <= |.x.| + |.y.| proof let x, y be real-valued FinSequence; ::_thesis: ( len x = len y implies |.(x + y).| <= |.x.| + |.y.| ) assume A1: len x = len y ; ::_thesis: |.(x + y).| <= |.x.| + |.y.| then ( |(x,y)| <= abs |(x,y)| & abs |(x,y)| <= |.x.| * |.y.| ) by Th15, ABSVALUE:4; then |(x,y)| <= |.x.| * |.y.| by XXREAL_0:2; then 2 * |(x,y)| <= 2 * (|.x.| * |.y.|) by XREAL_1:64; then A2: (|.x.| ^2) + (2 * |(x,y)|) <= (|.x.| ^2) + (2 * (|.x.| * |.y.|)) by XREAL_1:7; |.(x + y).| ^2 = ((|.x.| ^2) + (2 * |(y,x)|)) + (|.y.| ^2) by A1, Th11; then A3: |.(x + y).| ^2 <= ((|.x.| ^2) + ((2 * |.x.|) * |.y.|)) + (|.y.| ^2) by A2, XREAL_1:7; 0 <= |.(x + y).| ^2 by XREAL_1:63; then sqrt (|.(x + y).| ^2) <= sqrt ((|.x.| + |.y.|) ^2) by A3, SQUARE_1:26; then A4: |.(x + y).| <= sqrt ((|.x.| + |.y.|) ^2) by Th6, SQUARE_1:22; ( 0 <= |.x.| & 0 <= |.y.| ) by Th6; then 0 + 0 <= |.x.| + |.y.| by XREAL_1:7; hence |.(x + y).| <= |.x.| + |.y.| by A4, SQUARE_1:22; ::_thesis: verum end; begin theorem :: EUCLID_2:17 for n being Nat for p1, p2 being Point of (TOP-REAL n) holds |(p1,p2)| = (1 / 4) * ((|.(p1 + p2).| ^2) - (|.(p1 - p2).| ^2)) proof let n be Nat; ::_thesis: for p1, p2 being Point of (TOP-REAL n) holds |(p1,p2)| = (1 / 4) * ((|.(p1 + p2).| ^2) - (|.(p1 - p2).| ^2)) let p1, p2 be Point of (TOP-REAL n); ::_thesis: |(p1,p2)| = (1 / 4) * ((|.(p1 + p2).| ^2) - (|.(p1 - p2).| ^2)) reconsider q1 = p1, q2 = p2 as Element of REAL n by EUCLID:22; thus |(p1,p2)| = (1 / 4) * ((|.(q1 + q2).| ^2) - (|.(q1 - q2).| ^2)) by Th3 .= (1 / 4) * ((|.(p1 + p2).| ^2) - (|.(p1 - p2).| ^2)) ; ::_thesis: verum end; theorem Th18: :: EUCLID_2:18 for n being Nat for p1, p2, p3 being Point of (TOP-REAL n) holds |((p1 + p2),p3)| = |(p1,p3)| + |(p2,p3)| proof let n be Nat; ::_thesis: for p1, p2, p3 being Point of (TOP-REAL n) holds |((p1 + p2),p3)| = |(p1,p3)| + |(p2,p3)| let p1, p2, p3 be Point of (TOP-REAL n); ::_thesis: |((p1 + p2),p3)| = |(p1,p3)| + |(p2,p3)| reconsider f1 = p1, f2 = p2, f3 = p3 as FinSequence of REAL by EUCLID:24; reconsider q1 = p1, q2 = p2 as Element of REAL n by EUCLID:22; len f2 = n by CARD_1:def_7; then A1: ( len f1 = len f2 & len f2 = len f3 ) by CARD_1:def_7; thus |((p1 + p2),p3)| = |(p1,p3)| + |(p2,p3)| by A1, RVSUM_1:120; ::_thesis: verum end; theorem Th19: :: EUCLID_2:19 for n being Nat for p1, p2 being Point of (TOP-REAL n) for x being real number holds |((x * p1),p2)| = x * |(p1,p2)| proof let n be Nat; ::_thesis: for p1, p2 being Point of (TOP-REAL n) for x being real number holds |((x * p1),p2)| = x * |(p1,p2)| let p1, p2 be Point of (TOP-REAL n); ::_thesis: for x being real number holds |((x * p1),p2)| = x * |(p1,p2)| let x be real number ; ::_thesis: |((x * p1),p2)| = x * |(p1,p2)| reconsider f1 = p1, f2 = p2 as FinSequence of REAL by EUCLID:24; reconsider q1 = p1 as Element of REAL n by EUCLID:22; ( len f1 = n & len f2 = n ) by CARD_1:def_7; hence |((x * p1),p2)| = x * |(p1,p2)| by RVSUM_1:121; ::_thesis: verum end; theorem :: EUCLID_2:20 for n being Nat for p1, p2 being Point of (TOP-REAL n) for x being real number holds |(p1,(x * p2))| = x * |(p1,p2)| by Th19; theorem Th21: :: EUCLID_2:21 for n being Nat for p1, p2 being Point of (TOP-REAL n) holds |((- p1),p2)| = - |(p1,p2)| proof let n be Nat; ::_thesis: for p1, p2 being Point of (TOP-REAL n) holds |((- p1),p2)| = - |(p1,p2)| let p1, p2 be Point of (TOP-REAL n); ::_thesis: |((- p1),p2)| = - |(p1,p2)| |((- p1),p2)| = |(((- 1) * p1),p2)| .= (- 1) * |(p1,p2)| by Th19 ; hence |((- p1),p2)| = - |(p1,p2)| ; ::_thesis: verum end; theorem :: EUCLID_2:22 for n being Nat for p1, p2 being Point of (TOP-REAL n) holds |(p1,(- p2))| = - |(p1,p2)| by Th21; theorem :: EUCLID_2:23 for n being Nat for p1, p2 being Point of (TOP-REAL n) holds |((- p1),(- p2))| = |(p1,p2)| proof let n be Nat; ::_thesis: for p1, p2 being Point of (TOP-REAL n) holds |((- p1),(- p2))| = |(p1,p2)| let p1, p2 be Point of (TOP-REAL n); ::_thesis: |((- p1),(- p2))| = |(p1,p2)| |((- p1),(- p2))| = - |(p1,(- p2))| by Th21 .= - (- |(p1,p2)|) by Th21 ; hence |((- p1),(- p2))| = |(p1,p2)| ; ::_thesis: verum end; theorem Th24: :: EUCLID_2:24 for n being Nat for p1, p2, p3 being Point of (TOP-REAL n) holds |((p1 - p2),p3)| = |(p1,p3)| - |(p2,p3)| proof let n be Nat; ::_thesis: for p1, p2, p3 being Point of (TOP-REAL n) holds |((p1 - p2),p3)| = |(p1,p3)| - |(p2,p3)| let p1, p2, p3 be Point of (TOP-REAL n); ::_thesis: |((p1 - p2),p3)| = |(p1,p3)| - |(p2,p3)| |((p1 - p2),p3)| = |(p1,p3)| + |((- p2),p3)| by Th18 .= |(p1,p3)| + (- |(p2,p3)|) by Th21 ; hence |((p1 - p2),p3)| = |(p1,p3)| - |(p2,p3)| ; ::_thesis: verum end; theorem :: EUCLID_2:25 for n being Nat for x, y being real number for p1, p2, p3 being Point of (TOP-REAL n) holds |(((x * p1) + (y * p2)),p3)| = (x * |(p1,p3)|) + (y * |(p2,p3)|) proof let n be Nat; ::_thesis: for x, y being real number for p1, p2, p3 being Point of (TOP-REAL n) holds |(((x * p1) + (y * p2)),p3)| = (x * |(p1,p3)|) + (y * |(p2,p3)|) let x, y be real number ; ::_thesis: for p1, p2, p3 being Point of (TOP-REAL n) holds |(((x * p1) + (y * p2)),p3)| = (x * |(p1,p3)|) + (y * |(p2,p3)|) let p1, p2, p3 be Point of (TOP-REAL n); ::_thesis: |(((x * p1) + (y * p2)),p3)| = (x * |(p1,p3)|) + (y * |(p2,p3)|) |(((x * p1) + (y * p2)),p3)| = |((x * p1),p3)| + |((y * p2),p3)| by Th18 .= (x * |(p1,p3)|) + |((y * p2),p3)| by Th19 .= (x * |(p1,p3)|) + (y * |(p2,p3)|) by Th19 ; hence |(((x * p1) + (y * p2)),p3)| = (x * |(p1,p3)|) + (y * |(p2,p3)|) ; ::_thesis: verum end; theorem :: EUCLID_2:26 for n being Nat for p, q1, q2 being Point of (TOP-REAL n) holds |(p,(q1 + q2))| = |(p,q1)| + |(p,q2)| by Th18; theorem :: EUCLID_2:27 for n being Nat for p, q1, q2 being Point of (TOP-REAL n) holds |(p,(q1 - q2))| = |(p,q1)| - |(p,q2)| by Th24; theorem Th28: :: EUCLID_2:28 for n being Nat for p1, p2, q1, q2 being Point of (TOP-REAL n) holds |((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)| proof let n be Nat; ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL n) holds |((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)| let p1, p2, q1, q2 be Point of (TOP-REAL n); ::_thesis: |((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)| A1: ( |((p1 + p2),q1)| = |(p1,q1)| + |(p2,q1)| & |((p1 + p2),q2)| = |(p1,q2)| + |(p2,q2)| ) by Th18; |((p1 + p2),(q1 + q2))| = |((p1 + p2),q1)| + |((p1 + p2),q2)| by Th18 .= ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)| by A1 ; hence |((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)| ; ::_thesis: verum end; theorem Th29: :: EUCLID_2:29 for n being Nat for p1, p2, q1, q2 being Point of (TOP-REAL n) holds |((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)| proof let n be Nat; ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL n) holds |((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)| let p1, p2, q1, q2 be Point of (TOP-REAL n); ::_thesis: |((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)| A1: ( |(p1,(q1 - q2))| = |(p1,q1)| - |(p1,q2)| & |(p2,(q1 - q2))| = |(p2,q1)| - |(p2,q2)| ) by Th24; |((p1 - p2),(q1 - q2))| = |(p1,(q1 - q2))| - |(p2,(q1 - q2))| by Th24 .= ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)| by A1 ; hence |((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)| ; ::_thesis: verum end; theorem Th30: :: EUCLID_2:30 for n being Nat for p, q being Point of (TOP-REAL n) holds |((p + q),(p + q))| = (|(p,p)| + (2 * |(p,q)|)) + |(q,q)| proof let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n) holds |((p + q),(p + q))| = (|(p,p)| + (2 * |(p,q)|)) + |(q,q)| let p, q be Point of (TOP-REAL n); ::_thesis: |((p + q),(p + q))| = (|(p,p)| + (2 * |(p,q)|)) + |(q,q)| (|(p,p)| + |(p,q)|) + |(p,q)| = |(p,p)| + (2 * |(p,q)|) ; hence |((p + q),(p + q))| = (|(p,p)| + (2 * |(p,q)|)) + |(q,q)| by Th28; ::_thesis: verum end; theorem Th31: :: EUCLID_2:31 for n being Nat for p, q being Point of (TOP-REAL n) holds |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)| proof let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n) holds |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)| let p, q be Point of (TOP-REAL n); ::_thesis: |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)| |((p - q),(p - q))| = ((|(p,p)| - |(p,q)|) - |(p,q)|) + |(q,q)| by Th29 .= (|(p,p)| - (2 * |(p,q)|)) + |(q,q)| ; hence |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)| ; ::_thesis: verum end; theorem Th32: :: EUCLID_2:32 for n being Nat for p being Point of (TOP-REAL n) holds |(p,(0. (TOP-REAL n)))| = 0 proof let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) holds |(p,(0. (TOP-REAL n)))| = 0 let p be Point of (TOP-REAL n); ::_thesis: |(p,(0. (TOP-REAL n)))| = 0 reconsider f1 = p as FinSequence of REAL by EUCLID:24; len f1 = n by CARD_1:def_7; then 0* (len f1) = 0. (TOP-REAL n) by EUCLID:70; hence |(p,(0. (TOP-REAL n)))| = 0 by Th9; ::_thesis: verum end; theorem :: EUCLID_2:33 for n being Nat for p being Point of (TOP-REAL n) holds |((0. (TOP-REAL n)),p)| = 0 by Th32; theorem :: EUCLID_2:34 for n being Nat holds |((0. (TOP-REAL n)),(0. (TOP-REAL n)))| = 0 by Th32; theorem Th35: :: EUCLID_2:35 for n being Nat for p being Point of (TOP-REAL n) holds |(p,p)| >= 0 by RVSUM_1:119; theorem Th36: :: EUCLID_2:36 for n being Nat for p being Point of (TOP-REAL n) holds |(p,p)| = |.p.| ^2 by Th4; theorem Th37: :: EUCLID_2:37 for n being Nat for p being Point of (TOP-REAL n) holds |.p.| = sqrt |(p,p)| proof let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) holds |.p.| = sqrt |(p,p)| let p be Point of (TOP-REAL n); ::_thesis: |.p.| = sqrt |(p,p)| n in NAT by ORDINAL1:def_12; then |.p.| = sqrt (|.p.| ^2) by SQUARE_1:22, TOPRNS_1:25 .= sqrt |(p,p)| by Th36 ; hence |.p.| = sqrt |(p,p)| ; ::_thesis: verum end; theorem Th38: :: EUCLID_2:38 for n being Nat for p being Point of (TOP-REAL n) holds 0 <= |.p.| proof let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) holds 0 <= |.p.| let p be Point of (TOP-REAL n); ::_thesis: 0 <= |.p.| ( |.p.| = sqrt |(p,p)| & 0 <= |(p,p)| ) by Th35, Th37; hence 0 <= |.p.| by SQUARE_1:def_2; ::_thesis: verum end; theorem Th39: :: EUCLID_2:39 for n being Nat holds |.(0. (TOP-REAL n)).| = 0 proof let n be Nat; ::_thesis: |.(0. (TOP-REAL n)).| = 0 n in NAT by ORDINAL1:def_12; hence |.(0. (TOP-REAL n)).| = 0 by TOPRNS_1:23; ::_thesis: verum end; theorem Th40: :: EUCLID_2:40 for n being Nat for p being Point of (TOP-REAL n) holds ( |(p,p)| = 0 iff |.p.| = 0 ) proof let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) holds ( |(p,p)| = 0 iff |.p.| = 0 ) let p be Point of (TOP-REAL n); ::_thesis: ( |(p,p)| = 0 iff |.p.| = 0 ) A1: ( |(p,p)| = 0 ^2 implies |.p.| = 0 ) proof assume |(p,p)| = 0 ^2 ; ::_thesis: |.p.| = 0 then |.p.| ^2 = 0 by Th36; hence |.p.| = 0 by XCMPLX_1:6; ::_thesis: verum end; ( |.p.| = 0 implies |(p,p)| = 0 ^2 ) by Th36; hence ( |(p,p)| = 0 iff |.p.| = 0 ) by A1; ::_thesis: verum end; theorem Th41: :: EUCLID_2:41 for n being Nat for p being Point of (TOP-REAL n) holds ( |(p,p)| = 0 iff p = 0. (TOP-REAL n) ) proof let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) holds ( |(p,p)| = 0 iff p = 0. (TOP-REAL n) ) let p be Point of (TOP-REAL n); ::_thesis: ( |(p,p)| = 0 iff p = 0. (TOP-REAL n) ) ( |(p,p)| = 0 implies p = 0. (TOP-REAL n) ) proof assume |(p,p)| = 0 ; ::_thesis: p = 0. (TOP-REAL n) then ( n in NAT & |.p.| = 0 ) by Th40, ORDINAL1:def_12; hence p = 0. (TOP-REAL n) by TOPRNS_1:24; ::_thesis: verum end; hence ( |(p,p)| = 0 iff p = 0. (TOP-REAL n) ) by Th32; ::_thesis: verum end; theorem :: EUCLID_2:42 for n being Nat for p being Point of (TOP-REAL n) holds ( |.p.| = 0 iff p = 0. (TOP-REAL n) ) proof let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) holds ( |.p.| = 0 iff p = 0. (TOP-REAL n) ) let p be Point of (TOP-REAL n); ::_thesis: ( |.p.| = 0 iff p = 0. (TOP-REAL n) ) n in NAT by ORDINAL1:def_12; hence ( |.p.| = 0 iff p = 0. (TOP-REAL n) ) by Th39, TOPRNS_1:24; ::_thesis: verum end; theorem :: EUCLID_2:43 for n being Nat for p being Point of (TOP-REAL n) holds ( p <> 0. (TOP-REAL n) iff |(p,p)| > 0 ) proof let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) holds ( p <> 0. (TOP-REAL n) iff |(p,p)| > 0 ) let p be Point of (TOP-REAL n); ::_thesis: ( p <> 0. (TOP-REAL n) iff |(p,p)| > 0 ) ( p <> 0. (TOP-REAL n) implies |(p,p)| > 0 ) proof assume p <> 0. (TOP-REAL n) ; ::_thesis: |(p,p)| > 0 then A1: |(p,p)| <> 0 by Th41; 0 <= |(p,p)| by Th35; hence |(p,p)| > 0 by A1, XXREAL_0:1; ::_thesis: verum end; hence ( p <> 0. (TOP-REAL n) iff |(p,p)| > 0 ) by Th41; ::_thesis: verum end; theorem :: EUCLID_2:44 for n being Nat for p being Point of (TOP-REAL n) holds ( p <> 0. (TOP-REAL n) iff |.p.| > 0 ) proof let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) holds ( p <> 0. (TOP-REAL n) iff |.p.| > 0 ) let p be Point of (TOP-REAL n); ::_thesis: ( p <> 0. (TOP-REAL n) iff |.p.| > 0 ) ( p <> 0. (TOP-REAL n) implies |.p.| > 0 ) proof assume A1: p <> 0. (TOP-REAL n) ; ::_thesis: |.p.| > 0 ( n in NAT & 0 <= |.p.| ) by Th38, ORDINAL1:def_12; hence |.p.| > 0 by A1, TOPRNS_1:24, XXREAL_0:1; ::_thesis: verum end; hence ( p <> 0. (TOP-REAL n) iff |.p.| > 0 ) by Th39; ::_thesis: verum end; theorem Th45: :: EUCLID_2:45 for n being Nat for p, q being Point of (TOP-REAL n) holds |.(p + q).| ^2 = ((|.p.| ^2) + (2 * |(q,p)|)) + (|.q.| ^2) proof let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n) holds |.(p + q).| ^2 = ((|.p.| ^2) + (2 * |(q,p)|)) + (|.q.| ^2) let p, q be Point of (TOP-REAL n); ::_thesis: |.(p + q).| ^2 = ((|.p.| ^2) + (2 * |(q,p)|)) + (|.q.| ^2) |.(p + q).| ^2 = |((p + q),(p + q))| by Th36 .= (|(p,p)| + (2 * |(q,p)|)) + |(q,q)| by Th30 .= ((|.p.| ^2) + (2 * |(q,p)|)) + |(q,q)| by Th36 .= ((|.p.| ^2) + (2 * |(q,p)|)) + (|.q.| ^2) by Th36 ; hence |.(p + q).| ^2 = ((|.p.| ^2) + (2 * |(q,p)|)) + (|.q.| ^2) ; ::_thesis: verum end; theorem Th46: :: EUCLID_2:46 for n being Nat for p, q being Point of (TOP-REAL n) holds |.(p - q).| ^2 = ((|.p.| ^2) - (2 * |(q,p)|)) + (|.q.| ^2) proof let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n) holds |.(p - q).| ^2 = ((|.p.| ^2) - (2 * |(q,p)|)) + (|.q.| ^2) let p, q be Point of (TOP-REAL n); ::_thesis: |.(p - q).| ^2 = ((|.p.| ^2) - (2 * |(q,p)|)) + (|.q.| ^2) |.(p - q).| ^2 = |((p - q),(p - q))| by Th36 .= (|(p,p)| - (2 * |(q,p)|)) + |(q,q)| by Th31 .= ((|.p.| ^2) - (2 * |(q,p)|)) + |(q,q)| by Th36 .= ((|.p.| ^2) - (2 * |(q,p)|)) + (|.q.| ^2) by Th36 ; hence |.(p - q).| ^2 = ((|.p.| ^2) - (2 * |(q,p)|)) + (|.q.| ^2) ; ::_thesis: verum end; theorem :: EUCLID_2:47 for n being Nat for p, q being Point of (TOP-REAL n) holds (|.(p + q).| ^2) + (|.(p - q).| ^2) = 2 * ((|.p.| ^2) + (|.q.| ^2)) proof let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n) holds (|.(p + q).| ^2) + (|.(p - q).| ^2) = 2 * ((|.p.| ^2) + (|.q.| ^2)) let p, q be Point of (TOP-REAL n); ::_thesis: (|.(p + q).| ^2) + (|.(p - q).| ^2) = 2 * ((|.p.| ^2) + (|.q.| ^2)) A1: ((|.p.| ^2) - (2 * |(p,q)|)) + (|.q.| ^2) = ((|.p.| ^2) + (|.q.| ^2)) - (2 * |(p,q)|) ; (|.(p + q).| ^2) + (|.(p - q).| ^2) = (((|.p.| ^2) + (2 * |(p,q)|)) + (|.q.| ^2)) + (|.(p - q).| ^2) by Th45 .= (((|.p.| ^2) + (|.q.| ^2)) + (2 * |(p,q)|)) + (((|.p.| ^2) + (|.q.| ^2)) - (2 * |(p,q)|)) by A1, Th46 .= 2 * ((|.p.| ^2) + (|.q.| ^2)) ; hence (|.(p + q).| ^2) + (|.(p - q).| ^2) = 2 * ((|.p.| ^2) + (|.q.| ^2)) ; ::_thesis: verum end; theorem :: EUCLID_2:48 for n being Nat for p, q being Point of (TOP-REAL n) holds (|.(p + q).| ^2) - (|.(p - q).| ^2) = 4 * |(p,q)| proof let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n) holds (|.(p + q).| ^2) - (|.(p - q).| ^2) = 4 * |(p,q)| let p, q be Point of (TOP-REAL n); ::_thesis: (|.(p + q).| ^2) - (|.(p - q).| ^2) = 4 * |(p,q)| (|.(p + q).| ^2) - (|.(p - q).| ^2) = (((|.p.| ^2) + (2 * |(p,q)|)) + (|.q.| ^2)) - (|.(p - q).| ^2) by Th45 .= (((|.p.| ^2) + (2 * |(p,q)|)) + (|.q.| ^2)) - (((|.p.| ^2) - (2 * |(p,q)|)) + (|.q.| ^2)) by Th46 .= 4 * |(p,q)| ; hence (|.(p + q).| ^2) - (|.(p - q).| ^2) = 4 * |(p,q)| ; ::_thesis: verum end; theorem :: EUCLID_2:49 for n being Nat for p, q being Point of (TOP-REAL n) holds |(p,q)| = (1 / 4) * ((|.(p + q).| ^2) - (|.(p - q).| ^2)) proof let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n) holds |(p,q)| = (1 / 4) * ((|.(p + q).| ^2) - (|.(p - q).| ^2)) let p, q be Point of (TOP-REAL n); ::_thesis: |(p,q)| = (1 / 4) * ((|.(p + q).| ^2) - (|.(p - q).| ^2)) (|.(p + q).| ^2) - (|.(p - q).| ^2) = (((|.p.| ^2) + (2 * |(p,q)|)) + (|.q.| ^2)) - (|.(p - q).| ^2) by Th45 .= (((|.p.| ^2) + (2 * |(p,q)|)) + (|.q.| ^2)) - (((|.p.| ^2) - (2 * |(p,q)|)) + (|.q.| ^2)) by Th46 .= 4 * |(p,q)| ; hence |(p,q)| = (1 / 4) * ((|.(p + q).| ^2) - (|.(p - q).| ^2)) ; ::_thesis: verum end; theorem :: EUCLID_2:50 for n being Nat for p, q being Point of (TOP-REAL n) holds |(p,q)| <= |(p,p)| + |(q,q)| proof let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n) holds |(p,q)| <= |(p,p)| + |(q,q)| let p, q be Point of (TOP-REAL n); ::_thesis: |(p,q)| <= |(p,p)| + |(q,q)| ( 0 <= |(p,p)| & 0 <= |(q,q)| ) by Th35; then 0 + 0 <= |(p,p)| + |(q,q)| by XREAL_1:7; then A1: 0 / 2 <= (|(p,p)| + |(q,q)|) / 2 by XREAL_1:72; |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)| by Th31 .= (|(p,p)| + |(q,q)|) - (2 * |(p,q)|) ; then 2 * |(p,q)| <= (|(p,p)| + |(q,q)|) - 0 by Th35, XREAL_1:11; then (2 * |(p,q)|) / 2 <= (|(p,p)| + |(q,q)|) / 2 by XREAL_1:72; then 0 + |(p,q)| <= ((|(p,p)| + |(q,q)|) / 2) + ((|(p,p)| + |(q,q)|) / 2) by A1, XREAL_1:7; hence |(p,q)| <= |(p,p)| + |(q,q)| ; ::_thesis: verum end; theorem :: EUCLID_2:51 for n being Nat for p, q being Point of (TOP-REAL n) holds abs |(p,q)| <= |.p.| * |.q.| proof let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n) holds abs |(p,q)| <= |.p.| * |.q.| let p, q be Point of (TOP-REAL n); ::_thesis: abs |(p,q)| <= |.p.| * |.q.| ( len p = n & len q = n ) by CARD_1:def_7; hence abs |(p,q)| <= |.p.| * |.q.| by Th15; ::_thesis: verum end; theorem :: EUCLID_2:52 for n being Nat for p, q being Point of (TOP-REAL n) holds |.(p + q).| <= |.p.| + |.q.| proof let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n) holds |.(p + q).| <= |.p.| + |.q.| let p, q be Point of (TOP-REAL n); ::_thesis: |.(p + q).| <= |.p.| + |.q.| A1: ( len p = n & len q = n ) by CARD_1:def_7; thus |.(p + q).| <= |.p.| + |.q.| by A1, Th16; ::_thesis: verum end; theorem Th53: :: EUCLID_2:53 for n being Nat for p being Point of (TOP-REAL n) holds p, 0. (TOP-REAL n) are_orthogonal proof let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) holds p, 0. (TOP-REAL n) are_orthogonal let p be Point of (TOP-REAL n); ::_thesis: p, 0. (TOP-REAL n) are_orthogonal |(p,(0. (TOP-REAL n)))| = 0 by Th32; hence p, 0. (TOP-REAL n) are_orthogonal by RVSUM_1:def_17; ::_thesis: verum end; theorem :: EUCLID_2:54 for n being Nat for p being Point of (TOP-REAL n) holds 0. (TOP-REAL n),p are_orthogonal by Th53; theorem Th55: :: EUCLID_2:55 for n being Nat for p being Point of (TOP-REAL n) holds ( p,p are_orthogonal iff p = 0. (TOP-REAL n) ) proof let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) holds ( p,p are_orthogonal iff p = 0. (TOP-REAL n) ) let p be Point of (TOP-REAL n); ::_thesis: ( p,p are_orthogonal iff p = 0. (TOP-REAL n) ) ( p,p are_orthogonal iff |(p,p)| = 0 ) by RVSUM_1:def_17; hence ( p,p are_orthogonal iff p = 0. (TOP-REAL n) ) by Th41; ::_thesis: verum end; theorem Th56: :: EUCLID_2:56 for n being Nat for a being real number for p, q being Point of (TOP-REAL n) st p,q are_orthogonal holds a * p,q are_orthogonal proof let n be Nat; ::_thesis: for a being real number for p, q being Point of (TOP-REAL n) st p,q are_orthogonal holds a * p,q are_orthogonal let a be real number ; ::_thesis: for p, q being Point of (TOP-REAL n) st p,q are_orthogonal holds a * p,q are_orthogonal let p, q be Point of (TOP-REAL n); ::_thesis: ( p,q are_orthogonal implies a * p,q are_orthogonal ) assume p,q are_orthogonal ; ::_thesis: a * p,q are_orthogonal then |(p,q)| = 0 by RVSUM_1:def_17; then a * |(p,q)| = 0 ; then |((a * p),q)| = 0 by Th19; hence a * p,q are_orthogonal by RVSUM_1:def_17; ::_thesis: verum end; theorem :: EUCLID_2:57 for n being Nat for a being real number for p, q being Point of (TOP-REAL n) st p,q are_orthogonal holds p,a * q are_orthogonal by Th56; theorem :: EUCLID_2:58 for n being Nat for p being Point of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) holds p,q are_orthogonal ) holds p = 0. (TOP-REAL n) proof let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) holds p,q are_orthogonal ) holds p = 0. (TOP-REAL n) let p be Point of (TOP-REAL n); ::_thesis: ( ( for q being Point of (TOP-REAL n) holds p,q are_orthogonal ) implies p = 0. (TOP-REAL n) ) assume for q being Point of (TOP-REAL n) holds p,q are_orthogonal ; ::_thesis: p = 0. (TOP-REAL n) then p,p are_orthogonal ; hence p = 0. (TOP-REAL n) by Th55; ::_thesis: verum end;