let n be Nat; 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); (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) = Plane (p,(p1 + p2))
A1:
now for y being object st y in (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) holds
y in Plane (p,(p1 + p2))let y be
object ;
( 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))
;
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;
verum end;
now for y being object st y in Plane (p,(p1 + p2)) holds
y in (transl (p1,(TOP-REAL n))) .: (Plane (p,p2))let y be
object ;
( y in Plane (p,(p1 + p2)) implies y in (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) )assume
y in Plane (
p,
(p1 + p2))
;
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;
verum end;
hence
(transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) = Plane (p,(p1 + p2))
by A1, TARSKI:2; verum