let AS be AffinSpace; :: thesis: 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; :: thesis: 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); :: thesis: 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); :: thesis: ( 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 ; :: thesis: ( a on A iff Y '||' X )
A5: now :: thesis: ( a on A implies Y '||' X )
A6: now :: thesis: ( 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 ) ; :: thesis: Y '||' X
A10: K in AfLines AS by A7;
A11: X = K by A8, XTUPLE_0:1;
A12: now :: thesis: ( LDir Y = LDir K implies Y '||' X )
assume LDir Y = LDir K ; :: thesis: Y '||' X
then 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; :: thesis: verum
end;
now :: thesis: ( LDir Y in the carrier of AS implies not LDir Y in K )
assume that
A17: LDir Y in the carrier of AS and
LDir Y in K ; :: thesis: contradiction
a in Dir_of_Lines AS by A1, A3, Th14;
then the carrier of AS /\ (Dir_of_Lines AS) <> {} by A1, A17, XBOOLE_0:def 4;
then the carrier of AS meets Dir_of_Lines AS by XBOOLE_0:def 7;
hence contradiction by Th16; :: thesis: verum
end;
hence Y '||' X by A9, A12; :: thesis: verum
end;
assume a on A ; :: thesis: Y '||' X
then 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; :: thesis: verum
end;
now :: thesis: ( Y '||' X implies a on A )
assume Y '||' X ; :: thesis: a on A
then 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; :: thesis: verum
end;
hence ( a on A iff Y '||' X ) by A5; :: thesis: verum