let n be Nat; :: thesis: for p, p1, p2 being Point of (TOP-REAL n) holds (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) = Plane (p,(p1 + p2))

let p, p1, p2 be Point of (TOP-REAL n); :: thesis: (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) = Plane (p,(p1 + p2))

let p, p1, p2 be Point of (TOP-REAL n); :: thesis: (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) = Plane (p,(p1 + p2))

A1: now :: thesis: for y being object st y in (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) holds

y in Plane (p,(p1 + p2))

y in Plane (p,(p1 + p2))

let y be object ; :: thesis: ( y in (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) implies y in Plane (p,(p1 + p2)) )

assume y in (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) ; :: thesis: y in Plane (p,(p1 + p2))

then consider x being object such that

A2: ( [x,y] in transl (p1,(TOP-REAL n)) & x in Plane (p,p2) ) by RELAT_1:def 13;

consider x1 being Point of (TOP-REAL n) such that

A3: ( x = x1 & |(p,(x1 - p2))| = 0 ) by A2;

A4: y = (transl (p1,(TOP-REAL n))) . x1 by A2, A3, FUNCT_1:1

.= p1 + x1 by RLTOPSP1:def 10 ;

( x in dom (transl (p1,(TOP-REAL n))) & y = (transl (p1,(TOP-REAL n))) . x ) by A2, FUNCT_1:1;

then y in rng (transl (p1,(TOP-REAL n))) by FUNCT_1:3;

then reconsider y1 = y as Point of (TOP-REAL n) ;

x1 - p2 = (x1 - p2) + (0. (TOP-REAL n)) by RLVECT_1:4

.= (x1 - p2) + (p1 + (- p1)) by RLVECT_1:5

.= ((x1 + (- p2)) + p1) + (- p1) by RLVECT_1:def 3

.= (y1 - p2) - p1 by A4, RLVECT_1:def 3

.= y1 - (p1 + p2) by RLVECT_1:27 ;

hence y in Plane (p,(p1 + p2)) by A3; :: thesis: verum

end;assume y in (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) ; :: thesis: y in Plane (p,(p1 + p2))

then consider x being object such that

A2: ( [x,y] in transl (p1,(TOP-REAL n)) & x in Plane (p,p2) ) by RELAT_1:def 13;

consider x1 being Point of (TOP-REAL n) such that

A3: ( x = x1 & |(p,(x1 - p2))| = 0 ) by A2;

A4: y = (transl (p1,(TOP-REAL n))) . x1 by A2, A3, FUNCT_1:1

.= p1 + x1 by RLTOPSP1:def 10 ;

( x in dom (transl (p1,(TOP-REAL n))) & y = (transl (p1,(TOP-REAL n))) . x ) by A2, FUNCT_1:1;

then y in rng (transl (p1,(TOP-REAL n))) by FUNCT_1:3;

then reconsider y1 = y as Point of (TOP-REAL n) ;

x1 - p2 = (x1 - p2) + (0. (TOP-REAL n)) by RLVECT_1:4

.= (x1 - p2) + (p1 + (- p1)) by RLVECT_1:5

.= ((x1 + (- p2)) + p1) + (- p1) by RLVECT_1:def 3

.= (y1 - p2) - p1 by A4, RLVECT_1:def 3

.= y1 - (p1 + p2) by RLVECT_1:27 ;

hence y in Plane (p,(p1 + p2)) by A3; :: thesis: verum

now :: thesis: for y being object st y in Plane (p,(p1 + p2)) holds

y in (transl (p1,(TOP-REAL n))) .: (Plane (p,p2))

hence
(transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) = Plane (p,(p1 + p2))
by A1, TARSKI:2; :: thesis: verumy in (transl (p1,(TOP-REAL n))) .: (Plane (p,p2))

let y be object ; :: thesis: ( y in Plane (p,(p1 + p2)) implies y in (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) )

assume y in Plane (p,(p1 + p2)) ; :: thesis: y in (transl (p1,(TOP-REAL n))) .: (Plane (p,p2))

then consider y1 being Point of (TOP-REAL n) such that

A5: ( y = y1 & |(p,(y1 - (p1 + p2)))| = 0 ) ;

set x = y1 - p1;

y1 - p1 in the carrier of (TOP-REAL n) ;

then A6: y1 - p1 in dom (transl (p1,(TOP-REAL n))) by FUNCT_2:def 1;

p1 + (y1 - p1) = y1 by RLVECT_4:1;

then (transl (p1,(TOP-REAL n))) . (y1 - p1) = y1 by RLTOPSP1:def 10;

then A7: [(y1 - p1),y1] in transl (p1,(TOP-REAL n)) by A6, FUNCT_1:1;

(y1 - p1) - p2 = y1 - (p1 + p2) by RLVECT_1:27;

then y1 - p1 in Plane (p,p2) by A5;

hence y in (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) by A5, A7, RELAT_1:def 13; :: thesis: verum

end;assume y in Plane (p,(p1 + p2)) ; :: thesis: y in (transl (p1,(TOP-REAL n))) .: (Plane (p,p2))

then consider y1 being Point of (TOP-REAL n) such that

A5: ( y = y1 & |(p,(y1 - (p1 + p2)))| = 0 ) ;

set x = y1 - p1;

y1 - p1 in the carrier of (TOP-REAL n) ;

then A6: y1 - p1 in dom (transl (p1,(TOP-REAL n))) by FUNCT_2:def 1;

p1 + (y1 - p1) = y1 by RLVECT_4:1;

then (transl (p1,(TOP-REAL n))) . (y1 - p1) = y1 by RLTOPSP1:def 10;

then A7: [(y1 - p1),y1] in transl (p1,(TOP-REAL n)) by A6, FUNCT_1:1;

(y1 - p1) - p2 = y1 - (p1 + p2) by RLVECT_1:27;

then y1 - p1 in Plane (p,p2) by A5;

hence y in (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) by A5, A7, RELAT_1:def 13; :: thesis: verum