:: AFPROJ semantic presentation
theorem E1: :: 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
is_line &
Line c
3,c
5 is
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
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
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
is_plane
by E3, E8, XBOOLE_0:def 10;
end;
theorem E2: :: AFPROJ:2
theorem E3: :: AFPROJ:3
theorem :: AFPROJ:4
theorem E4: :: 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
is_line & c
3 is
is_line & c
4 is
is_plane & c
5 is
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 E5: :: AFPROJ:6
:: deftheorem defines AfLines AFPROJ:def 1 :
:: deftheorem defines AfPlanes AFPROJ:def 2 :
theorem E6: :: AFPROJ:7
theorem E7: :: AFPROJ:8
definition
let c
1 be
AffinSpace;
func LinesParallelity a
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 is_line & b2 is is_line & b1 '||' b2 ) } ;
coherence
{ [b1,b2] where B is Subset of c1, B is Subset of c1 : ( b1 is is_line & b2 is 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 is_line & b2 is 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
is_line & b
2 is
is_line ) implies ( (
[b1,b2] in { [b3,b4] where B is Subset of c1, B is Subset of c1 : ( b3 is is_line & b4 is 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 is_line & b2 is 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 is_line & b2 is 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
is_line )
by E10;
consider c
9 being
Subset of c
1 such that
E13:
( c
7 = c
9 & c
9 is
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
is_line )
by E11;
consider c
10 being
Subset of c
1 such that
E14:
( c
7 = c
10 & c
10 is
is_line )
by E11;
consider c
11 being
Subset of c
1 such that
E15:
( c
8 = c
11 & c
11 is
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 is_line & b2 is 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 defines LinesParallelity AFPROJ:def 3 :
definition
let c
1 be
AffinSpace;
func PlanesParallelity a
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 is_plane & b2 is is_plane & b1 '||' b2 ) } ;
coherence
{ [b1,b2] where B is Subset of c1, B is Subset of c1 : ( b1 is is_plane & b2 is 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 is_plane & b2 is 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
is_plane & b
2 is
is_plane ) implies ( (
[b1,b2] in { [b3,b4] where B is Subset of c1, B is Subset of c1 : ( b3 is is_plane & b4 is 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 is_plane & b2 is 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 is_plane & b2 is 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
is_plane )
by E11;
consider c
10 being
Subset of c
1 such that
E14:
( c
7 = c
10 & c
10 is
is_plane )
by E11;
consider c
11 being
Subset of c
1 such that
E15:
( c
8 = c
11 & c
11 is
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 is_plane & b2 is 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 defines PlanesParallelity AFPROJ:def 4 :
:: deftheorem E8 defines LDir AFPROJ:def 5 :
:: deftheorem E9 defines PDir AFPROJ:def 6 :
theorem E10: :: AFPROJ:9
proof
let c
1 be
AffinSpace;
let c
2 be
Subset of c
1;
assume E11:
c
2 is
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, E8;
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 is_line & b2 is 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
is_line & c
5 is
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
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
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 is_line & b2 is 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, E8;
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
is_line & c
2 '||' b
1 ) )
by E12;
end;
theorem E11: :: AFPROJ:10
proof
let c
1 be
AffinSpace;
let c
2 be
Subset of c
1;
assume E12:
c
2 is
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, E9;
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 is_plane & b2 is 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
is_plane & c
5 is
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
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
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 is_plane & b2 is 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, E9;
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
is_plane & c
2 '||' b
1 ) )
by E13;
end;
theorem E12: :: AFPROJ:11
theorem E13: :: AFPROJ:12
theorem E14: :: AFPROJ:13
:: deftheorem defines Dir_of_Lines AFPROJ:def 7 :
:: deftheorem defines Dir_of_Planes AFPROJ:def 8 :
theorem E15: :: AFPROJ:14
theorem E16: :: AFPROJ:15
theorem E17: :: AFPROJ:16
theorem :: AFPROJ:17
proof
let c
1 be
AffinSpace;
assume E18:
c
1 is
AffinPlane
;
assume
not
AfLines c
1 misses Dir_of_Planes c
1
;
then consider c
2 being
set such that
E19:
( c
2 in AfLines c
1 & c
2 in Dir_of_Planes c
1 )
by XBOOLE_0:3;
the
carrier of c
1 c= the
carrier of c
1
;
then reconsider c
3 = the
carrier of c
1 as
Subset of c
1 ;
E20:
c
3 is
is_plane
by E18, E1;
consider c
4 being
Subset of c
1 such that
E21:
c
2 = PDir c
4
and
E22:
c
4 is
is_plane
by E19, E16;
consider c
5 being
Subset of c
1 such that
E23:
c
2 = c
5
and
E24:
c
5 is
is_line
by E19;
consider c
6, c
7 being
Element of c
1 such that
E25:
c
6 in c
5
and
( c
7 in c
5 & c
6 <> c
7 )
by E24, AFF_1:31;
consider c
8 being
Subset of c
1 such that
E26:
c
6 = c
8
and
E27:
c
8 is
is_plane
and
c
4 '||' c
8
by E21, E22, E23, E25, E11;
E28:
c
8 = c
3
by E20, E27, AFF_4:33;
not c
8 in c
8
;
hence
not verum
by E26, E28;
end;
theorem E18: :: AFPROJ:18
theorem E19: :: AFPROJ:19