:: AFPROJ semantic presentation
theorem Th1: :: AFPROJ:1
proof
let c
1 be
AffinSpace;
let c
2 be
Subset of c
1;
assume that E2:
c
1 is
AffinPlane
and E3:
c
2 = the
carrier of c
1
;
consider c
3, c
4, c
5 being
Element of c
1 such that E4:
not
LIN c
3,c
4,c
5
by AFF_1:21;
E5:
( c
3 <> c
4 & c
3 <> c
5 )
by E4, AFF_1:16;
set c
6 =
Line c
3,c
4;
set c
7 =
Line c
3,c
5;
E6:
( c
3 in Line c
3,c
4 & c
3 in Line c
3,c
5 & c
4 in Line c
3,c
4 & c
5 in Line c
3,c
5 &
Line c
3,c
4 is_line &
Line c
3,c
5 is_line )
by E5, AFF_1:26, AFF_1:def 3;
E7:
not
Line c
3,c
5 // Line c
3,c
4
set c
8 =
Plane (Line c3,c5),
(Line c3,c4);
E8:
Plane (Line c3,c5),
(Line c3,c4) is_plane
by E6, E7, AFF_4:def 2;
now
let c
9 be
set ;
assume
c
9 in c
2
;
then reconsider c
10 = c
9 as
Element of c
1 ;
set c
11 = c
10 * (Line c3,c5);
E9:
( c
10 * (Line c3,c5) is_line &
Line c
3,c
5 // c
10 * (Line c3,c5) & c
10 in c
10 * (Line c3,c5) )
by E6, AFF_4:27, AFF_4:def 3;
then
not c
10 * (Line c3,c5) // Line c
3,c
4
by E7, AFF_1:58;
then consider c
12 being
Element of c
1 such that E10:
( c
12 in c
10 * (Line c3,c5) & c
12 in Line c
3,c
4 )
by E2, E6, E9, AFF_1:72;
c
10,c
12 // Line c
3,c
5
by E9, E10, AFF_1:54;
then
c
10 in { b1 where B is Element of c1 : ex b1 being Element of c1 st
( b1,b2 // Line c3,c5 & b2 in Line c3,c4 ) }
by E10;
hence
c
9 in Plane (Line c3,c5),
(Line c3,c4)
by AFF_4:def 1;
end;
then
c
2 c= Plane (Line c3,c5),
(Line c3,c4)
by TARSKI:def 3;
hence
c
2 is_plane
by E3, E8, XBOOLE_0:def 10;
end;
theorem Th2: :: AFPROJ:2
theorem Th3: :: AFPROJ:3
theorem Th4: :: AFPROJ:4
theorem Th5: :: AFPROJ:5
proof
let c
1 be
AffinSpace;
let c
2, c
3, c
4, c
5 be
Subset of c
1;
assume that E5:
not c
2 // c
3
and E6:
( c
2 '||' c
4 & c
2 '||' c
5 & c
3 '||' c
4 & c
3 '||' c
5 )
and E7:
( c
2 is_line & c
3 is_line & c
4 is_plane & c
5 is_plane )
;
E8:
( c
4 <> {} & c
5 <> {} )
by E7, AFF_4:59;
consider c
6 being
Element of c
4;
consider c
7 being
Element of c
5;
reconsider c
8 = c
6, c
9 = c
7 as
Element of c
1 by E8, TARSKI:def 3;
( c
8 * c
2 c= c
8 + c
4 & c
8 * c
3 c= c
8 + c
4 & c
9 * c
2 c= c
9 + c
5 & c
9 * c
3 c= c
9 + c
5 )
by E6, E7, AFF_4:68;
then E9:
( c
8 * c
2 c= c
4 & c
8 * c
3 c= c
4 & c
9 * c
2 c= c
5 & c
9 * c
3 c= c
5 )
by E7, E8, AFF_4:66;
E10:
( c
2 // c
8 * c
2 & c
2 // c
9 * c
2 & c
3 // c
8 * c
3 & c
3 // c
9 * c
3 )
by E7, AFF_4:def 3;
E11:
not c
8 * c
2 // c
8 * c
3
( c
8 * c
2 // c
9 * c
2 & c
8 * c
3 // c
9 * c
3 )
by E10, AFF_1:58;
hence
c
4 '||' c
5
by E7, E9, E11, AFF_4:55;
end;
theorem Th6: :: AFPROJ:6
:: deftheorem Def1 defines AfLines AFPROJ:def 1 :
:: deftheorem Def2 defines AfPlanes AFPROJ:def 2 :
theorem Th7: :: AFPROJ:7
theorem Th8: :: AFPROJ:8
definition
let c
1 be
AffinSpace;
func LinesParallelity c
1 -> Equivalence_Relation of
AfLines a
1 equals :: AFPROJ:def 3
{ [b1,b2] where B is Subset of a1, B is Subset of a1 : ( b1 is_line & b2 is_line & b1 '||' b2 ) } ;
coherence
{ [b1,b2] where B is Subset of c1, B is Subset of c1 : ( b1 is_line & b2 is_line & b1 '||' b2 ) } is Equivalence_Relation of AfLines c1
proof
set c
2 =
{ [b1,b2] where B is Subset of c1, B is Subset of c1 : ( b1 is_line & b2 is_line & b1 '||' b2 ) } ;
set c
3 =
AfLines c
1;
set c
4 =
[:(AfLines c1),(AfLines c1):];
E8:
for b
1, b
2 being
Subset of c
1 holds
( b
1 is_line & b
2 is_line implies (
[b1,b2] in { [b3,b4] where B is Subset of c1, B is Subset of c1 : ( b3 is_line & b4 is_line & b3 '||' b4 ) } iff b
1 '||' b
2 ) )
then
{ [b1,b2] where B is Subset of c1, B is Subset of c1 : ( b1 is_line & b2 is_line & b1 '||' b2 ) } c= [:(AfLines c1),(AfLines c1):]
by TARSKI:def 3;
then reconsider c
5 =
{ [b1,b2] where B is Subset of c1, B is Subset of c1 : ( b1 is_line & b2 is_line & b1 '||' b2 ) } as
Relation of
AfLines c
1,
AfLines c
1 by RELSET_1:def 1;
then
c
5 is_reflexive_in AfLines c
1
by RELAT_2:def 1;
then E9:
(
dom c
5 = AfLines c
1 &
field c
5 = AfLines c
1 )
by ORDERS_1:98;
now
let c
6, c
7 be
set ;
assume that E10:
( c
6 in AfLines c
1 & c
7 in AfLines c
1 )
and E11:
[c6,c7] in c
5
;
consider c
8 being
Subset of c
1 such that E12:
( c
6 = c
8 & c
8 is_line )
by E10;
consider c
9 being
Subset of c
1 such that E13:
( c
7 = c
9 & c
9 is_line )
by E10;
c
8 '||' c
9
by E8, E11, E12, E13;
then
c
8 // c
9
by E12, E13, AFF_4:40;
then
c
9 '||' c
8
by E12, E13, AFF_4:40;
hence
[c7,c6] in c
5
by E12, E13;
end;
then E10:
c
5 is_symmetric_in AfLines c
1
by RELAT_2:def 3;
now
let c
6, c
7, c
8 be
set ;
assume that E11:
( c
6 in AfLines c
1 & c
7 in AfLines c
1 & c
8 in AfLines c
1 )
and E12:
(
[c6,c7] in c
5 &
[c7,c8] in c
5 )
;
consider c
9 being
Subset of c
1 such that E13:
( c
6 = c
9 & c
9 is_line )
by E11;
consider c
10 being
Subset of c
1 such that E14:
( c
7 = c
10 & c
10 is_line )
by E11;
consider c
11 being
Subset of c
1 such that E15:
( c
8 = c
11 & c
11 is_line )
by E11;
( c
9 '||' c
10 & c
10 '||' c
11 )
by E8, E12, E13, E14, E15;
then
( c
9 // c
10 & c
10 // c
11 )
by E13, E14, E15, AFF_4:40;
then
c
9 // c
11
by AFF_1:58;
then
c
9 '||' c
11
by E13, E15, AFF_4:40;
hence
[c6,c8] in c
5
by E13, E15;
end;
then
c
5 is_transitive_in AfLines c
1
by RELAT_2:def 8;
hence
{ [b1,b2] where B is Subset of c1, B is Subset of c1 : ( b1 is_line & b2 is_line & b1 '||' b2 ) } is
Equivalence_Relation of
AfLines c
1
by E9, E10, PARTFUN1:def 4, RELAT_2:def 11, RELAT_2:def 16;
end;
end;
:: deftheorem Def3 defines LinesParallelity AFPROJ:def 3 :
definition
let c
1 be
AffinSpace;
func PlanesParallelity c
1 -> Equivalence_Relation of
AfPlanes a
1 equals :: AFPROJ:def 4
{ [b1,b2] where B is Subset of a1, B is Subset of a1 : ( b1 is_plane & b2 is_plane & b1 '||' b2 ) } ;
coherence
{ [b1,b2] where B is Subset of c1, B is Subset of c1 : ( b1 is_plane & b2 is_plane & b1 '||' b2 ) } is Equivalence_Relation of AfPlanes c1
proof
set c
2 =
{ [b1,b2] where B is Subset of c1, B is Subset of c1 : ( b1 is_plane & b2 is_plane & b1 '||' b2 ) } ;
set c
3 =
AfPlanes c
1;
set c
4 =
[:(AfPlanes c1),(AfPlanes c1):];
E8:
for b
1, b
2 being
Subset of c
1 holds
( b
1 is_plane & b
2 is_plane implies (
[b1,b2] in { [b3,b4] where B is Subset of c1, B is Subset of c1 : ( b3 is_plane & b4 is_plane & b3 '||' b4 ) } iff b
1 '||' b
2 ) )
then
{ [b1,b2] where B is Subset of c1, B is Subset of c1 : ( b1 is_plane & b2 is_plane & b1 '||' b2 ) } c= [:(AfPlanes c1),(AfPlanes c1):]
by TARSKI:def 3;
then reconsider c
5 =
{ [b1,b2] where B is Subset of c1, B is Subset of c1 : ( b1 is_plane & b2 is_plane & b1 '||' b2 ) } as
Relation of
AfPlanes c
1,
AfPlanes c
1 by RELSET_1:def 1;
then
c
5 is_reflexive_in AfPlanes c
1
by RELAT_2:def 1;
then E9:
(
dom c
5 = AfPlanes c
1 &
field c
5 = AfPlanes c
1 )
by ORDERS_1:98;
then E10:
c
5 is_symmetric_in AfPlanes c
1
by RELAT_2:def 3;
now
let c
6, c
7, c
8 be
set ;
assume that E11:
( c
6 in AfPlanes c
1 & c
7 in AfPlanes c
1 & c
8 in AfPlanes c
1 )
and E12:
(
[c6,c7] in c
5 &
[c7,c8] in c
5 )
;
consider c
9 being
Subset of c
1 such that E13:
( c
6 = c
9 & c
9 is_plane )
by E11;
consider c
10 being
Subset of c
1 such that E14:
( c
7 = c
10 & c
10 is_plane )
by E11;
consider c
11 being
Subset of c
1 such that E15:
( c
8 = c
11 & c
11 is_plane )
by E11;
( c
9 '||' c
10 & c
10 '||' c
11 )
by E8, E12, E13, E14, E15;
then
c
9 '||' c
11
by E13, E14, E15, AFF_4:61;
hence
[c6,c8] in c
5
by E13, E15;
end;
then
c
5 is_transitive_in AfPlanes c
1
by RELAT_2:def 8;
hence
{ [b1,b2] where B is Subset of c1, B is Subset of c1 : ( b1 is_plane & b2 is_plane & b1 '||' b2 ) } is
Equivalence_Relation of
AfPlanes c
1
by E9, E10, PARTFUN1:def 4, RELAT_2:def 11, RELAT_2:def 16;
end;
end;
:: deftheorem Def4 defines PlanesParallelity AFPROJ:def 4 :
:: deftheorem Def5 defines LDir AFPROJ:def 5 :
:: deftheorem Def6 defines PDir AFPROJ:def 6 :
theorem Th9: :: AFPROJ:9
proof
let c
1 be
AffinSpace;
let c
2 be
Subset of c
1;
assume E11:
c
2 is_line
;
let c
3 be
set ;
E12:
now
assume
c
3 in LDir c
2
;
then
c
3 in Class (LinesParallelity c1),c
2
by E11, Def5;
then
[c3,c2] in LinesParallelity c
1
by EQREL_1:27;
then
[c3,c2] in { [b1,b2] where B is Subset of c1, B is Subset of c1 : ( b1 is_line & b2 is_line & b1 '||' b2 ) }
;
then consider c
4, c
5 being
Subset of c
1 such that E13:
[c3,c2] = [c4,c5]
and E14:
( c
4 is_line & c
5 is_line & c
4 '||' c
5 )
;
E15:
( c
3 = c
4 & c
2 = c
5 )
by E13, ZFMISC_1:33;
take c
6 = c
4;
c
4 // c
5
by E14, AFF_4:40;
hence
( c
3 = c
6 & c
6 is_line & c
2 '||' c
6 )
by E14, E15, AFF_4:40;
end;
now
given c
4 being
Subset of c
1 such that E13:
( c
3 = c
4 & c
4 is_line & c
2 '||' c
4 )
;
c
2 // c
4
by E11, E13, AFF_4:40;
then
c
4 '||' c
2
by E11, E13, AFF_4:40;
then
[c4,c2] in { [b1,b2] where B is Subset of c1, B is Subset of c1 : ( b1 is_line & b2 is_line & b1 '||' b2 ) }
by E11, E13;
then
[c4,c2] in LinesParallelity c
1
;
then
c
4 in Class (LinesParallelity c1),c
2
by EQREL_1:27;
hence
c
3 in LDir c
2
by E11, E13, Def5;
end;
hence
( c
3 in LDir c
2 iff ex b
1 being
Subset of c
1 st
( c
3 = b
1 & b
1 is_line & c
2 '||' b
1 ) )
by E12;
end;
theorem Th10: :: AFPROJ:10
proof
let c
1 be
AffinSpace;
let c
2 be
Subset of c
1;
assume E12:
c
2 is_plane
;
let c
3 be
set ;
E13:
now
assume
c
3 in PDir c
2
;
then
c
3 in Class (PlanesParallelity c1),c
2
by E12, Def6;
then
[c3,c2] in PlanesParallelity c
1
by EQREL_1:27;
then
[c3,c2] in { [b1,b2] where B is Subset of c1, B is Subset of c1 : ( b1 is_plane & b2 is_plane & b1 '||' b2 ) }
;
then consider c
4, c
5 being
Subset of c
1 such that E14:
[c3,c2] = [c4,c5]
and E15:
( c
4 is_plane & c
5 is_plane & c
4 '||' c
5 )
;
E16:
( c
3 = c
4 & c
2 = c
5 )
by E14, ZFMISC_1:33;
take c
6 = c
4;
thus
( c
3 = c
6 & c
6 is_plane & c
2 '||' c
6 )
by E15, E16, AFF_4:58;
end;
now
given c
4 being
Subset of c
1 such that E14:
( c
3 = c
4 & c
4 is_plane & c
2 '||' c
4 )
;
c
4 '||' c
2
by E12, E14, AFF_4:58;
then
[c4,c2] in { [b1,b2] where B is Subset of c1, B is Subset of c1 : ( b1 is_plane & b2 is_plane & b1 '||' b2 ) }
by E12, E14;
then
[c4,c2] in PlanesParallelity c
1
;
then
c
4 in Class (PlanesParallelity c1),c
2
by EQREL_1:27;
hence
c
3 in PDir c
2
by E12, E14, Def6;
end;
hence
( c
3 in PDir c
2 iff ex b
1 being
Subset of c
1 st
( c
3 = b
1 & b
1 is_plane & c
2 '||' b
1 ) )
by E13;
end;
theorem Th11: :: AFPROJ:11
theorem Th12: :: AFPROJ:12
theorem Th13: :: AFPROJ:13
:: deftheorem Def7 defines Dir_of_Lines AFPROJ:def 7 :
:: deftheorem Def8 defines Dir_of_Planes AFPROJ:def 8 :
theorem Th14: :: AFPROJ:14
theorem Th15: :: AFPROJ:15