let n be Nat; :: thesis: for p, p1, p2 being Point of () holds (transl (p1,())) .: (Plane (p,p2)) = Plane (p,(p1 + p2))
let p, p1, p2 be Point of (); :: thesis: (transl (p1,())) .: (Plane (p,p2)) = Plane (p,(p1 + p2))
A1: now :: thesis: for y being object st y in (transl (p1,())) .: (Plane (p,p2)) holds
y in Plane (p,(p1 + p2))
let y be object ; :: thesis: ( y in (transl (p1,())) .: (Plane (p,p2)) implies y in Plane (p,(p1 + p2)) )
assume y in (transl (p1,())) .: (Plane (p,p2)) ; :: thesis: y in Plane (p,(p1 + p2))
then consider x being object such that
A2: ( [x,y] in transl (p1,()) & x in Plane (p,p2) ) by RELAT_1:def 13;
consider x1 being Point of () such that
A3: ( x = x1 & |(p,(x1 - p2))| = 0 ) by A2;
A4: y = (transl (p1,())) . x1 by
.= p1 + x1 by RLTOPSP1:def 10 ;
( x in dom (transl (p1,())) & y = (transl (p1,())) . x ) by ;
then y in rng (transl (p1,())) by FUNCT_1:3;
then reconsider y1 = y as Point of () ;
x1 - p2 = (x1 - p2) + (0. ()) 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
.= y1 - (p1 + p2) by RLVECT_1:27 ;
hence y in Plane (p,(p1 + p2)) by A3; :: thesis: verum
end;
now :: thesis: for y being object st y in Plane (p,(p1 + p2)) holds
y in (transl (p1,())) .: (Plane (p,p2))
let y be object ; :: thesis: ( y in Plane (p,(p1 + p2)) implies y in (transl (p1,())) .: (Plane (p,p2)) )
assume y in Plane (p,(p1 + p2)) ; :: thesis: y in (transl (p1,())) .: (Plane (p,p2))
then consider y1 being Point of () such that
A5: ( y = y1 & |(p,(y1 - (p1 + p2)))| = 0 ) ;
set x = y1 - p1;
y1 - p1 in the carrier of () ;
then A6: y1 - p1 in dom (transl (p1,())) by FUNCT_2:def 1;
p1 + (y1 - p1) = y1 by RLVECT_4:1;
then (transl (p1,())) . (y1 - p1) = y1 by RLTOPSP1:def 10;
then A7: [(y1 - p1),y1] in transl (p1,()) by ;
(y1 - p1) - p2 = y1 - (p1 + p2) by RLVECT_1:27;
then y1 - p1 in Plane (p,p2) by A5;
hence y in (transl (p1,())) .: (Plane (p,p2)) by ; :: thesis: verum
end;
hence (transl (p1,())) .: (Plane (p,p2)) = Plane (p,(p1 + p2)) by ; :: thesis: verum