let V be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; 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; ( 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
; M is_parallel_to N
consider v1 being Element of V such that
A3:
M = L + {v1}
by A1;
consider u1 being Element of V such that
A4:
L = N + {u1}
by A2;
set w = u1 + v1;
for x being object st x in N + {(u1 + v1)} holds
x in M
proof
let x be
object ;
( x in N + {(u1 + v1)} implies x in M )
A5:
u1 in {u1}
by TARSKI:def 1;
assume A6:
x in N + {(u1 + v1)}
;
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 A6, RUSUB_4:def 9;
then consider u2,
v2 being
Element of
V such that A7:
x = u2 + v2
and A8:
u2 in N
and A9:
v2 in {(u1 + v1)}
;
x =
u2 + (u1 + v1)
by A7, A9, TARSKI:def 1
.=
(u2 + u1) + v1
by RLVECT_1:def 3
;
then x - v1 =
(u2 + u1) + (v1 - v1)
by RLVECT_1:def 3
.=
(u2 + u1) + (0. V)
by RLVECT_1:15
.=
u2 + u1
;
then
x - v1 in { (u + v) where u, v is Element of V : ( u in N & v in {u1} ) }
by A8, A5;
then A10:
x - v1 in L
by A4, RUSUB_4:def 9;
set y =
x - v1;
A11:
v1 in {v1}
by TARSKI:def 1;
(x - v1) + v1 =
x - (v1 - v1)
by RLVECT_1:29
.=
x - (0. V)
by RLVECT_1:15
.=
x
;
then
x in { (u + v) where u, v is Element of V : ( u in L & v in {v1} ) }
by A10, A11;
hence
x in M
by A3, RUSUB_4:def 9;
verum
end;
then A12:
N + {(u1 + v1)} c= M
;
for x being object st x in M holds
x in N + {(u1 + v1)}
proof
let x be
object ;
( x in M implies x in N + {(u1 + v1)} )
A13:
u1 + v1 in {(u1 + v1)}
by TARSKI:def 1;
assume A14:
x in M
;
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, A14, RUSUB_4:def 9;
then consider u2,
v2 being
Element of
V such that A15:
x = u2 + v2
and A16:
u2 in L
and A17:
v2 in {v1}
;
A18:
v2 = v1
by A17, TARSKI:def 1;
u2 in { (u + v) where u, v is Element of V : ( u in N & v in {u1} ) }
by A4, A16, RUSUB_4:def 9;
then consider u3,
v3 being
Element of
V such that A19:
u2 = u3 + v3
and A20:
u3 in N
and A21:
v3 in {u1}
;
v3 = u1
by A21, TARSKI:def 1;
then
x = u3 + (u1 + v1)
by A15, A19, A18, RLVECT_1:def 3;
then
x in { (u + v) where u, v is Element of V : ( u in N & v in {(u1 + v1)} ) }
by A20, A13;
hence
x in N + {(u1 + v1)}
by RUSUB_4:def 9;
verum
end;
then
M c= N + {(u1 + v1)}
;
then
M = N + {(u1 + v1)}
by A12;
hence
M is_parallel_to N
; verum