let AS be AffinSpace; for X, Y being Subset of AS
for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st a = LDir Y & [X,1] = A & Y is being_line & X is being_line holds
( a on A iff Y '||' X )
let X, Y be Subset of AS; for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st a = LDir Y & [X,1] = A & Y is being_line & X is being_line holds
( a on A iff Y '||' X )
let a be POINT of (IncProjSp_of AS); for A being LINE of (IncProjSp_of AS) st a = LDir Y & [X,1] = A & Y is being_line & X is being_line holds
( a on A iff Y '||' X )
let A be LINE of (IncProjSp_of AS); ( a = LDir Y & [X,1] = A & Y is being_line & X is being_line implies ( a on A iff Y '||' X ) )
assume that
A1:
a = LDir Y
and
A2:
[X,1] = A
and
A3:
Y is being_line
and
A4:
X is being_line
; ( a on A iff Y '||' X )
A5:
now ( a on A implies Y '||' X )A6:
now ( ex K being Subset of AS st
( K is being_line & [X,1] = [K,1] & ( ( LDir Y in the carrier of AS & LDir Y in K ) or LDir Y = LDir K ) ) implies Y '||' X )given K being
Subset of
AS such that A7:
K is
being_line
and A8:
[X,1] = [K,1]
and A9:
( (
LDir Y in the
carrier of
AS &
LDir Y in K ) or
LDir Y = LDir K )
;
Y '||' XA10:
K in AfLines AS
by A7;
A11:
X = K
by A8, XTUPLE_0:1;
A12:
now ( LDir Y = LDir K implies Y '||' X )assume
LDir Y = LDir K
;
Y '||' Xthen A13:
Y in Class (
(LinesParallelity AS),
K)
by A10, EQREL_1:23;
LDir K = Class (
(LinesParallelity AS),
K)
;
then consider K9 being
Subset of
AS such that A14:
Y = K9
and A15:
K9 is
being_line
and A16:
K '||' K9
by A7, A13, Th9;
K // K9
by A7, A15, A16, AFF_4:40;
hence
Y '||' X
by A7, A11, A14, A15, AFF_4:40;
verum end; hence
Y '||' X
by A9, A12;
verum end; assume
a on A
;
Y '||' Xthen A18:
[a,A] in the
Inc of
(IncProjSp_of AS)
by INCSP_1:def 1;
for
K,
X9 being
Subset of
AS holds
( not
K is
being_line or not
X9 is
being_plane or not
LDir Y = LDir K or not
[X,1] = [(PDir X9),2] or not
K '||' X9 )
by XTUPLE_0:1;
hence
Y '||' X
by A1, A2, A18, A6, Def11;
verum end;
now ( Y '||' X implies a on A )assume
Y '||' X
;
a on Athen A19:
X in LDir Y
by A3, A4, Th9;
A20:
LDir X = Class (
(LinesParallelity AS),
X)
;
Y in AfLines AS
by A3;
then
Class (
(LinesParallelity AS),
X)
= Class (
(LinesParallelity AS),
Y)
by A19, EQREL_1:23;
then
[a,A] in Proj_Inc AS
by A1, A2, A4, A20, Def11;
hence
a on A
by INCSP_1:def 1;
verum end;
hence
( a on A iff Y '||' X )
by A5; verum