:: EUCLID_5 semantic presentation begin theorem Th1: :: EUCLID_5:1 for p being Point of (TOP-REAL 3) ex x, y, z being Real st p = <*x,y,z*> proof let p be Point of (TOP-REAL 3); ::_thesis: ex x, y, z being Real st p = <*x,y,z*> the carrier of (TOP-REAL 3) = REAL 3 by EUCLID:22; then p is Element of 3 -tuples_on REAL by EUCLID:def_1; then p in 3 -tuples_on REAL ; then reconsider p = p as Tuple of 3, REAL by FINSEQ_2:131; ex x, y, z being Real st p = <*x,y,z*> by FINSEQ_2:103; hence ex x, y, z being Real st p = <*x,y,z*> ; ::_thesis: verum end; definition let p be Point of (TOP-REAL 3); funcp `1 -> Real equals :: EUCLID_5:def 1 p . 1; coherence p . 1 is Real ; funcp `2 -> Real equals :: EUCLID_5:def 2 p . 2; coherence p . 2 is Real ; funcp `3 -> Real equals :: EUCLID_5:def 3 p . 3; coherence p . 3 is Real ; end; :: deftheorem defines `1 EUCLID_5:def_1_:_ for p being Point of (TOP-REAL 3) holds p `1 = p . 1; :: deftheorem defines `2 EUCLID_5:def_2_:_ for p being Point of (TOP-REAL 3) holds p `2 = p . 2; :: deftheorem defines `3 EUCLID_5:def_3_:_ for p being Point of (TOP-REAL 3) holds p `3 = p . 3; notation let x, y, z be real number ; synonym |[x,y,z]| for <*x,y,z*>; end; definition let x, y, z be real number ; :: original: |[ redefine func|[x,y,z]| -> Point of (TOP-REAL 3); coherence |[x,y,z]| is Point of (TOP-REAL 3) proof reconsider x = x, y = y, z = z as Real by XREAL_0:def_1; <*x,y,z*> is Element of 3 -tuples_on REAL by FINSEQ_2:104; then <*x,y,z*> is Element of REAL 3 by EUCLID:def_1; hence |[x,y,z]| is Point of (TOP-REAL 3) by EUCLID:22; ::_thesis: verum end; end; theorem :: EUCLID_5:2 for x, y, z being Real holds ( |[x,y,z]| `1 = x & |[x,y,z]| `2 = y & |[x,y,z]| `3 = z ) by FINSEQ_1:45; theorem Th3: :: EUCLID_5:3 for p being Point of (TOP-REAL 3) holds p = |[(p `1),(p `2),(p `3)]| proof let p be Point of (TOP-REAL 3); ::_thesis: p = |[(p `1),(p `2),(p `3)]| consider x, y, z being Real such that A1: p = <*x,y,z*> by Th1; ( p `1 = x & p `2 = y ) by A1, FINSEQ_1:45; hence p = |[(p `1),(p `2),(p `3)]| by A1, FINSEQ_1:45; ::_thesis: verum end; theorem Th4: :: EUCLID_5:4 0. (TOP-REAL 3) = |[0,0,0]| proof 0. (TOP-REAL 3) = 0* 3 by EUCLID:70 .= 3 |-> 0 by EUCLID:def_4 .= <*0,0,0*> by FINSEQ_2:62 ; hence 0. (TOP-REAL 3) = |[0,0,0]| ; ::_thesis: verum end; theorem Th5: :: EUCLID_5:5 for p1, p2 being Point of (TOP-REAL 3) holds p1 + p2 = |[((p1 `1) + (p2 `1)),((p1 `2) + (p2 `2)),((p1 `3) + (p2 `3))]| proof let p1, p2 be Point of (TOP-REAL 3); ::_thesis: p1 + p2 = |[((p1 `1) + (p2 `1)),((p1 `2) + (p2 `2)),((p1 `3) + (p2 `3))]| reconsider p19 = p1, p29 = p2 as Element of REAL 3 by EUCLID:22; len (p19 + p29) = 3 by CARD_1:def_7; then A1: dom (p19 + p29) = Seg 3 by FINSEQ_1:def_3; then 2 in dom (p19 + p29) by FINSEQ_1:1; then (p19 + p29) . 2 = (p19 . 2) + (p29 . 2) by VALUED_1:def_1; then A2: (p1 + p2) `2 = (p1 `2) + (p2 `2) ; 3 in dom (p19 + p29) by A1, FINSEQ_1:1; then (p19 + p29) . 3 = (p19 . 3) + (p29 . 3) by VALUED_1:def_1; then A3: (p1 + p2) `3 = (p1 `3) + (p2 `3) ; 1 in dom (p19 + p29) by A1, FINSEQ_1:1; then (p19 + p29) . 1 = (p19 . 1) + (p29 . 1) by VALUED_1:def_1; then (p1 + p2) `1 = (p1 `1) + (p2 `1) ; hence p1 + p2 = |[((p1 `1) + (p2 `1)),((p1 `2) + (p2 `2)),((p1 `3) + (p2 `3))]| by A2, A3, Th3; ::_thesis: verum end; theorem Th6: :: EUCLID_5:6 for x1, y1, z1, x2, y2, z2 being Real holds |[x1,y1,z1]| + |[x2,y2,z2]| = |[(x1 + x2),(y1 + y2),(z1 + z2)]| proof let x1, y1, z1, x2, y2, z2 be Real; ::_thesis: |[x1,y1,z1]| + |[x2,y2,z2]| = |[(x1 + x2),(y1 + y2),(z1 + z2)]| A1: ( |[x1,y1,z1]| `3 = z1 & |[x2,y2,z2]| `1 = x2 ) by FINSEQ_1:45; A2: ( |[x2,y2,z2]| `2 = y2 & |[x2,y2,z2]| `3 = z2 ) by FINSEQ_1:45; ( |[x1,y1,z1]| `1 = x1 & |[x1,y1,z1]| `2 = y1 ) by FINSEQ_1:45; hence |[x1,y1,z1]| + |[x2,y2,z2]| = |[(x1 + x2),(y1 + y2),(z1 + z2)]| by A1, A2, Th5; ::_thesis: verum end; theorem Th7: :: EUCLID_5:7 for x being Real for p being Point of (TOP-REAL 3) holds x * p = |[(x * (p `1)),(x * (p `2)),(x * (p `3))]| proof let x be Real; ::_thesis: for p being Point of (TOP-REAL 3) holds x * p = |[(x * (p `1)),(x * (p `2)),(x * (p `3))]| let p be Point of (TOP-REAL 3); ::_thesis: x * p = |[(x * (p `1)),(x * (p `2)),(x * (p `3))]| reconsider q = p as Element of REAL 3 by EUCLID:22; (x * q) . 2 = x * (q . 2) by RVSUM_1:44; then A1: (x * p) `2 = x * (p `2) ; (x * q) . 3 = x * (q . 3) by RVSUM_1:44; then A2: (x * p) `3 = x * (p `3) ; (x * q) . 1 = x * (q . 1) by RVSUM_1:44; then (x * p) `1 = x * (p `1) ; hence x * p = |[(x * (p `1)),(x * (p `2)),(x * (p `3))]| by A1, A2, Th3; ::_thesis: verum end; theorem Th8: :: EUCLID_5:8 for x, x1, y1, z1 being Real holds x * |[x1,y1,z1]| = |[(x * x1),(x * y1),(x * z1)]| proof let x, x1, y1, z1 be Real; ::_thesis: x * |[x1,y1,z1]| = |[(x * x1),(x * y1),(x * z1)]| A1: |[x1,y1,z1]| `3 = z1 by FINSEQ_1:45; ( |[x1,y1,z1]| `1 = x1 & |[x1,y1,z1]| `2 = y1 ) by FINSEQ_1:45; hence x * |[x1,y1,z1]| = |[(x * x1),(x * y1),(x * z1)]| by A1, Th7; ::_thesis: verum end; theorem :: EUCLID_5:9 for x being Real for p being Point of (TOP-REAL 3) holds ( (x * p) `1 = x * (p `1) & (x * p) `2 = x * (p `2) & (x * p) `3 = x * (p `3) ) proof let x be Real; ::_thesis: for p being Point of (TOP-REAL 3) holds ( (x * p) `1 = x * (p `1) & (x * p) `2 = x * (p `2) & (x * p) `3 = x * (p `3) ) let p be Point of (TOP-REAL 3); ::_thesis: ( (x * p) `1 = x * (p `1) & (x * p) `2 = x * (p `2) & (x * p) `3 = x * (p `3) ) A1: (x * p) `3 = |[(x * (p `1)),(x * (p `2)),(x * (p `3))]| `3 by Th7; ( (x * p) `1 = |[(x * (p `1)),(x * (p `2)),(x * (p `3))]| `1 & (x * p) `2 = |[(x * (p `1)),(x * (p `2)),(x * (p `3))]| `2 ) by Th7; hence ( (x * p) `1 = x * (p `1) & (x * p) `2 = x * (p `2) & (x * p) `3 = x * (p `3) ) by A1, FINSEQ_1:45; ::_thesis: verum end; theorem Th10: :: EUCLID_5:10 for p being Point of (TOP-REAL 3) holds - p = |[(- (p `1)),(- (p `2)),(- (p `3))]| proof let p be Point of (TOP-REAL 3); ::_thesis: - p = |[(- (p `1)),(- (p `2)),(- (p `3))]| thus - p = (- 1) * p by EUCLID:39 .= |[((- 1) * (p `1)),((- 1) * (p `2)),((- 1) * (p `3))]| by Th7 .= |[(- (p `1)),(- (p `2)),(- (p `3))]| ; ::_thesis: verum end; theorem :: EUCLID_5:11 for x1, y1, z1 being Real holds - |[x1,y1,z1]| = |[(- x1),(- y1),(- z1)]| proof let x1, y1, z1 be Real; ::_thesis: - |[x1,y1,z1]| = |[(- x1),(- y1),(- z1)]| A1: |[x1,y1,z1]| `3 = z1 by FINSEQ_1:45; ( |[x1,y1,z1]| `1 = x1 & |[x1,y1,z1]| `2 = y1 ) by FINSEQ_1:45; hence - |[x1,y1,z1]| = |[(- x1),(- y1),(- z1)]| by A1, Th10; ::_thesis: verum end; theorem Th12: :: EUCLID_5:12 for p1, p2 being Point of (TOP-REAL 3) holds p1 - p2 = |[((p1 `1) - (p2 `1)),((p1 `2) - (p2 `2)),((p1 `3) - (p2 `3))]| proof let p1, p2 be Point of (TOP-REAL 3); ::_thesis: p1 - p2 = |[((p1 `1) - (p2 `1)),((p1 `2) - (p2 `2)),((p1 `3) - (p2 `3))]| A1: - p2 = |[(- (p2 `1)),(- (p2 `2)),(- (p2 `3))]| by Th10; then A2: (- p2) `3 = - (p2 `3) by FINSEQ_1:45; ( (- p2) `1 = - (p2 `1) & (- p2) `2 = - (p2 `2) ) by A1, FINSEQ_1:45; hence p1 - p2 = |[((p1 `1) + (- (p2 `1))),((p1 `2) + (- (p2 `2))),((p1 `3) + (- (p2 `3)))]| by A2, Th5 .= |[((p1 `1) - (p2 `1)),((p1 `2) - (p2 `2)),((p1 `3) - (p2 `3))]| ; ::_thesis: verum end; theorem Th13: :: EUCLID_5:13 for x1, y1, z1, x2, y2, z2 being Real holds |[x1,y1,z1]| - |[x2,y2,z2]| = |[(x1 - x2),(y1 - y2),(z1 - z2)]| proof let x1, y1, z1, x2, y2, z2 be Real; ::_thesis: |[x1,y1,z1]| - |[x2,y2,z2]| = |[(x1 - x2),(y1 - y2),(z1 - z2)]| A1: ( |[x1,y1,z1]| `3 = z1 & |[x2,y2,z2]| `1 = x2 ) by FINSEQ_1:45; A2: ( |[x2,y2,z2]| `2 = y2 & |[x2,y2,z2]| `3 = z2 ) by FINSEQ_1:45; ( |[x1,y1,z1]| `1 = x1 & |[x1,y1,z1]| `2 = y1 ) by FINSEQ_1:45; hence |[x1,y1,z1]| - |[x2,y2,z2]| = |[(x1 - x2),(y1 - y2),(z1 - z2)]| by A1, A2, Th12; ::_thesis: verum end; definition let p1, p2 be Point of (TOP-REAL 3); funcp1 p2 -> Point of (TOP-REAL 3) equals :: EUCLID_5:def 4 |[(((p1 `2) * (p2 `3)) - ((p1 `3) * (p2 `2))),(((p1 `3) * (p2 `1)) - ((p1 `1) * (p2 `3))),(((p1 `1) * (p2 `2)) - ((p1 `2) * (p2 `1)))]|; correctness coherence |[(((p1 `2) * (p2 `3)) - ((p1 `3) * (p2 `2))),(((p1 `3) * (p2 `1)) - ((p1 `1) * (p2 `3))),(((p1 `1) * (p2 `2)) - ((p1 `2) * (p2 `1)))]| is Point of (TOP-REAL 3); ; end; :: deftheorem defines EUCLID_5:def_4_:_ for p1, p2 being Point of (TOP-REAL 3) holds p1 p2 = |[(((p1 `2) * (p2 `3)) - ((p1 `3) * (p2 `2))),(((p1 `3) * (p2 `1)) - ((p1 `1) * (p2 `3))),(((p1 `1) * (p2 `2)) - ((p1 `2) * (p2 `1)))]|; theorem :: EUCLID_5:14 for x, y, z being Real for p being Point of (TOP-REAL 3) st p = |[x,y,z]| holds ( p `1 = x & p `2 = y & p `3 = z ) by FINSEQ_1:45; theorem Th15: :: EUCLID_5:15 for x1, y1, z1, x2, y2, z2 being Real holds |[x1,y1,z1]| |[x2,y2,z2]| = |[((y1 * z2) - (z1 * y2)),((z1 * x2) - (x1 * z2)),((x1 * y2) - (y1 * x2))]| proof let x1, y1, z1, x2, y2, z2 be Real; ::_thesis: |[x1,y1,z1]| |[x2,y2,z2]| = |[((y1 * z2) - (z1 * y2)),((z1 * x2) - (x1 * z2)),((x1 * y2) - (y1 * x2))]| consider p1 being Point of (TOP-REAL 3) such that A1: p1 = |[x1,y1,z1]| ; A2: p1 `3 = z1 by A1, FINSEQ_1:45; consider p2 being Point of (TOP-REAL 3) such that A3: p2 = |[x2,y2,z2]| ; A4: p2 `3 = z2 by A3, FINSEQ_1:45; A5: ( p2 `1 = x2 & p2 `2 = y2 ) by A3, FINSEQ_1:45; ( p1 `1 = x1 & p1 `2 = y1 ) by A1, FINSEQ_1:45; hence |[x1,y1,z1]| |[x2,y2,z2]| = |[((y1 * z2) - (z1 * y2)),((z1 * x2) - (x1 * z2)),((x1 * y2) - (y1 * x2))]| by A1, A2, A3, A5, A4; ::_thesis: verum end; theorem :: EUCLID_5:16 for x being Real for p1, p2 being Point of (TOP-REAL 3) holds ( (x * p1) p2 = x * (p1 p2) & (x * p1) p2 = p1 (x * p2) ) proof let x be Real; ::_thesis: for p1, p2 being Point of (TOP-REAL 3) holds ( (x * p1) p2 = x * (p1 p2) & (x * p1) p2 = p1 (x * p2) ) let p1, p2 be Point of (TOP-REAL 3); ::_thesis: ( (x * p1) p2 = x * (p1 p2) & (x * p1) p2 = p1 (x * p2) ) A1: (x * p1) p2 = |[(x * (p1 `1)),(x * (p1 `2)),(x * (p1 `3))]| p2 by Th7 .= |[(x * (p1 `1)),(x * (p1 `2)),(x * (p1 `3))]| |[(p2 `1),(p2 `2),(p2 `3)]| by Th3 .= |[(((x * (p1 `2)) * (p2 `3)) - ((x * (p1 `3)) * (p2 `2))),(((x * (p1 `3)) * (p2 `1)) - ((x * (p1 `1)) * (p2 `3))),(((x * (p1 `1)) * (p2 `2)) - ((x * (p1 `2)) * (p2 `1)))]| by Th15 ; then A2: (x * p1) p2 = |[(x * (((p1 `2) * (p2 `3)) - ((p1 `3) * (p2 `2)))),(x * (((p1 `3) * (p2 `1)) - ((p1 `1) * (p2 `3)))),(x * (((p1 `1) * (p2 `2)) - ((p1 `2) * (p2 `1))))]| .= x * (p1 p2) by Th8 ; (x * p1) p2 = |[(((p1 `2) * (x * (p2 `3))) - ((p1 `3) * (x * (p2 `2)))),(((p1 `3) * (x * (p2 `1))) - ((p1 `1) * (x * (p2 `3)))),(((p1 `1) * (x * (p2 `2))) - ((p1 `2) * (x * (p2 `1))))]| by A1 .= |[(p1 `1),(p1 `2),(p1 `3)]| |[(x * (p2 `1)),(x * (p2 `2)),(x * (p2 `3))]| by Th15 .= p1 |[(x * (p2 `1)),(x * (p2 `2)),(x * (p2 `3))]| by Th3 .= p1 (x * p2) by Th7 ; hence ( (x * p1) p2 = x * (p1 p2) & (x * p1) p2 = p1 (x * p2) ) by A2; ::_thesis: verum end; theorem Th17: :: EUCLID_5:17 for p1, p2 being Point of (TOP-REAL 3) holds p1 p2 = - (p2 p1) proof let p1, p2 be Point of (TOP-REAL 3); ::_thesis: p1 p2 = - (p2 p1) - (p2 p1) = (- 1) * (p2 p1) by EUCLID:39 .= |[((- 1) * (((p2 `2) * (p1 `3)) - ((p2 `3) * (p1 `2)))),((- 1) * (((p2 `3) * (p1 `1)) - ((p2 `1) * (p1 `3)))),((- 1) * (((p2 `1) * (p1 `2)) - ((p2 `2) * (p1 `1))))]| by Th8 .= p1 p2 ; hence p1 p2 = - (p2 p1) ; ::_thesis: verum end; theorem :: EUCLID_5:18 for p1, p2 being Point of (TOP-REAL 3) holds (- p1) p2 = p1 (- p2) proof let p1, p2 be Point of (TOP-REAL 3); ::_thesis: (- p1) p2 = p1 (- p2) (- p1) p2 = |[(- (p1 `1)),(- (p1 `2)),(- (p1 `3))]| p2 by Th10 .= |[(- (p1 `1)),(- (p1 `2)),(- (p1 `3))]| |[(p2 `1),(p2 `2),(p2 `3)]| by Th3 .= |[(((- (p1 `2)) * (p2 `3)) - ((- (p1 `3)) * (p2 `2))),(((- (p1 `3)) * (p2 `1)) - ((- (p1 `1)) * (p2 `3))),(((- (p1 `1)) * (p2 `2)) - ((- (p1 `2)) * (p2 `1)))]| by Th15 .= |[(((p1 `2) * (- (p2 `3))) - ((p1 `3) * (- (p2 `2)))),(((p1 `3) * (- (p2 `1))) - ((p1 `1) * (- (p2 `3)))),(((p1 `1) * (- (p2 `2))) - ((p1 `2) * (- (p2 `1))))]| .= |[(p1 `1),(p1 `2),(p1 `3)]| |[(- (p2 `1)),(- (p2 `2)),(- (p2 `3))]| by Th15 .= |[(p1 `1),(p1 `2),(p1 `3)]| (- p2) by Th10 ; hence (- p1) p2 = p1 (- p2) by Th3; ::_thesis: verum end; theorem :: EUCLID_5:19 for x, y, z being Real holds |[0,0,0]| |[x,y,z]| = 0. (TOP-REAL 3) proof let x, y, z be Real; ::_thesis: |[0,0,0]| |[x,y,z]| = 0. (TOP-REAL 3) |[0,0,0]| |[x,y,z]| = |[((0 * z) - (0 * y)),((0 * x) - (0 * z)),((0 * y) - (0 * x))]| by Th15 .= |[(0 * (z - y)),(0 * (x - z)),(0 * (y - x))]| .= 0 * |[(z - y),(x - z),(y - x)]| by Th8 ; hence |[0,0,0]| |[x,y,z]| = 0. (TOP-REAL 3) by EUCLID:29; ::_thesis: verum end; theorem :: EUCLID_5:20 for x1, x2 being Real holds |[x1,0,0]| |[x2,0,0]| = 0. (TOP-REAL 3) proof let x1, x2 be Real; ::_thesis: |[x1,0,0]| |[x2,0,0]| = 0. (TOP-REAL 3) |[x1,0,0]| |[x2,0,0]| = |[((0 * 0) - (0 * 0)),((0 * x2) - (x1 * 0)),((x1 * 0) - (0 * x2))]| by Th15 .= |[(0 * (0 - 0)),(0 * (x2 - x1)),(0 * (x1 - x2))]| .= 0 * |[(0 - 0),(x2 - x1),(x1 - x2)]| by Th8 .= 0. (TOP-REAL 3) by EUCLID:29 ; hence |[x1,0,0]| |[x2,0,0]| = 0. (TOP-REAL 3) ; ::_thesis: verum end; theorem :: EUCLID_5:21 for y1, y2 being Real holds |[0,y1,0]| |[0,y2,0]| = 0. (TOP-REAL 3) proof let y1, y2 be Real; ::_thesis: |[0,y1,0]| |[0,y2,0]| = 0. (TOP-REAL 3) |[0,y1,0]| |[0,y2,0]| = |[((y1 * 0) - (0 * y2)),((0 * 0) - (0 * 0)),((0 * y2) - (y1 * 0))]| by Th15 .= |[(0 * (y1 - y2)),(0 * (0 - 0)),(0 * (y2 - y1))]| .= 0 * |[(y1 - y2),(0 - 0),(y2 - y1)]| by Th8 .= 0. (TOP-REAL 3) by EUCLID:29 ; hence |[0,y1,0]| |[0,y2,0]| = 0. (TOP-REAL 3) ; ::_thesis: verum end; theorem :: EUCLID_5:22 for z1, z2 being Real holds |[0,0,z1]| |[0,0,z2]| = 0. (TOP-REAL 3) proof let z1, z2 be Real; ::_thesis: |[0,0,z1]| |[0,0,z2]| = 0. (TOP-REAL 3) |[0,0,z1]| |[0,0,z2]| = |[((0 * z2) - (z1 * 0)),((z1 * 0) - (0 * z2)),((0 * 0) - (0 * 0))]| by Th15 .= |[(0 * (z2 - z1)),(0 * (z1 - z2)),(0 * (0 * 0))]| .= 0 * |[(z2 - z1),(z1 - z2),(0 - 0)]| by Th8 .= 0. (TOP-REAL 3) by EUCLID:29 ; hence |[0,0,z1]| |[0,0,z2]| = 0. (TOP-REAL 3) ; ::_thesis: verum end; theorem Th23: :: EUCLID_5:23 for p1, p2, p3 being Point of (TOP-REAL 3) holds p1 (p2 + p3) = (p1 p2) + (p1 p3) proof let p1, p2, p3 be Point of (TOP-REAL 3); ::_thesis: p1 (p2 + p3) = (p1 p2) + (p1 p3) A1: (p1 p2) + (p1 p3) = |[((((p1 `2) * (p2 `3)) - ((p1 `3) * (p2 `2))) + (((p1 `2) * (p3 `3)) - ((p1 `3) * (p3 `2)))),((((p1 `3) * (p2 `1)) - ((p1 `1) * (p2 `3))) + (((p1 `3) * (p3 `1)) - ((p1 `1) * (p3 `3)))),((((p1 `1) * (p2 `2)) - ((p1 `2) * (p2 `1))) + (((p1 `1) * (p3 `2)) - ((p1 `2) * (p3 `1))))]| by Th6 .= |[(((((p1 `2) * (p2 `3)) - ((p1 `3) * (p2 `2))) + ((p1 `2) * (p3 `3))) - ((p1 `3) * (p3 `2))),(((((p1 `3) * (p2 `1)) - ((p1 `1) * (p2 `3))) + ((p1 `3) * (p3 `1))) - ((p1 `1) * (p3 `3))),(((((p1 `1) * (p2 `2)) - ((p1 `2) * (p2 `1))) + ((p1 `1) * (p3 `2))) - ((p1 `2) * (p3 `1)))]| ; A2: p2 + p3 = |[((p2 `1) + (p3 `1)),((p2 `2) + (p3 `2)),((p2 `3) + (p3 `3))]| by Th5; then A3: (p2 + p3) `3 = (p2 `3) + (p3 `3) by FINSEQ_1:45; ( (p2 + p3) `1 = (p2 `1) + (p3 `1) & (p2 + p3) `2 = (p2 `2) + (p3 `2) ) by A2, FINSEQ_1:45; hence p1 (p2 + p3) = (p1 p2) + (p1 p3) by A3, A1; ::_thesis: verum end; theorem Th24: :: EUCLID_5:24 for p1, p2, p3 being Point of (TOP-REAL 3) holds (p1 + p2) p3 = (p1 p3) + (p2 p3) proof let p1, p2, p3 be Point of (TOP-REAL 3); ::_thesis: (p1 + p2) p3 = (p1 p3) + (p2 p3) (p1 + p2) p3 = - (p3 (p1 + p2)) by Th17 .= - ((p3 p1) + (p3 p2)) by Th23 .= - ((p3 p1) - (p2 p3)) by Th17 .= (- (p3 p1)) + (p2 p3) by EUCLID:44 ; hence (p1 + p2) p3 = (p1 p3) + (p2 p3) by Th17; ::_thesis: verum end; theorem :: EUCLID_5:25 for p1 being Point of (TOP-REAL 3) holds p1 p1 = 0. (TOP-REAL 3) by Th4; theorem :: EUCLID_5:26 for p1, p2, p3, p4 being Point of (TOP-REAL 3) holds (p1 + p2) (p3 + p4) = (((p1 p3) + (p1 p4)) + (p2 p3)) + (p2 p4) proof let p1, p2, p3, p4 be Point of (TOP-REAL 3); ::_thesis: (p1 + p2) (p3 + p4) = (((p1 p3) + (p1 p4)) + (p2 p3)) + (p2 p4) (p1 + p2) (p3 + p4) = (p1 (p3 + p4)) + (p2 (p3 + p4)) by Th24 .= ((p1 p3) + (p1 p4)) + (p2 (p3 + p4)) by Th23 .= ((p1 p3) + (p1 p4)) + ((p2 p3) + (p2 p4)) by Th23 ; hence (p1 + p2) (p3 + p4) = (((p1 p3) + (p1 p4)) + (p2 p3)) + (p2 p4) by EUCLID:26; ::_thesis: verum end; theorem Th27: :: EUCLID_5:27 for p being Point of (TOP-REAL 3) holds p = <*(p `1),(p `2),(p `3)*> proof let p be Point of (TOP-REAL 3); ::_thesis: p = <*(p `1),(p `2),(p `3)*> reconsider f = p as FinSequence ; consider x, y, z being Element of REAL such that A1: p = <*x,y,z*> by Th1; <*x,y,z*> = <*(f . 1),y,z*> by A1, FINSEQ_1:45 .= <*(f . 1),(f . 2),z*> by A1, FINSEQ_1:45 .= <*(p `1),(p `2),(p `3)*> by A1, FINSEQ_1:45 ; hence p = <*(p `1),(p `2),(p `3)*> by A1; ::_thesis: verum end; theorem Th28: :: EUCLID_5:28 for f1, f2 being FinSequence of REAL st len f1 = 3 & len f2 = 3 holds mlt (f1,f2) = <*((f1 . 1) * (f2 . 1)),((f1 . 2) * (f2 . 2)),((f1 . 3) * (f2 . 3))*> proof let f1, f2 be FinSequence of REAL ; ::_thesis: ( len f1 = 3 & len f2 = 3 implies mlt (f1,f2) = <*((f1 . 1) * (f2 . 1)),((f1 . 2) * (f2 . 2)),((f1 . 3) * (f2 . 3))*> ) assume that A1: len f1 = 3 and A2: len f2 = 3 ; ::_thesis: mlt (f1,f2) = <*((f1 . 1) * (f2 . 1)),((f1 . 2) * (f2 . 2)),((f1 . 3) * (f2 . 3))*> A3: f2 = <*(f2 . 1),(f2 . 2),(f2 . 3)*> by A2, FINSEQ_1:45; mlt (f1,f2) = multreal .: (f1,f2) by RVSUM_1:def_9 .= multreal .: (<*(f1 . 1),(f1 . 2),(f1 . 3)*>,<*(f2 . 1),(f2 . 2),(f2 . 3)*>) by A1, A3, FINSEQ_1:45 .= <*(multreal . ((f1 . 1),(f2 . 1))),(multreal . ((f1 . 2),(f2 . 2))),(multreal . ((f1 . 3),(f2 . 3)))*> by FINSEQ_2:76 .= <*((f1 . 1) * (f2 . 1)),(multreal . ((f1 . 2),(f2 . 2))),(multreal . ((f1 . 3),(f2 . 3)))*> by BINOP_2:def_11 .= <*((f1 . 1) * (f2 . 1)),((f1 . 2) * (f2 . 2)),(multreal . ((f1 . 3),(f2 . 3)))*> by BINOP_2:def_11 ; hence mlt (f1,f2) = <*((f1 . 1) * (f2 . 1)),((f1 . 2) * (f2 . 2)),((f1 . 3) * (f2 . 3))*> by BINOP_2:def_11; ::_thesis: verum end; theorem Th29: :: EUCLID_5:29 for p1, p2 being Point of (TOP-REAL 3) holds |(p1,p2)| = (((p1 `1) * (p2 `1)) + ((p1 `2) * (p2 `2))) + ((p1 `3) * (p2 `3)) proof let p1, p2 be Point of (TOP-REAL 3); ::_thesis: |(p1,p2)| = (((p1 `1) * (p2 `1)) + ((p1 `2) * (p2 `2))) + ((p1 `3) * (p2 `3)) reconsider f1 = p1, f2 = p2 as FinSequence of REAL by EUCLID:24; A1: len f1 = len <*(p1 `1),(p1 `2),(p1 `3)*> by Th27 .= 3 by FINSEQ_1:45 ; A2: len f2 = len <*(p2 `1),(p2 `2),(p2 `3)*> by Th27 .= 3 by FINSEQ_1:45 ; |(p1,p2)| = Sum (mlt (f1,f2)) by RVSUM_1:def_16 .= Sum <*((f1 . 1) * (f2 . 1)),((f1 . 2) * (f2 . 2)),((f1 . 3) * (f2 . 3))*> by A1, A2, Th28 .= (((p1 `1) * (p2 `1)) + ((p1 `2) * (p2 `2))) + ((p1 `3) * (f2 . 3)) by RVSUM_1:78 ; hence |(p1,p2)| = (((p1 `1) * (p2 `1)) + ((p1 `2) * (p2 `2))) + ((p1 `3) * (p2 `3)) ; ::_thesis: verum end; theorem Th30: :: EUCLID_5:30 for x3, y3 being Element of REAL for x1, x2, y1, y2 being Real holds |(|[x1,x2,x3]|,|[y1,y2,y3]|)| = ((x1 * y1) + (x2 * y2)) + (x3 * y3) proof let x3, y3 be Element of REAL ; ::_thesis: for x1, x2, y1, y2 being Real holds |(|[x1,x2,x3]|,|[y1,y2,y3]|)| = ((x1 * y1) + (x2 * y2)) + (x3 * y3) let x1, x2, y1, y2 be Real; ::_thesis: |(|[x1,x2,x3]|,|[y1,y2,y3]|)| = ((x1 * y1) + (x2 * y2)) + (x3 * y3) consider p1 being Point of (TOP-REAL 3) such that A1: p1 = |[x1,x2,x3]| ; A2: p1 `3 = x3 by A1, FINSEQ_1:45; consider p2 being Point of (TOP-REAL 3) such that A3: p2 = |[y1,y2,y3]| ; A4: p2 `3 = y3 by A3, FINSEQ_1:45; A5: ( p2 `1 = y1 & p2 `2 = y2 ) by A3, FINSEQ_1:45; ( p1 `1 = x1 & p1 `2 = x2 ) by A1, FINSEQ_1:45; hence |(|[x1,x2,x3]|,|[y1,y2,y3]|)| = ((x1 * y1) + (x2 * y2)) + (x3 * y3) by A1, A2, A3, A5, A4, Th29; ::_thesis: verum end; definition let p1, p2, p3 be Point of (TOP-REAL 3); func|{p1,p2,p3}| -> real number equals :: EUCLID_5:def 5 |(p1,(p2 p3))|; coherence |(p1,(p2 p3))| is real number ; end; :: deftheorem defines |{ EUCLID_5:def_5_:_ for p1, p2, p3 being Point of (TOP-REAL 3) holds |{p1,p2,p3}| = |(p1,(p2 p3))|; theorem :: EUCLID_5:31 for p1, p2 being Point of (TOP-REAL 3) holds ( |{p1,p1,p2}| = 0 & |{p2,p1,p2}| = 0 ) proof let p1, p2 be Point of (TOP-REAL 3); ::_thesis: ( |{p1,p1,p2}| = 0 & |{p2,p1,p2}| = 0 ) A1: |{p2,p1,p2}| = (((p2 `1) * ((p1 p2) `1)) + ((p2 `2) * ((p1 p2) `2))) + ((p2 `3) * ((p1 p2) `3)) by Th29 .= (((p2 `1) * (((p1 `2) * (p2 `3)) - ((p1 `3) * (p2 `2)))) + ((p2 `2) * ((p1 p2) `2))) + ((p2 `3) * ((p1 p2) `3)) by FINSEQ_1:45 .= (((p2 `1) * (((p1 `2) * (p2 `3)) - ((p1 `3) * (p2 `2)))) + ((p2 `2) * (((p1 `3) * (p2 `1)) - ((p1 `1) * (p2 `3))))) + ((p2 `3) * ((p1 p2) `3)) by FINSEQ_1:45 .= ((((p2 `1) * ((p1 `2) * (p2 `3))) - ((p2 `1) * ((p1 `3) * (p2 `2)))) + ((p2 `2) * (((p1 `3) * (p2 `1)) - ((p1 `1) * (p2 `3))))) + ((p2 `3) * (((p1 `1) * (p2 `2)) - ((p1 `2) * (p2 `1)))) by FINSEQ_1:45 .= (0 - ((p2 `2) * ((p1 `1) * (p2 `3)))) + ((p2 `2) * ((p1 `1) * (p2 `3))) ; |{p1,p1,p2}| = (((p1 `1) * ((p1 p2) `1)) + ((p1 `2) * ((p1 p2) `2))) + ((p1 `3) * ((p1 p2) `3)) by Th29 .= (((p1 `1) * (((p1 `2) * (p2 `3)) - ((p1 `3) * (p2 `2)))) + ((p1 `2) * ((p1 p2) `2))) + ((p1 `3) * ((p1 p2) `3)) by FINSEQ_1:45 .= (((p1 `1) * (((p1 `2) * (p2 `3)) - ((p1 `3) * (p2 `2)))) + ((p1 `2) * (((p1 `3) * (p2 `1)) - ((p1 `1) * (p2 `3))))) + ((p1 `3) * ((p1 p2) `3)) by FINSEQ_1:45 .= ((((p1 `1) * ((p1 `2) * (p2 `3))) - ((p1 `1) * ((p1 `3) * (p2 `2)))) + ((p1 `2) * (((p1 `3) * (p2 `1)) - ((p1 `1) * (p2 `3))))) + ((p1 `3) * (((p1 `1) * (p2 `2)) - ((p1 `2) * (p2 `1)))) by FINSEQ_1:45 .= 0 ; hence ( |{p1,p1,p2}| = 0 & |{p2,p1,p2}| = 0 ) by A1; ::_thesis: verum end; theorem :: EUCLID_5:32 for p1, p2, p3 being Point of (TOP-REAL 3) holds p1 (p2 p3) = (|(p1,p3)| * p2) - (|(p1,p2)| * p3) proof let p1, p2, p3 be Point of (TOP-REAL 3); ::_thesis: p1 (p2 p3) = (|(p1,p3)| * p2) - (|(p1,p2)| * p3) A1: ( ((p1 `2) * (((p2 `1) * (p3 `2)) - ((p2 `2) * (p3 `1)))) - ((p1 `3) * (((p2 `3) * (p3 `1)) - ((p2 `1) * (p3 `3)))) = (((((p1 `2) * (p3 `2)) + ((p1 `3) * (p3 `3))) + ((p1 `1) * (p3 `1))) * (p2 `1)) - (((((p1 `2) * (p2 `2)) + ((p1 `3) * (p2 `3))) + ((p1 `1) * (p2 `1))) * (p3 `1)) & ((p1 `3) * (((p2 `2) * (p3 `3)) - ((p2 `3) * (p3 `2)))) - ((p1 `1) * (((p2 `1) * (p3 `2)) - ((p2 `2) * (p3 `1)))) = (((((p1 `3) * (p3 `3)) + ((p1 `1) * (p3 `1))) + ((p1 `2) * (p3 `2))) * (p2 `2)) - (((((p1 `3) * (p2 `3)) + ((p1 `1) * (p2 `1))) + ((p1 `2) * (p2 `2))) * (p3 `2)) ) ; A2: ((p1 `1) * (((p2 `3) * (p3 `1)) - ((p2 `1) * (p3 `3)))) - ((p1 `2) * (((p2 `2) * (p3 `3)) - ((p2 `3) * (p3 `2)))) = (((((p1 `1) * (p3 `1)) + ((p1 `2) * (p3 `2))) + ((p1 `3) * (p3 `3))) * (p2 `3)) - (((((p1 `1) * (p2 `1)) + ((p1 `2) * (p2 `2))) + ((p1 `3) * (p2 `3))) * (p3 `3)) ; p1 (p2 p3) = |[(p1 `1),(p1 `2),(p1 `3)]| |[(((p2 `2) * (p3 `3)) - ((p2 `3) * (p3 `2))),(((p2 `3) * (p3 `1)) - ((p2 `1) * (p3 `3))),(((p2 `1) * (p3 `2)) - ((p2 `2) * (p3 `1)))]| by Th3 .= |[(((p1 `2) * (((p2 `1) * (p3 `2)) - ((p2 `2) * (p3 `1)))) - ((p1 `3) * (((p2 `3) * (p3 `1)) - ((p2 `1) * (p3 `3))))),(((p1 `3) * (((p2 `2) * (p3 `3)) - ((p2 `3) * (p3 `2)))) - ((p1 `1) * (((p2 `1) * (p3 `2)) - ((p2 `2) * (p3 `1))))),(((p1 `1) * (((p2 `3) * (p3 `1)) - ((p2 `1) * (p3 `3)))) - ((p1 `2) * (((p2 `2) * (p3 `3)) - ((p2 `3) * (p3 `2)))))]| by Th15 ; then p1 (p2 p3) = |[(((((p1 `1) * (p3 `1)) + ((p1 `2) * (p3 `2))) + ((p1 `3) * (p3 `3))) * (p2 `1)),(((((p1 `1) * (p3 `1)) + ((p1 `2) * (p3 `2))) + ((p1 `3) * (p3 `3))) * (p2 `2)),(((((p1 `1) * (p3 `1)) + ((p1 `2) * (p3 `2))) + ((p1 `3) * (p3 `3))) * (p2 `3))]| - |[(((((p1 `1) * (p2 `1)) + ((p1 `2) * (p2 `2))) + ((p1 `3) * (p2 `3))) * (p3 `1)),(((((p1 `1) * (p2 `1)) + ((p1 `2) * (p2 `2))) + ((p1 `3) * (p2 `3))) * (p3 `2)),(((((p1 `1) * (p2 `1)) + ((p1 `2) * (p2 `2))) + ((p1 `3) * (p2 `3))) * (p3 `3))]| by A1, A2, Th13 .= (((((p1 `1) * (p3 `1)) + ((p1 `2) * (p3 `2))) + ((p1 `3) * (p3 `3))) * |[(p2 `1),(p2 `2),(p2 `3)]|) - |[(((((p1 `1) * (p2 `1)) + ((p1 `2) * (p2 `2))) + ((p1 `3) * (p2 `3))) * (p3 `1)),(((((p1 `1) * (p2 `1)) + ((p1 `2) * (p2 `2))) + ((p1 `3) * (p2 `3))) * (p3 `2)),(((((p1 `1) * (p2 `1)) + ((p1 `2) * (p2 `2))) + ((p1 `3) * (p2 `3))) * (p3 `3))]| by Th8 .= (((((p1 `1) * (p3 `1)) + ((p1 `2) * (p3 `2))) + ((p1 `3) * (p3 `3))) * |[(p2 `1),(p2 `2),(p2 `3)]|) - (((((p1 `1) * (p2 `1)) + ((p1 `2) * (p2 `2))) + ((p1 `3) * (p2 `3))) * |[(p3 `1),(p3 `2),(p3 `3)]|) by Th8 .= (|(p1,p3)| * |[(p2 `1),(p2 `2),(p2 `3)]|) - (((((p1 `1) * (p2 `1)) + ((p1 `2) * (p2 `2))) + ((p1 `3) * (p2 `3))) * |[(p3 `1),(p3 `2),(p3 `3)]|) by Th29 .= (|(p1,p3)| * |[(p2 `1),(p2 `2),(p2 `3)]|) - (|(p1,p2)| * |[(p3 `1),(p3 `2),(p3 `3)]|) by Th29 .= (|(p1,p3)| * p2) - (|(p1,p2)| * |[(p3 `1),(p3 `2),(p3 `3)]|) by Th3 ; hence p1 (p2 p3) = (|(p1,p3)| * p2) - (|(p1,p2)| * p3) by Th3; ::_thesis: verum end; theorem Th33: :: EUCLID_5:33 for p1, p2, p3 being Point of (TOP-REAL 3) holds |{p1,p2,p3}| = |{p2,p3,p1}| proof let p1, p2, p3 be Point of (TOP-REAL 3); ::_thesis: |{p1,p2,p3}| = |{p2,p3,p1}| |{p1,p2,p3}| = |(|[(p1 `1),(p1 `2),(p1 `3)]|,|[(((p2 `2) * (p3 `3)) - ((p2 `3) * (p3 `2))),(((p2 `3) * (p3 `1)) - ((p2 `1) * (p3 `3))),(((p2 `1) * (p3 `2)) - ((p2 `2) * (p3 `1)))]|)| by Th3 .= (((p1 `1) * (((p2 `2) * (p3 `3)) - ((p2 `3) * (p3 `2)))) + ((p1 `2) * (((p2 `3) * (p3 `1)) - ((p2 `1) * (p3 `3))))) + ((p1 `3) * (((p2 `1) * (p3 `2)) - ((p2 `2) * (p3 `1)))) by Th30 .= (((p2 `1) * (((p3 `2) * (p1 `3)) - ((p3 `3) * (p1 `2)))) + ((p2 `2) * (((p3 `3) * (p1 `1)) - ((p3 `1) * (p1 `3))))) + ((p2 `3) * (((p3 `1) * (p1 `2)) - ((p3 `2) * (p1 `1)))) .= |(|[(p2 `1),(p2 `2),(p2 `3)]|,|[(((p3 `2) * (p1 `3)) - ((p3 `3) * (p1 `2))),(((p3 `3) * (p1 `1)) - ((p3 `1) * (p1 `3))),(((p3 `1) * (p1 `2)) - ((p3 `2) * (p1 `1)))]|)| by Th30 .= |(p2,(p3 p1))| by Th3 ; hence |{p1,p2,p3}| = |{p2,p3,p1}| ; ::_thesis: verum end; theorem :: EUCLID_5:34 for p1, p2, p3 being Point of (TOP-REAL 3) holds |{p1,p2,p3}| = |{p3,p1,p2}| by Th33; theorem :: EUCLID_5:35 for p1, p2, p3 being Point of (TOP-REAL 3) holds |{p1,p2,p3}| = |((p1 p2),p3)| proof let p1, p2, p3 be Point of (TOP-REAL 3); ::_thesis: |{p1,p2,p3}| = |((p1 p2),p3)| |{p1,p2,p3}| = |(|[(p1 `1),(p1 `2),(p1 `3)]|,|[(((p2 `2) * (p3 `3)) - ((p2 `3) * (p3 `2))),(((p2 `3) * (p3 `1)) - ((p2 `1) * (p3 `3))),(((p2 `1) * (p3 `2)) - ((p2 `2) * (p3 `1)))]|)| by Th3 .= (((p1 `1) * (((p2 `2) * (p3 `3)) - ((p2 `3) * (p3 `2)))) + ((p1 `2) * (((p2 `3) * (p3 `1)) - ((p2 `1) * (p3 `3))))) + ((p1 `3) * (((p2 `1) * (p3 `2)) - ((p2 `2) * (p3 `1)))) by Th30 .= ((((p2 `2) * ((p1 `1) * (p3 `3))) - ((p2 `3) * ((p1 `1) * (p3 `2)))) + (((p2 `3) * ((p1 `2) * (p3 `1))) - ((p2 `1) * ((p1 `2) * (p3 `3))))) + (((p2 `1) * ((p1 `3) * (p3 `2))) - ((p2 `2) * ((p1 `3) * (p3 `1)))) ; then |{p1,p2,p3}| = (((((p2 `3) * (p1 `2)) - ((p2 `2) * (p1 `3))) * (p3 `1)) + ((((p2 `1) * (p1 `3)) - ((p2 `3) * (p1 `1))) * (p3 `2))) + ((((p2 `2) * (p1 `1)) - ((p2 `1) * (p1 `2))) * (p3 `3)) .= |((p1 p2),|[(p3 `1),(p3 `2),(p3 `3)]|)| by Th30 .= |((p1 p2),p3)| by Th3 ; hence |{p1,p2,p3}| = |((p1 p2),p3)| ; ::_thesis: verum end;