let V be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for M, L, N being Affine Subset of V st M is_parallel_to L & L is_parallel_to N holds
M is_parallel_to N
let M, L, N be Affine Subset of V; :: thesis: ( M is_parallel_to L & L is_parallel_to N implies M is_parallel_to N )
assume that
A1:
M is_parallel_to L
and
A2:
L is_parallel_to N
; :: thesis: M is_parallel_to N
consider v1 being Element of V such that
A3:
M = L + {v1}
by A1, Def1;
consider u1 being Element of V such that
A4:
L = N + {u1}
by A2, Def1;
set w = u1 + v1;
for x being set st x in M holds
x in N + {(u1 + v1)}
proof
let x be
set ;
:: thesis: ( x in M implies x in N + {(u1 + v1)} )
assume A5:
x in M
;
:: thesis: x in N + {(u1 + v1)}
then reconsider x =
x as
Element of
V ;
x in { (u + v) where u, v is Element of V : ( u in L & v in {v1} ) }
by A3, A5, RUSUB_4:def 10;
then consider u2,
v2 being
Element of
V such that A6:
(
x = u2 + v2 &
u2 in L &
v2 in {v1} )
;
u2 in { (u + v) where u, v is Element of V : ( u in N & v in {u1} ) }
by A4, A6, RUSUB_4:def 10;
then consider u3,
v3 being
Element of
V such that A7:
(
u2 = u3 + v3 &
u3 in N &
v3 in {u1} )
;
(
v2 = v1 &
v3 = u1 )
by A6, A7, TARSKI:def 1;
then A8:
x = u3 + (u1 + v1)
by A6, A7, RLVECT_1:def 6;
u1 + v1 in {(u1 + v1)}
by TARSKI:def 1;
then
x in { (u + v) where u, v is Element of V : ( u in N & v in {(u1 + v1)} ) }
by A7, A8;
hence
x in N + {(u1 + v1)}
by RUSUB_4:def 10;
:: thesis: verum
end;
then A9:
M c= N + {(u1 + v1)}
by TARSKI:def 3;
for x being set st x in N + {(u1 + v1)} holds
x in M
proof
let x be
set ;
:: thesis: ( x in N + {(u1 + v1)} implies x in M )
assume A10:
x in N + {(u1 + v1)}
;
:: thesis: x in M
then reconsider x =
x as
Element of
V ;
x in { (u + v) where u, v is Element of V : ( u in N & v in {(u1 + v1)} ) }
by A10, RUSUB_4:def 10;
then consider u2,
v2 being
Element of
V such that A11:
(
x = u2 + v2 &
u2 in N &
v2 in {(u1 + v1)} )
;
x =
u2 + (u1 + v1)
by A11, TARSKI:def 1
.=
(u2 + u1) + v1
by RLVECT_1:def 6
;
then A12:
x - v1 =
(u2 + u1) + (v1 - v1)
by RLVECT_1:def 6
.=
(u2 + u1) + (0. V)
by RLVECT_1:28
.=
u2 + u1
by RLVECT_1:10
;
u1 in {u1}
by TARSKI:def 1;
then
x - v1 in { (u + v) where u, v is Element of V : ( u in N & v in {u1} ) }
by A11, A12;
then A13:
x - v1 in L
by A4, RUSUB_4:def 10;
set y =
x - v1;
A14:
(x - v1) + v1 =
x - (v1 - v1)
by RLVECT_1:43
.=
x - (0. V)
by RLVECT_1:28
.=
x
by RLVECT_1:26
;
v1 in {v1}
by TARSKI:def 1;
then
x in { (u + v) where u, v is Element of V : ( u in L & v in {v1} ) }
by A13, A14;
hence
x in M
by A3, RUSUB_4:def 10;
:: thesis: verum
end;
then
N + {(u1 + v1)} c= M
by TARSKI:def 3;
then
M = N + {(u1 + v1)}
by A9, XBOOLE_0:def 10;
hence
M is_parallel_to N
by Def1; :: thesis: verum