:: AFPROJ semantic presentation
begin
theorem Th1: :: AFPROJ:1
for AS being AffinSpace
for X being Subset of AS st AS is AffinPlane & X = the carrier of AS holds
X is being_plane
proof
let AS be AffinSpace; ::_thesis: for X being Subset of AS st AS is AffinPlane & X = the carrier of AS holds
X is being_plane
let X be Subset of AS; ::_thesis: ( AS is AffinPlane & X = the carrier of AS implies X is being_plane )
assume that
A1: AS is AffinPlane and
A2: X = the carrier of AS ; ::_thesis: X is being_plane
consider a, b, c being Element of AS such that
A3: not LIN a,b,c by AFF_1:12;
set P = Line (a,b);
set K = Line (a,c);
A4: b in Line (a,b) by AFF_1:15;
A5: c in Line (a,c) by AFF_1:15;
a <> b by A3, AFF_1:7;
then A6: Line (a,b) is being_line by AFF_1:def_3;
set Y = Plane ((Line (a,c)),(Line (a,b)));
A7: a in Line (a,b) by AFF_1:15;
a <> c by A3, AFF_1:7;
then A8: Line (a,c) is being_line by AFF_1:def_3;
A9: a in Line (a,c) by AFF_1:15;
A10: not Line (a,c) // Line (a,b)
proof
assume Line (a,c) // Line (a,b) ; ::_thesis: contradiction
then c in Line (a,b) by A7, A9, A5, AFF_1:45;
hence contradiction by A3, A7, A4, A6, AFF_1:21; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_X_holds_
x_in_Plane_((Line_(a,c)),(Line_(a,b)))
let x be set ; ::_thesis: ( x in X implies x in Plane ((Line (a,c)),(Line (a,b))) )
assume x in X ; ::_thesis: x in Plane ((Line (a,c)),(Line (a,b)))
then reconsider a = x as Element of AS ;
set K9 = a * (Line (a,c));
A11: a * (Line (a,c)) is being_line by A8, AFF_4:27;
A12: Line (a,c) // a * (Line (a,c)) by A8, AFF_4:def_3;
then not a * (Line (a,c)) // Line (a,b) by A10, AFF_1:44;
then consider b being Element of AS such that
A13: b in a * (Line (a,c)) and
A14: b in Line (a,b) by A1, A6, A11, AFF_1:58;
a in a * (Line (a,c)) by A8, AFF_4:def_3;
then a,b // Line (a,c) by A12, A13, AFF_1:40;
then a in { zz where zz is Element of AS : ex b being Element of AS st
( zz,b // Line (a,c) & b in Line (a,b) ) } by A14;
hence x in Plane ((Line (a,c)),(Line (a,b))) by AFF_4:def_1; ::_thesis: verum
end;
then A15: X c= Plane ((Line (a,c)),(Line (a,b))) by TARSKI:def_3;
Plane ((Line (a,c)),(Line (a,b))) is being_plane by A6, A8, A10, AFF_4:def_2;
hence X is being_plane by A2, A15, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th2: :: AFPROJ:2
for AS being AffinSpace
for X being Subset of AS st AS is AffinPlane & X is being_plane holds
X = the carrier of AS
proof
let AS be AffinSpace; ::_thesis: for X being Subset of AS st AS is AffinPlane & X is being_plane holds
X = the carrier of AS
let X be Subset of AS; ::_thesis: ( AS is AffinPlane & X is being_plane implies X = the carrier of AS )
assume that
A1: AS is AffinPlane and
A2: X is being_plane ; ::_thesis: X = the carrier of AS
the carrier of AS c= the carrier of AS ;
then reconsider Z = the carrier of AS as Subset of AS ;
Z is being_plane by A1, Th1;
hence X = the carrier of AS by A2, AFF_4:33; ::_thesis: verum
end;
theorem Th3: :: AFPROJ:3
for AS being AffinSpace
for X, Y being Subset of AS st AS is AffinPlane & X is being_plane & Y is being_plane holds
X = Y
proof
let AS be AffinSpace; ::_thesis: for X, Y being Subset of AS st AS is AffinPlane & X is being_plane & Y is being_plane holds
X = Y
let X, Y be Subset of AS; ::_thesis: ( AS is AffinPlane & X is being_plane & Y is being_plane implies X = Y )
assume that
A1: AS is AffinPlane and
A2: X is being_plane and
A3: Y is being_plane ; ::_thesis: X = Y
X = the carrier of AS by A1, A2, Th2;
hence X = Y by A1, A3, Th2; ::_thesis: verum
end;
theorem :: AFPROJ:4
for AS being AffinSpace
for X being Subset of AS st X = the carrier of AS & X is being_plane holds
AS is AffinPlane
proof
let AS be AffinSpace; ::_thesis: for X being Subset of AS st X = the carrier of AS & X is being_plane holds
AS is AffinPlane
let X be Subset of AS; ::_thesis: ( X = the carrier of AS & X is being_plane implies AS is AffinPlane )
assume that
A1: X = the carrier of AS and
A2: X is being_plane ; ::_thesis: AS is AffinPlane
assume AS is not AffinPlane ; ::_thesis: contradiction
then not for zz being Element of AS holds zz in X by A2, AFF_4:48;
hence contradiction by A1; ::_thesis: verum
end;
theorem Th5: :: AFPROJ:5
for AS being AffinSpace
for A, K, X, Y being Subset of AS st not A // K & A '||' X & A '||' Y & K '||' X & K '||' Y & A is being_line & K is being_line & X is being_plane & Y is being_plane holds
X '||' Y
proof
let AS be AffinSpace; ::_thesis: for A, K, X, Y being Subset of AS st not A // K & A '||' X & A '||' Y & K '||' X & K '||' Y & A is being_line & K is being_line & X is being_plane & Y is being_plane holds
X '||' Y
let A, K, X, Y be Subset of AS; ::_thesis: ( not A // K & A '||' X & A '||' Y & K '||' X & K '||' Y & A is being_line & K is being_line & X is being_plane & Y is being_plane implies X '||' Y )
assume that
A1: not A // K and
A2: A '||' X and
A3: A '||' Y and
A4: K '||' X and
A5: K '||' Y and
A6: A is being_line and
A7: K is being_line and
A8: X is being_plane and
A9: Y is being_plane ; ::_thesis: X '||' Y
set y = the Element of Y;
set x = the Element of X;
A10: Y <> {} by A9, AFF_4:59;
A11: X <> {} by A8, AFF_4:59;
then reconsider a = the Element of X, b = the Element of Y as Element of AS by A10, TARSKI:def_3;
A12: K // a * K by A7, AFF_4:def_3;
A13: A // a * A by A6, AFF_4:def_3;
A14: not a * A // a * K
proof
assume a * A // a * K ; ::_thesis: contradiction
then a * A // K by A12, AFF_1:44;
hence contradiction by A1, A13, AFF_1:44; ::_thesis: verum
end;
a * K c= a + X by A4, A7, A8, AFF_4:68;
then A15: a * K c= X by A8, A11, AFF_4:66;
K // b * K by A7, AFF_4:def_3;
then A16: a * K // b * K by A12, AFF_1:44;
b * A c= b + Y by A3, A6, A9, AFF_4:68;
then A17: b * A c= Y by A9, A10, AFF_4:66;
A // b * A by A6, AFF_4:def_3;
then A18: a * A // b * A by A13, AFF_1:44;
b * K c= b + Y by A5, A7, A9, AFF_4:68;
then A19: b * K c= Y by A9, A10, AFF_4:66;
a * A c= a + X by A2, A6, A8, AFF_4:68;
then a * A c= X by A8, A11, AFF_4:66;
hence X '||' Y by A8, A9, A15, A17, A19, A14, A18, A16, AFF_4:55; ::_thesis: verum
end;
theorem :: AFPROJ:6
for AS being AffinSpace
for X, A, Y being Subset of AS st X is being_plane & A '||' X & X '||' Y holds
A '||' Y by AFF_4:59, AFF_4:60;
definition
let AS be AffinSpace;
func AfLines AS -> Subset-Family of AS equals :: AFPROJ:def 1
{ A where A is Subset of AS : A is being_line } ;
coherence
{ A where A is Subset of AS : A is being_line } is Subset-Family of AS
proof
set X = { A where A is Subset of AS : A is being_line } ;
{ A where A is Subset of AS : A is being_line } c= bool the carrier of AS
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { A where A is Subset of AS : A is being_line } or x in bool the carrier of AS )
assume x in { A where A is Subset of AS : A is being_line } ; ::_thesis: x in bool the carrier of AS
then ex A being Subset of AS st
( x = A & A is being_line ) ;
hence x in bool the carrier of AS ; ::_thesis: verum
end;
hence { A where A is Subset of AS : A is being_line } is Subset-Family of AS ; ::_thesis: verum
end;
end;
:: deftheorem defines AfLines AFPROJ:def_1_:_
for AS being AffinSpace holds AfLines AS = { A where A is Subset of AS : A is being_line } ;
definition
let AS be AffinSpace;
func AfPlanes AS -> Subset-Family of AS equals :: AFPROJ:def 2
{ A where A is Subset of AS : A is being_plane } ;
coherence
{ A where A is Subset of AS : A is being_plane } is Subset-Family of AS
proof
set X = { A where A is Subset of AS : A is being_plane } ;
{ A where A is Subset of AS : A is being_plane } c= bool the carrier of AS
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { A where A is Subset of AS : A is being_plane } or x in bool the carrier of AS )
assume x in { A where A is Subset of AS : A is being_plane } ; ::_thesis: x in bool the carrier of AS
then ex A being Subset of AS st
( x = A & A is being_plane ) ;
hence x in bool the carrier of AS ; ::_thesis: verum
end;
hence { A where A is Subset of AS : A is being_plane } is Subset-Family of AS ; ::_thesis: verum
end;
end;
:: deftheorem defines AfPlanes AFPROJ:def_2_:_
for AS being AffinSpace holds AfPlanes AS = { A where A is Subset of AS : A is being_plane } ;
theorem :: AFPROJ:7
for AS being AffinSpace
for x being set holds
( x in AfLines AS iff ex X being Subset of AS st
( x = X & X is being_line ) ) ;
theorem :: AFPROJ:8
for AS being AffinSpace
for x being set holds
( x in AfPlanes AS iff ex X being Subset of AS st
( x = X & X is being_plane ) ) ;
definition
let AS be AffinSpace;
func LinesParallelity AS -> Equivalence_Relation of (AfLines AS) equals :: AFPROJ:def 3
{ [K,M] where K, M is Subset of AS : ( K is being_line & M is being_line & K '||' M ) } ;
coherence
{ [K,M] where K, M is Subset of AS : ( K is being_line & M is being_line & K '||' M ) } is Equivalence_Relation of (AfLines AS)
proof
set AFL = AfLines AS;
set AFL2 = [:(AfLines AS),(AfLines AS):];
set R1 = { [X,Y] where X, Y is Subset of AS : ( X is being_line & Y is being_line & X '||' Y ) } ;
now__::_thesis:_for_x_being_set_st_x_in__{__[X,Y]_where_X,_Y_is_Subset_of_AS_:_(_X_is_being_line_&_Y_is_being_line_&_X_'||'_Y_)__}__holds_
x_in_[:(AfLines_AS),(AfLines_AS):]
let x be set ; ::_thesis: ( x in { [X,Y] where X, Y is Subset of AS : ( X is being_line & Y is being_line & X '||' Y ) } implies x in [:(AfLines AS),(AfLines AS):] )
assume x in { [X,Y] where X, Y is Subset of AS : ( X is being_line & Y is being_line & X '||' Y ) } ; ::_thesis: x in [:(AfLines AS),(AfLines AS):]
then consider X, Y being Subset of AS such that
A1: x = [X,Y] and
A2: X is being_line and
A3: Y is being_line and
X '||' Y ;
A4: Y in AfLines AS by A3;
X in AfLines AS by A2;
hence x in [:(AfLines AS),(AfLines AS):] by A1, A4, ZFMISC_1:def_2; ::_thesis: verum
end;
then reconsider R2 = { [X,Y] where X, Y is Subset of AS : ( X is being_line & Y is being_line & X '||' Y ) } as Relation of (AfLines AS),(AfLines AS) by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_AfLines_AS_holds_
[x,x]_in_R2
let x be set ; ::_thesis: ( x in AfLines AS implies [x,x] in R2 )
assume x in AfLines AS ; ::_thesis: [x,x] in R2
then consider X being Subset of AS such that
A5: x = X and
A6: X is being_line ;
X // X by A6, AFF_1:41;
then X '||' X by A6, AFF_4:40;
hence [x,x] in R2 by A5, A6; ::_thesis: verum
end;
then A7: R2 is_reflexive_in AfLines AS by RELAT_2:def_1;
then A8: field R2 = AfLines AS by ORDERS_1:13;
A9: for X, Y being Subset of AS st X is being_line & Y is being_line holds
( [X,Y] in { [X,Y] where X, Y is Subset of AS : ( X is being_line & Y is being_line & X '||' Y ) } iff X '||' Y )
proof
let X, Y be Subset of AS; ::_thesis: ( X is being_line & Y is being_line implies ( [X,Y] in { [X,Y] where X, Y is Subset of AS : ( X is being_line & Y is being_line & X '||' Y ) } iff X '||' Y ) )
assume that
A10: X is being_line and
A11: Y is being_line ; ::_thesis: ( [X,Y] in { [X,Y] where X, Y is Subset of AS : ( X is being_line & Y is being_line & X '||' Y ) } iff X '||' Y )
now__::_thesis:_(_[X,Y]_in__{__[X,Y]_where_X,_Y_is_Subset_of_AS_:_(_X_is_being_line_&_Y_is_being_line_&_X_'||'_Y_)__}__implies_X_'||'_Y_)
assume [X,Y] in { [X,Y] where X, Y is Subset of AS : ( X is being_line & Y is being_line & X '||' Y ) } ; ::_thesis: X '||' Y
then consider X9, Y9 being Subset of AS such that
A12: [X,Y] = [X9,Y9] and
X9 is being_line and
Y9 is being_line and
A13: X9 '||' Y9 ;
X = X9 by A12, XTUPLE_0:1;
hence X '||' Y by A12, A13, XTUPLE_0:1; ::_thesis: verum
end;
hence ( [X,Y] in { [X,Y] where X, Y is Subset of AS : ( X is being_line & Y is being_line & X '||' Y ) } iff X '||' Y ) by A10, A11; ::_thesis: verum
end;
now__::_thesis:_for_x,_y,_z_being_set_st_x_in_AfLines_AS_&_y_in_AfLines_AS_&_z_in_AfLines_AS_&_[x,y]_in_R2_&_[y,z]_in_R2_holds_
[x,z]_in_R2
let x, y, z be set ; ::_thesis: ( x in AfLines AS & y in AfLines AS & z in AfLines AS & [x,y] in R2 & [y,z] in R2 implies [x,z] in R2 )
assume that
A14: x in AfLines AS and
A15: y in AfLines AS and
A16: z in AfLines AS and
A17: [x,y] in R2 and
A18: [y,z] in R2 ; ::_thesis: [x,z] in R2
consider Y being Subset of AS such that
A19: y = Y and
A20: Y is being_line by A15;
consider Z being Subset of AS such that
A21: z = Z and
A22: Z is being_line by A16;
Y '||' Z by A9, A18, A19, A20, A21, A22;
then A23: Y // Z by A20, A22, AFF_4:40;
consider X being Subset of AS such that
A24: x = X and
A25: X is being_line by A14;
X '||' Y by A9, A17, A24, A25, A19, A20;
then X // Y by A25, A20, AFF_4:40;
then X // Z by A23, AFF_1:44;
then X '||' Z by A25, A22, AFF_4:40;
hence [x,z] in R2 by A24, A25, A21, A22; ::_thesis: verum
end;
then A26: R2 is_transitive_in AfLines AS by RELAT_2:def_8;
now__::_thesis:_for_x,_y_being_set_st_x_in_AfLines_AS_&_y_in_AfLines_AS_&_[x,y]_in_R2_holds_
[y,x]_in_R2
let x, y be set ; ::_thesis: ( x in AfLines AS & y in AfLines AS & [x,y] in R2 implies [y,x] in R2 )
assume that
A27: x in AfLines AS and
A28: y in AfLines AS and
A29: [x,y] in R2 ; ::_thesis: [y,x] in R2
consider X being Subset of AS such that
A30: x = X and
A31: X is being_line by A27;
consider Y being Subset of AS such that
A32: y = Y and
A33: Y is being_line by A28;
X '||' Y by A9, A29, A30, A31, A32, A33;
then X // Y by A31, A33, AFF_4:40;
then Y '||' X by A31, A33, AFF_4:40;
hence [y,x] in R2 by A30, A31, A32, A33; ::_thesis: verum
end;
then A34: R2 is_symmetric_in AfLines AS by RELAT_2:def_3;
dom R2 = AfLines AS by A7, ORDERS_1:13;
hence { [K,M] where K, M is Subset of AS : ( K is being_line & M is being_line & K '||' M ) } is Equivalence_Relation of (AfLines AS) by A8, A34, A26, PARTFUN1:def_2, RELAT_2:def_11, RELAT_2:def_16; ::_thesis: verum
end;
end;
:: deftheorem defines LinesParallelity AFPROJ:def_3_:_
for AS being AffinSpace holds LinesParallelity AS = { [K,M] where K, M is Subset of AS : ( K is being_line & M is being_line & K '||' M ) } ;
definition
let AS be AffinSpace;
func PlanesParallelity AS -> Equivalence_Relation of (AfPlanes AS) equals :: AFPROJ:def 4
{ [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } ;
coherence
{ [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } is Equivalence_Relation of (AfPlanes AS)
proof
set AFP = AfPlanes AS;
set AFP2 = [:(AfPlanes AS),(AfPlanes AS):];
set R1 = { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } ;
now__::_thesis:_for_x_being_set_st_x_in__{__[X,Y]_where_X,_Y_is_Subset_of_AS_:_(_X_is_being_plane_&_Y_is_being_plane_&_X_'||'_Y_)__}__holds_
x_in_[:(AfPlanes_AS),(AfPlanes_AS):]
let x be set ; ::_thesis: ( x in { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } implies x in [:(AfPlanes AS),(AfPlanes AS):] )
assume x in { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } ; ::_thesis: x in [:(AfPlanes AS),(AfPlanes AS):]
then consider X, Y being Subset of AS such that
A1: x = [X,Y] and
A2: X is being_plane and
A3: Y is being_plane and
X '||' Y ;
A4: Y in AfPlanes AS by A3;
X in AfPlanes AS by A2;
hence x in [:(AfPlanes AS),(AfPlanes AS):] by A1, A4, ZFMISC_1:def_2; ::_thesis: verum
end;
then reconsider R2 = { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } as Relation of (AfPlanes AS),(AfPlanes AS) by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_AfPlanes_AS_holds_
[x,x]_in_R2
let x be set ; ::_thesis: ( x in AfPlanes AS implies [x,x] in R2 )
assume x in AfPlanes AS ; ::_thesis: [x,x] in R2
then consider X being Subset of AS such that
A5: x = X and
A6: X is being_plane ;
X '||' X by A6, AFF_4:57;
hence [x,x] in R2 by A5, A6; ::_thesis: verum
end;
then A7: R2 is_reflexive_in AfPlanes AS by RELAT_2:def_1;
then A8: field R2 = AfPlanes AS by ORDERS_1:13;
A9: for X, Y being Subset of AS st X is being_plane & Y is being_plane holds
( [X,Y] in { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } iff X '||' Y )
proof
let X, Y be Subset of AS; ::_thesis: ( X is being_plane & Y is being_plane implies ( [X,Y] in { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } iff X '||' Y ) )
assume that
A10: X is being_plane and
A11: Y is being_plane ; ::_thesis: ( [X,Y] in { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } iff X '||' Y )
now__::_thesis:_(_[X,Y]_in__{__[X,Y]_where_X,_Y_is_Subset_of_AS_:_(_X_is_being_plane_&_Y_is_being_plane_&_X_'||'_Y_)__}__implies_X_'||'_Y_)
assume [X,Y] in { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } ; ::_thesis: X '||' Y
then consider X9, Y9 being Subset of AS such that
A12: [X,Y] = [X9,Y9] and
X9 is being_plane and
Y9 is being_plane and
A13: X9 '||' Y9 ;
X = X9 by A12, XTUPLE_0:1;
hence X '||' Y by A12, A13, XTUPLE_0:1; ::_thesis: verum
end;
hence ( [X,Y] in { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } iff X '||' Y ) by A10, A11; ::_thesis: verum
end;
now__::_thesis:_for_x,_y,_z_being_set_st_x_in_AfPlanes_AS_&_y_in_AfPlanes_AS_&_z_in_AfPlanes_AS_&_[x,y]_in_R2_&_[y,z]_in_R2_holds_
[x,z]_in_R2
let x, y, z be set ; ::_thesis: ( x in AfPlanes AS & y in AfPlanes AS & z in AfPlanes AS & [x,y] in R2 & [y,z] in R2 implies [x,z] in R2 )
assume that
A14: x in AfPlanes AS and
A15: y in AfPlanes AS and
A16: z in AfPlanes AS and
A17: [x,y] in R2 and
A18: [y,z] in R2 ; ::_thesis: [x,z] in R2
consider X being Subset of AS such that
A19: x = X and
A20: X is being_plane by A14;
consider Y being Subset of AS such that
A21: y = Y and
A22: Y is being_plane by A15;
consider Z being Subset of AS such that
A23: z = Z and
A24: Z is being_plane by A16;
A25: Y '||' Z by A9, A18, A21, A22, A23, A24;
X '||' Y by A9, A17, A19, A20, A21, A22;
then X '||' Z by A20, A22, A24, A25, AFF_4:61;
hence [x,z] in R2 by A19, A20, A23, A24; ::_thesis: verum
end;
then A26: R2 is_transitive_in AfPlanes AS by RELAT_2:def_8;
now__::_thesis:_for_x,_y_being_set_st_x_in_AfPlanes_AS_&_y_in_AfPlanes_AS_&_[x,y]_in_R2_holds_
[y,x]_in_R2
let x, y be set ; ::_thesis: ( x in AfPlanes AS & y in AfPlanes AS & [x,y] in R2 implies [y,x] in R2 )
assume that
A27: x in AfPlanes AS and
A28: y in AfPlanes AS and
A29: [x,y] in R2 ; ::_thesis: [y,x] in R2
consider X being Subset of AS such that
A30: x = X and
A31: X is being_plane by A27;
consider Y being Subset of AS such that
A32: y = Y and
A33: Y is being_plane by A28;
X '||' Y by A9, A29, A30, A31, A32, A33;
then Y '||' X by A31, A33, AFF_4:58;
hence [y,x] in R2 by A30, A31, A32, A33; ::_thesis: verum
end;
then A34: R2 is_symmetric_in AfPlanes AS by RELAT_2:def_3;
dom R2 = AfPlanes AS by A7, ORDERS_1:13;
hence { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } is Equivalence_Relation of (AfPlanes AS) by A8, A34, A26, PARTFUN1:def_2, RELAT_2:def_11, RELAT_2:def_16; ::_thesis: verum
end;
end;
:: deftheorem defines PlanesParallelity AFPROJ:def_4_:_
for AS being AffinSpace holds PlanesParallelity AS = { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } ;
definition
let AS be AffinSpace;
let X be Subset of AS;
func LDir X -> Subset of (AfLines AS) equals :: AFPROJ:def 5
Class ((LinesParallelity AS),X);
correctness
coherence
Class ((LinesParallelity AS),X) is Subset of (AfLines AS);
;
end;
:: deftheorem defines LDir AFPROJ:def_5_:_
for AS being AffinSpace
for X being Subset of AS holds LDir X = Class ((LinesParallelity AS),X);
definition
let AS be AffinSpace;
let X be Subset of AS;
func PDir X -> Subset of (AfPlanes AS) equals :: AFPROJ:def 6
Class ((PlanesParallelity AS),X);
correctness
coherence
Class ((PlanesParallelity AS),X) is Subset of (AfPlanes AS);
;
end;
:: deftheorem defines PDir AFPROJ:def_6_:_
for AS being AffinSpace
for X being Subset of AS holds PDir X = Class ((PlanesParallelity AS),X);
theorem Th9: :: AFPROJ:9
for AS being AffinSpace
for X being Subset of AS st X is being_line holds
for x being set holds
( x in LDir X iff ex Y being Subset of AS st
( x = Y & Y is being_line & X '||' Y ) )
proof
let AS be AffinSpace; ::_thesis: for X being Subset of AS st X is being_line holds
for x being set holds
( x in LDir X iff ex Y being Subset of AS st
( x = Y & Y is being_line & X '||' Y ) )
let X be Subset of AS; ::_thesis: ( X is being_line implies for x being set holds
( x in LDir X iff ex Y being Subset of AS st
( x = Y & Y is being_line & X '||' Y ) ) )
assume A1: X is being_line ; ::_thesis: for x being set holds
( x in LDir X iff ex Y being Subset of AS st
( x = Y & Y is being_line & X '||' Y ) )
let x be set ; ::_thesis: ( x in LDir X iff ex Y being Subset of AS st
( x = Y & Y is being_line & X '||' Y ) )
A2: now__::_thesis:_(_x_in_LDir_X_implies_ex_Y_being_Subset_of_AS_st_
(_x_=_Y_&_Y_is_being_line_&_X_'||'_Y_)_)
assume x in LDir X ; ::_thesis: ex Y being Subset of AS st
( x = Y & Y is being_line & X '||' Y )
then [x,X] in LinesParallelity AS by EQREL_1:19;
then consider K, M being Subset of AS such that
A3: [x,X] = [K,M] and
A4: K is being_line and
A5: M is being_line and
A6: K '||' M ;
take Y = K; ::_thesis: ( x = Y & Y is being_line & X '||' Y )
A7: X = M by A3, XTUPLE_0:1;
K // M by A4, A5, A6, AFF_4:40;
hence ( x = Y & Y is being_line & X '||' Y ) by A3, A4, A5, A7, AFF_4:40, XTUPLE_0:1; ::_thesis: verum
end;
now__::_thesis:_(_ex_Y_being_Subset_of_AS_st_
(_x_=_Y_&_Y_is_being_line_&_X_'||'_Y_)_implies_x_in_LDir_X_)
given Y being Subset of AS such that A8: x = Y and
A9: Y is being_line and
A10: X '||' Y ; ::_thesis: x in LDir X
X // Y by A1, A9, A10, AFF_4:40;
then Y '||' X by A1, A9, AFF_4:40;
then [Y,X] in { [K,M] where K, M is Subset of AS : ( K is being_line & M is being_line & K '||' M ) } by A1, A9;
hence x in LDir X by A8, EQREL_1:19; ::_thesis: verum
end;
hence ( x in LDir X iff ex Y being Subset of AS st
( x = Y & Y is being_line & X '||' Y ) ) by A2; ::_thesis: verum
end;
theorem Th10: :: AFPROJ:10
for AS being AffinSpace
for X being Subset of AS st X is being_plane holds
for x being set holds
( x in PDir X iff ex Y being Subset of AS st
( x = Y & Y is being_plane & X '||' Y ) )
proof
let AS be AffinSpace; ::_thesis: for X being Subset of AS st X is being_plane holds
for x being set holds
( x in PDir X iff ex Y being Subset of AS st
( x = Y & Y is being_plane & X '||' Y ) )
let X be Subset of AS; ::_thesis: ( X is being_plane implies for x being set holds
( x in PDir X iff ex Y being Subset of AS st
( x = Y & Y is being_plane & X '||' Y ) ) )
assume A1: X is being_plane ; ::_thesis: for x being set holds
( x in PDir X iff ex Y being Subset of AS st
( x = Y & Y is being_plane & X '||' Y ) )
let x be set ; ::_thesis: ( x in PDir X iff ex Y being Subset of AS st
( x = Y & Y is being_plane & X '||' Y ) )
A2: now__::_thesis:_(_x_in_PDir_X_implies_ex_Y_being_Subset_of_AS_st_
(_x_=_Y_&_Y_is_being_plane_&_X_'||'_Y_)_)
assume x in PDir X ; ::_thesis: ex Y being Subset of AS st
( x = Y & Y is being_plane & X '||' Y )
then [x,X] in PlanesParallelity AS by EQREL_1:19;
then consider K, M being Subset of AS such that
A3: [x,X] = [K,M] and
A4: K is being_plane and
A5: M is being_plane and
A6: K '||' M ;
take Y = K; ::_thesis: ( x = Y & Y is being_plane & X '||' Y )
X = M by A3, XTUPLE_0:1;
hence ( x = Y & Y is being_plane & X '||' Y ) by A3, A4, A5, A6, AFF_4:58, XTUPLE_0:1; ::_thesis: verum
end;
now__::_thesis:_(_ex_Y_being_Subset_of_AS_st_
(_x_=_Y_&_Y_is_being_plane_&_X_'||'_Y_)_implies_x_in_PDir_X_)
given Y being Subset of AS such that A7: x = Y and
A8: Y is being_plane and
A9: X '||' Y ; ::_thesis: x in PDir X
Y '||' X by A1, A8, A9, AFF_4:58;
then [Y,X] in { [K,M] where K, M is Subset of AS : ( K is being_plane & M is being_plane & K '||' M ) } by A1, A8;
hence x in PDir X by A7, EQREL_1:19; ::_thesis: verum
end;
hence ( x in PDir X iff ex Y being Subset of AS st
( x = Y & Y is being_plane & X '||' Y ) ) by A2; ::_thesis: verum
end;
theorem Th11: :: AFPROJ:11
for AS being AffinSpace
for X, Y being Subset of AS st X is being_line & Y is being_line holds
( LDir X = LDir Y iff X // Y )
proof
let AS be AffinSpace; ::_thesis: for X, Y being Subset of AS st X is being_line & Y is being_line holds
( LDir X = LDir Y iff X // Y )
let X, Y be Subset of AS; ::_thesis: ( X is being_line & Y is being_line implies ( LDir X = LDir Y iff X // Y ) )
assume that
A1: X is being_line and
A2: Y is being_line ; ::_thesis: ( LDir X = LDir Y iff X // Y )
A3: LDir Y = Class ((LinesParallelity AS),Y) ;
A4: Y in AfLines AS by A2;
A5: now__::_thesis:_(_LDir_X_=_LDir_Y_implies_X_//_Y_)
assume LDir X = LDir Y ; ::_thesis: X // Y
then X in Class ((LinesParallelity AS),Y) by A4, EQREL_1:23;
then ex Y9 being Subset of AS st
( X = Y9 & Y9 is being_line & Y '||' Y9 ) by A2, A3, Th9;
hence X // Y by A2, AFF_4:40; ::_thesis: verum
end;
A6: LDir X = Class ((LinesParallelity AS),X) ;
A7: X in AfLines AS by A1;
now__::_thesis:_(_X_//_Y_implies_LDir_X_=_LDir_Y_)
assume X // Y ; ::_thesis: LDir X = LDir Y
then X '||' Y by A1, A2, AFF_4:40;
then Y in Class ((LinesParallelity AS),X) by A1, A2, A6, Th9;
hence LDir X = LDir Y by A7, EQREL_1:23; ::_thesis: verum
end;
hence ( LDir X = LDir Y iff X // Y ) by A5; ::_thesis: verum
end;
theorem Th12: :: AFPROJ:12
for AS being AffinSpace
for X, Y being Subset of AS st X is being_line & Y is being_line holds
( LDir X = LDir Y iff X '||' Y )
proof
let AS be AffinSpace; ::_thesis: for X, Y being Subset of AS st X is being_line & Y is being_line holds
( LDir X = LDir Y iff X '||' Y )
let X, Y be Subset of AS; ::_thesis: ( X is being_line & Y is being_line implies ( LDir X = LDir Y iff X '||' Y ) )
assume that
A1: X is being_line and
A2: Y is being_line ; ::_thesis: ( LDir X = LDir Y iff X '||' Y )
( LDir X = LDir Y iff X // Y ) by A1, A2, Th11;
hence ( LDir X = LDir Y iff X '||' Y ) by A1, A2, AFF_4:40; ::_thesis: verum
end;
theorem Th13: :: AFPROJ:13
for AS being AffinSpace
for X, Y being Subset of AS st X is being_plane & Y is being_plane holds
( PDir X = PDir Y iff X '||' Y )
proof
let AS be AffinSpace; ::_thesis: for X, Y being Subset of AS st X is being_plane & Y is being_plane holds
( PDir X = PDir Y iff X '||' Y )
let X, Y be Subset of AS; ::_thesis: ( X is being_plane & Y is being_plane implies ( PDir X = PDir Y iff X '||' Y ) )
assume that
A1: X is being_plane and
A2: Y is being_plane ; ::_thesis: ( PDir X = PDir Y iff X '||' Y )
A3: PDir Y = Class ((PlanesParallelity AS),Y) ;
A4: Y in AfPlanes AS by A2;
A5: now__::_thesis:_(_PDir_X_=_PDir_Y_implies_X_'||'_Y_)
assume PDir X = PDir Y ; ::_thesis: X '||' Y
then X in Class ((PlanesParallelity AS),Y) by A4, EQREL_1:23;
then ex Y9 being Subset of AS st
( X = Y9 & Y9 is being_plane & Y '||' Y9 ) by A2, A3, Th10;
hence X '||' Y by A2, AFF_4:58; ::_thesis: verum
end;
A6: PDir X = Class ((PlanesParallelity AS),X) ;
A7: X in AfPlanes AS by A1;
now__::_thesis:_(_X_'||'_Y_implies_PDir_X_=_PDir_Y_)
assume X '||' Y ; ::_thesis: PDir X = PDir Y
then Y in Class ((PlanesParallelity AS),X) by A1, A2, A6, Th10;
hence PDir X = PDir Y by A7, EQREL_1:23; ::_thesis: verum
end;
hence ( PDir X = PDir Y iff X '||' Y ) by A5; ::_thesis: verum
end;
definition
let AS be AffinSpace;
func Dir_of_Lines AS -> non empty set equals :: AFPROJ:def 7
Class (LinesParallelity AS);
coherence
Class (LinesParallelity AS) is non empty set
proof
consider a, b being Element of AS such that
A1: a <> b by DIRAF:40;
set A = Line (a,b);
Line (a,b) is being_line by A1, AFF_1:def_3;
then Line (a,b) in AfLines AS ;
then Class ((LinesParallelity AS),(Line (a,b))) in Class (LinesParallelity AS) by EQREL_1:def_3;
hence Class (LinesParallelity AS) is non empty set ; ::_thesis: verum
end;
end;
:: deftheorem defines Dir_of_Lines AFPROJ:def_7_:_
for AS being AffinSpace holds Dir_of_Lines AS = Class (LinesParallelity AS);
definition
let AS be AffinSpace;
func Dir_of_Planes AS -> non empty set equals :: AFPROJ:def 8
Class (PlanesParallelity AS);
coherence
Class (PlanesParallelity AS) is non empty set
proof
set a = the Element of AS;
consider A being Subset of AS such that
the Element of AS in A and
the Element of AS in A and
the Element of AS in A and
A1: A is being_plane by AFF_4:37;
A in AfPlanes AS by A1;
then Class ((PlanesParallelity AS),A) in Class (PlanesParallelity AS) by EQREL_1:def_3;
hence Class (PlanesParallelity AS) is non empty set ; ::_thesis: verum
end;
end;
:: deftheorem defines Dir_of_Planes AFPROJ:def_8_:_
for AS being AffinSpace holds Dir_of_Planes AS = Class (PlanesParallelity AS);
theorem Th14: :: AFPROJ:14
for AS being AffinSpace
for x being set holds
( x in Dir_of_Lines AS iff ex X being Subset of AS st
( x = LDir X & X is being_line ) )
proof
let AS be AffinSpace; ::_thesis: for x being set holds
( x in Dir_of_Lines AS iff ex X being Subset of AS st
( x = LDir X & X is being_line ) )
let x be set ; ::_thesis: ( x in Dir_of_Lines AS iff ex X being Subset of AS st
( x = LDir X & X is being_line ) )
A1: now__::_thesis:_(_x_in_Dir_of_Lines_AS_implies_ex_X_being_Subset_of_AS_st_
(_x_=_LDir_X_&_X_is_being_line_)_)
assume A2: x in Dir_of_Lines AS ; ::_thesis: ex X being Subset of AS st
( x = LDir X & X is being_line )
then reconsider x99 = x as Subset of (AfLines AS) ;
consider x9 being set such that
A3: x9 in AfLines AS and
A4: x99 = Class ((LinesParallelity AS),x9) by A2, EQREL_1:def_3;
consider X being Subset of AS such that
A5: x9 = X and
A6: X is being_line by A3;
take X = X; ::_thesis: ( x = LDir X & X is being_line )
thus x = LDir X by A4, A5; ::_thesis: X is being_line
thus X is being_line by A6; ::_thesis: verum
end;
now__::_thesis:_(_ex_X_being_Subset_of_AS_st_
(_x_=_LDir_X_&_X_is_being_line_)_implies_x_in_Dir_of_Lines_AS_)
given X being Subset of AS such that A7: x = LDir X and
A8: X is being_line ; ::_thesis: x in Dir_of_Lines AS
X in AfLines AS by A8;
hence x in Dir_of_Lines AS by A7, EQREL_1:def_3; ::_thesis: verum
end;
hence ( x in Dir_of_Lines AS iff ex X being Subset of AS st
( x = LDir X & X is being_line ) ) by A1; ::_thesis: verum
end;
theorem Th15: :: AFPROJ:15
for AS being AffinSpace
for x being set holds
( x in Dir_of_Planes AS iff ex X being Subset of AS st
( x = PDir X & X is being_plane ) )
proof
let AS be AffinSpace; ::_thesis: for x being set holds
( x in Dir_of_Planes AS iff ex X being Subset of AS st
( x = PDir X & X is being_plane ) )
let x be set ; ::_thesis: ( x in Dir_of_Planes AS iff ex X being Subset of AS st
( x = PDir X & X is being_plane ) )
A1: now__::_thesis:_(_x_in_Dir_of_Planes_AS_implies_ex_X_being_Subset_of_AS_st_
(_x_=_PDir_X_&_X_is_being_plane_)_)
assume A2: x in Dir_of_Planes AS ; ::_thesis: ex X being Subset of AS st
( x = PDir X & X is being_plane )
then reconsider x99 = x as Subset of (AfPlanes AS) ;
consider x9 being set such that
A3: x9 in AfPlanes AS and
A4: x99 = Class ((PlanesParallelity AS),x9) by A2, EQREL_1:def_3;
consider X being Subset of AS such that
A5: x9 = X and
A6: X is being_plane by A3;
take X = X; ::_thesis: ( x = PDir X & X is being_plane )
thus x = PDir X by A4, A5; ::_thesis: X is being_plane
thus X is being_plane by A6; ::_thesis: verum
end;
now__::_thesis:_(_ex_X_being_Subset_of_AS_st_
(_x_=_PDir_X_&_X_is_being_plane_)_implies_x_in_Dir_of_Planes_AS_)
given X being Subset of AS such that A7: x = PDir X and
A8: X is being_plane ; ::_thesis: x in Dir_of_Planes AS
X in AfPlanes AS by A8;
hence x in Dir_of_Planes AS by A7, EQREL_1:def_3; ::_thesis: verum
end;
hence ( x in Dir_of_Planes AS iff ex X being Subset of AS st
( x = PDir X & X is being_plane ) ) by A1; ::_thesis: verum
end;
theorem Th16: :: AFPROJ:16
for AS being AffinSpace holds the carrier of AS misses Dir_of_Lines AS
proof
let AS be AffinSpace; ::_thesis: the carrier of AS misses Dir_of_Lines AS
assume not the carrier of AS misses Dir_of_Lines AS ; ::_thesis: contradiction
then consider x being set such that
A1: x in the carrier of AS and
A2: x in Dir_of_Lines AS by XBOOLE_0:3;
reconsider a = x as Element of AS by A1;
consider X being Subset of AS such that
A3: x = LDir X and
A4: X is being_line by A2, Th14;
set A = a * X;
A5: a * X is being_line by A4, AFF_4:27;
X // a * X by A4, AFF_4:def_3;
then X '||' a * X by A4, A5, AFF_4:40;
then a * X in x by A3, A4, A5, Th9;
hence contradiction by A4, AFF_4:def_3; ::_thesis: verum
end;
theorem :: AFPROJ:17
for AS being AffinSpace st AS is AffinPlane holds
AfLines AS misses Dir_of_Planes AS
proof
let AS be AffinSpace; ::_thesis: ( AS is AffinPlane implies AfLines AS misses Dir_of_Planes AS )
the carrier of AS c= the carrier of AS ;
then reconsider X9 = the carrier of AS as Subset of AS ;
assume AS is AffinPlane ; ::_thesis: AfLines AS misses Dir_of_Planes AS
then A1: X9 is being_plane by Th1;
assume not AfLines AS misses Dir_of_Planes AS ; ::_thesis: contradiction
then consider x being set such that
A2: x in AfLines AS and
A3: x in Dir_of_Planes AS by XBOOLE_0:3;
consider Y being Subset of AS such that
A4: x = Y and
A5: Y is being_line by A2;
consider X being Subset of AS such that
A6: x = PDir X and
A7: X is being_plane by A3, Th15;
consider a, b being Element of AS such that
A8: a in Y and
b in Y and
a <> b by A5, AFF_1:19;
consider Y9 being Subset of AS such that
A9: a = Y9 and
A10: Y9 is being_plane and
X '||' Y9 by A6, A7, A4, A8, Th10;
A11: not Y9 in Y9 ;
Y9 = X9 by A1, A10, AFF_4:33;
hence contradiction by A9, A11; ::_thesis: verum
end;
theorem Th18: :: AFPROJ:18
for AS being AffinSpace
for x being set holds
( x in [:(AfLines AS),{1}:] iff ex X being Subset of AS st
( x = [X,1] & X is being_line ) )
proof
let AS be AffinSpace; ::_thesis: for x being set holds
( x in [:(AfLines AS),{1}:] iff ex X being Subset of AS st
( x = [X,1] & X is being_line ) )
let x be set ; ::_thesis: ( x in [:(AfLines AS),{1}:] iff ex X being Subset of AS st
( x = [X,1] & X is being_line ) )
A1: now__::_thesis:_(_x_in_[:(AfLines_AS),{1}:]_implies_ex_X_being_Subset_of_AS_st_
(_x_=_[X,1]_&_X_is_being_line_)_)
assume x in [:(AfLines AS),{1}:] ; ::_thesis: ex X being Subset of AS st
( x = [X,1] & X is being_line )
then consider x1, x2 being set such that
A2: x1 in AfLines AS and
A3: x2 in {1} and
A4: x = [x1,x2] by ZFMISC_1:def_2;
consider X being Subset of AS such that
A5: x1 = X and
A6: X is being_line by A2;
take X = X; ::_thesis: ( x = [X,1] & X is being_line )
thus x = [X,1] by A3, A4, A5, TARSKI:def_1; ::_thesis: X is being_line
thus X is being_line by A6; ::_thesis: verum
end;
now__::_thesis:_(_ex_X_being_Subset_of_AS_st_
(_x_=_[X,1]_&_X_is_being_line_)_implies_x_in_[:(AfLines_AS),{1}:]_)
given X being Subset of AS such that A7: x = [X,1] and
A8: X is being_line ; ::_thesis: x in [:(AfLines AS),{1}:]
X in AfLines AS by A8;
hence x in [:(AfLines AS),{1}:] by A7, ZFMISC_1:106; ::_thesis: verum
end;
hence ( x in [:(AfLines AS),{1}:] iff ex X being Subset of AS st
( x = [X,1] & X is being_line ) ) by A1; ::_thesis: verum
end;
theorem Th19: :: AFPROJ:19
for AS being AffinSpace
for x being set holds
( x in [:(Dir_of_Planes AS),{2}:] iff ex X being Subset of AS st
( x = [(PDir X),2] & X is being_plane ) )
proof
let AS be AffinSpace; ::_thesis: for x being set holds
( x in [:(Dir_of_Planes AS),{2}:] iff ex X being Subset of AS st
( x = [(PDir X),2] & X is being_plane ) )
let x be set ; ::_thesis: ( x in [:(Dir_of_Planes AS),{2}:] iff ex X being Subset of AS st
( x = [(PDir X),2] & X is being_plane ) )
A1: now__::_thesis:_(_x_in_[:(Dir_of_Planes_AS),{2}:]_implies_ex_X_being_Subset_of_AS_st_
(_x_=_[(PDir_X),2]_&_X_is_being_plane_)_)
assume x in [:(Dir_of_Planes AS),{2}:] ; ::_thesis: ex X being Subset of AS st
( x = [(PDir X),2] & X is being_plane )
then consider x1, x2 being set such that
A2: x1 in Dir_of_Planes AS and
A3: x2 in {2} and
A4: x = [x1,x2] by ZFMISC_1:def_2;
consider X being Subset of AS such that
A5: x1 = PDir X and
A6: X is being_plane by A2, Th15;
take X = X; ::_thesis: ( x = [(PDir X),2] & X is being_plane )
thus x = [(PDir X),2] by A3, A4, A5, TARSKI:def_1; ::_thesis: X is being_plane
thus X is being_plane by A6; ::_thesis: verum
end;
now__::_thesis:_(_ex_X_being_Subset_of_AS_st_
(_x_=_[(PDir_X),2]_&_X_is_being_plane_)_implies_x_in_[:(Dir_of_Planes_AS),{2}:]_)
given X being Subset of AS such that A7: x = [(PDir X),2] and
A8: X is being_plane ; ::_thesis: x in [:(Dir_of_Planes AS),{2}:]
PDir X in Dir_of_Planes AS by A8, Th15;
hence x in [:(Dir_of_Planes AS),{2}:] by A7, ZFMISC_1:106; ::_thesis: verum
end;
hence ( x in [:(Dir_of_Planes AS),{2}:] iff ex X being Subset of AS st
( x = [(PDir X),2] & X is being_plane ) ) by A1; ::_thesis: verum
end;
definition
let AS be AffinSpace;
func ProjectivePoints AS -> non empty set equals :: AFPROJ:def 9
the carrier of AS \/ (Dir_of_Lines AS);
correctness
coherence
the carrier of AS \/ (Dir_of_Lines AS) is non empty set ;
;
end;
:: deftheorem defines ProjectivePoints AFPROJ:def_9_:_
for AS being AffinSpace holds ProjectivePoints AS = the carrier of AS \/ (Dir_of_Lines AS);
definition
let AS be AffinSpace;
func ProjectiveLines AS -> non empty set equals :: AFPROJ:def 10
[:(AfLines AS),{1}:] \/ [:(Dir_of_Planes AS),{2}:];
coherence
[:(AfLines AS),{1}:] \/ [:(Dir_of_Planes AS),{2}:] is non empty set ;
end;
:: deftheorem defines ProjectiveLines AFPROJ:def_10_:_
for AS being AffinSpace holds ProjectiveLines AS = [:(AfLines AS),{1}:] \/ [:(Dir_of_Planes AS),{2}:];
definition
let AS be AffinSpace;
func Proj_Inc AS -> Relation of (ProjectivePoints AS),(ProjectiveLines AS) means :Def11: :: AFPROJ:def 11
for x, y being set holds
( [x,y] in it iff ( ex K being Subset of AS st
( K is being_line & y = [K,1] & ( ( x in the carrier of AS & x in K ) or x = LDir K ) ) or ex K, X being Subset of AS st
( K is being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) );
existence
ex b1 being Relation of (ProjectivePoints AS),(ProjectiveLines AS) st
for x, y being set holds
( [x,y] in b1 iff ( ex K being Subset of AS st
( K is being_line & y = [K,1] & ( ( x in the carrier of AS & x in K ) or x = LDir K ) ) or ex K, X being Subset of AS st
( K is being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) )
proof
defpred S1[ set , set ] means ( ex K being Subset of AS st
( K is being_line & $2 = [K,1] & ( ( $1 in the carrier of AS & $1 in K ) or $1 = LDir K ) ) or ex K, X being Subset of AS st
( K is being_line & X is being_plane & $1 = LDir K & $2 = [(PDir X),2] & K '||' X ) );
set VV1 = ProjectivePoints AS;
set VV2 = ProjectiveLines AS;
consider P being Relation of (ProjectivePoints AS),(ProjectiveLines AS) such that
A1: for x, y being set holds
( [x,y] in P iff ( x in ProjectivePoints AS & y in ProjectiveLines AS & S1[x,y] ) ) from RELSET_1:sch_1();
take P ; ::_thesis: for x, y being set holds
( [x,y] in P iff ( ex K being Subset of AS st
( K is being_line & y = [K,1] & ( ( x in the carrier of AS & x in K ) or x = LDir K ) ) or ex K, X being Subset of AS st
( K is being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) )
let x, y be set ; ::_thesis: ( [x,y] in P iff ( ex K being Subset of AS st
( K is being_line & y = [K,1] & ( ( x in the carrier of AS & x in K ) or x = LDir K ) ) or ex K, X being Subset of AS st
( K is being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) )
thus ( not [x,y] in P or ex K being Subset of AS st
( K is being_line & y = [K,1] & ( ( x in the carrier of AS & x in K ) or x = LDir K ) ) or ex K, X being Subset of AS st
( K is being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) by A1; ::_thesis: ( ( ex K being Subset of AS st
( K is being_line & y = [K,1] & ( ( x in the carrier of AS & x in K ) or x = LDir K ) ) or ex K, X being Subset of AS st
( K is being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) implies [x,y] in P )
assume A2: ( ex K being Subset of AS st
( K is being_line & y = [K,1] & ( ( x in the carrier of AS & x in K ) or x = LDir K ) ) or ex K, X being Subset of AS st
( K is being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) ; ::_thesis: [x,y] in P
( x in ProjectivePoints AS & y in ProjectiveLines AS )
proof
A3: now__::_thesis:_(_ex_K_being_Subset_of_AS_st_
(_K_is_being_line_&_y_=_[K,1]_&_(_(_x_in_the_carrier_of_AS_&_x_in_K_)_or_x_=_LDir_K_)_)_implies_(_x_in_ProjectivePoints_AS_&_y_in_ProjectiveLines_AS_)_)
given K being Subset of AS such that A4: K is being_line and
A5: y = [K,1] and
A6: ( ( x in the carrier of AS & x in K ) or x = LDir K ) ; ::_thesis: ( x in ProjectivePoints AS & y in ProjectiveLines AS )
A7: now__::_thesis:_(_x_=_LDir_K_implies_x_in_ProjectivePoints_AS_)
assume x = LDir K ; ::_thesis: x in ProjectivePoints AS
then x in Dir_of_Lines AS by A4, Th14;
hence x in ProjectivePoints AS by XBOOLE_0:def_3; ::_thesis: verum
end;
y in [:(AfLines AS),{1}:] by A4, A5, Th18;
hence ( x in ProjectivePoints AS & y in ProjectiveLines AS ) by A6, A7, XBOOLE_0:def_3; ::_thesis: verum
end;
now__::_thesis:_(_ex_K,_X_being_Subset_of_AS_st_
(_K_is_being_line_&_X_is_being_plane_&_x_=_LDir_K_&_y_=_[(PDir_X),2]_&_K_'||'_X_)_implies_(_x_in_ProjectivePoints_AS_&_y_in_ProjectiveLines_AS_)_)
given K, X being Subset of AS such that A8: K is being_line and
A9: X is being_plane and
A10: x = LDir K and
A11: y = [(PDir X),2] and
K '||' X ; ::_thesis: ( x in ProjectivePoints AS & y in ProjectiveLines AS )
x in Dir_of_Lines AS by A8, A10, Th14;
hence x in ProjectivePoints AS by XBOOLE_0:def_3; ::_thesis: y in ProjectiveLines AS
y in [:(Dir_of_Planes AS),{2}:] by A9, A11, Th19;
hence y in ProjectiveLines AS by XBOOLE_0:def_3; ::_thesis: verum
end;
hence ( x in ProjectivePoints AS & y in ProjectiveLines AS ) by A2, A3; ::_thesis: verum
end;
hence [x,y] in P by A1, A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being Relation of (ProjectivePoints AS),(ProjectiveLines AS) st ( for x, y being set holds
( [x,y] in b1 iff ( ex K being Subset of AS st
( K is being_line & y = [K,1] & ( ( x in the carrier of AS & x in K ) or x = LDir K ) ) or ex K, X being Subset of AS st
( K is being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) ) ) & ( for x, y being set holds
( [x,y] in b2 iff ( ex K being Subset of AS st
( K is being_line & y = [K,1] & ( ( x in the carrier of AS & x in K ) or x = LDir K ) ) or ex K, X being Subset of AS st
( K is being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) ) ) holds
b1 = b2
proof
let P, Q be Relation of (ProjectivePoints AS),(ProjectiveLines AS); ::_thesis: ( ( for x, y being set holds
( [x,y] in P iff ( ex K being Subset of AS st
( K is being_line & y = [K,1] & ( ( x in the carrier of AS & x in K ) or x = LDir K ) ) or ex K, X being Subset of AS st
( K is being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) ) ) & ( for x, y being set holds
( [x,y] in Q iff ( ex K being Subset of AS st
( K is being_line & y = [K,1] & ( ( x in the carrier of AS & x in K ) or x = LDir K ) ) or ex K, X being Subset of AS st
( K is being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) ) ) implies P = Q )
assume that
A12: for x, y being set holds
( [x,y] in P iff ( ex K being Subset of AS st
( K is being_line & y = [K,1] & ( ( x in the carrier of AS & x in K ) or x = LDir K ) ) or ex K, X being Subset of AS st
( K is being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) ) and
A13: for x, y being set holds
( [x,y] in Q iff ( ex K being Subset of AS st
( K is being_line & y = [K,1] & ( ( x in the carrier of AS & x in K ) or x = LDir K ) ) or ex K, X being Subset of AS st
( K is being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) ) ; ::_thesis: P = Q
for x, y being set holds
( [x,y] in P iff [x,y] in Q )
proof
let x, y be set ; ::_thesis: ( [x,y] in P iff [x,y] in Q )
( [x,y] in P iff ( ex K being Subset of AS st
( K is being_line & y = [K,1] & ( ( x in the carrier of AS & x in K ) or x = LDir K ) ) or ex K, X being Subset of AS st
( K is being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) ) by A12;
hence ( [x,y] in P iff [x,y] in Q ) by A13; ::_thesis: verum
end;
hence P = Q by RELAT_1:def_2; ::_thesis: verum
end;
end;
:: deftheorem Def11 defines Proj_Inc AFPROJ:def_11_:_
for AS being AffinSpace
for b2 being Relation of (ProjectivePoints AS),(ProjectiveLines AS) holds
( b2 = Proj_Inc AS iff for x, y being set holds
( [x,y] in b2 iff ( ex K being Subset of AS st
( K is being_line & y = [K,1] & ( ( x in the carrier of AS & x in K ) or x = LDir K ) ) or ex K, X being Subset of AS st
( K is being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) ) );
definition
let AS be AffinSpace;
func Inc_of_Dir AS -> Relation of (Dir_of_Lines AS),(Dir_of_Planes AS) means :Def12: :: AFPROJ:def 12
for x, y being set holds
( [x,y] in it iff ex A, X being Subset of AS st
( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) );
existence
ex b1 being Relation of (Dir_of_Lines AS),(Dir_of_Planes AS) st
for x, y being set holds
( [x,y] in b1 iff ex A, X being Subset of AS st
( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) )
proof
defpred S1[ set , set ] means ex A, X being Subset of AS st
( $1 = LDir A & $2 = PDir X & A is being_line & X is being_plane & A '||' X );
set VV1 = Dir_of_Lines AS;
set VV2 = Dir_of_Planes AS;
consider P being Relation of (Dir_of_Lines AS),(Dir_of_Planes AS) such that
A1: for x, y being set holds
( [x,y] in P iff ( x in Dir_of_Lines AS & y in Dir_of_Planes AS & S1[x,y] ) ) from RELSET_1:sch_1();
take P ; ::_thesis: for x, y being set holds
( [x,y] in P iff ex A, X being Subset of AS st
( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) )
let x, y be set ; ::_thesis: ( [x,y] in P iff ex A, X being Subset of AS st
( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) )
thus ( [x,y] in P implies ex A, X being Subset of AS st
( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) ) by A1; ::_thesis: ( ex A, X being Subset of AS st
( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) implies [x,y] in P )
assume A2: ex A, X being Subset of AS st
( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) ; ::_thesis: [x,y] in P
then A3: y in Dir_of_Planes AS by Th15;
x in Dir_of_Lines AS by A2, Th14;
hence [x,y] in P by A1, A2, A3; ::_thesis: verum
end;
uniqueness
for b1, b2 being Relation of (Dir_of_Lines AS),(Dir_of_Planes AS) st ( for x, y being set holds
( [x,y] in b1 iff ex A, X being Subset of AS st
( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) ) ) & ( for x, y being set holds
( [x,y] in b2 iff ex A, X being Subset of AS st
( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) ) ) holds
b1 = b2
proof
let P, Q be Relation of (Dir_of_Lines AS),(Dir_of_Planes AS); ::_thesis: ( ( for x, y being set holds
( [x,y] in P iff ex A, X being Subset of AS st
( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) ) ) & ( for x, y being set holds
( [x,y] in Q iff ex A, X being Subset of AS st
( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) ) ) implies P = Q )
assume that
A4: for x, y being set holds
( [x,y] in P iff ex A, X being Subset of AS st
( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) ) and
A5: for x, y being set holds
( [x,y] in Q iff ex A, X being Subset of AS st
( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) ) ; ::_thesis: P = Q
for x, y being set holds
( [x,y] in P iff [x,y] in Q )
proof
let x, y be set ; ::_thesis: ( [x,y] in P iff [x,y] in Q )
( [x,y] in P iff ex A, X being Subset of AS st
( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) ) by A4;
hence ( [x,y] in P iff [x,y] in Q ) by A5; ::_thesis: verum
end;
hence P = Q by RELAT_1:def_2; ::_thesis: verum
end;
end;
:: deftheorem Def12 defines Inc_of_Dir AFPROJ:def_12_:_
for AS being AffinSpace
for b2 being Relation of (Dir_of_Lines AS),(Dir_of_Planes AS) holds
( b2 = Inc_of_Dir AS iff for x, y being set holds
( [x,y] in b2 iff ex A, X being Subset of AS st
( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) ) );
definition
let AS be AffinSpace;
func IncProjSp_of AS -> strict IncProjStr equals :: AFPROJ:def 13
IncProjStr(# (ProjectivePoints AS),(ProjectiveLines AS),(Proj_Inc AS) #);
correctness
coherence
IncProjStr(# (ProjectivePoints AS),(ProjectiveLines AS),(Proj_Inc AS) #) is strict IncProjStr ;
;
end;
:: deftheorem defines IncProjSp_of AFPROJ:def_13_:_
for AS being AffinSpace holds IncProjSp_of AS = IncProjStr(# (ProjectivePoints AS),(ProjectiveLines AS),(Proj_Inc AS) #);
definition
let AS be AffinSpace;
func ProjHorizon AS -> strict IncProjStr equals :: AFPROJ:def 14
IncProjStr(# (Dir_of_Lines AS),(Dir_of_Planes AS),(Inc_of_Dir AS) #);
correctness
coherence
IncProjStr(# (Dir_of_Lines AS),(Dir_of_Planes AS),(Inc_of_Dir AS) #) is strict IncProjStr ;
;
end;
:: deftheorem defines ProjHorizon AFPROJ:def_14_:_
for AS being AffinSpace holds ProjHorizon AS = IncProjStr(# (Dir_of_Lines AS),(Dir_of_Planes AS),(Inc_of_Dir AS) #);
theorem Th20: :: AFPROJ:20
for AS being AffinSpace
for x being set holds
( x is POINT of (IncProjSp_of AS) iff ( x is Element of AS or ex X being Subset of AS st
( x = LDir X & X is being_line ) ) )
proof
let AS be AffinSpace; ::_thesis: for x being set holds
( x is POINT of (IncProjSp_of AS) iff ( x is Element of AS or ex X being Subset of AS st
( x = LDir X & X is being_line ) ) )
let x be set ; ::_thesis: ( x is POINT of (IncProjSp_of AS) iff ( x is Element of AS or ex X being Subset of AS st
( x = LDir X & X is being_line ) ) )
A1: now__::_thesis:_(_(_x_is_Element_of_AS_or_ex_X_being_Subset_of_AS_st_
(_x_=_LDir_X_&_X_is_being_line_)_)_implies_x_is_POINT_of_(IncProjSp_of_AS)_)
A2: now__::_thesis:_(_ex_X_being_Subset_of_AS_st_
(_x_=_LDir_X_&_X_is_being_line_)_implies_x_is_POINT_of_(IncProjSp_of_AS)_)
given X being Subset of AS such that A3: x = LDir X and
A4: X is being_line ; ::_thesis: x is POINT of (IncProjSp_of AS)
x in Dir_of_Lines AS by A3, A4, Th14;
hence x is POINT of (IncProjSp_of AS) by XBOOLE_0:def_3; ::_thesis: verum
end;
assume ( x is Element of AS or ex X being Subset of AS st
( x = LDir X & X is being_line ) ) ; ::_thesis: x is POINT of (IncProjSp_of AS)
hence x is POINT of (IncProjSp_of AS) by A2, XBOOLE_0:def_3; ::_thesis: verum
end;
now__::_thesis:_(_not_x_is_POINT_of_(IncProjSp_of_AS)_or_x_is_Element_of_AS_or_ex_X_being_Subset_of_AS_st_
(_x_=_LDir_X_&_X_is_being_line_)_)
assume A5: x is POINT of (IncProjSp_of AS) ; ::_thesis: ( x is Element of AS or ex X being Subset of AS st
( x = LDir X & X is being_line ) )
( x in Dir_of_Lines AS implies ex X being Subset of AS st
( x = LDir X & X is being_line ) ) by Th14;
hence ( x is Element of AS or ex X being Subset of AS st
( x = LDir X & X is being_line ) ) by A5, XBOOLE_0:def_3; ::_thesis: verum
end;
hence ( x is POINT of (IncProjSp_of AS) iff ( x is Element of AS or ex X being Subset of AS st
( x = LDir X & X is being_line ) ) ) by A1; ::_thesis: verum
end;
theorem :: AFPROJ:21
for AS being AffinSpace
for x being set holds
( x is Element of the Points of (ProjHorizon AS) iff ex X being Subset of AS st
( x = LDir X & X is being_line ) ) by Th14;
theorem Th22: :: AFPROJ:22
for AS being AffinSpace
for x being set st x is Element of the Points of (ProjHorizon AS) holds
x is POINT of (IncProjSp_of AS)
proof
let AS be AffinSpace; ::_thesis: for x being set st x is Element of the Points of (ProjHorizon AS) holds
x is POINT of (IncProjSp_of AS)
let x be set ; ::_thesis: ( x is Element of the Points of (ProjHorizon AS) implies x is POINT of (IncProjSp_of AS) )
assume x is Element of the Points of (ProjHorizon AS) ; ::_thesis: x is POINT of (IncProjSp_of AS)
then ex X being Subset of AS st
( x = LDir X & X is being_line ) by Th14;
hence x is POINT of (IncProjSp_of AS) by Th20; ::_thesis: verum
end;
theorem Th23: :: AFPROJ:23
for AS being AffinSpace
for x being set holds
( x is LINE of (IncProjSp_of AS) iff ex X being Subset of AS st
( ( x = [X,1] & X is being_line ) or ( x = [(PDir X),2] & X is being_plane ) ) )
proof
let AS be AffinSpace; ::_thesis: for x being set holds
( x is LINE of (IncProjSp_of AS) iff ex X being Subset of AS st
( ( x = [X,1] & X is being_line ) or ( x = [(PDir X),2] & X is being_plane ) ) )
let x be set ; ::_thesis: ( x is LINE of (IncProjSp_of AS) iff ex X being Subset of AS st
( ( x = [X,1] & X is being_line ) or ( x = [(PDir X),2] & X is being_plane ) ) )
A1: now__::_thesis:_(_ex_X_being_Subset_of_AS_st_
(_(_x_=_[X,1]_&_X_is_being_line_)_or_(_x_=_[(PDir_X),2]_&_X_is_being_plane_)_)_implies_x_is_LINE_of_(IncProjSp_of_AS)_)
given X being Subset of AS such that A2: ( ( x = [X,1] & X is being_line ) or ( x = [(PDir X),2] & X is being_plane ) ) ; ::_thesis: x is LINE of (IncProjSp_of AS)
A3: now__::_thesis:_(_x_=_[(PDir_X),2]_&_X_is_being_plane_implies_x_is_LINE_of_(IncProjSp_of_AS)_)
assume that
A4: x = [(PDir X),2] and
A5: X is being_plane ; ::_thesis: x is LINE of (IncProjSp_of AS)
x in [:(Dir_of_Planes AS),{2}:] by A4, A5, Th19;
hence x is LINE of (IncProjSp_of AS) by XBOOLE_0:def_3; ::_thesis: verum
end;
now__::_thesis:_(_x_=_[X,1]_&_X_is_being_line_implies_x_is_LINE_of_(IncProjSp_of_AS)_)
assume that
A6: x = [X,1] and
A7: X is being_line ; ::_thesis: x is LINE of (IncProjSp_of AS)
x in [:(AfLines AS),{1}:] by A6, A7, Th18;
hence x is LINE of (IncProjSp_of AS) by XBOOLE_0:def_3; ::_thesis: verum
end;
hence x is LINE of (IncProjSp_of AS) by A2, A3; ::_thesis: verum
end;
now__::_thesis:_(_x_is_LINE_of_(IncProjSp_of_AS)_implies_ex_X_being_Subset_of_AS_st_
(_(_x_=_[X,1]_&_X_is_being_line_)_or_(_x_=_[(PDir_X),2]_&_X_is_being_plane_)_)_)
A8: ( x in [:(Dir_of_Planes AS),{2}:] implies ex X being Subset of AS st
( ( x = [X,1] & X is being_line ) or ( x = [(PDir X),2] & X is being_plane ) ) ) by Th19;
assume A9: x is LINE of (IncProjSp_of AS) ; ::_thesis: ex X being Subset of AS st
( ( x = [X,1] & X is being_line ) or ( x = [(PDir X),2] & X is being_plane ) )
( x in [:(AfLines AS),{1}:] implies ex X being Subset of AS st
( ( x = [X,1] & X is being_line ) or ( x = [(PDir X),2] & X is being_plane ) ) ) by Th18;
hence ex X being Subset of AS st
( ( x = [X,1] & X is being_line ) or ( x = [(PDir X),2] & X is being_plane ) ) by A9, A8, XBOOLE_0:def_3; ::_thesis: verum
end;
hence ( x is LINE of (IncProjSp_of AS) iff ex X being Subset of AS st
( ( x = [X,1] & X is being_line ) or ( x = [(PDir X),2] & X is being_plane ) ) ) by A1; ::_thesis: verum
end;
theorem :: AFPROJ:24
for AS being AffinSpace
for x being set holds
( x is Element of the Lines of (ProjHorizon AS) iff ex X being Subset of AS st
( x = PDir X & X is being_plane ) ) by Th15;
theorem Th25: :: AFPROJ:25
for AS being AffinSpace
for x being set st x is Element of the Lines of (ProjHorizon AS) holds
[x,2] is LINE of (IncProjSp_of AS)
proof
let AS be AffinSpace; ::_thesis: for x being set st x is Element of the Lines of (ProjHorizon AS) holds
[x,2] is LINE of (IncProjSp_of AS)
let x be set ; ::_thesis: ( x is Element of the Lines of (ProjHorizon AS) implies [x,2] is LINE of (IncProjSp_of AS) )
assume x is Element of the Lines of (ProjHorizon AS) ; ::_thesis: [x,2] is LINE of (IncProjSp_of AS)
then ex X being Subset of AS st
( x = PDir X & X is being_plane ) by Th15;
hence [x,2] is LINE of (IncProjSp_of AS) by Th23; ::_thesis: verum
end;
theorem Th26: :: AFPROJ:26
for AS being AffinSpace
for x being Element of AS
for X being Subset of AS
for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st x = a & [X,1] = A holds
( a on A iff ( X is being_line & x in X ) )
proof
let AS be AffinSpace; ::_thesis: for x being Element of AS
for X being Subset of AS
for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st x = a & [X,1] = A holds
( a on A iff ( X is being_line & x in X ) )
let x be Element of AS; ::_thesis: for X being Subset of AS
for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st x = a & [X,1] = A holds
( a on A iff ( X is being_line & x in X ) )
let X be Subset of AS; ::_thesis: for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st x = a & [X,1] = A holds
( a on A iff ( X is being_line & x in X ) )
let a be POINT of (IncProjSp_of AS); ::_thesis: for A being LINE of (IncProjSp_of AS) st x = a & [X,1] = A holds
( a on A iff ( X is being_line & x in X ) )
let A be LINE of (IncProjSp_of AS); ::_thesis: ( x = a & [X,1] = A implies ( a on A iff ( X is being_line & x in X ) ) )
assume that
A1: x = a and
A2: [X,1] = A ; ::_thesis: ( a on A iff ( X is being_line & x in X ) )
A3: now__::_thesis:_(_a_on_A_implies_(_X_is_being_line_&_x_in_X_)_)
A4: now__::_thesis:_(_ex_K_being_Subset_of_AS_st_
(_K_is_being_line_&_[X,1]_=_[K,1]_&_(_(_x_in_the_carrier_of_AS_&_x_in_K_)_or_x_=_LDir_K_)_)_implies_(_X_is_being_line_&_x_in_X_)_)
given K being Subset of AS such that A5: K is being_line and
A6: [X,1] = [K,1] and
A7: ( ( x in the carrier of AS & x in K ) or x = LDir K ) ; ::_thesis: ( X is being_line & x in X )
A8: now__::_thesis:_not_x_=_LDir_K
assume x = LDir K ; ::_thesis: contradiction
then x in Dir_of_Lines AS by A5, Th14;
then the carrier of AS /\ (Dir_of_Lines AS) <> {} by 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;
X = [K,1] `1 by A6, MCART_1:7
.= K ;
hence ( X is being_line & x in X ) by A5, A7, A8; ::_thesis: verum
end;
assume a on A ; ::_thesis: ( X is being_line & x in X )
then A9: [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 x = LDir K or not [X,1] = [(PDir X9),2] or not K '||' X9 ) by XTUPLE_0:1;
hence ( X is being_line & x in X ) by A1, A2, A9, A4, Def11; ::_thesis: verum
end;
now__::_thesis:_(_X_is_being_line_&_x_in_X_implies_a_on_A_)
assume that
A10: X is being_line and
A11: x in X ; ::_thesis: a on A
[x,[X,1]] in Proj_Inc AS by A10, A11, Def11;
hence a on A by A1, A2, INCSP_1:def_1; ::_thesis: verum
end;
hence ( a on A iff ( X is being_line & x in X ) ) by A3; ::_thesis: verum
end;
theorem Th27: :: AFPROJ:27
for AS being AffinSpace
for x being Element of AS
for X being Subset of AS
for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st x = a & [(PDir X),2] = A holds
not a on A
proof
let AS be AffinSpace; ::_thesis: for x being Element of AS
for X being Subset of AS
for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st x = a & [(PDir X),2] = A holds
not a on A
let x be Element of AS; ::_thesis: for X being Subset of AS
for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st x = a & [(PDir X),2] = A holds
not a on A
let X be Subset of AS; ::_thesis: for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st x = a & [(PDir X),2] = A holds
not a on A
let a be POINT of (IncProjSp_of AS); ::_thesis: for A being LINE of (IncProjSp_of AS) st x = a & [(PDir X),2] = A holds
not a on A
let A be LINE of (IncProjSp_of AS); ::_thesis: ( x = a & [(PDir X),2] = A implies not a on A )
assume that
A1: x = a and
A2: [(PDir X),2] = A ; ::_thesis: not a on A
A3: now__::_thesis:_for_K_being_Subset_of_AS_holds_
(_not_K_is_being_line_or_not_[(PDir_X),2]_=_[K,1]_or_(_not_(_x_in_the_carrier_of_AS_&_x_in_K_)_&_not_x_=_LDir_K_)_)
given K being Subset of AS such that K is being_line and
A4: [(PDir X),2] = [K,1] and
( ( x in the carrier of AS & x in K ) or x = LDir K ) ; ::_thesis: contradiction
2 = [K,1] `2 by A4, MCART_1:7
.= 1 ;
hence contradiction ; ::_thesis: verum
end;
A5: now__::_thesis:_for_K,_X9_being_Subset_of_AS_holds_
(_not_K_is_being_line_or_not_X9_is_being_plane_or_not_x_=_LDir_K_or_not_[(PDir_X),2]_=_[(PDir_X9),2]_or_not_K_'||'_X9_)
given K, X9 being Subset of AS such that A6: K is being_line and
X9 is being_plane and
A7: x = LDir K and
[(PDir X),2] = [(PDir X9),2] and
K '||' X9 ; ::_thesis: contradiction
x in Dir_of_Lines AS by A6, A7, Th14;
then the carrier of AS /\ (Dir_of_Lines AS) <> {} by 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;
assume a on A ; ::_thesis: contradiction
then [a,A] in the Inc of (IncProjSp_of AS) by INCSP_1:def_1;
hence contradiction by A1, A2, A3, A5, Def11; ::_thesis: verum
end;
theorem Th28: :: AFPROJ:28
for AS being AffinSpace
for Y, X 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 )
proof
let AS be AffinSpace; ::_thesis: for Y, X 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 Y, X 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
end;
theorem Th29: :: AFPROJ:29
for AS being AffinSpace
for Y, X being Subset of AS
for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st a = LDir Y & A = [(PDir X),2] & Y is being_line & X is being_plane holds
( a on A iff Y '||' X )
proof
let AS be AffinSpace; ::_thesis: for Y, X being Subset of AS
for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st a = LDir Y & A = [(PDir X),2] & Y is being_line & X is being_plane holds
( a on A iff Y '||' X )
let Y, X 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 & A = [(PDir X),2] & Y is being_line & X is being_plane 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 & A = [(PDir X),2] & Y is being_line & X is being_plane holds
( a on A iff Y '||' X )
let A be LINE of (IncProjSp_of AS); ::_thesis: ( a = LDir Y & A = [(PDir X),2] & Y is being_line & X is being_plane implies ( a on A iff Y '||' X ) )
assume that
A1: a = LDir Y and
A2: A = [(PDir X),2] and
A3: Y is being_line and
A4: X is being_plane ; ::_thesis: ( a on A iff Y '||' X )
A5: now__::_thesis:_(_a_on_A_implies_Y_'||'_X_)
A6: now__::_thesis:_(_ex_K,_X9_being_Subset_of_AS_st_
(_K_is_being_line_&_X9_is_being_plane_&_LDir_Y_=_LDir_K_&_[(PDir_X),2]_=_[(PDir_X9),2]_&_K_'||'_X9_)_implies_Y_'||'_X_)
given K, X9 being Subset of AS such that A7: K is being_line and
A8: X9 is being_plane and
A9: LDir Y = LDir K and
A10: [(PDir X),2] = [(PDir X9),2] and
A11: K '||' X9 ; ::_thesis: Y '||' X
A12: X9 in AfPlanes AS by A8;
A13: Class ((PlanesParallelity AS),X9) = PDir X9 ;
PDir X = PDir X9 by A10, XTUPLE_0:1;
then X in Class ((PlanesParallelity AS),X9) by A12, EQREL_1:23;
then A14: ex X99 being Subset of AS st
( X = X99 & X99 is being_plane & X9 '||' X99 ) by A8, A13, Th10;
K in AfLines AS by A7;
then A15: Y in Class ((LinesParallelity AS),K) by A9, EQREL_1:23;
Class ((LinesParallelity AS),K) = LDir K ;
then consider K9 being Subset of AS such that
A16: Y = K9 and
A17: K9 is being_line and
A18: K '||' K9 by A7, A15, Th9;
K // K9 by A7, A17, A18, AFF_4:40;
then K9 '||' X9 by A11, AFF_4:56;
hence Y '||' X by A8, A16, A14, AFF_4:59, AFF_4:60; ::_thesis: verum
end;
assume a on A ; ::_thesis: Y '||' X
then A19: [a,A] in the Inc of (IncProjSp_of AS) by INCSP_1:def_1;
for K being Subset of AS holds
( not K is being_line or not [(PDir X),2] = [K,1] or ( not ( LDir Y in the carrier of AS & LDir Y in K ) & not LDir Y = LDir K ) ) by XTUPLE_0:1;
hence Y '||' X by A1, A2, A19, A6, Def11; ::_thesis: verum
end;
now__::_thesis:_(_Y_'||'_X_implies_a_on_A_)
assume Y '||' X ; ::_thesis: a on A
then [(LDir Y),[(PDir X),2]] in Proj_Inc AS by A3, A4, Def11;
hence a on A by A1, A2, INCSP_1:def_1; ::_thesis: verum
end;
hence ( a on A iff Y '||' X ) by A5; ::_thesis: verum
end;
theorem Th30: :: AFPROJ:30
for AS being AffinSpace
for X being Subset of AS
for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st X is being_line & a = LDir X & A = [X,1] holds
a on A
proof
let AS be AffinSpace; ::_thesis: for X being Subset of AS
for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st X is being_line & a = LDir X & A = [X,1] holds
a on A
let X be Subset of AS; ::_thesis: for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st X is being_line & a = LDir X & A = [X,1] holds
a on A
let a be POINT of (IncProjSp_of AS); ::_thesis: for A being LINE of (IncProjSp_of AS) st X is being_line & a = LDir X & A = [X,1] holds
a on A
let A be LINE of (IncProjSp_of AS); ::_thesis: ( X is being_line & a = LDir X & A = [X,1] implies a on A )
assume that
A1: X is being_line and
A2: a = LDir X and
A3: A = [X,1] ; ::_thesis: a on A
X // X by A1, AFF_1:41;
then X '||' X by A1, AFF_4:40;
hence a on A by A1, A2, A3, Th28; ::_thesis: verum
end;
theorem Th31: :: AFPROJ:31
for AS being 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 X is being_line & Y is being_plane & X c= Y & a = LDir X & A = [(PDir Y),2] holds
a on A
proof
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 X is being_line & Y is being_plane & X c= Y & a = LDir X & A = [(PDir Y),2] holds
a on A
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 X is being_line & Y is being_plane & X c= Y & a = LDir X & A = [(PDir Y),2] holds
a on A
let a be POINT of (IncProjSp_of AS); ::_thesis: for A being LINE of (IncProjSp_of AS) st X is being_line & Y is being_plane & X c= Y & a = LDir X & A = [(PDir Y),2] holds
a on A
let A be LINE of (IncProjSp_of AS); ::_thesis: ( X is being_line & Y is being_plane & X c= Y & a = LDir X & A = [(PDir Y),2] implies a on A )
assume that
A1: X is being_line and
A2: Y is being_plane and
A3: X c= Y and
A4: a = LDir X and
A5: A = [(PDir Y),2] ; ::_thesis: a on A
X '||' Y by A1, A2, A3, AFF_4:42;
hence a on A by A1, A2, A4, A5, Th29; ::_thesis: verum
end;
theorem Th32: :: AFPROJ:32
for AS being AffinSpace
for Y, X, X9 being Subset of AS
for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st Y is being_plane & X c= Y & X9 // X & a = LDir X9 & A = [(PDir Y),2] holds
a on A
proof
let AS be AffinSpace; ::_thesis: for Y, X, X9 being Subset of AS
for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st Y is being_plane & X c= Y & X9 // X & a = LDir X9 & A = [(PDir Y),2] holds
a on A
let Y, X, X9 be Subset of AS; ::_thesis: for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st Y is being_plane & X c= Y & X9 // X & a = LDir X9 & A = [(PDir Y),2] holds
a on A
let a be POINT of (IncProjSp_of AS); ::_thesis: for A being LINE of (IncProjSp_of AS) st Y is being_plane & X c= Y & X9 // X & a = LDir X9 & A = [(PDir Y),2] holds
a on A
let A be LINE of (IncProjSp_of AS); ::_thesis: ( Y is being_plane & X c= Y & X9 // X & a = LDir X9 & A = [(PDir Y),2] implies a on A )
assume that
A1: Y is being_plane and
A2: X c= Y and
A3: X9 // X and
A4: a = LDir X9 and
A5: A = [(PDir Y),2] ; ::_thesis: a on A
X is being_line by A3, AFF_1:36;
then A6: X9 '||' Y by A1, A2, A3, AFF_4:42, AFF_4:56;
X9 is being_line by A3, AFF_1:36;
hence a on A by A1, A4, A5, A6, Th29; ::_thesis: verum
end;
theorem :: AFPROJ:33
for AS being AffinSpace
for X being Subset of AS
for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st A = [(PDir X),2] & X is being_plane & a on A holds
not a is Element of AS by Th27;
theorem Th34: :: AFPROJ:34
for AS being AffinSpace
for X being Subset of AS
for p being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st A = [X,1] & X is being_line & p on A & p is not Element of AS holds
p = LDir X
proof
let AS be AffinSpace; ::_thesis: for X being Subset of AS
for p being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st A = [X,1] & X is being_line & p on A & p is not Element of AS holds
p = LDir X
let X be Subset of AS; ::_thesis: for p being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st A = [X,1] & X is being_line & p on A & p is not Element of AS holds
p = LDir X
let p be POINT of (IncProjSp_of AS); ::_thesis: for A being LINE of (IncProjSp_of AS) st A = [X,1] & X is being_line & p on A & p is not Element of AS holds
p = LDir X
let A be LINE of (IncProjSp_of AS); ::_thesis: ( A = [X,1] & X is being_line & p on A & p is not Element of AS implies p = LDir X )
assume that
A1: A = [X,1] and
A2: X is being_line and
A3: p on A and
A4: p is not Element of AS ; ::_thesis: p = LDir X
consider Xp being Subset of AS such that
A5: p = LDir Xp and
A6: Xp is being_line by A4, Th20;
Xp '||' X by A1, A2, A3, A5, A6, Th28;
hence p = LDir X by A2, A5, A6, Th12; ::_thesis: verum
end;
theorem Th35: :: AFPROJ:35
for AS being AffinSpace
for X being Subset of AS
for p, a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st A = [X,1] & X is being_line & p on A & a on A & a <> p & p is not Element of AS holds
a is Element of AS
proof
let AS be AffinSpace; ::_thesis: for X being Subset of AS
for p, a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st A = [X,1] & X is being_line & p on A & a on A & a <> p & p is not Element of AS holds
a is Element of AS
let X be Subset of AS; ::_thesis: for p, a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st A = [X,1] & X is being_line & p on A & a on A & a <> p & p is not Element of AS holds
a is Element of AS
let p, a be POINT of (IncProjSp_of AS); ::_thesis: for A being LINE of (IncProjSp_of AS) st A = [X,1] & X is being_line & p on A & a on A & a <> p & p is not Element of AS holds
a is Element of AS
let A be LINE of (IncProjSp_of AS); ::_thesis: ( A = [X,1] & X is being_line & p on A & a on A & a <> p & p is not Element of AS implies a is Element of AS )
assume that
A1: A = [X,1] and
A2: X is being_line and
A3: p on A and
A4: a on A and
A5: a <> p and
A6: p is not Element of AS ; ::_thesis: a is Element of AS
assume a is not Element of AS ; ::_thesis: contradiction
then a = LDir X by A1, A2, A4, Th34;
hence contradiction by A1, A2, A3, A5, A6, Th34; ::_thesis: verum
end;
theorem Th36: :: AFPROJ:36
for AS being AffinSpace
for X, Y being Subset of AS
for a being Element of the Points of (ProjHorizon AS)
for A being Element of the Lines of (ProjHorizon AS) st a = LDir X & A = PDir Y & X is being_line & Y is being_plane holds
( a on A iff X '||' Y )
proof
let AS be AffinSpace; ::_thesis: for X, Y being Subset of AS
for a being Element of the Points of (ProjHorizon AS)
for A being Element of the Lines of (ProjHorizon AS) st a = LDir X & A = PDir Y & X is being_line & Y is being_plane holds
( a on A iff X '||' Y )
let X, Y be Subset of AS; ::_thesis: for a being Element of the Points of (ProjHorizon AS)
for A being Element of the Lines of (ProjHorizon AS) st a = LDir X & A = PDir Y & X is being_line & Y is being_plane holds
( a on A iff X '||' Y )
let a be Element of the Points of (ProjHorizon AS); ::_thesis: for A being Element of the Lines of (ProjHorizon AS) st a = LDir X & A = PDir Y & X is being_line & Y is being_plane holds
( a on A iff X '||' Y )
let A be Element of the Lines of (ProjHorizon AS); ::_thesis: ( a = LDir X & A = PDir Y & X is being_line & Y is being_plane implies ( a on A iff X '||' Y ) )
assume that
A1: a = LDir X and
A2: A = PDir Y and
A3: X is being_line and
A4: Y is being_plane ; ::_thesis: ( a on A iff X '||' Y )
A5: now__::_thesis:_(_a_on_A_implies_X_'||'_Y_)
assume a on A ; ::_thesis: X '||' Y
then [a,A] in the Inc of (ProjHorizon AS) by INCSP_1:def_1;
then consider X9, Y9 being Subset of AS such that
A6: a = LDir X9 and
A7: A = PDir Y9 and
A8: X9 is being_line and
A9: Y9 is being_plane and
A10: X9 '||' Y9 by Def12;
X // X9 by A1, A3, A6, A8, Th11;
then A11: X '||' Y9 by A10, AFF_4:56;
Y9 '||' Y by A2, A4, A7, A9, Th13;
hence X '||' Y by A9, A11, AFF_4:59, AFF_4:60; ::_thesis: verum
end;
now__::_thesis:_(_X_'||'_Y_implies_a_on_A_)
assume X '||' Y ; ::_thesis: a on A
then [a,A] in Inc_of_Dir AS by A1, A2, A3, A4, Def12;
hence a on A by INCSP_1:def_1; ::_thesis: verum
end;
hence ( a on A iff X '||' Y ) by A5; ::_thesis: verum
end;
theorem Th37: :: AFPROJ:37
for AS being AffinSpace
for a being Element of the Points of (ProjHorizon AS)
for a9 being Element of the Points of (IncProjSp_of AS)
for A being Element of the Lines of (ProjHorizon AS)
for A9 being LINE of (IncProjSp_of AS) st a9 = a & A9 = [A,2] holds
( a on A iff a9 on A9 )
proof
let AS be AffinSpace; ::_thesis: for a being Element of the Points of (ProjHorizon AS)
for a9 being Element of the Points of (IncProjSp_of AS)
for A being Element of the Lines of (ProjHorizon AS)
for A9 being LINE of (IncProjSp_of AS) st a9 = a & A9 = [A,2] holds
( a on A iff a9 on A9 )
let a be Element of the Points of (ProjHorizon AS); ::_thesis: for a9 being Element of the Points of (IncProjSp_of AS)
for A being Element of the Lines of (ProjHorizon AS)
for A9 being LINE of (IncProjSp_of AS) st a9 = a & A9 = [A,2] holds
( a on A iff a9 on A9 )
let a9 be Element of the Points of (IncProjSp_of AS); ::_thesis: for A being Element of the Lines of (ProjHorizon AS)
for A9 being LINE of (IncProjSp_of AS) st a9 = a & A9 = [A,2] holds
( a on A iff a9 on A9 )
let A be Element of the Lines of (ProjHorizon AS); ::_thesis: for A9 being LINE of (IncProjSp_of AS) st a9 = a & A9 = [A,2] holds
( a on A iff a9 on A9 )
let A9 be LINE of (IncProjSp_of AS); ::_thesis: ( a9 = a & A9 = [A,2] implies ( a on A iff a9 on A9 ) )
assume that
A1: a9 = a and
A2: A9 = [A,2] ; ::_thesis: ( a on A iff a9 on A9 )
consider X being Subset of AS such that
A3: a = LDir X and
A4: X is being_line by Th14;
consider Y being Subset of AS such that
A5: A = PDir Y and
A6: Y is being_plane by Th15;
A7: now__::_thesis:_(_a9_on_A9_implies_a_on_A_)
assume a9 on A9 ; ::_thesis: a on A
then X '||' Y by A1, A2, A3, A4, A5, A6, Th29;
hence a on A by A3, A4, A5, A6, Th36; ::_thesis: verum
end;
now__::_thesis:_(_a_on_A_implies_a9_on_A9_)
assume a on A ; ::_thesis: a9 on A9
then X '||' Y by A3, A4, A5, A6, Th36;
hence a9 on A9 by A1, A2, A3, A4, A5, A6, Th29; ::_thesis: verum
end;
hence ( a on A iff a9 on A9 ) by A7; ::_thesis: verum
end;
theorem Th38: :: AFPROJ:38
for AS being AffinSpace
for a, b being Element of the Points of (ProjHorizon AS)
for A, K being Element of the Lines of (ProjHorizon AS) st a on A & a on K & b on A & b on K & not a = b holds
A = K
proof
let AS be AffinSpace; ::_thesis: for a, b being Element of the Points of (ProjHorizon AS)
for A, K being Element of the Lines of (ProjHorizon AS) st a on A & a on K & b on A & b on K & not a = b holds
A = K
let a, b be Element of the Points of (ProjHorizon AS); ::_thesis: for A, K being Element of the Lines of (ProjHorizon AS) st a on A & a on K & b on A & b on K & not a = b holds
A = K
let A, K be Element of the Lines of (ProjHorizon AS); ::_thesis: ( a on A & a on K & b on A & b on K & not a = b implies A = K )
assume that
A1: a on A and
A2: a on K and
A3: b on A and
A4: b on K ; ::_thesis: ( a = b or A = K )
consider Y9 being Subset of AS such that
A5: b = LDir Y9 and
A6: Y9 is being_line by Th14;
consider X9 being Subset of AS such that
A7: K = PDir X9 and
A8: X9 is being_plane by Th15;
A9: Y9 '||' X9 by A4, A5, A6, A7, A8, Th36;
consider Y being Subset of AS such that
A10: a = LDir Y and
A11: Y is being_line by Th14;
assume a <> b ; ::_thesis: A = K
then A12: not Y // Y9 by A10, A11, A5, A6, Th11;
consider X being Subset of AS such that
A13: A = PDir X and
A14: X is being_plane by Th15;
A15: Y9 '||' X by A3, A5, A6, A13, A14, Th36;
A16: Y '||' X9 by A2, A10, A11, A7, A8, Th36;
Y '||' X by A1, A10, A11, A13, A14, Th36;
then X '||' X9 by A11, A6, A14, A8, A12, A16, A15, A9, Th5;
hence A = K by A13, A14, A7, A8, Th13; ::_thesis: verum
end;
theorem Th39: :: AFPROJ:39
for AS being AffinSpace
for A being Element of the Lines of (ProjHorizon AS) ex a, b, c being Element of the Points of (ProjHorizon AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )
proof
let AS be AffinSpace; ::_thesis: for A being Element of the Lines of (ProjHorizon AS) ex a, b, c being Element of the Points of (ProjHorizon AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )
let A be Element of the Lines of (ProjHorizon AS); ::_thesis: ex a, b, c being Element of the Points of (ProjHorizon AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )
consider X being Subset of AS such that
A1: A = PDir X and
A2: X is being_plane by Th15;
consider x, y, z being Element of AS such that
A3: x in X and
A4: y in X and
A5: z in X and
A6: not LIN x,y,z by A2, AFF_4:34;
A7: y <> z by A6, AFF_1:7;
then A8: Line (y,z) is being_line by AFF_1:def_3;
then A9: Line (y,z) '||' X by A2, A4, A5, A7, AFF_4:19, AFF_4:42;
A10: z <> x by A6, AFF_1:7;
then A11: Line (x,z) is being_line by AFF_1:def_3;
then A12: Line (x,z) '||' X by A2, A3, A5, A10, AFF_4:19, AFF_4:42;
A13: x <> y by A6, AFF_1:7;
then A14: Line (x,y) is being_line by AFF_1:def_3;
then reconsider a = LDir (Line (x,y)), b = LDir (Line (y,z)), c = LDir (Line (x,z)) as Element of the Points of (ProjHorizon AS) by A8, A11, Th14;
take a ; ::_thesis: ex b, c being Element of the Points of (ProjHorizon AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )
take b ; ::_thesis: ex c being Element of the Points of (ProjHorizon AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )
take c ; ::_thesis: ( a on A & b on A & c on A & a <> b & b <> c & c <> a )
Line (x,y) '||' X by A2, A3, A4, A13, A14, AFF_4:19, AFF_4:42;
hence ( a on A & b on A & c on A ) by A1, A2, A14, A8, A11, A9, A12, Th36; ::_thesis: ( a <> b & b <> c & c <> a )
A15: x in Line (x,y) by AFF_1:15;
A16: z in Line (y,z) by AFF_1:15;
A17: y in Line (x,y) by AFF_1:15;
A18: y in Line (y,z) by AFF_1:15;
thus a <> b ::_thesis: ( b <> c & c <> a )
proof
assume not a <> b ; ::_thesis: contradiction
then Line (x,y) // Line (y,z) by A14, A8, Th11;
then z in Line (x,y) by A17, A18, A16, AFF_1:45;
hence contradiction by A6, A14, A15, A17, AFF_1:21; ::_thesis: verum
end;
A19: z in Line (x,z) by AFF_1:15;
A20: x in Line (x,z) by AFF_1:15;
thus b <> c ::_thesis: c <> a
proof
assume not b <> c ; ::_thesis: contradiction
then Line (y,z) // Line (x,z) by A8, A11, Th11;
then x in Line (y,z) by A16, A20, A19, AFF_1:45;
hence contradiction by A6, A8, A18, A16, AFF_1:21; ::_thesis: verum
end;
thus c <> a ::_thesis: verum
proof
assume not c <> a ; ::_thesis: contradiction
then Line (x,y) // Line (x,z) by A14, A11, Th11;
then z in Line (x,y) by A15, A20, A19, AFF_1:45;
hence contradiction by A6, A14, A15, A17, AFF_1:21; ::_thesis: verum
end;
end;
theorem Th40: :: AFPROJ:40
for AS being AffinSpace
for a, b being Element of the Points of (ProjHorizon AS) ex A being Element of the Lines of (ProjHorizon AS) st
( a on A & b on A )
proof
let AS be AffinSpace; ::_thesis: for a, b being Element of the Points of (ProjHorizon AS) ex A being Element of the Lines of (ProjHorizon AS) st
( a on A & b on A )
let a, b be Element of the Points of (ProjHorizon AS); ::_thesis: ex A being Element of the Lines of (ProjHorizon AS) st
( a on A & b on A )
consider X being Subset of AS such that
A1: a = LDir X and
A2: X is being_line by Th14;
consider X9 being Subset of AS such that
A3: b = LDir X9 and
A4: X9 is being_line by Th14;
consider x, y being Element of AS such that
A5: x in X9 and
y in X9 and
x <> y by A4, AFF_1:19;
A6: x in x * X by A2, AFF_4:def_3;
x * X is being_line by A2, AFF_4:27;
then consider Z being Subset of AS such that
A7: X9 c= Z and
A8: x * X c= Z and
A9: Z is being_plane by A4, A5, A6, AFF_4:38;
A10: X9 '||' Z by A4, A7, A9, AFF_4:42;
reconsider A = PDir Z as Element of the Lines of (ProjHorizon AS) by A9, Th15;
take A ; ::_thesis: ( a on A & b on A )
X // x * X by A2, AFF_4:def_3;
then X '||' Z by A2, A8, A9, AFF_4:41;
hence ( a on A & b on A ) by A1, A2, A3, A4, A9, A10, Th36; ::_thesis: verum
end;
Lm1: for AS being AffinSpace st AS is not AffinPlane holds
ex a being Element of the Points of (ProjHorizon AS) ex A being Element of the Lines of (ProjHorizon AS) st not a on A
proof
let AS be AffinSpace; ::_thesis: ( AS is not AffinPlane implies ex a being Element of the Points of (ProjHorizon AS) ex A being Element of the Lines of (ProjHorizon AS) st not a on A )
set x = the Element of AS;
consider X being Subset of AS such that
A1: the Element of AS in X and
the Element of AS in X and
the Element of AS in X and
A2: X is being_plane by AFF_4:37;
reconsider A = PDir X as Element of the Lines of (ProjHorizon AS) by A2, Th15;
assume AS is not AffinPlane ; ::_thesis: not for a being Element of the Points of (ProjHorizon AS)
for A being Element of the Lines of (ProjHorizon AS) holds a on A
then consider t being Element of AS such that
A3: not t in X by A2, AFF_4:48;
set Y = Line ( the Element of AS,t);
A4: Line ( the Element of AS,t) is being_line by A1, A3, AFF_1:def_3;
then reconsider a = LDir (Line ( the Element of AS,t)) as Element of the Points of (ProjHorizon AS) by Th14;
take a ; ::_thesis: not for A being Element of the Lines of (ProjHorizon AS) holds a on A
take A ; ::_thesis: not a on A
A5: t in Line ( the Element of AS,t) by AFF_1:15;
A6: the Element of AS in Line ( the Element of AS,t) by AFF_1:15;
thus not a on A ::_thesis: verum
proof
assume a on A ; ::_thesis: contradiction
then Line ( the Element of AS,t) '||' X by A2, A4, Th36;
then Line ( the Element of AS,t) c= X by A1, A2, A4, A6, AFF_4:43;
hence contradiction by A3, A5; ::_thesis: verum
end;
end;
Lm2: for AS being AffinSpace
for a, b being POINT of (IncProjSp_of AS)
for A, K being LINE of (IncProjSp_of AS) st a on A & a on K & b on A & b on K & not a = b holds
A = K
proof
let AS be AffinSpace; ::_thesis: for a, b being POINT of (IncProjSp_of AS)
for A, K being LINE of (IncProjSp_of AS) st a on A & a on K & b on A & b on K & not a = b holds
A = K
let a, b be POINT of (IncProjSp_of AS); ::_thesis: for A, K being LINE of (IncProjSp_of AS) st a on A & a on K & b on A & b on K & not a = b holds
A = K
let A, K be LINE of (IncProjSp_of AS); ::_thesis: ( a on A & a on K & b on A & b on K & not a = b implies A = K )
assume that
A1: a on A and
A2: a on K and
A3: b on A and
A4: b on K ; ::_thesis: ( a = b or A = K )
consider X being Subset of AS such that
A5: ( ( A = [X,1] & X is being_line ) or ( A = [(PDir X),2] & X is being_plane ) ) by Th23;
consider X9 being Subset of AS such that
A6: ( ( K = [X9,1] & X9 is being_line ) or ( K = [(PDir X9),2] & X9 is being_plane ) ) by Th23;
assume A7: a <> b ; ::_thesis: A = K
A8: now__::_thesis:_(_ex_Y_being_Subset_of_AS_st_
(_a_=_LDir_Y_&_Y_is_being_line_)_implies_A_=_K_)
given Y being Subset of AS such that A9: a = LDir Y and
A10: Y is being_line ; ::_thesis: A = K
A11: now__::_thesis:_(_ex_Y9_being_Subset_of_AS_st_
(_b_=_LDir_Y9_&_Y9_is_being_line_)_implies_A_=_K_)
given Y9 being Subset of AS such that A12: b = LDir Y9 and
A13: Y9 is being_line ; ::_thesis: A = K
A14: not Y // Y9 by A7, A9, A10, A12, A13, Th11;
A15: for Z being Subset of AS
for M being LINE of (IncProjSp_of AS) st M = [Z,1] & Z is being_line & a on M holds
not b on M
proof
let Z be Subset of AS; ::_thesis: for M being LINE of (IncProjSp_of AS) st M = [Z,1] & Z is being_line & a on M holds
not b on M
let M be LINE of (IncProjSp_of AS); ::_thesis: ( M = [Z,1] & Z is being_line & a on M implies not b on M )
assume that
A16: M = [Z,1] and
A17: Z is being_line ; ::_thesis: ( not a on M or not b on M )
assume A18: ( a on M & b on M ) ; ::_thesis: contradiction
then Y9 '||' Z by A12, A13, A16, A17, Th28;
then A19: Y9 // Z by A13, A17, AFF_4:40;
Y '||' Z by A9, A10, A16, A17, A18, Th28;
then Y // Z by A10, A17, AFF_4:40;
then Y // Y9 by A19, AFF_1:44;
hence contradiction by A7, A9, A10, A12, A13, Th11; ::_thesis: verum
end;
then A20: Y9 '||' X by A1, A3, A5, A12, A13, Th29;
A21: Y9 '||' X9 by A2, A4, A6, A12, A13, A15, Th29;
A22: Y '||' X9 by A2, A4, A6, A9, A10, A15, Th29;
Y '||' X by A1, A3, A5, A9, A10, A15, Th29;
then X '||' X9 by A1, A2, A3, A4, A5, A6, A10, A13, A15, A14, A22, A20, A21, Th5;
hence A = K by A1, A2, A3, A4, A5, A6, A15, Th13; ::_thesis: verum
end;
now__::_thesis:_(_b_is_Element_of_AS_implies_A_=_K_)
assume b is Element of AS ; ::_thesis: A = K
then reconsider y = b as Element of AS ;
A23: y in X9 by A4, A6, Th26, Th27;
A24: y = b ;
then Y '||' X9 by A2, A4, A6, A9, A10, Th27, Th28;
then A25: Y // X9 by A4, A6, A10, A24, Th27, AFF_4:40;
Y '||' X by A1, A3, A5, A9, A10, A24, Th27, Th28;
then Y // X by A3, A5, A10, A24, Th27, AFF_4:40;
then A26: X // X9 by A25, AFF_1:44;
y in X by A3, A5, Th26, Th27;
hence A = K by A3, A4, A5, A6, A23, A26, Th27, AFF_1:45; ::_thesis: verum
end;
hence A = K by A11, Th20; ::_thesis: verum
end;
now__::_thesis:_(_a_is_Element_of_AS_implies_A_=_K_)
assume a is Element of AS ; ::_thesis: A = K
then reconsider x = a as Element of AS ;
A27: x = a ;
A28: x in X9 by A2, A6, Th26, Th27;
A29: x in X by A1, A5, Th26, Th27;
A30: now__::_thesis:_(_ex_Y_being_Subset_of_AS_st_
(_b_=_LDir_Y_&_Y_is_being_line_)_implies_A_=_K_)
given Y being Subset of AS such that A31: b = LDir Y and
A32: Y is being_line ; ::_thesis: A = K
Y '||' X9 by A2, A4, A6, A27, A31, A32, Th27, Th28;
then A33: Y // X9 by A2, A6, A27, A32, Th27, AFF_4:40;
Y '||' X by A1, A3, A5, A27, A31, A32, Th27, Th28;
then Y // X by A1, A5, A27, A32, Th27, AFF_4:40;
then X // X9 by A33, AFF_1:44;
hence A = K by A1, A2, A5, A6, A29, A28, Th27, AFF_1:45; ::_thesis: verum
end;
now__::_thesis:_(_b_is_Element_of_AS_implies_A_=_K_)
assume b is Element of AS ; ::_thesis: A = K
then reconsider y = b as Element of AS ;
A34: y in X9 by A4, A6, Th26, Th27;
y in X by A3, A5, Th26, Th27;
hence A = K by A1, A2, A7, A5, A6, A29, A28, A34, Th27, AFF_1:18; ::_thesis: verum
end;
hence A = K by A30, Th20; ::_thesis: verum
end;
hence A = K by A8, Th20; ::_thesis: verum
end;
Lm3: for AS being AffinSpace
for A being LINE of (IncProjSp_of AS) ex a, b, c being POINT of (IncProjSp_of AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )
proof
let AS be AffinSpace; ::_thesis: for A being LINE of (IncProjSp_of AS) ex a, b, c being POINT of (IncProjSp_of AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )
let A be LINE of (IncProjSp_of AS); ::_thesis: ex a, b, c being POINT of (IncProjSp_of AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )
consider X being Subset of AS such that
A1: ( ( A = [X,1] & X is being_line ) or ( A = [(PDir X),2] & X is being_plane ) ) by Th23;
A2: now__::_thesis:_(_A_=_[(PDir_X),2]_&_X_is_being_plane_implies_ex_a,_b,_c_being_POINT_of_(IncProjSp_of_AS)_st_
(_a_on_A_&_b_on_A_&_c_on_A_&_a_<>_b_&_b_<>_c_&_c_<>_a_)_)
assume that
A3: A = [(PDir X),2] and
A4: X is being_plane ; ::_thesis: ex a, b, c being POINT of (IncProjSp_of AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )
consider x, y, z being Element of AS such that
A5: x in X and
A6: y in X and
A7: z in X and
A8: not LIN x,y,z by A4, AFF_4:34;
A9: y <> z by A8, AFF_1:7;
then A10: Line (y,z) is being_line by AFF_1:def_3;
then A11: Line (y,z) '||' X by A4, A6, A7, A9, AFF_4:19, AFF_4:42;
A12: z <> x by A8, AFF_1:7;
then A13: Line (x,z) is being_line by AFF_1:def_3;
then A14: Line (x,z) '||' X by A4, A5, A7, A12, AFF_4:19, AFF_4:42;
A15: x <> y by A8, AFF_1:7;
then A16: Line (x,y) is being_line by AFF_1:def_3;
then reconsider a = LDir (Line (x,y)), b = LDir (Line (y,z)), c = LDir (Line (x,z)) as POINT of (IncProjSp_of AS) by A10, A13, Th20;
take a = a; ::_thesis: ex b, c being POINT of (IncProjSp_of AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )
take b = b; ::_thesis: ex c being POINT of (IncProjSp_of AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )
take c = c; ::_thesis: ( a on A & b on A & c on A & a <> b & b <> c & c <> a )
Line (x,y) '||' X by A4, A5, A6, A15, A16, AFF_4:19, AFF_4:42;
hence ( a on A & b on A & c on A ) by A3, A4, A16, A10, A13, A11, A14, Th29; ::_thesis: ( a <> b & b <> c & c <> a )
A17: x in Line (x,y) by AFF_1:15;
A18: z in Line (y,z) by AFF_1:15;
A19: y in Line (x,y) by AFF_1:15;
A20: y in Line (y,z) by AFF_1:15;
thus a <> b ::_thesis: ( b <> c & c <> a )
proof
assume not a <> b ; ::_thesis: contradiction
then Line (x,y) // Line (y,z) by A16, A10, Th11;
then z in Line (x,y) by A19, A20, A18, AFF_1:45;
hence contradiction by A8, A16, A17, A19, AFF_1:21; ::_thesis: verum
end;
A21: z in Line (x,z) by AFF_1:15;
A22: x in Line (x,z) by AFF_1:15;
thus b <> c ::_thesis: c <> a
proof
assume not b <> c ; ::_thesis: contradiction
then Line (y,z) // Line (x,z) by A10, A13, Th11;
then x in Line (y,z) by A18, A22, A21, AFF_1:45;
hence contradiction by A8, A10, A20, A18, AFF_1:21; ::_thesis: verum
end;
thus c <> a ::_thesis: verum
proof
assume not c <> a ; ::_thesis: contradiction
then Line (x,y) // Line (x,z) by A16, A13, Th11;
then z in Line (x,y) by A17, A22, A21, AFF_1:45;
hence contradiction by A8, A16, A17, A19, AFF_1:21; ::_thesis: verum
end;
end;
now__::_thesis:_(_A_=_[X,1]_&_X_is_being_line_implies_ex_a,_b_being_Element_of_the_Points_of_(IncProjSp_of_AS)_ex_c_being_POINT_of_(IncProjSp_of_AS)_st_
(_a_on_A_&_b_on_A_&_c_on_A_&_a_<>_b_&_b_<>_c_&_c_<>_a_)_)
assume that
A23: A = [X,1] and
A24: X is being_line ; ::_thesis: ex a, b being Element of the Points of (IncProjSp_of AS) ex c being POINT of (IncProjSp_of AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )
reconsider c = LDir X as POINT of (IncProjSp_of AS) by A24, Th20;
consider x, y being Element of AS such that
A25: x in X and
A26: y in X and
A27: x <> y by A24, AFF_1:19;
reconsider a = x, b = y as Element of the Points of (IncProjSp_of AS) by Th20;
take a = a; ::_thesis: ex b being Element of the Points of (IncProjSp_of AS) ex c being POINT of (IncProjSp_of AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )
take b = b; ::_thesis: ex c being POINT of (IncProjSp_of AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )
take c = c; ::_thesis: ( a on A & b on A & c on A & a <> b & b <> c & c <> a )
X // X by A24, AFF_1:41;
then X '||' X by A24, AFF_4:40;
hence ( a on A & b on A & c on A ) by A23, A24, A25, A26, Th26, Th28; ::_thesis: ( a <> b & b <> c & c <> a )
thus a <> b by A27; ::_thesis: ( b <> c & c <> a )
thus ( b <> c & c <> a ) ::_thesis: verum
proof
assume A28: ( not b <> c or not c <> a ) ; ::_thesis: contradiction
c in Dir_of_Lines AS by A24, Th14;
then the carrier of AS /\ (Dir_of_Lines AS) <> {} by A28, 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;
end;
hence ex a, b, c being POINT of (IncProjSp_of AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a ) by A1, A2; ::_thesis: verum
end;
Lm4: for AS being AffinSpace
for a, b being POINT of (IncProjSp_of AS) ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A )
proof
let AS be AffinSpace; ::_thesis: for a, b being POINT of (IncProjSp_of AS) ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A )
let a, b be POINT of (IncProjSp_of AS); ::_thesis: ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A )
A1: now__::_thesis:_(_ex_X_being_Subset_of_AS_st_
(_a_=_LDir_X_&_X_is_being_line_)_implies_ex_A_being_LINE_of_(IncProjSp_of_AS)_st_
(_a_on_A_&_b_on_A_)_)
given X being Subset of AS such that A2: a = LDir X and
A3: X is being_line ; ::_thesis: ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A )
A4: now__::_thesis:_(_ex_X9_being_Subset_of_AS_st_
(_b_=_LDir_X9_&_X9_is_being_line_)_implies_ex_A_being_LINE_of_(IncProjSp_of_AS)_st_
(_a_on_A_&_b_on_A_)_)
given X9 being Subset of AS such that A5: b = LDir X9 and
A6: X9 is being_line ; ::_thesis: ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A )
consider x, y being Element of AS such that
A7: x in X9 and
y in X9 and
x <> y by A6, AFF_1:19;
A8: x in x * X by A3, AFF_4:def_3;
x * X is being_line by A3, AFF_4:27;
then consider Z being Subset of AS such that
A9: X9 c= Z and
A10: x * X c= Z and
A11: Z is being_plane by A6, A7, A8, AFF_4:38;
A12: X9 '||' Z by A6, A9, A11, AFF_4:42;
reconsider A = [(PDir Z),2] as LINE of (IncProjSp_of AS) by A11, Th23;
take A = A; ::_thesis: ( a on A & b on A )
X // x * X by A3, AFF_4:def_3;
then X '||' Z by A3, A10, A11, AFF_4:41;
hence ( a on A & b on A ) by A2, A3, A5, A6, A11, A12, Th29; ::_thesis: verum
end;
now__::_thesis:_(_b_is_Element_of_AS_implies_ex_A_being_LINE_of_(IncProjSp_of_AS)_st_
(_a_on_A_&_b_on_A_)_)
assume b is Element of AS ; ::_thesis: ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A )
then reconsider y = b as Element of AS ;
A13: y * X is being_line by A3, AFF_4:27;
then reconsider A = [(y * X),1] as LINE of (IncProjSp_of AS) by Th23;
take A = A; ::_thesis: ( a on A & b on A )
X // y * X by A3, AFF_4:def_3;
then X '||' y * X by A3, A13, AFF_4:40;
hence a on A by A2, A3, A13, Th28; ::_thesis: b on A
y in y * X by A3, AFF_4:def_3;
hence b on A by A13, Th26; ::_thesis: verum
end;
hence ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A ) by A4, Th20; ::_thesis: verum
end;
now__::_thesis:_(_a_is_Element_of_AS_implies_ex_A_being_LINE_of_(IncProjSp_of_AS)_st_
(_a_on_A_&_b_on_A_)_)
assume a is Element of AS ; ::_thesis: ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A )
then reconsider x = a as Element of AS ;
A14: now__::_thesis:_(_ex_X9_being_Subset_of_AS_st_
(_b_=_LDir_X9_&_X9_is_being_line_)_implies_ex_A_being_LINE_of_(IncProjSp_of_AS)_st_
(_a_on_A_&_b_on_A_)_)
given X9 being Subset of AS such that A15: b = LDir X9 and
A16: X9 is being_line ; ::_thesis: ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A )
A17: x * X9 is being_line by A16, AFF_4:27;
then reconsider A = [(x * X9),1] as LINE of (IncProjSp_of AS) by Th23;
take A = A; ::_thesis: ( a on A & b on A )
x in x * X9 by A16, AFF_4:def_3;
hence a on A by A17, Th26; ::_thesis: b on A
X9 // x * X9 by A16, AFF_4:def_3;
then X9 '||' x * X9 by A16, A17, AFF_4:40;
hence b on A by A15, A16, A17, Th28; ::_thesis: verum
end;
now__::_thesis:_(_b_is_Element_of_AS_implies_ex_A_being_LINE_of_(IncProjSp_of_AS)_st_
(_a_on_A_&_b_on_A_)_)
assume b is Element of AS ; ::_thesis: ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A )
then reconsider y = b as Element of AS ;
consider Y being Subset of AS such that
A18: x in Y and
A19: y in Y and
A20: Y is being_line by AFF_4:11;
reconsider A = [Y,1] as LINE of (IncProjSp_of AS) by A20, Th23;
take A = A; ::_thesis: ( a on A & b on A )
thus ( a on A & b on A ) by A18, A19, A20, Th26; ::_thesis: verum
end;
hence ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A ) by A14, Th20; ::_thesis: verum
end;
hence ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A ) by A1, Th20; ::_thesis: verum
end;
Lm5: for AS being AffinSpace
for A, K being LINE of (IncProjSp_of AS) st AS is AffinPlane holds
ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K )
proof
let AS be AffinSpace; ::_thesis: for A, K being LINE of (IncProjSp_of AS) st AS is AffinPlane holds
ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K )
let A, K be LINE of (IncProjSp_of AS); ::_thesis: ( AS is AffinPlane implies ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K ) )
consider X being Subset of AS such that
A1: ( ( A = [X,1] & X is being_line ) or ( A = [(PDir X),2] & X is being_plane ) ) by Th23;
consider X9 being Subset of AS such that
A2: ( ( K = [X9,1] & X9 is being_line ) or ( K = [(PDir X9),2] & X9 is being_plane ) ) by Th23;
assume A3: AS is AffinPlane ; ::_thesis: ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K )
A4: now__::_thesis:_(_A_=_[X,1]_&_X_is_being_line_implies_ex_a_being_POINT_of_(IncProjSp_of_AS)_st_
(_a_on_A_&_a_on_K_)_)
assume that
A5: A = [X,1] and
A6: X is being_line ; ::_thesis: ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K )
A7: now__::_thesis:_(_K_=_[X9,1]_&_X9_is_being_line_implies_ex_a_being_POINT_of_(IncProjSp_of_AS)_st_
(_a_on_A_&_a_on_K_)_)
assume that
A8: K = [X9,1] and
A9: X9 is being_line ; ::_thesis: ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K )
A10: now__::_thesis:_(_X_//_X9_implies_ex_a_being_Element_of_the_Points_of_(IncProjSp_of_AS)_st_
(_a_on_A_&_a_on_K_)_)
reconsider a = LDir X, b = LDir X9 as Element of the Points of (IncProjSp_of AS) by A6, A9, Th20;
X9 // X9 by A9, AFF_1:41;
then A11: X9 '||' X9 by A9, AFF_4:40;
assume X // X9 ; ::_thesis: ex a being Element of the Points of (IncProjSp_of AS) st
( a on A & a on K )
then A12: a = b by A6, A9, Th11;
take a = a; ::_thesis: ( a on A & a on K )
X // X by A6, AFF_1:41;
then X '||' X by A6, AFF_4:40;
hence ( a on A & a on K ) by A5, A6, A8, A9, A12, A11, Th28; ::_thesis: verum
end;
now__::_thesis:_(_not_X_//_X9_implies_ex_a_being_Element_of_the_Points_of_(IncProjSp_of_AS)_st_
(_a_on_A_&_a_on_K_)_)
assume not X // X9 ; ::_thesis: ex a being Element of the Points of (IncProjSp_of AS) st
( a on A & a on K )
then consider x being Element of AS such that
A13: x in X and
A14: x in X9 by A3, A6, A9, AFF_1:58;
reconsider a = x as Element of the Points of (IncProjSp_of AS) by Th20;
take a = a; ::_thesis: ( a on A & a on K )
thus ( a on A & a on K ) by A5, A6, A8, A9, A13, A14, Th26; ::_thesis: verum
end;
hence ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K ) by A10; ::_thesis: verum
end;
now__::_thesis:_(_K_=_[(PDir_X9),2]_&_X9_is_being_plane_implies_ex_a_being_Element_of_the_Points_of_(IncProjSp_of_AS)_st_
(_a_on_A_&_a_on_K_)_)
X // X by A6, AFF_1:41;
then A15: X '||' X by A6, AFF_4:40;
reconsider a = LDir X as Element of the Points of (IncProjSp_of AS) by A6, Th20;
assume that
A16: K = [(PDir X9),2] and
A17: X9 is being_plane ; ::_thesis: ex a being Element of the Points of (IncProjSp_of AS) st
( a on A & a on K )
take a = a; ::_thesis: ( a on A & a on K )
X9 = the carrier of AS by A3, A17, Th2;
then X '||' X9 by A6, A17, AFF_4:42;
hence ( a on A & a on K ) by A5, A6, A16, A17, A15, Th28, Th29; ::_thesis: verum
end;
hence ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K ) by A2, A7; ::_thesis: verum
end;
now__::_thesis:_(_A_=_[(PDir_X),2]_&_X_is_being_plane_implies_ex_a_being_POINT_of_(IncProjSp_of_AS)_st_
(_a_on_A_&_a_on_K_)_)
assume that
A18: A = [(PDir X),2] and
A19: X is being_plane ; ::_thesis: ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K )
A20: X = the carrier of AS by A3, A19, Th2;
A21: now__::_thesis:_(_K_=_[X9,1]_&_X9_is_being_line_implies_ex_a_being_POINT_of_(IncProjSp_of_AS)_st_
(_a_on_A_&_a_on_K_)_)
assume that
A22: K = [X9,1] and
A23: X9 is being_line ; ::_thesis: ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K )
X9 // X9 by A23, AFF_1:41;
then A24: X9 '||' X9 by A23, AFF_4:40;
reconsider a = LDir X9 as POINT of (IncProjSp_of AS) by A23, Th20;
take a = a; ::_thesis: ( a on A & a on K )
X9 '||' X by A19, A20, A23, AFF_4:42;
hence ( a on A & a on K ) by A18, A19, A22, A23, A24, Th28, Th29; ::_thesis: verum
end;
now__::_thesis:_(_K_=_[(PDir_X9),2]_&_X9_is_being_plane_implies_ex_a_being_POINT_of_(IncProjSp_of_AS)_st_
(_a_on_A_&_a_on_K_)_)
consider a, b, c being POINT of (IncProjSp_of AS) such that
A25: a on A and
b on A and
c on A and
a <> b and
b <> c and
c <> a by Lm3;
assume that
A26: K = [(PDir X9),2] and
A27: X9 is being_plane ; ::_thesis: ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K )
take a = a; ::_thesis: ( a on A & a on K )
thus ( a on A & a on K ) by A3, A18, A19, A26, A27, A25, Th3; ::_thesis: verum
end;
hence ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K ) by A2, A21; ::_thesis: verum
end;
hence ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K ) by A1, A4; ::_thesis: verum
end;
Lm6: for AS being AffinSpace holds
not for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) holds a on A
proof
let AS be AffinSpace; ::_thesis: not for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) holds a on A
consider x, y, z being Element of AS such that
A1: not LIN x,y,z by AFF_1:12;
y <> z by A1, AFF_1:7;
then A2: Line (y,z) is being_line by AFF_1:def_3;
then reconsider A = [(Line (y,z)),1] as LINE of (IncProjSp_of AS) by Th23;
reconsider a = x as POINT of (IncProjSp_of AS) by Th20;
take a ; ::_thesis: not for A being LINE of (IncProjSp_of AS) holds a on A
take A ; ::_thesis: not a on A
thus not a on A ::_thesis: verum
proof
assume a on A ; ::_thesis: contradiction
then A3: x in Line (y,z) by Th26;
A4: z in Line (y,z) by AFF_1:15;
y in Line (y,z) by AFF_1:15;
hence contradiction by A1, A2, A3, A4, AFF_1:21; ::_thesis: verum
end;
end;
theorem Th41: :: AFPROJ:41
for AS being AffinSpace
for x, y being Element of the Points of (ProjHorizon AS)
for X being Element of the Lines of (IncProjSp_of AS) st x <> y & [x,X] in the Inc of (IncProjSp_of AS) & [y,X] in the Inc of (IncProjSp_of AS) holds
ex Y being Element of the Lines of (ProjHorizon AS) st X = [Y,2]
proof
let AS be AffinSpace; ::_thesis: for x, y being Element of the Points of (ProjHorizon AS)
for X being Element of the Lines of (IncProjSp_of AS) st x <> y & [x,X] in the Inc of (IncProjSp_of AS) & [y,X] in the Inc of (IncProjSp_of AS) holds
ex Y being Element of the Lines of (ProjHorizon AS) st X = [Y,2]
let x, y be Element of the Points of (ProjHorizon AS); ::_thesis: for X being Element of the Lines of (IncProjSp_of AS) st x <> y & [x,X] in the Inc of (IncProjSp_of AS) & [y,X] in the Inc of (IncProjSp_of AS) holds
ex Y being Element of the Lines of (ProjHorizon AS) st X = [Y,2]
let X be Element of the Lines of (IncProjSp_of AS); ::_thesis: ( x <> y & [x,X] in the Inc of (IncProjSp_of AS) & [y,X] in the Inc of (IncProjSp_of AS) implies ex Y being Element of the Lines of (ProjHorizon AS) st X = [Y,2] )
reconsider a = x, b = y as POINT of (IncProjSp_of AS) by Th22;
assume that
A1: x <> y and
A2: [x,X] in the Inc of (IncProjSp_of AS) and
A3: [y,X] in the Inc of (IncProjSp_of AS) ; ::_thesis: ex Y being Element of the Lines of (ProjHorizon AS) st X = [Y,2]
A4: b on X by A3, INCSP_1:def_1;
consider Y being Element of the Lines of (ProjHorizon AS) such that
A5: x on Y and
A6: y on Y by Th40;
reconsider A = [Y,2] as LINE of (IncProjSp_of AS) by Th25;
consider Z being Subset of AS such that
A7: Y = PDir Z and
A8: Z is being_plane by Th15;
consider X2 being Subset of AS such that
A9: y = LDir X2 and
A10: X2 is being_line by Th14;
X2 '||' Z by A9, A10, A6, A7, A8, Th36;
then A11: b on A by A9, A10, A7, A8, Th29;
take Y ; ::_thesis: X = [Y,2]
consider X1 being Subset of AS such that
A12: x = LDir X1 and
A13: X1 is being_line by Th14;
X1 '||' Z by A12, A13, A5, A7, A8, Th36;
then A14: a on A by A12, A13, A7, A8, Th29;
a on X by A2, INCSP_1:def_1;
hence X = [Y,2] by A1, A4, A14, A11, Lm2; ::_thesis: verum
end;
theorem Th42: :: AFPROJ:42
for AS being AffinSpace
for x being POINT of (IncProjSp_of AS)
for X being Element of the Lines of (ProjHorizon AS) st [x,[X,2]] in the Inc of (IncProjSp_of AS) holds
x is Element of the Points of (ProjHorizon AS)
proof
let AS be AffinSpace; ::_thesis: for x being POINT of (IncProjSp_of AS)
for X being Element of the Lines of (ProjHorizon AS) st [x,[X,2]] in the Inc of (IncProjSp_of AS) holds
x is Element of the Points of (ProjHorizon AS)
let x be POINT of (IncProjSp_of AS); ::_thesis: for X being Element of the Lines of (ProjHorizon AS) st [x,[X,2]] in the Inc of (IncProjSp_of AS) holds
x is Element of the Points of (ProjHorizon AS)
let X be Element of the Lines of (ProjHorizon AS); ::_thesis: ( [x,[X,2]] in the Inc of (IncProjSp_of AS) implies x is Element of the Points of (ProjHorizon AS) )
assume A1: [x,[X,2]] in the Inc of (IncProjSp_of AS) ; ::_thesis: x is Element of the Points of (ProjHorizon AS)
reconsider A = [X,2] as LINE of (IncProjSp_of AS) by Th25;
A2: ex Y being Subset of AS st
( X = PDir Y & Y is being_plane ) by Th15;
x is not Element of AS
proof
assume x is Element of AS ; ::_thesis: contradiction
then reconsider a = x as Element of AS ;
A3: a = x ;
x on A by A1, INCSP_1:def_1;
hence contradiction by A2, A3, Th27; ::_thesis: verum
end;
then ex Y9 being Subset of AS st
( x = LDir Y9 & Y9 is being_line ) by Th20;
hence x is Element of the Points of (ProjHorizon AS) by Th14; ::_thesis: verum
end;
Lm7: for AS being AffinSpace
for X, X9, Y, Y9 being Subset of AS
for b, c being POINT of (IncProjSp_of AS)
for A, K, M being LINE of (IncProjSp_of AS) st X is being_line & X9 is being_line & Y is being_plane & X c= Y & X9 c= Y & A = [X,1] & K = [X9,1] & b on A & c on K & b on M & c on M & b <> c & M = [Y9,1] & Y9 is being_line holds
Y9 c= Y
proof
let AS be AffinSpace; ::_thesis: for X, X9, Y, Y9 being Subset of AS
for b, c being POINT of (IncProjSp_of AS)
for A, K, M being LINE of (IncProjSp_of AS) st X is being_line & X9 is being_line & Y is being_plane & X c= Y & X9 c= Y & A = [X,1] & K = [X9,1] & b on A & c on K & b on M & c on M & b <> c & M = [Y9,1] & Y9 is being_line holds
Y9 c= Y
let X, X9, Y, Y9 be Subset of AS; ::_thesis: for b, c being POINT of (IncProjSp_of AS)
for A, K, M being LINE of (IncProjSp_of AS) st X is being_line & X9 is being_line & Y is being_plane & X c= Y & X9 c= Y & A = [X,1] & K = [X9,1] & b on A & c on K & b on M & c on M & b <> c & M = [Y9,1] & Y9 is being_line holds
Y9 c= Y
let b, c be POINT of (IncProjSp_of AS); ::_thesis: for A, K, M being LINE of (IncProjSp_of AS) st X is being_line & X9 is being_line & Y is being_plane & X c= Y & X9 c= Y & A = [X,1] & K = [X9,1] & b on A & c on K & b on M & c on M & b <> c & M = [Y9,1] & Y9 is being_line holds
Y9 c= Y
let A, K, M be LINE of (IncProjSp_of AS); ::_thesis: ( X is being_line & X9 is being_line & Y is being_plane & X c= Y & X9 c= Y & A = [X,1] & K = [X9,1] & b on A & c on K & b on M & c on M & b <> c & M = [Y9,1] & Y9 is being_line implies Y9 c= Y )
assume that
A1: X is being_line and
A2: X9 is being_line and
A3: Y is being_plane and
A4: X c= Y and
A5: X9 c= Y and
A6: A = [X,1] and
A7: K = [X9,1] and
A8: b on A and
A9: c on K and
A10: b on M and
A11: c on M and
A12: b <> c and
A13: M = [Y9,1] and
A14: Y9 is being_line ; ::_thesis: Y9 c= Y
A15: now__::_thesis:_(_b_is_Element_of_AS_implies_Y9_c=_Y_)
assume b is Element of AS ; ::_thesis: Y9 c= Y
then reconsider y = b as Element of AS ;
A16: now__::_thesis:_(_ex_Xc_being_Subset_of_AS_st_
(_c_=_LDir_Xc_&_Xc_is_being_line_)_implies_Y9_c=_Y_)
given Xc being Subset of AS such that A17: c = LDir Xc and
A18: Xc is being_line ; ::_thesis: Y9 c= Y
Xc '||' X9 by A2, A7, A9, A17, A18, Th28;
then A19: Xc // X9 by A2, A18, AFF_4:40;
Xc '||' Y9 by A11, A13, A14, A17, A18, Th28;
then Xc // Y9 by A14, A18, AFF_4:40;
then A20: X9 // Y9 by A19, AFF_1:44;
y in Y9 by A10, A13, Th26;
then A21: Y9 = y * X9 by A2, A20, AFF_4:def_3;
y in X by A6, A8, Th26;
hence Y9 c= Y by A2, A3, A4, A5, A21, AFF_4:28; ::_thesis: verum
end;
now__::_thesis:_(_c_is_Element_of_AS_implies_Y9_c=_Y_)
assume c is Element of AS ; ::_thesis: Y9 c= Y
then reconsider z = c as Element of AS ;
A22: z in Y9 by A11, A13, Th26;
y in Y9 by A10, A13, Th26;
then A23: Y9 = Line (y,z) by A12, A14, A22, AFF_1:57;
A24: z in X9 by A7, A9, Th26;
y in X by A6, A8, Th26;
hence Y9 c= Y by A3, A4, A5, A12, A24, A23, AFF_4:19; ::_thesis: verum
end;
hence Y9 c= Y by A16, Th20; ::_thesis: verum
end;
now__::_thesis:_(_ex_Xb_being_Subset_of_AS_st_
(_b_=_LDir_Xb_&_Xb_is_being_line_)_implies_Y9_c=_Y_)
given Xb being Subset of AS such that A25: b = LDir Xb and
A26: Xb is being_line ; ::_thesis: Y9 c= Y
A27: now__::_thesis:_(_c_is_Element_of_AS_implies_Y9_c=_Y_)
assume c is Element of AS ; ::_thesis: Y9 c= Y
then reconsider y = c as Element of AS ;
Xb '||' X by A1, A6, A8, A25, A26, Th28;
then A28: Xb // X by A1, A26, AFF_4:40;
Xb '||' Y9 by A10, A13, A14, A25, A26, Th28;
then Xb // Y9 by A14, A26, AFF_4:40;
then A29: X // Y9 by A28, AFF_1:44;
y in Y9 by A11, A13, Th26;
then A30: Y9 = y * X by A1, A29, AFF_4:def_3;
y in X9 by A7, A9, Th26;
hence Y9 c= Y by A1, A3, A4, A5, A30, AFF_4:28; ::_thesis: verum
end;
now__::_thesis:_for_Xc_being_Subset_of_AS_holds_
(_not_c_=_LDir_Xc_or_not_Xc_is_being_line_)
Xb '||' Y9 by A10, A13, A14, A25, A26, Th28;
then A31: Xb // Y9 by A14, A26, AFF_4:40;
given Xc being Subset of AS such that A32: c = LDir Xc and
A33: Xc is being_line ; ::_thesis: contradiction
Xc '||' Y9 by A11, A13, A14, A32, A33, Th28;
then Xc // Y9 by A14, A33, AFF_4:40;
then Xc // Xb by A31, AFF_1:44;
hence contradiction by A12, A25, A26, A32, A33, Th11; ::_thesis: verum
end;
hence Y9 c= Y by A27, Th20; ::_thesis: verum
end;
hence Y9 c= Y by A15, Th20; ::_thesis: verum
end;
Lm8: for AS being AffinSpace
for X, X9, Y, Y9 being Subset of AS
for b, c being POINT of (IncProjSp_of AS)
for A, K, M being LINE of (IncProjSp_of AS) st X is being_line & X9 is being_line & Y is being_plane & X c= Y & X9 c= Y & A = [X,1] & K = [X9,1] & b on A & c on K & b on M & c on M & b <> c & M = [(PDir Y9),2] & Y9 is being_plane holds
( Y9 '||' Y & Y '||' Y9 )
proof
let AS be AffinSpace; ::_thesis: for X, X9, Y, Y9 being Subset of AS
for b, c being POINT of (IncProjSp_of AS)
for A, K, M being LINE of (IncProjSp_of AS) st X is being_line & X9 is being_line & Y is being_plane & X c= Y & X9 c= Y & A = [X,1] & K = [X9,1] & b on A & c on K & b on M & c on M & b <> c & M = [(PDir Y9),2] & Y9 is being_plane holds
( Y9 '||' Y & Y '||' Y9 )
let X, X9, Y, Y9 be Subset of AS; ::_thesis: for b, c being POINT of (IncProjSp_of AS)
for A, K, M being LINE of (IncProjSp_of AS) st X is being_line & X9 is being_line & Y is being_plane & X c= Y & X9 c= Y & A = [X,1] & K = [X9,1] & b on A & c on K & b on M & c on M & b <> c & M = [(PDir Y9),2] & Y9 is being_plane holds
( Y9 '||' Y & Y '||' Y9 )
let b, c be POINT of (IncProjSp_of AS); ::_thesis: for A, K, M being LINE of (IncProjSp_of AS) st X is being_line & X9 is being_line & Y is being_plane & X c= Y & X9 c= Y & A = [X,1] & K = [X9,1] & b on A & c on K & b on M & c on M & b <> c & M = [(PDir Y9),2] & Y9 is being_plane holds
( Y9 '||' Y & Y '||' Y9 )
let A, K, M be LINE of (IncProjSp_of AS); ::_thesis: ( X is being_line & X9 is being_line & Y is being_plane & X c= Y & X9 c= Y & A = [X,1] & K = [X9,1] & b on A & c on K & b on M & c on M & b <> c & M = [(PDir Y9),2] & Y9 is being_plane implies ( Y9 '||' Y & Y '||' Y9 ) )
assume that
A1: X is being_line and
A2: X9 is being_line and
A3: Y is being_plane and
A4: X c= Y and
A5: X9 c= Y and
A6: A = [X,1] and
A7: K = [X9,1] and
A8: b on A and
A9: c on K and
A10: b on M and
A11: c on M and
A12: b <> c and
A13: M = [(PDir Y9),2] and
A14: Y9 is being_plane ; ::_thesis: ( Y9 '||' Y & Y '||' Y9 )
( b is Element of AS or ex Xb being Subset of AS st
( b = LDir Xb & Xb is being_line ) ) by Th20;
then consider Xb being Subset of AS such that
A15: b = LDir Xb and
A16: Xb is being_line by A10, A13, Th27;
A17: Xb '||' Y9 by A10, A13, A14, A15, A16, Th29;
Xb '||' X by A1, A6, A8, A15, A16, Th28;
then Xb // X by A1, A16, AFF_4:40;
then A18: Xb '||' Y by A1, A3, A4, AFF_4:42, AFF_4:56;
( c is Element of AS or ex Xc being Subset of AS st
( c = LDir Xc & Xc is being_line ) ) by Th20;
then consider Xc being Subset of AS such that
A19: c = LDir Xc and
A20: Xc is being_line by A11, A13, Th27;
A21: Xc '||' Y9 by A11, A13, A14, A19, A20, Th29;
Xc '||' X9 by A2, A7, A9, A19, A20, Th28;
then Xc // X9 by A2, A20, AFF_4:40;
then A22: Xc '||' Y by A2, A3, A5, AFF_4:42, AFF_4:56;
not Xb // Xc by A12, A15, A16, A19, A20, Th11;
hence ( Y9 '||' Y & Y '||' Y9 ) by A3, A14, A16, A20, A17, A21, A18, A22, Th5; ::_thesis: verum
end;
theorem Th43: :: AFPROJ:43
for AS being AffinSpace
for Y, X, X9 being Subset of AS
for P, Q being LINE of (IncProjSp_of AS) st Y is being_plane & X is being_line & X9 is being_line & X c= Y & X9 c= Y & P = [X,1] & Q = [X9,1] holds
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
proof
let AS be AffinSpace; ::_thesis: for Y, X, X9 being Subset of AS
for P, Q being LINE of (IncProjSp_of AS) st Y is being_plane & X is being_line & X9 is being_line & X c= Y & X9 c= Y & P = [X,1] & Q = [X9,1] holds
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
let Y, X, X9 be Subset of AS; ::_thesis: for P, Q being LINE of (IncProjSp_of AS) st Y is being_plane & X is being_line & X9 is being_line & X c= Y & X9 c= Y & P = [X,1] & Q = [X9,1] holds
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
let P, Q be LINE of (IncProjSp_of AS); ::_thesis: ( Y is being_plane & X is being_line & X9 is being_line & X c= Y & X9 c= Y & P = [X,1] & Q = [X9,1] implies ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) )
assume that
A1: Y is being_plane and
A2: X is being_line and
A3: X9 is being_line and
A4: X c= Y and
A5: X9 c= Y and
A6: P = [X,1] and
A7: Q = [X9,1] ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
A8: now__::_thesis:_(_X_//_X9_implies_ex_q_being_POINT_of_(IncProjSp_of_AS)_st_
(_q_on_P_&_q_on_Q_)_)
reconsider q = LDir X as POINT of (IncProjSp_of AS) by A2, Th20;
assume A9: X // X9 ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
take q = q; ::_thesis: ( q on P & q on Q )
LDir X = LDir X9 by A2, A3, A9, Th11;
hence ( q on P & q on Q ) by A2, A3, A6, A7, Th30; ::_thesis: verum
end;
now__::_thesis:_(_ex_y_being_Element_of_AS_st_
(_y_in_X_&_y_in_X9_)_implies_ex_q_being_Element_of_the_Points_of_(IncProjSp_of_AS)_st_
(_q_on_P_&_q_on_Q_)_)
given y being Element of AS such that A10: y in X and
A11: y in X9 ; ::_thesis: ex q being Element of the Points of (IncProjSp_of AS) st
( q on P & q on Q )
reconsider q = y as Element of the Points of (IncProjSp_of AS) by Th20;
take q = q; ::_thesis: ( q on P & q on Q )
thus ( q on P & q on Q ) by A2, A3, A6, A7, A10, A11, Th26; ::_thesis: verum
end;
hence ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) by A1, A2, A3, A4, A5, A8, AFF_4:22; ::_thesis: verum
end;
Lm9: for AS being AffinSpace
for a, b, c, d, p being POINT of (IncProjSp_of AS)
for M, N, P, Q being LINE of (IncProjSp_of AS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N & p is Element of AS holds
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
proof
let AS be AffinSpace; ::_thesis: for a, b, c, d, p being POINT of (IncProjSp_of AS)
for M, N, P, Q being LINE of (IncProjSp_of AS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N & p is Element of AS holds
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
let a, b, c, d, p be POINT of (IncProjSp_of AS); ::_thesis: for M, N, P, Q being LINE of (IncProjSp_of AS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N & p is Element of AS holds
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
let M, N, P, Q be LINE of (IncProjSp_of AS); ::_thesis: ( a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N & p is Element of AS implies ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) )
assume that
A1: a on M and
A2: b on M and
A3: c on N and
A4: d on N and
A5: p on M and
A6: p on N and
A7: a on P and
A8: c on P and
A9: b on Q and
A10: d on Q and
A11: not p on P and
A12: not p on Q and
A13: M <> N and
A14: p is Element of AS ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
A15: b <> d by A2, A4, A5, A6, A9, A12, A13, Lm2;
reconsider x = p as Element of AS by A14;
consider XM being Subset of AS such that
A16: ( ( M = [XM,1] & XM is being_line ) or ( M = [(PDir XM),2] & XM is being_plane ) ) by Th23;
consider XQ being Subset of AS such that
A17: ( ( Q = [XQ,1] & XQ is being_line ) or ( Q = [(PDir XQ),2] & XQ is being_plane ) ) by Th23;
consider XP being Subset of AS such that
A18: ( ( P = [XP,1] & XP is being_line ) or ( P = [(PDir XP),2] & XP is being_plane ) ) by Th23;
consider XN being Subset of AS such that
A19: ( ( N = [XN,1] & XN is being_line ) or ( N = [(PDir XN),2] & XN is being_plane ) ) by Th23;
A20: x in XM by A5, A16, Th26, Th27;
x in XN by A6, A19, Th26, Th27;
then consider Y being Subset of AS such that
A21: XM c= Y and
A22: XN c= Y and
A23: Y is being_plane by A5, A6, A16, A19, A20, Th27, AFF_4:38;
A24: a <> c by A1, A3, A5, A6, A7, A11, A13, Lm2;
A25: now__::_thesis:_(_P_=_[(PDir_XP),2]_&_XP_is_being_plane_implies_ex_q_being_POINT_of_(IncProjSp_of_AS)_st_
(_q_on_P_&_q_on_Q_)_)
assume that
A26: P = [(PDir XP),2] and
A27: XP is being_plane ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
A28: Y '||' XP by A1, A3, A5, A6, A7, A8, A24, A16, A19, A20, A21, A22, A23, A26, A27, Lm8, Th27;
A29: now__::_thesis:_(_Q_=_[XQ,1]_&_XQ_is_being_line_implies_ex_q_being_POINT_of_(IncProjSp_of_AS)_st_
(_q_on_P_&_q_on_Q_)_)
assume that
A30: Q = [XQ,1] and
A31: XQ is being_line ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
reconsider q = LDir XQ as POINT of (IncProjSp_of AS) by A31, Th20;
take q = q; ::_thesis: ( q on P & q on Q )
XQ c= Y by A2, A4, A5, A6, A9, A10, A15, A16, A19, A20, A21, A22, A23, A30, A31, Lm7, Th27;
then XQ '||' Y by A23, A31, AFF_4:42;
then XQ '||' XP by A23, A28, AFF_4:59, AFF_4:60;
hence q on P by A26, A27, A31, Th29; ::_thesis: q on Q
thus q on Q by A30, A31, Th30; ::_thesis: verum
end;
now__::_thesis:_(_Q_=_[(PDir_XQ),2]_&_XQ_is_being_plane_implies_ex_q_being_POINT_of_(IncProjSp_of_AS)_st_
(_q_on_P_&_q_on_Q_)_)
consider q, r, p9 being POINT of (IncProjSp_of AS) such that
A32: q on P and
r on P and
p9 on P and
q <> r and
r <> p9 and
p9 <> q by Lm3;
assume that
A33: Q = [(PDir XQ),2] and
A34: XQ is being_plane ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
take q = q; ::_thesis: ( q on P & q on Q )
thus q on P by A32; ::_thesis: q on Q
Y '||' XQ by A2, A4, A5, A6, A9, A10, A15, A16, A19, A20, A21, A22, A23, A33, A34, Lm8, Th27;
then XP '||' XQ by A23, A27, A28, A34, AFF_4:61;
hence q on Q by A26, A27, A33, A34, A32, Th13; ::_thesis: verum
end;
hence ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) by A17, A29; ::_thesis: verum
end;
now__::_thesis:_(_P_=_[XP,1]_&_XP_is_being_line_implies_ex_q_being_POINT_of_(IncProjSp_of_AS)_st_
(_q_on_P_&_q_on_Q_)_)
assume that
A35: P = [XP,1] and
A36: XP is being_line ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
A37: XP c= Y by A1, A3, A5, A6, A7, A8, A24, A16, A19, A20, A21, A22, A23, A35, A36, Lm7, Th27;
A38: now__::_thesis:_(_Q_=_[(PDir_XQ),2]_&_XQ_is_being_plane_implies_ex_q_being_POINT_of_(IncProjSp_of_AS)_st_
(_q_on_P_&_q_on_Q_)_)
A39: XP '||' Y by A23, A36, A37, AFF_4:42;
reconsider q = LDir XP as POINT of (IncProjSp_of AS) by A36, Th20;
assume that
A40: Q = [(PDir XQ),2] and
A41: XQ is being_plane ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
take q = q; ::_thesis: ( q on P & q on Q )
thus q on P by A35, A36, Th30; ::_thesis: q on Q
Y '||' XQ by A2, A4, A5, A6, A9, A10, A15, A16, A19, A20, A21, A22, A23, A40, A41, Lm8, Th27;
then XP '||' XQ by A23, A39, AFF_4:59, AFF_4:60;
hence q on Q by A36, A40, A41, Th29; ::_thesis: verum
end;
now__::_thesis:_(_Q_=_[XQ,1]_&_XQ_is_being_line_implies_ex_q_being_POINT_of_(IncProjSp_of_AS)_st_
(_q_on_P_&_q_on_Q_)_)
assume that
A42: Q = [XQ,1] and
A43: XQ is being_line ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
XQ c= Y by A2, A4, A5, A6, A9, A10, A15, A16, A19, A20, A21, A22, A23, A42, A43, Lm7, Th27;
hence ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) by A23, A35, A36, A37, A42, A43, Th43; ::_thesis: verum
end;
hence ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) by A17, A38; ::_thesis: verum
end;
hence ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) by A18, A25; ::_thesis: verum
end;
Lm10: for AS being AffinSpace
for a, b, c, d, p being POINT of (IncProjSp_of AS)
for M, N, P, Q being LINE of (IncProjSp_of AS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N & p is not Element of AS & a is Element of AS holds
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
proof
let AS be AffinSpace; ::_thesis: for a, b, c, d, p being POINT of (IncProjSp_of AS)
for M, N, P, Q being LINE of (IncProjSp_of AS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N & p is not Element of AS & a is Element of AS holds
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
let a, b, c, d, p be POINT of (IncProjSp_of AS); ::_thesis: for M, N, P, Q being LINE of (IncProjSp_of AS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N & p is not Element of AS & a is Element of AS holds
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
let M, N, P, Q be LINE of (IncProjSp_of AS); ::_thesis: ( a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N & p is not Element of AS & a is Element of AS implies ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) )
assume that
A1: a on M and
A2: b on M and
A3: c on N and
A4: d on N and
A5: p on M and
A6: p on N and
A7: a on P and
A8: c on P and
A9: b on Q and
A10: d on Q and
A11: not p on P and
A12: not p on Q and
A13: M <> N and
A14: p is not Element of AS and
A15: a is Element of AS ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
reconsider x = a as Element of AS by A15;
consider XM being Subset of AS such that
A16: ( ( M = [XM,1] & XM is being_line ) or ( M = [(PDir XM),2] & XM is being_plane ) ) by Th23;
A17: x in XM by A1, A16, Th26, Th27;
A18: b <> d by A2, A4, A5, A6, A9, A12, A13, Lm2;
consider XN being Subset of AS such that
A19: ( ( N = [XN,1] & XN is being_line ) or ( N = [(PDir XN),2] & XN is being_plane ) ) by Th23;
consider XP being Subset of AS such that
A20: ( ( P = [XP,1] & XP is being_line ) or ( P = [(PDir XP),2] & XP is being_plane ) ) by Th23;
A21: x = a ;
then reconsider y = b as Element of AS by A1, A2, A5, A9, A12, A14, A16, Th27, Th35;
A22: y in XM by A2, A16, Th26, Th27;
consider X being Subset of AS such that
A23: p = LDir X and
A24: X is being_line by A14, Th20;
consider XQ being Subset of AS such that
A25: ( ( Q = [XQ,1] & XQ is being_line ) or ( Q = [(PDir XQ),2] & XQ is being_plane ) ) by Th23;
A26: x in XP by A7, A20, Th26, Th27;
then consider Y being Subset of AS such that
A27: XM c= Y and
A28: XP c= Y and
A29: Y is being_plane by A1, A7, A16, A20, A17, Th27, AFF_4:38;
A30: y = b ;
A31: X '||' XM by A1, A5, A23, A24, A16, A21, Th27, Th28;
then A32: X // XM by A1, A24, A16, A21, Th27, AFF_4:40;
A33: y in XQ by A9, A25, Th26, Th27;
A34: not XM // XP by A1, A5, A7, A11, A16, A20, A17, A26, Th27, AFF_1:45;
A35: now__::_thesis:_(_N_=_[XN,1]_&_XN_is_being_line_implies_ex_q_being_POINT_of_(IncProjSp_of_AS)_st_
(_q_on_P_&_q_on_Q_)_)
A36: X // XM by A1, A24, A16, A21, A31, Th27, AFF_4:40;
assume that
A37: N = [XN,1] and
A38: XN is being_line ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
X '||' XN by A6, A23, A24, A37, A38, Th28;
then X // XN by A24, A38, AFF_4:40;
then A39: XM // XN by A36, AFF_1:44;
c is Element of AS
proof
assume c is not Element of AS ; ::_thesis: contradiction
then c = LDir XN by A3, A37, A38, Th34;
then XN '||' XP by A7, A8, A20, A21, A38, Th27, Th28;
then XN // XP by A7, A20, A21, A38, Th27, AFF_4:40;
hence contradiction by A34, A39, AFF_1:44; ::_thesis: verum
end;
then reconsider z = c as Element of AS ;
z in XN by A3, A37, Th26;
then A40: XN = z * XM by A1, A16, A21, A39, Th27, AFF_4:def_3;
A41: not XN // XQ
proof
assume XN // XQ ; ::_thesis: contradiction
then XM // XQ by A39, AFF_1:44;
hence contradiction by A2, A5, A9, A12, A16, A25, A33, A22, Th27, AFF_1:45; ::_thesis: verum
end;
now__::_thesis:_d_is_Element_of_AS
assume d is not Element of AS ; ::_thesis: contradiction
then consider Xd being Subset of AS such that
A42: d = LDir Xd and
A43: Xd is being_line by Th20;
Xd '||' XN by A4, A37, A38, A42, A43, Th28;
then A44: Xd // XN by A38, A43, AFF_4:40;
Xd '||' XQ by A9, A10, A25, A30, A42, A43, Th27, Th28;
then Xd // XQ by A9, A25, A30, A43, Th27, AFF_4:40;
hence contradiction by A41, A44, AFF_1:44; ::_thesis: verum
end;
then reconsider w = d as Element of AS ;
w in XQ by A10, A25, Th26, Th27;
then A45: XQ = Line (y,w) by A9, A18, A25, A33, Th27, AFF_1:57;
z in XP by A8, A20, Th26, Th27;
then A46: XN c= Y by A1, A16, A21, A27, A28, A29, A40, Th27, AFF_4:28;
w in XN by A4, A37, Th26;
then XQ c= Y by A18, A27, A29, A22, A46, A45, AFF_4:19;
hence ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) by A7, A9, A20, A25, A21, A28, A29, A30, Th27, Th43; ::_thesis: verum
end;
A47: XP '||' Y by A7, A20, A21, A28, A29, Th27, AFF_4:42;
A48: XM '||' Y by A1, A16, A21, A27, A29, Th27, AFF_4:42;
now__::_thesis:_(_N_=_[(PDir_XN),2]_&_XN_is_being_plane_implies_ex_q_being_POINT_of_(IncProjSp_of_AS)_st_
(_q_on_P_&_q_on_Q_)_)
assume that
A49: N = [(PDir XN),2] and
A50: XN is being_plane ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
c is not Element of AS by A3, A49, Th27;
then c = LDir XP by A7, A8, A20, A21, Th27, Th34;
then A51: XP '||' XN by A3, A7, A20, A21, A49, A50, Th27, Th29;
d is not Element of AS by A4, A49, Th27;
then d = LDir XQ by A9, A10, A25, A30, Th27, Th34;
then A52: XQ '||' XN by A4, A9, A25, A30, A49, A50, Th27, Th29;
X '||' XN by A6, A23, A24, A49, A50, Th29;
then XM '||' XN by A32, AFF_4:56;
then XN '||' Y by A1, A5, A7, A11, A16, A20, A17, A26, A29, A48, A47, A50, A51, Th5, Th27, AFF_1:45;
then XQ '||' Y by A50, A52, AFF_4:59, AFF_4:60;
then XQ c= Y by A9, A25, A27, A29, A33, A22, Th27, AFF_4:43;
hence ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) by A7, A9, A20, A25, A21, A28, A29, A30, Th27, Th43; ::_thesis: verum
end;
hence ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) by A19, A35; ::_thesis: verum
end;
Lm11: for AS being AffinSpace
for a, b, c, d, p being POINT of (IncProjSp_of AS)
for M, N, P, Q being LINE of (IncProjSp_of AS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N & p is not Element of AS & ( a is Element of AS or b is Element of AS or c is Element of AS or d is Element of AS ) holds
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
proof
let AS be AffinSpace; ::_thesis: for a, b, c, d, p being POINT of (IncProjSp_of AS)
for M, N, P, Q being LINE of (IncProjSp_of AS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N & p is not Element of AS & ( a is Element of AS or b is Element of AS or c is Element of AS or d is Element of AS ) holds
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
let a, b, c, d, p be POINT of (IncProjSp_of AS); ::_thesis: for M, N, P, Q being LINE of (IncProjSp_of AS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N & p is not Element of AS & ( a is Element of AS or b is Element of AS or c is Element of AS or d is Element of AS ) holds
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
let M, N, P, Q be LINE of (IncProjSp_of AS); ::_thesis: ( a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N & p is not Element of AS & ( a is Element of AS or b is Element of AS or c is Element of AS or d is Element of AS ) implies ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) )
assume that
A1: a on M and
A2: b on M and
A3: c on N and
A4: d on N and
A5: p on M and
A6: p on N and
A7: a on P and
A8: c on P and
A9: b on Q and
A10: d on Q and
A11: not p on P and
A12: not p on Q and
A13: M <> N and
A14: p is not Element of AS and
A15: ( a is Element of AS or b is Element of AS or c is Element of AS or d is Element of AS ) ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
now__::_thesis:_(_(_b_is_Element_of_AS_or_d_is_Element_of_AS_)_implies_ex_q_being_POINT_of_(IncProjSp_of_AS)_st_
(_q_on_P_&_q_on_Q_)_)
assume ( b is Element of AS or d is Element of AS ) ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
then ex q being POINT of (IncProjSp_of AS) st
( q on Q & q on P ) by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, Lm10;
hence ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) ; ::_thesis: verum
end;
hence ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, Lm10; ::_thesis: verum
end;
Lm12: for AS being AffinSpace
for a, b, c, d, p being POINT of (IncProjSp_of AS)
for M, N, P, Q being LINE of (IncProjSp_of AS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N holds
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
proof
let AS be AffinSpace; ::_thesis: for a, b, c, d, p being POINT of (IncProjSp_of AS)
for M, N, P, Q being LINE of (IncProjSp_of AS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N holds
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
let a, b, c, d, p be POINT of (IncProjSp_of AS); ::_thesis: for M, N, P, Q being LINE of (IncProjSp_of AS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N holds
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
let M, N, P, Q be LINE of (IncProjSp_of AS); ::_thesis: ( a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N implies ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) )
assume that
A1: a on M and
A2: b on M and
A3: c on N and
A4: d on N and
A5: p on M and
A6: p on N and
A7: a on P and
A8: c on P and
A9: b on Q and
A10: d on Q and
A11: not p on P and
A12: not p on Q and
A13: M <> N ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
now__::_thesis:_(_p_is_not_Element_of_AS_implies_ex_q_being_POINT_of_(IncProjSp_of_AS)_st_
(_q_on_P_&_q_on_Q_)_)
assume A14: p is not Element of AS ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
now__::_thesis:_(_a_is_not_Element_of_AS_&_b_is_not_Element_of_AS_&_c_is_not_Element_of_AS_&_d_is_not_Element_of_AS_implies_ex_q_being_POINT_of_(IncProjSp_of_AS)_st_
(_q_on_P_&_q_on_Q_)_)
A15: b <> d by A2, A4, A5, A6, A9, A12, A13, Lm2;
set x = the Element of AS;
assume that
A16: a is not Element of AS and
A17: b is not Element of AS and
A18: c is not Element of AS and
A19: d is not Element of AS ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
consider Xa being Subset of AS such that
A20: a = LDir Xa and
A21: Xa is being_line by A16, Th20;
consider Xc being Subset of AS such that
A22: c = LDir Xc and
A23: Xc is being_line by A18, Th20;
consider Xb being Subset of AS such that
A24: b = LDir Xb and
A25: Xb is being_line by A17, Th20;
consider Xd being Subset of AS such that
A26: d = LDir Xd and
A27: Xd is being_line by A19, Th20;
consider Xp being Subset of AS such that
A28: p = LDir Xp and
A29: Xp is being_line by A14, Th20;
set Xa9 = the Element of AS * Xa;
set Xb9 = the Element of AS * Xb;
set Xc9 = the Element of AS * Xc;
set Xd9 = the Element of AS * Xd;
set Xp9 = the Element of AS * Xp;
consider y being Element of AS such that
A30: the Element of AS <> y and
A31: y in the Element of AS * Xa by A21, AFF_1:20, AFF_4:27;
A32: Xp // the Element of AS * Xp by A29, AFF_4:def_3;
consider t being Element of AS such that
A33: the Element of AS <> t and
A34: t in the Element of AS * Xc by A23, AFF_1:20, AFF_4:27;
set Y1 = y * ( the Element of AS * Xp);
set Y2 = t * ( the Element of AS * Xp);
A35: the Element of AS * Xp is being_line by A29, AFF_4:27;
then A36: y * ( the Element of AS * Xp) is being_line by AFF_4:27;
A37: t * ( the Element of AS * Xp) is being_line by A35, AFF_4:27;
A38: Xb // the Element of AS * Xb by A25, AFF_4:def_3;
A39: the Element of AS * Xd is being_line by A27, AFF_4:27;
A40: Xd // the Element of AS * Xd by A27, AFF_4:def_3;
A41: the Element of AS in the Element of AS * Xc by A23, AFF_4:def_3;
A42: the Element of AS in the Element of AS * Xb by A25, AFF_4:def_3;
A43: the Element of AS * Xb is being_line by A25, AFF_4:27;
A44: the Element of AS in the Element of AS * Xd by A27, AFF_4:def_3;
then consider XQ being Subset of AS such that
A45: the Element of AS * Xb c= XQ and
A46: the Element of AS * Xd c= XQ and
A47: XQ is being_plane by A43, A39, A42, AFF_4:38;
A48: the Element of AS * Xa is being_line by A21, AFF_4:27;
A49: the Element of AS * Xp // t * ( the Element of AS * Xp) by A35, AFF_4:def_3;
A50: not the Element of AS * Xd // t * ( the Element of AS * Xp)
proof
assume the Element of AS * Xd // t * ( the Element of AS * Xp) ; ::_thesis: contradiction
then Xd // t * ( the Element of AS * Xp) by A40, AFF_1:44;
then Xd // the Element of AS * Xp by A49, AFF_1:44;
then Xd // Xp by A32, AFF_1:44;
hence contradiction by A10, A12, A28, A29, A26, A27, Th11; ::_thesis: verum
end;
A51: the Element of AS * Xp // y * ( the Element of AS * Xp) by A35, AFF_4:def_3;
A52: not the Element of AS * Xb // y * ( the Element of AS * Xp)
proof
assume the Element of AS * Xb // y * ( the Element of AS * Xp) ; ::_thesis: contradiction
then Xb // y * ( the Element of AS * Xp) by A38, AFF_1:44;
then Xb // the Element of AS * Xp by A51, AFF_1:44;
then Xb // Xp by A32, AFF_1:44;
hence contradiction by A9, A12, A28, A29, A24, A25, Th11; ::_thesis: verum
end;
A53: the Element of AS in the Element of AS * Xa by A21, AFF_4:def_3;
A54: the Element of AS * Xc is being_line by A23, AFF_4:27;
then consider XP being Subset of AS such that
A55: the Element of AS * Xa c= XP and
A56: the Element of AS * Xc c= XP and
A57: XP is being_plane by A48, A53, A41, AFF_4:38;
A58: the Element of AS in the Element of AS * Xp by A29, AFF_4:def_3;
then consider X2 being Subset of AS such that
A59: the Element of AS * Xc c= X2 and
A60: the Element of AS * Xp c= X2 and
A61: X2 is being_plane by A54, A35, A41, AFF_4:38;
A62: Xc // the Element of AS * Xc by A23, AFF_4:def_3;
N = [(PDir X2),2]
proof
reconsider N9 = [(PDir X2),2] as Element of the Lines of (IncProjSp_of AS) by A61, Th23;
A63: c on N9 by A22, A62, A59, A61, Th32;
p on N9 by A28, A32, A60, A61, Th32;
hence N = [(PDir X2),2] by A3, A6, A8, A11, A63, Lm2; ::_thesis: verum
end;
then Xd '||' X2 by A4, A26, A27, A61, Th29;
then A64: the Element of AS * Xd c= X2 by A39, A41, A44, A40, A59, A61, AFF_4:43, AFF_4:56;
consider X1 being Subset of the carrier of AS such that
A65: the Element of AS * Xa c= X1 and
A66: the Element of AS * Xp c= X1 and
A67: X1 is being_plane by A48, A35, A53, A58, AFF_4:38;
A68: Xa // the Element of AS * Xa by A21, AFF_4:def_3;
M = [(PDir X1),2]
proof
reconsider M9 = [(PDir X1),2] as Element of the Lines of (IncProjSp_of AS) by A67, Th23;
A69: a on M9 by A20, A68, A65, A67, Th32;
p on M9 by A28, A32, A66, A67, Th32;
hence M = [(PDir X1),2] by A1, A5, A7, A11, A69, Lm2; ::_thesis: verum
end;
then Xb '||' X1 by A2, A24, A25, A67, Th29;
then A70: the Element of AS * Xb c= X1 by A43, A53, A42, A38, A65, A67, AFF_4:43, AFF_4:56;
y * ( the Element of AS * Xp) c= X1 by A29, A31, A65, A66, A67, AFF_4:27, AFF_4:28;
then consider z being Element of AS such that
A71: z in the Element of AS * Xb and
A72: z in y * ( the Element of AS * Xp) by A43, A36, A67, A70, A52, AFF_4:22;
t * ( the Element of AS * Xp) c= X2 by A29, A34, A59, A60, A61, AFF_4:27, AFF_4:28;
then consider u being Element of AS such that
A73: u in the Element of AS * Xd and
A74: u in t * ( the Element of AS * Xp) by A39, A37, A61, A64, A50, AFF_4:22;
set AC = Line (y,t);
set BD = Line (z,u);
A75: y in Line (y,t) by AFF_1:15;
A76: y in y * ( the Element of AS * Xp) by A35, AFF_4:def_3;
A77: the Element of AS <> z
proof
assume A78: not the Element of AS <> z ; ::_thesis: contradiction
a = LDir ( the Element of AS * Xa) by A20, A21, A48, A68, Th11
.= LDir (y * ( the Element of AS * Xp)) by A48, A53, A30, A31, A36, A76, A72, A78, AFF_1:18
.= LDir ( the Element of AS * Xp) by A35, A36, A51, Th11
.= p by A28, A29, A35, A32, Th11 ;
hence contradiction by A7, A11; ::_thesis: verum
end;
A79: z <> u
proof
assume A80: not z <> u ; ::_thesis: contradiction
b = LDir ( the Element of AS * Xb) by A24, A25, A43, A38, Th11
.= LDir ( the Element of AS * Xd) by A43, A39, A42, A44, A71, A73, A77, A80, AFF_1:18
.= d by A26, A27, A39, A40, Th11 ;
hence contradiction by A2, A4, A5, A6, A9, A12, A13, Lm2; ::_thesis: verum
end;
then A81: Line (z,u) is being_line by AFF_1:def_3;
A82: the Element of AS * Xa <> the Element of AS * Xc
proof
assume the Element of AS * Xa = the Element of AS * Xc ; ::_thesis: contradiction
then a = LDir ( the Element of AS * Xc) by A20, A21, A48, A68, Th11
.= c by A22, A23, A54, A62, Th11 ;
hence contradiction by A1, A3, A5, A6, A7, A11, A13, Lm2; ::_thesis: verum
end;
then A83: y <> t by A48, A54, A53, A41, A30, A31, A34, AFF_1:18;
then A84: Line (y,t) is being_line by AFF_1:def_3;
A85: Line (z,u) c= XQ by A71, A73, A79, A45, A46, A47, AFF_4:19;
A86: t in Line (y,t) by AFF_1:15;
y * ( the Element of AS * Xp) // t * ( the Element of AS * Xp) by A51, A49, AFF_1:44;
then consider X3 being Subset of AS such that
A87: y * ( the Element of AS * Xp) c= X3 and
A88: t * ( the Element of AS * Xp) c= X3 and
A89: X3 is being_plane by AFF_4:39;
A90: Line (z,u) c= X3 by A87, A88, A89, A72, A74, A79, AFF_4:19;
A91: a <> c by A1, A3, A5, A6, A7, A11, A13, Lm2;
A92: ( P = [(PDir XP),2] & Q = [(PDir XQ),2] )
proof
reconsider P9 = [(PDir XP),2], Q9 = [(PDir XQ),2] as LINE of (IncProjSp_of AS) by A57, A47, Th23;
A93: c on P9 by A22, A62, A56, A57, Th32;
A94: b on Q9 by A24, A38, A45, A47, Th32;
A95: d on Q9 by A26, A40, A46, A47, Th32;
a on P9 by A20, A68, A55, A57, Th32;
hence ( P = [(PDir XP),2] & Q = [(PDir XQ),2] ) by A7, A8, A9, A10, A91, A15, A93, A94, A95, Lm2; ::_thesis: verum
end;
A96: now__::_thesis:_(_Line_(y,t)_//_Line_(z,u)_implies_ex_q_being_Element_of_the_Points_of_(IncProjSp_of_AS)_st_
(_q_on_P_&_q_on_Q_)_)
reconsider q = LDir (Line (y,t)), q9 = LDir (Line (z,u)) as Element of the Points of (IncProjSp_of AS) by A84, A81, Th20;
assume A97: Line (y,t) // Line (z,u) ; ::_thesis: ex q being Element of the Points of (IncProjSp_of AS) st
( q on P & q on Q )
take q = q; ::_thesis: ( q on P & q on Q )
q = q9 by A84, A81, A97, Th11;
hence ( q on P & q on Q ) by A31, A34, A71, A73, A83, A79, A84, A81, A55, A56, A57, A45, A46, A47, A92, Th31, AFF_4:19; ::_thesis: verum
end;
A98: Line (y,t) c= XP by A31, A34, A83, A55, A56, A57, AFF_4:19;
A99: now__::_thesis:_(_ex_w_being_Element_of_AS_st_
(_w_in_Line_(y,t)_&_w_in_Line_(z,u)_)_implies_ex_q_being_POINT_of_(IncProjSp_of_AS)_st_
(_q_on_P_&_q_on_Q_)_)
given w being Element of AS such that A100: w in Line (y,t) and
A101: w in Line (z,u) ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
set R = Line ( the Element of AS,w);
A102: the Element of AS <> w
proof
assume A103: the Element of AS = w ; ::_thesis: contradiction
then the Element of AS * Xa = Line (y,t) by A48, A53, A30, A31, A84, A75, A100, AFF_1:18;
hence contradiction by A54, A41, A33, A34, A82, A84, A86, A100, A103, AFF_1:18; ::_thesis: verum
end;
then A104: Line ( the Element of AS,w) is being_line by AFF_1:def_3;
then reconsider q = LDir (Line ( the Element of AS,w)) as POINT of (IncProjSp_of AS) by Th20;
take q = q; ::_thesis: ( q on P & q on Q )
thus ( q on P & q on Q ) by A53, A42, A55, A57, A45, A47, A92, A98, A85, A100, A101, A102, A104, Th31, AFF_4:19; ::_thesis: verum
end;
t in t * ( the Element of AS * Xp) by A35, AFF_4:def_3;
then Line (y,t) c= X3 by A76, A87, A88, A89, A83, AFF_4:19;
hence ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) by A89, A84, A81, A90, A96, A99, AFF_4:22; ::_thesis: verum
end;
hence ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, Lm11; ::_thesis: verum
end;
hence ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, Lm9; ::_thesis: verum
end;
theorem Th44: :: AFPROJ:44
for AS being AffinSpace
for a, b, c, d, p being Element of the Points of (ProjHorizon AS)
for M, N, P, Q being Element of the Lines of (ProjHorizon AS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N holds
ex q being Element of the Points of (ProjHorizon AS) st
( q on P & q on Q )
proof
let AS be AffinSpace; ::_thesis: for a, b, c, d, p being Element of the Points of (ProjHorizon AS)
for M, N, P, Q being Element of the Lines of (ProjHorizon AS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N holds
ex q being Element of the Points of (ProjHorizon AS) st
( q on P & q on Q )
let a, b, c, d, p be Element of the Points of (ProjHorizon AS); ::_thesis: for M, N, P, Q being Element of the Lines of (ProjHorizon AS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N holds
ex q being Element of the Points of (ProjHorizon AS) st
( q on P & q on Q )
let M, N, P, Q be Element of the Lines of (ProjHorizon AS); ::_thesis: ( a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N implies ex q being Element of the Points of (ProjHorizon AS) st
( q on P & q on Q ) )
assume that
A1: a on M and
A2: b on M and
A3: c on N and
A4: d on N and
A5: p on M and
A6: p on N and
A7: a on P and
A8: c on P and
A9: b on Q and
A10: d on Q and
A11: not p on P and
A12: not p on Q and
A13: M <> N ; ::_thesis: ex q being Element of the Points of (ProjHorizon AS) st
( q on P & q on Q )
reconsider M9 = [M,2], N9 = [N,2], P9 = [P,2], Q9 = [Q,2] as LINE of (IncProjSp_of AS) by Th25;
reconsider a9 = a, b9 = b, c9 = c, d9 = d, p9 = p as POINT of (IncProjSp_of AS) by Th22;
A14: b9 on M9 by A2, Th37;
A15: M9 <> N9
proof
assume M9 = N9 ; ::_thesis: contradiction
then M = [N,2] `1 by MCART_1:7
.= N ;
hence contradiction by A13; ::_thesis: verum
end;
A16: d9 on N9 by A4, Th37;
A17: c9 on N9 by A3, Th37;
A18: c9 on P9 by A8, Th37;
A19: a9 on P9 by A7, Th37;
A20: p9 on N9 by A6, Th37;
A21: p9 on M9 by A5, Th37;
A22: not p9 on Q9 by A12, Th37;
A23: not p9 on P9 by A11, Th37;
A24: d9 on Q9 by A10, Th37;
A25: b9 on Q9 by A9, Th37;
a9 on M9 by A1, Th37;
then consider q9 being POINT of (IncProjSp_of AS) such that
A26: q9 on P9 and
A27: q9 on Q9 by A14, A17, A16, A21, A20, A19, A18, A25, A24, A23, A22, A15, Lm12;
[q9,[P,2]] in the Inc of (IncProjSp_of AS) by A26, INCSP_1:def_1;
then reconsider q = q9 as Element of the Points of (ProjHorizon AS) by Th42;
take q ; ::_thesis: ( q on P & q on Q )
thus ( q on P & q on Q ) by A26, A27, Th37; ::_thesis: verum
end;
registration
let AS be AffinSpace;
cluster IncProjSp_of AS -> strict linear partial up-2-dimensional up-3-rank Vebleian ;
correctness
coherence
( IncProjSp_of AS is partial & IncProjSp_of AS is linear & IncProjSp_of AS is up-2-dimensional & IncProjSp_of AS is up-3-rank & IncProjSp_of AS is Vebleian );
proof
set XX = IncProjSp_of AS;
A1: for a, b being POINT of (IncProjSp_of AS) ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A ) by Lm4;
A2: not for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) holds a on A by Lm6;
A3: for A being LINE of (IncProjSp_of AS) ex a, b, c being POINT of (IncProjSp_of AS) st
( a <> b & b <> c & c <> a & a on A & b on A & c on A )
proof
let A be LINE of (IncProjSp_of AS); ::_thesis: ex a, b, c being POINT of (IncProjSp_of AS) st
( a <> b & b <> c & c <> a & a on A & b on A & c on A )
consider a, b, c being POINT of (IncProjSp_of AS) such that
A4: a on A and
A5: b on A and
A6: c on A and
A7: a <> b and
A8: b <> c and
A9: c <> a by Lm3;
take a ; ::_thesis: ex b, c being POINT of (IncProjSp_of AS) st
( a <> b & b <> c & c <> a & a on A & b on A & c on A )
take b ; ::_thesis: ex c being POINT of (IncProjSp_of AS) st
( a <> b & b <> c & c <> a & a on A & b on A & c on A )
take c ; ::_thesis: ( a <> b & b <> c & c <> a & a on A & b on A & c on A )
thus ( a <> b & b <> c & c <> a & a on A & b on A & c on A ) by A4, A5, A6, A7, A8, A9; ::_thesis: verum
end;
A10: for a, b, c, d, p, q being POINT of (IncProjSp_of AS)
for M, N, P, Q being LINE of (IncProjSp_of AS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N holds
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) by Lm12;
for a, b being POINT of (IncProjSp_of AS)
for A, K being LINE of (IncProjSp_of AS) st a on A & b on A & a on K & b on K & not a = b holds
A = K by Lm2;
hence ( IncProjSp_of AS is partial & IncProjSp_of AS is linear & IncProjSp_of AS is up-2-dimensional & IncProjSp_of AS is up-3-rank & IncProjSp_of AS is Vebleian ) by A1, A2, A3, A10, INCPROJ:def_4, INCPROJ:def_5, INCPROJ:def_6, INCPROJ:def_7, INCPROJ:def_8; ::_thesis: verum
end;
end;
registration
cluster strict linear partial up-2-dimensional up-3-rank Vebleian 2-dimensional for IncProjStr ;
existence
ex b1 being IncProjSp st
( b1 is strict & b1 is 2-dimensional )
proof
set AS = the AffinPlane;
set XX = IncProjSp_of the AffinPlane;
for A, K being LINE of (IncProjSp_of the AffinPlane) ex a being POINT of (IncProjSp_of the AffinPlane) st
( a on A & a on K ) by Lm5;
then IncProjSp_of the AffinPlane is 2-dimensional IncProjSp by INCPROJ:def_9;
hence ex b1 being IncProjSp st
( b1 is strict & b1 is 2-dimensional ) ; ::_thesis: verum
end;
end;
registration
let AS be AffinPlane;
cluster IncProjSp_of AS -> strict 2-dimensional ;
correctness
coherence
IncProjSp_of AS is 2-dimensional ;
proof
set XX = IncProjSp_of AS;
for A, K being LINE of (IncProjSp_of AS) ex a being Element of the Points of (IncProjSp_of AS) st
( a on A & a on K ) by Lm5;
hence IncProjSp_of AS is 2-dimensional by INCPROJ:def_9; ::_thesis: verum
end;
end;
theorem :: AFPROJ:45
for AS being AffinSpace st IncProjSp_of AS is 2-dimensional holds
AS is AffinPlane
proof
let AS be AffinSpace; ::_thesis: ( IncProjSp_of AS is 2-dimensional implies AS is AffinPlane )
set x = the Element of AS;
assume A1: IncProjSp_of AS is 2-dimensional ; ::_thesis: AS is AffinPlane
consider X being Subset of AS such that
A2: the Element of AS in X and
the Element of AS in X and
the Element of AS in X and
A3: X is being_plane by AFF_4:37;
assume AS is not AffinPlane ; ::_thesis: contradiction
then consider z being Element of AS such that
A4: not z in X by A3, AFF_4:48;
set Y = Line ( the Element of AS,z);
A5: Line ( the Element of AS,z) is being_line by A2, A4, AFF_1:def_3;
then reconsider A = [(PDir X),2], K = [(Line ( the Element of AS,z)),1] as LINE of (IncProjSp_of AS) by A3, Th23;
consider a being POINT of (IncProjSp_of AS) such that
A6: a on A and
A7: a on K by A1, INCPROJ:def_9;
a is not Element of AS by A6, Th27;
then consider Y9 being Subset of AS such that
A8: a = LDir Y9 and
A9: Y9 is being_line by Th20;
Y9 '||' Line ( the Element of AS,z) by A5, A7, A8, A9, Th28;
then A10: Y9 // Line ( the Element of AS,z) by A5, A9, AFF_4:40;
A11: z in Line ( the Element of AS,z) by AFF_1:15;
A12: the Element of AS in Line ( the Element of AS,z) by AFF_1:15;
Y9 '||' X by A3, A6, A8, A9, Th29;
then Line ( the Element of AS,z) c= X by A2, A3, A5, A12, A10, AFF_4:43, AFF_4:56;
hence contradiction by A4, A11; ::_thesis: verum
end;
theorem :: AFPROJ:46
for AS being AffinSpace st AS is not AffinPlane holds
ProjHorizon AS is IncProjSp
proof
let AS be AffinSpace; ::_thesis: ( AS is not AffinPlane implies ProjHorizon AS is IncProjSp )
set XX = ProjHorizon AS;
A1: for a, b being Element of the Points of (ProjHorizon AS) ex A being Element of the Lines of (ProjHorizon AS) st
( a on A & b on A ) by Th40;
A2: for A being Element of the Lines of (ProjHorizon AS) ex a, b, c being Element of the Points of (ProjHorizon AS) st
( a <> b & b <> c & c <> a & a on A & b on A & c on A )
proof
let A be Element of the Lines of (ProjHorizon AS); ::_thesis: ex a, b, c being Element of the Points of (ProjHorizon AS) st
( a <> b & b <> c & c <> a & a on A & b on A & c on A )
consider a, b, c being Element of the Points of (ProjHorizon AS) such that
A3: a on A and
A4: b on A and
A5: c on A and
A6: a <> b and
A7: b <> c and
A8: c <> a by Th39;
take a ; ::_thesis: ex b, c being Element of the Points of (ProjHorizon AS) st
( a <> b & b <> c & c <> a & a on A & b on A & c on A )
take b ; ::_thesis: ex c being Element of the Points of (ProjHorizon AS) st
( a <> b & b <> c & c <> a & a on A & b on A & c on A )
take c ; ::_thesis: ( a <> b & b <> c & c <> a & a on A & b on A & c on A )
thus ( a <> b & b <> c & c <> a & a on A & b on A & c on A ) by A3, A4, A5, A6, A7, A8; ::_thesis: verum
end;
assume AS is not AffinPlane ; ::_thesis: ProjHorizon AS is IncProjSp
then A9: not for a being Element of the Points of (ProjHorizon AS)
for A being Element of the Lines of (ProjHorizon AS) holds a on A by Lm1;
A10: for a, b, c, d, p, q being Element of the Points of (ProjHorizon AS)
for M, N, P, Q being Element of the Lines of (ProjHorizon AS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N holds
ex q being Element of the Points of (ProjHorizon AS) st
( q on P & q on Q ) by Th44;
for a, b being Element of the Points of (ProjHorizon AS)
for A, K being Element of the Lines of (ProjHorizon AS) st a on A & b on A & a on K & b on K & not a = b holds
A = K by Th38;
hence ProjHorizon AS is IncProjSp by A1, A9, A2, A10, INCPROJ:def_4, INCPROJ:def_5, INCPROJ:def_6, INCPROJ:def_7, INCPROJ:def_8; ::_thesis: verum
end;
theorem :: AFPROJ:47
for AS being AffinSpace st ProjHorizon AS is IncProjSp holds
not AS is AffinPlane
proof
let AS be AffinSpace; ::_thesis: ( ProjHorizon AS is IncProjSp implies not AS is AffinPlane )
set XX = ProjHorizon AS;
assume ProjHorizon AS is IncProjSp ; ::_thesis: AS is not AffinPlane
then consider a being Element of the Points of (ProjHorizon AS), A being Element of the Lines of (ProjHorizon AS) such that
A1: not a on A by INCPROJ:def_6;
consider X being Subset of AS such that
A2: a = LDir X and
A3: X is being_line by Th14;
consider Y being Subset of AS such that
A4: A = PDir Y and
A5: Y is being_plane by Th15;
assume AS is AffinPlane ; ::_thesis: contradiction
then Y = the carrier of AS by A5, Th2;
then X '||' Y by A3, A5, AFF_4:42;
hence contradiction by A1, A2, A3, A4, A5, Th36; ::_thesis: verum
end;
theorem Th48: :: AFPROJ:48
for AS being AffinSpace
for M, N being Subset of AS
for o, a, b, c, a9, b9, c9 being Element of AS st M is being_line & N is being_line & M <> N & o in M & o in N & o <> b & o <> b9 & o <> c9 & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 & ( a = b or b = c or a = c ) holds
a,c9 // c,a9
proof
let AS be AffinSpace; ::_thesis: for M, N being Subset of AS
for o, a, b, c, a9, b9, c9 being Element of AS st M is being_line & N is being_line & M <> N & o in M & o in N & o <> b & o <> b9 & o <> c9 & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 & ( a = b or b = c or a = c ) holds
a,c9 // c,a9
let M, N be Subset of AS; ::_thesis: for o, a, b, c, a9, b9, c9 being Element of AS st M is being_line & N is being_line & M <> N & o in M & o in N & o <> b & o <> b9 & o <> c9 & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 & ( a = b or b = c or a = c ) holds
a,c9 // c,a9
let o, a, b, c, a9, b9, c9 be Element of AS; ::_thesis: ( M is being_line & N is being_line & M <> N & o in M & o in N & o <> b & o <> b9 & o <> c9 & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 & ( a = b or b = c or a = c ) implies a,c9 // c,a9 )
assume that
A1: M is being_line and
A2: N is being_line and
A3: M <> N and
A4: o in M and
A5: o in N and
A6: o <> b and
A7: o <> b9 and
A8: o <> c9 and
A9: b in M and
A10: c in M and
A11: a9 in N and
A12: b9 in N and
A13: c9 in N and
A14: a,b9 // b,a9 and
A15: b,c9 // c,b9 and
A16: ( a = b or b = c or a = c ) ; ::_thesis: a,c9 // c,a9
A17: c <> b9 by A1, A2, A3, A4, A5, A7, A10, A12, AFF_1:18;
now__::_thesis:_(_a_=_c_implies_a,c9_//_c,a9_)
assume A18: a = c ; ::_thesis: a,c9 // c,a9
then b,c9 // b,a9 by A14, A15, A17, AFF_1:5;
then a9 = c9 by A1, A2, A3, A4, A5, A6, A8, A9, A11, A13, AFF_4:9;
hence a,c9 // c,a9 by A18, AFF_1:2; ::_thesis: verum
end;
hence a,c9 // c,a9 by A1, A2, A3, A4, A5, A6, A7, A8, A9, A11, A12, A13, A14, A15, A16, AFF_4:9; ::_thesis: verum
end;
theorem :: AFPROJ:49
for AS being AffinSpace st IncProjSp_of AS is Pappian holds
AS is Pappian
proof
let AS be AffinSpace; ::_thesis: ( IncProjSp_of AS is Pappian implies AS is Pappian )
set XX = IncProjSp_of AS;
assume A1: IncProjSp_of AS is Pappian ; ::_thesis: AS is Pappian
for M, N being Subset of AS
for o, a, b, c, a9, b9, c9 being Element of AS st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9
proof
let M, N be Subset of AS; ::_thesis: for o, a, b, c, a9, b9, c9 being Element of AS st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9
let o, a, b, c, a9, b9, c9 be Element of AS; ::_thesis: ( M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 implies a,c9 // c,a9 )
assume that
A2: M is being_line and
A3: N is being_line and
A4: M <> N and
A5: o in M and
A6: o in N and
A7: o <> a and
A8: o <> a9 and
A9: o <> b and
A10: o <> b9 and
A11: o <> c and
A12: o <> c9 and
A13: a in M and
A14: b in M and
A15: c in M and
A16: a9 in N and
A17: b9 in N and
A18: c9 in N and
A19: a,b9 // b,a9 and
A20: b,c9 // c,b9 ; ::_thesis: a,c9 // c,a9
A21: b <> c9 by A2, A3, A4, A5, A6, A9, A14, A18, AFF_1:18;
then A22: Line (b,c9) is being_line by AFF_1:def_3;
c <> a9 by A2, A3, A4, A5, A6, A8, A15, A16, AFF_1:18;
then A23: Line (c,a9) is being_line by AFF_1:def_3;
A24: b <> a9 by A2, A3, A4, A5, A6, A8, A14, A16, AFF_1:18;
then A25: Line (b,a9) is being_line by AFF_1:def_3;
A26: c <> b9 by A2, A3, A4, A5, A6, A10, A15, A17, AFF_1:18;
then A27: Line (c,b9) is being_line by AFF_1:def_3;
reconsider A3 = [M,1], B3 = [N,1] as Element of the Lines of (IncProjSp_of AS) by A2, A3, Th23;
reconsider p = o, a1 = a9, a2 = c9, a3 = b9, b1 = a, b2 = c, b3 = b as Element of the Points of (IncProjSp_of AS) by Th20;
A28: p on A3 by A2, A5, Th26;
A29: a <> b9 by A2, A3, A4, A5, A6, A7, A13, A17, AFF_1:18;
then A30: Line (a,b9) is being_line by AFF_1:def_3;
then reconsider c1 = LDir (Line (b,c9)), c2 = LDir (Line (a,b9)) as Element of the Points of (IncProjSp_of AS) by A22, Th20;
A31: b1 on A3 by A2, A13, Th26;
a <> c9 by A2, A3, A4, A5, A6, A7, A13, A18, AFF_1:18;
then A32: Line (a,c9) is being_line by AFF_1:def_3;
then reconsider A1 = [(Line (b,c9)),1], A2 = [(Line (b,a9)),1], B1 = [(Line (a,b9)),1], B2 = [(Line (c,b9)),1], C1 = [(Line (c,a9)),1], C2 = [(Line (a,c9)),1] as Element of the Lines of (IncProjSp_of AS) by A30, A25, A22, A27, A23, Th23;
A33: c2 on B1 by A30, Th30;
A34: b3 on A3 by A2, A14, Th26;
A35: b2 on A3 by A2, A15, Th26;
consider Y being Subset of AS such that
A36: M c= Y and
A37: N c= Y and
A38: Y is being_plane by A2, A3, A5, A6, AFF_4:38;
reconsider C39 = [(PDir Y),2] as Element of the Lines of (IncProjSp_of AS) by A38, Th23;
A39: c1 on C39 by A14, A18, A36, A37, A38, A21, A22, Th31, AFF_4:19;
A40: c2 on C39 by A13, A17, A36, A37, A38, A29, A30, Th31, AFF_4:19;
A41: a1 on B3 by A3, A16, Th26;
A42: a3 on B3 by A3, A17, Th26;
A43: p on B3 by A3, A6, Th26;
b9 in Line (a,b9) by AFF_1:15;
then A44: a3 on B1 by A30, Th26;
a in Line (a,b9) by AFF_1:15;
then A45: b1 on B1 by A30, Th26;
A46: c in Line (c,a9) by AFF_1:15;
then A47: b2 on C1 by A23, Th26;
Line (b,c9) // Line (c,b9) by A20, A21, A26, AFF_1:37;
then Line (b,c9) '||' Line (c,b9) by A22, A27, AFF_4:40;
then A48: c1 on B2 by A22, A27, Th28;
A49: c9 in Line (a,c9) by AFF_1:15;
then A50: a2 on C2 by A32, Th26;
b9 in Line (c,b9) by AFF_1:15;
then A51: a3 on B2 by A27, Th26;
c in Line (c,b9) by AFF_1:15;
then A52: b2 on B2 by A27, Th26;
c9 in Line (b,c9) by AFF_1:15;
then A53: a2 on A1 by A22, Th26;
b in Line (b,c9) by AFF_1:15;
then A54: b3 on A1 by A22, Th26;
A55: a2 on B3 by A3, A18, Th26;
Line (a,b9) // Line (b,a9) by A19, A29, A24, AFF_1:37;
then Line (a,b9) '||' Line (b,a9) by A30, A25, AFF_4:40;
then A56: c2 on A2 by A30, A25, Th28;
A57: a in Line (a,c9) by AFF_1:15;
then A58: b1 on C2 by A32, Th26;
a9 in Line (b,a9) by AFF_1:15;
then A59: a1 on A2 by A25, Th26;
b in Line (b,a9) by AFF_1:15;
then A60: b3 on A2 by A25, Th26;
A61: a9 in Line (c,a9) by AFF_1:15;
then A62: a1 on C1 by A23, Th26;
A63: c1 on A1 by A22, Th30;
now__::_thesis:_(_b1_<>_b2_&_b2_<>_b3_&_b3_<>_b1_implies_a,c9_//_c,a9_)
A64: A3 <> B3
proof
assume A3 = B3 ; ::_thesis: contradiction
then M = [N,1] `1 by MCART_1:7
.= N ;
hence contradiction by A4; ::_thesis: verum
end;
( not p on C1 & not p on C2 )
proof
assume ( p on C1 or p on C2 ) ; ::_thesis: contradiction
then ( a1 on A3 or a2 on A3 ) by A7, A11, A28, A31, A35, A58, A50, A47, A62, Lm2;
hence contradiction by A8, A12, A28, A43, A41, A55, A64, INCPROJ:def_4; ::_thesis: verum
end;
then consider c3 being Element of the Points of (IncProjSp_of AS) such that
A65: c3 on C1 and
A66: c3 on C2 by A28, A31, A35, A43, A41, A55, A58, A50, A47, A62, A64, INCPROJ:def_8;
A67: {a2,b1,c3} on C2 by A58, A50, A66, INCSP_1:2;
A68: {a1,b3,c2} on A2 by A60, A59, A56, INCSP_1:2;
A69: {a3,b1,c2} on B1 by A45, A44, A33, INCSP_1:2;
assume that
A70: b1 <> b2 and
A71: b2 <> b3 and
A72: b3 <> b1 ; ::_thesis: a,c9 // c,a9
A73: p,b1,b2,b3 are_mutually_different by A7, A9, A11, A70, A71, A72, ZFMISC_1:def_6;
( a1 <> a2 & a2 <> a3 & a1 <> a3 )
proof
A74: now__::_thesis:_not_a9_=_c9
assume a9 = c9 ; ::_thesis: contradiction
then a,b9 // c,b9 by A19, A20, A24, AFF_1:5;
hence contradiction by A2, A3, A4, A5, A6, A7, A10, A13, A15, A17, A70, AFF_4:9; ::_thesis: verum
end;
assume ( not a1 <> a2 or not a2 <> a3 or not a1 <> a3 ) ; ::_thesis: contradiction
hence contradiction by A2, A3, A4, A5, A6, A7, A9, A10, A13, A14, A15, A17, A19, A20, A71, A72, A74, AFF_4:9; ::_thesis: verum
end;
then A75: p,a1,a2,a3 are_mutually_different by A8, A10, A12, ZFMISC_1:def_6;
A76: {a1,a2,a3} on B3 by A41, A55, A42, INCSP_1:2;
A77: {b1,b2,b3} on A3 by A31, A35, A34, INCSP_1:2;
A78: {a3,b2,c1} on B2 by A51, A52, A48, INCSP_1:2;
A79: {a2,b3,c1} on A1 by A53, A54, A63, INCSP_1:2;
A80: p on B3 by A3, A6, Th26;
A81: p on A3 by A2, A5, Th26;
A82: {c1,c2} on C39 by A39, A40, INCSP_1:1;
{a1,b2,c3} on C1 by A47, A62, A65, INCSP_1:2;
then c3 on C39 by A1, A75, A73, A64, A81, A80, A79, A69, A68, A78, A67, A77, A76, A82, INCPROJ:def_14;
then c3 is not Element of AS by Th27;
then consider Y being Subset of AS such that
A83: c3 = LDir Y and
A84: Y is being_line by Th20;
Y '||' Line (c,a9) by A23, A65, A83, A84, Th28;
then A85: Y // Line (c,a9) by A23, A84, AFF_4:40;
Y '||' Line (a,c9) by A32, A66, A83, A84, Th28;
then Y // Line (a,c9) by A32, A84, AFF_4:40;
then Line (a,c9) // Line (c,a9) by A85, AFF_1:44;
hence a,c9 // c,a9 by A57, A49, A46, A61, AFF_1:39; ::_thesis: verum
end;
hence a,c9 // c,a9 by A2, A3, A4, A5, A6, A9, A10, A12, A14, A15, A16, A17, A18, A19, A20, Th48; ::_thesis: verum
end;
hence AS is Pappian by AFF_2:def_2; ::_thesis: verum
end;
theorem Th50: :: AFPROJ:50
for AS being AffinSpace
for A, P, C being Subset of AS
for o, a, b, c, a9, b9, c9 being Element of AS st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & ( o = a9 or a = a9 ) holds
b,c // b9,c9
proof
let AS be AffinSpace; ::_thesis: for A, P, C being Subset of AS
for o, a, b, c, a9, b9, c9 being Element of AS st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & ( o = a9 or a = a9 ) holds
b,c // b9,c9
let A, P, C be Subset of AS; ::_thesis: for o, a, b, c, a9, b9, c9 being Element of AS st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & ( o = a9 or a = a9 ) holds
b,c // b9,c9
let o, a, b, c, a9, b9, c9 be Element of AS; ::_thesis: ( o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & ( o = a9 or a = a9 ) implies b,c // b9,c9 )
assume that
A1: o in A and
A2: o in P and
A3: o in C and
A4: o <> a and
A5: o <> b and
A6: o <> c and
A7: a in A and
A8: b in P and
A9: b9 in P and
A10: c in C and
A11: c9 in C and
A12: A is being_line and
A13: P is being_line and
A14: C is being_line and
A15: A <> P and
A16: A <> C and
A17: a,b // a9,b9 and
A18: a,c // a9,c9 and
A19: ( o = a9 or a = a9 ) ; ::_thesis: b,c // b9,c9
A20: now__::_thesis:_(_a_=_a9_implies_b,c_//_b9,c9_)
assume A21: a = a9 ; ::_thesis: b,c // b9,c9
then A22: c = c9 by A1, A3, A4, A6, A7, A10, A11, A12, A14, A16, A18, AFF_4:9;
b = b9 by A1, A2, A4, A5, A7, A8, A9, A12, A13, A15, A17, A21, AFF_4:9;
hence b,c // b9,c9 by A22, AFF_1:2; ::_thesis: verum
end;
now__::_thesis:_(_o_=_a9_implies_b,c_//_b9,c9_)
assume A23: o = a9 ; ::_thesis: b,c // b9,c9
then A24: o = c9 by A1, A3, A4, A6, A7, A10, A11, A12, A14, A16, A18, AFF_4:8;
o = b9 by A1, A2, A4, A5, A7, A8, A9, A12, A13, A15, A17, A23, AFF_4:8;
hence b,c // b9,c9 by A24, AFF_1:3; ::_thesis: verum
end;
hence b,c // b9,c9 by A19, A20; ::_thesis: verum
end;
theorem :: AFPROJ:51
for AS being AffinSpace st IncProjSp_of AS is Desarguesian holds
AS is Desarguesian
proof
let AS be AffinSpace; ::_thesis: ( IncProjSp_of AS is Desarguesian implies AS is Desarguesian )
set XX = IncProjSp_of AS;
assume A1: IncProjSp_of AS is Desarguesian ; ::_thesis: AS is Desarguesian
for A, P, C being Subset of AS
for o, a, b, c, a9, b9, c9 being Element of AS st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9
proof
let A, P, C be Subset of AS; ::_thesis: for o, a, b, c, a9, b9, c9 being Element of AS st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9
let o, a, b, c, a9, b9, c9 be Element of AS; ::_thesis: ( o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )
assume that
A2: o in A and
A3: o in P and
A4: o in C and
A5: o <> a and
A6: o <> b and
A7: o <> c and
A8: a in A and
A9: a9 in A and
A10: b in P and
A11: b9 in P and
A12: c in C and
A13: c9 in C and
A14: A is being_line and
A15: P is being_line and
A16: C is being_line and
A17: A <> P and
A18: A <> C and
A19: a,b // a9,b9 and
A20: a,c // a9,c9 ; ::_thesis: b,c // b9,c9
now__::_thesis:_(_P_<>_C_implies_b,c_//_b9,c9_)
assume A21: P <> C ; ::_thesis: b,c // b9,c9
now__::_thesis:_(_a_<>_a9_&_o_<>_a9_implies_b,c_//_b9,c9_)
reconsider p = o, a1 = a, b1 = a9, a2 = b, b2 = b9, a3 = c, b3 = c9 as Element of the Points of (IncProjSp_of AS) by Th20;
reconsider C1 = [A,1], C2 = [P,1], C39 = [C,1] as Element of the Lines of (IncProjSp_of AS) by A14, A15, A16, Th23;
assume that
A22: a <> a9 and
A23: o <> a9 ; ::_thesis: b,c // b9,c9
A24: o <> c9 by A2, A4, A5, A7, A8, A9, A12, A14, A16, A18, A20, A23, AFF_4:8;
A25: a9 <> c9 by A2, A4, A9, A13, A14, A16, A18, A23, AFF_1:18;
then A26: Line (a9,c9) is being_line by AFF_1:def_3;
A27: o <> b9 by A2, A3, A5, A6, A8, A9, A10, A14, A15, A17, A19, A23, AFF_4:8;
then b9 <> c9 by A3, A4, A11, A13, A15, A16, A21, AFF_1:18;
then A28: Line (b9,c9) is being_line by AFF_1:def_3;
b <> c by A3, A4, A6, A10, A12, A15, A16, A21, AFF_1:18;
then A29: Line (b,c) is being_line by AFF_1:def_3;
A30: a <> c by A2, A4, A5, A8, A12, A14, A16, A18, AFF_1:18;
then A31: Line (a,c) is being_line by AFF_1:def_3;
A32: a <> b by A2, A3, A5, A8, A10, A14, A15, A17, AFF_1:18;
then A33: Line (a,b) is being_line by AFF_1:def_3;
then reconsider s = LDir (Line (a,b)), r = LDir (Line (a,c)) as Element of the Points of (IncProjSp_of AS) by A31, Th20;
A34: p on C2 by A3, A15, Th26;
A35: a9 <> b9 by A2, A3, A9, A11, A14, A15, A17, A23, AFF_1:18;
then A36: Line (a9,b9) is being_line by AFF_1:def_3;
then reconsider A1 = [(Line (b,c)),1], A2 = [(Line (a,c)),1], A3 = [(Line (a,b)),1], B1 = [(Line (b9,c9)),1], B2 = [(Line (a9,c9)),1], B3 = [(Line (a9,b9)),1] as Element of the Lines of (IncProjSp_of AS) by A33, A29, A31, A28, A26, Th23;
A37: r on A2 by A31, Th30;
A38: c in Line (b,c) by AFF_1:15;
then A39: a3 on A1 by A29, Th26;
A40: a3 on A1 by A29, A38, Th26;
A41: c9 in Line (a9,c9) by AFF_1:15;
then A42: b3 on B2 by A26, Th26;
A43: a9 in Line (a9,c9) by AFF_1:15;
then A44: b1 on B2 by A26, Th26;
A45: Line (a,c) // Line (a9,c9) by A20, A30, A25, AFF_1:37;
then Line (a,c) '||' Line (a9,c9) by A31, A26, AFF_4:40;
then r on B2 by A31, A26, Th28;
then A46: {b1,r,b3} on B2 by A44, A42, INCSP_1:2;
A47: c <> c9 by A2, A4, A5, A7, A8, A9, A12, A14, A16, A18, A20, A22, AFF_4:9;
A48: b1 on C1 by A9, A14, Th26;
A49: a3 on C39 by A12, A16, Th26;
A50: b9 in Line (a9,b9) by AFF_1:15;
then A51: b2 on B3 by A36, Th26;
A52: a9 in Line (a9,b9) by AFF_1:15;
then A53: b1 on B3 by A36, Th26;
A54: Line (a,b) // Line (a9,b9) by A19, A32, A35, AFF_1:37;
then Line (a,b) '||' Line (a9,b9) by A33, A36, AFF_4:40;
then s on B3 by A33, A36, Th28;
then A55: {b1,s,b2} on B3 by A53, A51, INCSP_1:2;
A56: now__::_thesis:_not_C2_=_C39
assume C2 = C39 ; ::_thesis: contradiction
then P = [C,1] `1 by MCART_1:7
.= C ;
hence contradiction by A21; ::_thesis: verum
end;
A57: now__::_thesis:_not_C1_=_C39
assume C1 = C39 ; ::_thesis: contradiction
then A = [C,1] `1 by MCART_1:7
.= C ;
hence contradiction by A18; ::_thesis: verum
end;
now__::_thesis:_not_C1_=_C2
assume C1 = C2 ; ::_thesis: contradiction
then A = [P,1] `1 by MCART_1:7
.= P ;
hence contradiction by A17; ::_thesis: verum
end;
then A58: C1,C2,C39 are_mutually_different by A56, A57, ZFMISC_1:def_5;
A59: a1 on C1 by A8, A14, Th26;
A60: b3 on C39 by A13, A16, Th26;
A61: p on C39 by A4, A16, Th26;
then A62: {p,a3,b3} on C39 by A49, A60, INCSP_1:2;
p on C1 by A2, A14, Th26;
then A63: {p,b1,a1} on C1 by A48, A59, INCSP_1:2;
A64: b2 on C2 by A11, A15, Th26;
A65: a in Line (a,c) by AFF_1:15;
then A66: a1 on A2 by A31, Th26;
A67: c in Line (a,c) by AFF_1:15;
then a3 on A2 by A31, Th26;
then A68: {a3,r,a1} on A2 by A37, A66, INCSP_1:2;
A69: b9 in Line (b9,c9) by AFF_1:15;
then A70: b2 on B1 by A28, Th26;
A71: c9 in Line (b9,c9) by AFF_1:15;
then A72: b3 on B1 by A28, Th26;
A73: b3 on B1 by A28, A71, Th26;
A74: a2 on C2 by A10, A15, Th26;
then A75: {p,a2,b2} on C2 by A34, A64, INCSP_1:2;
A76: b in Line (b,c) by AFF_1:15;
then A77: a2 on A1 by A29, Th26;
( not p on A1 & not p on B1 )
proof
assume ( p on A1 or p on B1 ) ; ::_thesis: contradiction
then ( a3 on C2 or b3 on C2 ) by A6, A27, A34, A74, A64, A77, A40, A70, A73, INCPROJ:def_4;
hence contradiction by A7, A24, A34, A61, A49, A60, A56, INCPROJ:def_4; ::_thesis: verum
end;
then consider t being Element of the Points of (IncProjSp_of AS) such that
A78: t on A1 and
A79: t on B1 by A34, A61, A74, A64, A49, A60, A77, A40, A70, A73, A56, INCPROJ:def_8;
a2 on A1 by A29, A76, Th26;
then A80: {a3,a2,t} on A1 by A78, A39, INCSP_1:2;
b2 on B1 by A28, A69, Th26;
then A81: {t,b2,b3} on B1 by A79, A72, INCSP_1:2;
A82: a in Line (a,b) by AFF_1:15;
then A83: a1 on A3 by A33, Th26;
A84: s on A3 by A33, Th30;
A85: b in Line (a,b) by AFF_1:15;
then a2 on A3 by A33, Th26;
then A86: {a2,s,a1} on A3 by A84, A83, INCSP_1:2;
b <> b9 by A2, A3, A5, A6, A8, A9, A10, A14, A15, A17, A19, A22, AFF_4:9;
then consider O being Element of the Lines of (IncProjSp_of AS) such that
A87: {r,s,t} on O by A1, A5, A6, A7, A22, A23, A27, A24, A47, A63, A75, A62, A80, A68, A86, A81, A46, A55, A58, INCPROJ:def_13;
A88: t on O by A87, INCSP_1:2;
A89: s on O by A87, INCSP_1:2;
A90: r on O by A87, INCSP_1:2;
A91: now__::_thesis:_(_r_<>_s_implies_b,c_//_b9,c9_)
assume A92: r <> s ; ::_thesis: b,c // b9,c9
ex X being Subset of AS st
( O = [(PDir X),2] & X is being_plane )
proof
reconsider x = LDir (Line (a,b)), y = LDir (Line (a,c)) as Element of the Points of (ProjHorizon AS) by A33, A31, Th14;
A93: [y,O] in the Inc of (IncProjSp_of AS) by A90, INCSP_1:def_1;
[x,O] in the Inc of (IncProjSp_of AS) by A89, INCSP_1:def_1;
then consider Z9 being Element of the Lines of (ProjHorizon AS) such that
A94: O = [Z9,2] by A92, A93, Th41;
consider X being Subset of AS such that
A95: Z9 = PDir X and
A96: X is being_plane by Th15;
take X ; ::_thesis: ( O = [(PDir X),2] & X is being_plane )
thus ( O = [(PDir X),2] & X is being_plane ) by A94, A95, A96; ::_thesis: verum
end;
then t is not Element of AS by A88, Th27;
then consider Y being Subset of AS such that
A97: t = LDir Y and
A98: Y is being_line by Th20;
Y '||' Line (b9,c9) by A28, A79, A97, A98, Th28;
then A99: Y // Line (b9,c9) by A28, A98, AFF_4:40;
Y '||' Line (b,c) by A29, A78, A97, A98, Th28;
then Y // Line (b,c) by A29, A98, AFF_4:40;
then Line (b,c) // Line (b9,c9) by A99, AFF_1:44;
hence b,c // b9,c9 by A76, A38, A69, A71, AFF_1:39; ::_thesis: verum
end;
now__::_thesis:_(_r_=_s_implies_b,c_//_b9,c9_)
assume r = s ; ::_thesis: b,c // b9,c9
then A100: Line (a,b) // Line (a,c) by A33, A31, Th11;
then Line (a,b) // Line (a9,c9) by A45, AFF_1:44;
then Line (a9,b9) // Line (a9,c9) by A54, AFF_1:44;
then A101: c9 in Line (a9,b9) by A52, A43, A41, AFF_1:45;
c in Line (a,b) by A82, A65, A67, A100, AFF_1:45;
hence b,c // b9,c9 by A85, A50, A54, A101, AFF_1:39; ::_thesis: verum
end;
hence b,c // b9,c9 by A91; ::_thesis: verum
end;
hence b,c // b9,c9 by A2, A3, A4, A5, A6, A7, A8, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, Th50; ::_thesis: verum
end;
hence b,c // b9,c9 by A10, A11, A12, A13, A15, AFF_1:51; ::_thesis: verum
end;
hence AS is Desarguesian by AFF_2:def_4; ::_thesis: verum
end;
theorem :: AFPROJ:52
for AS being AffinSpace st IncProjSp_of AS is Fanoian holds
AS is Fanoian
proof
let AS be AffinSpace; ::_thesis: ( IncProjSp_of AS is Fanoian implies AS is Fanoian )
set XX = IncProjSp_of AS;
assume A1: IncProjSp_of AS is Fanoian ; ::_thesis: AS is Fanoian
for a, b, c, d being Element of AS st a,b // c,d & a,c // b,d & a,d // b,c holds
a,b // a,c
proof
let a, b, c, d be Element of AS; ::_thesis: ( a,b // c,d & a,c // b,d & a,d // b,c implies a,b // a,c )
assume that
A2: a,b // c,d and
A3: a,c // b,d and
A4: a,d // b,c ; ::_thesis: a,b // a,c
assume A5: not a,b // a,c ; ::_thesis: contradiction
then A6: a <> d by A2, AFF_1:4;
then A7: Line (a,d) is being_line by AFF_1:def_3;
A8: now__::_thesis:_not_b_=_d
assume b = d ; ::_thesis: contradiction
then b,a // b,c by A2, AFF_1:4;
then LIN b,a,c by AFF_1:def_1;
then LIN a,b,c by AFF_1:6;
hence contradiction by A5, AFF_1:def_1; ::_thesis: verum
end;
then A9: Line (b,d) is being_line by AFF_1:def_3;
A10: now__::_thesis:_not_c_=_d
assume c = d ; ::_thesis: contradiction
then c,a // c,b by A3, AFF_1:4;
then LIN c,a,b by AFF_1:def_1;
then LIN a,b,c by AFF_1:6;
hence contradiction by A5, AFF_1:def_1; ::_thesis: verum
end;
then A11: Line (c,d) is being_line by AFF_1:def_3;
A12: a <> c by A5, AFF_1:3;
then A13: Line (a,c) is being_line by AFF_1:def_3;
A14: a <> b by A5, AFF_1:3;
then A15: Line (a,b) is being_line by AFF_1:def_3;
then reconsider a9 = LDir (Line (a,b)), b9 = LDir (Line (a,c)), c9 = LDir (Line (a,d)) as Element of the Points of (IncProjSp_of AS) by A13, A7, Th20;
A16: b <> c by A5, AFF_1:2;
then A17: Line (b,c) is being_line by AFF_1:def_3;
then reconsider L1 = [(Line (a,b)),1], Q1 = [(Line (c,d)),1], R1 = [(Line (b,d)),1], S1 = [(Line (a,c)),1], A1 = [(Line (a,d)),1], B1 = [(Line (b,c)),1] as Element of the Lines of (IncProjSp_of AS) by A15, A11, A9, A13, A7, Th23;
reconsider p = a, q = d, r = c, s = b as Element of the Points of (IncProjSp_of AS) by Th20;
A18: a9 on L1 by A15, Th30;
c in Line (b,c) by AFF_1:15;
then A19: r on B1 by A17, Th26;
b in Line (b,c) by AFF_1:15;
then A20: s on B1 by A17, Th26;
Line (a,d) // Line (b,c) by A4, A16, A6, AFF_1:37;
then Line (a,d) '||' Line (b,c) by A7, A17, AFF_4:40;
then c9 on B1 by A7, A17, Th28;
then A21: {c9,r,s} on B1 by A19, A20, INCSP_1:2;
A22: d in Line (b,d) by AFF_1:15;
then A23: q on R1 by A9, Th26;
A24: c in Line (a,c) by AFF_1:15;
then A25: r on S1 by A13, Th26;
A26: b9 on S1 by A13, Th30;
A27: a in Line (a,c) by AFF_1:15;
then p on S1 by A13, Th26;
then A28: {b9,p,r} on S1 by A25, A26, INCSP_1:2;
A29: Line (a,c) // Line (b,d) by A3, A12, A8, AFF_1:37;
then Line (a,c) '||' Line (b,d) by A9, A13, AFF_4:40;
then A30: b9 on R1 by A9, A13, Th28;
A31: b in Line (b,d) by AFF_1:15;
then s on R1 by A9, Th26;
then A32: {b9,q,s} on R1 by A23, A30, INCSP_1:2;
A33: now__::_thesis:_not_Line_(a,c)_=_Line_(b,d)
assume Line (a,c) = Line (b,d) ; ::_thesis: contradiction
then LIN a,c,b by A31, AFF_1:def_2;
then LIN a,b,c by AFF_1:6;
hence contradiction by A5, AFF_1:def_1; ::_thesis: verum
end;
A34: now__::_thesis:_(_not_q_on_S1_&_not_s_on_S1_)
assume ( q on S1 or s on S1 ) ; ::_thesis: contradiction
then ( d in Line (a,c) or b in Line (a,c) ) by Th26;
hence contradiction by A31, A22, A33, A29, AFF_1:45; ::_thesis: verum
end;
A35: now__::_thesis:_(_not_p_on_R1_&_not_r_on_R1_)
assume ( p on R1 or r on R1 ) ; ::_thesis: contradiction
then ( a in Line (b,d) or c in Line (b,d) ) by Th26;
hence contradiction by A27, A24, A33, A29, AFF_1:45; ::_thesis: verum
end;
A36: a in Line (a,b) by AFF_1:15;
then consider Y being Subset of AS such that
A37: Line (a,b) c= Y and
A38: Line (a,c) c= Y and
A39: Y is being_plane by A27, A15, A13, AFF_4:38;
reconsider C1 = [(PDir Y),2] as Element of the Lines of (IncProjSp_of AS) by A39, Th23;
A40: b9 on C1 by A13, A38, A39, Th31;
A41: Line (a,b) // Line (c,d) by A2, A14, A10, AFF_1:37;
then Line (a,b) '||' Line (c,d) by A15, A11, AFF_4:40;
then A42: a9 on Q1 by A15, A11, Th28;
d in Line (a,d) by AFF_1:15;
then A43: q on A1 by A7, Th26;
a in Line (a,d) by AFF_1:15;
then A44: p on A1 by A7, Th26;
c9 on A1 by A7, Th30;
then A45: {c9,p,q} on A1 by A44, A43, INCSP_1:2;
A46: b in Line (a,b) by AFF_1:15;
then A47: s on L1 by A15, Th26;
a9 on C1 by A15, A37, A39, Th31;
then A48: {a9,b9} on C1 by A40, INCSP_1:1;
A49: d in Line (c,d) by AFF_1:15;
then A50: q on Q1 by A11, Th26;
A51: c in Line (c,d) by AFF_1:15;
then r on Q1 by A11, Th26;
then A52: {a9,q,r} on Q1 by A50, A42, INCSP_1:2;
A53: now__::_thesis:_not_Line_(a,b)_=_Line_(c,d)
assume Line (a,b) = Line (c,d) ; ::_thesis: contradiction
then LIN a,b,c by A51, AFF_1:def_2;
hence contradiction by A5, AFF_1:def_1; ::_thesis: verum
end;
A54: now__::_thesis:_(_not_q_on_L1_&_not_r_on_L1_)
assume ( q on L1 or r on L1 ) ; ::_thesis: contradiction
then ( d in Line (a,b) or c in Line (a,b) ) by Th26;
hence contradiction by A51, A49, A53, A41, AFF_1:45; ::_thesis: verum
end;
A55: now__::_thesis:_(_not_p_on_Q1_&_not_s_on_Q1_)
assume ( p on Q1 or s on Q1 ) ; ::_thesis: contradiction
then ( a in Line (c,d) or b in Line (c,d) ) by Th26;
hence contradiction by A36, A46, A53, A41, AFF_1:45; ::_thesis: verum
end;
Line (b,d) = b * (Line (a,c)) by A31, A13, A29, AFF_4:def_3;
then Line (b,d) c= Y by A46, A13, A37, A38, A39, AFF_4:28;
then A56: c9 on C1 by A36, A22, A6, A7, A37, A39, Th31, AFF_4:19;
p on L1 by A36, A15, Th26;
then {a9,p,s} on L1 by A47, A18, INCSP_1:2;
hence contradiction by A1, A56, A54, A34, A55, A35, A52, A32, A28, A45, A21, A48, INCPROJ:def_12; ::_thesis: verum
end;
hence AS is Fanoian by PAPDESAF:def_1; ::_thesis: verum
end;