:: Planes in Affine Spaces
:: by Wojciech Leo\'nczuk, Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received December 5, 1990
:: Copyright (c) 1990 Association of Mizar Users
Lm1:
for AS being AffinSpace
for X being Subset of AS
for x being set st x in X holds
x is Element of AS
;
theorem Th1: :: AFF_4:1
for
AS being
AffinSpace for
p,
a,
a',
b being
Element of
AS st (
LIN p,
a,
a' or
LIN p,
a',
a ) &
p <> a holds
ex
b' being
Element of
AS st
(
LIN p,
b,
b' &
a,
b // a',
b' )
theorem Th2: :: AFF_4:2
theorem Th3: :: AFF_4:3
theorem Th4: :: AFF_4:4
for
AS being
AffinSpace for
a,
b,
c,
d being
Element of
AS for
A being
Subset of
AS st (
a,
b // A or
b,
a // A ) & (
a,
b // c,
d or
c,
d // a,
b ) &
a <> b holds
(
c,
d // A &
d,
c // A )
theorem :: AFF_4:5
theorem :: AFF_4:6
theorem Th7: :: AFF_4:7
Lm2:
for AS being AffinSpace
for a, a', d being Element of AS
for A, K being Subset of AS st A // K & a in A & a' in A & d in K holds
ex d' being Element of AS st
( d' in K & a,d // a',d' )
theorem Th8: :: AFF_4:8
theorem Th9: :: AFF_4:9
theorem Th10: :: AFF_4:10
for
AS being
AffinSpace for
a,
a',
b,
b' being
Element of
AS for
M,
N being
Subset of
AS st (
M // N or
N // M ) &
a in M &
a' in M &
b in N &
b' in N &
M <> N & (
a,
b // a',
b' or
b,
a // b',
a' ) &
a = a' holds
b = b'
theorem Th11: :: AFF_4:11
theorem Th12: :: AFF_4:12
:: deftheorem defines Plane AFF_4:def 1 :
:: deftheorem Def2 defines being_plane AFF_4:def 2 :
Lm3:
for AS being AffinSpace
for K, P being Subset of AS
for q being Element of AS holds
( q in Plane K,P iff ex b being Element of AS st
( q,b // K & b in P ) )
theorem :: AFF_4:13
theorem Th14: :: AFF_4:14
theorem :: AFF_4:15
theorem Th16: :: AFF_4:16
theorem :: AFF_4:17
theorem Th18: :: AFF_4:18
Lm4:
for AS being AffinSpace
for a being Element of AS
for K, P, Q being Subset of AS st K is being_line & P is being_line & a in Q & a in Plane K,P & K // Q holds
Q c= Plane K,P
Lm5:
for AS being AffinSpace
for a, b being Element of AS
for K, P, Q being Subset of AS st K is being_line & P is being_line & Q is being_line & a in Plane K,P & b in Plane K,P & a <> b & a in Q & b in Q holds
Q c= Plane K,P
theorem Th19: :: AFF_4:19
Lm6:
for AS being AffinSpace
for K, P, Q being Subset of AS st K is being_line & P is being_line & Q is being_line & Q c= Plane K,P holds
Plane K,Q c= Plane K,P
theorem Th20: :: AFF_4:20
theorem Th21: :: AFF_4:21
theorem Th22: :: AFF_4:22
theorem Th23: :: AFF_4:23
theorem Th24: :: AFF_4:24
theorem Th25: :: AFF_4:25
Lm7:
for AS being AffinSpace
for a, b, c being Element of AS
for M being Subset of AS st M is being_line & a in M & b in M & a <> b & not c in M holds
not LIN a,b,c
theorem Th26: :: AFF_4:26
:: deftheorem Def3 defines * AFF_4:def 3 :
theorem Th27: :: AFF_4:27
theorem Th28: :: AFF_4:28
theorem Th29: :: AFF_4:29
theorem :: AFF_4:30
theorem Th31: :: AFF_4:31
Lm8:
for AS being AffinSpace
for a being Element of AS
for A being Subset of AS st A is being_line & a in A holds
a * A = A
theorem Th32: :: AFF_4:32
:: deftheorem Def4 defines '||' AFF_4:def 4 :
theorem Th33: :: AFF_4:33
theorem Th34: :: AFF_4:34
Lm9:
for AS being AffinSpace
for a being Element of AS
for X being Subset of AS st X is being_plane holds
ex b, c being Element of AS st
( b in X & c in X & not LIN a,b,c )
theorem :: AFF_4:35
theorem Th36: :: AFF_4:36
theorem Th37: :: AFF_4:37
theorem Th38: :: AFF_4:38
theorem Th39: :: AFF_4:39
theorem :: AFF_4:40
theorem Th41: :: AFF_4:41
theorem :: AFF_4:42
theorem :: AFF_4:43
:: deftheorem Def5 defines is_coplanar AFF_4:def 5 :
theorem Th44: :: AFF_4:44
for
AS being
AffinSpace for
K,
M,
N being
Subset of
AS st
K,
M,
N is_coplanar holds
(
K,
N,
M is_coplanar &
M,
K,
N is_coplanar &
M,
N,
K is_coplanar &
N,
K,
M is_coplanar &
N,
M,
K is_coplanar )
theorem :: AFF_4:45
theorem Th46: :: AFF_4:46
theorem Th47: :: AFF_4:47
theorem Th48: :: AFF_4:48
Lm10:
for AS being AffinSpace
for q, a, b, c, a', b', c' being Element of AS
for A, P, C being Subset of AS st q in A & q in P & q in C & not A,P,C is_coplanar & q <> a & q <> b & q <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c'
theorem Th49: :: AFF_4:49
for
AS being
AffinSpace for
q,
a,
b,
c,
a',
b',
c' being
Element of
AS for
A,
P,
C being
Subset of
AS st
AS is not
AffinPlane &
q in A &
q in P &
q in C &
q <> a &
q <> b &
q <> c &
a in A &
a' in A &
b in P &
b' in P &
c in C &
c' in C &
A is
being_line &
P is
being_line &
C is
being_line &
A <> P &
A <> C &
a,
b // a',
b' &
a,
c // a',
c' holds
b,
c // b',
c'
theorem :: AFF_4:50
Lm11:
for AS being AffinSpace
for a, a', b, b', c, c' being Element of AS
for A, P, C being Subset of AS st A // P & A // C & not A,P,C is_coplanar & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c'
theorem Th51: :: AFF_4:51
for
AS being
AffinSpace for
a,
a',
b,
b',
c,
c' being
Element of
AS for
A,
P,
C being
Subset of
AS st
AS is not
AffinPlane &
A // P &
A // C &
a in A &
a' in A &
b in P &
b' in P &
c in C &
c' in C &
A is
being_line &
P is
being_line &
C is
being_line &
A <> P &
A <> C &
a,
b // a',
b' &
a,
c // a',
c' holds
b,
c // b',
c'
theorem :: AFF_4:52
theorem Th53: :: AFF_4:53
for
AS being
AffinSpace for
a,
b,
c,
a',
b' being
Element of
AS st
AS is
AffinPlane & not
LIN a,
b,
c holds
ex
c' being
Element of
AS st
(
a,
c // a',
c' &
b,
c // b',
c' )
Lm12:
for AS being AffinSpace
for a, b, c, a', b' being Element of AS
for X being Subset of AS st not LIN a,b,c & a' <> b' & a,b // a',b' & a in X & b in X & c in X & X is being_plane & a' in X holds
ex c' being Element of AS st
( a,c // a',c' & b,c // b',c' )
theorem Th54: :: AFF_4:54
for
AS being
AffinSpace for
a,
b,
c,
a',
b' being
Element of
AS st not
LIN a,
b,
c &
a' <> b' &
a,
b // a',
b' holds
ex
c' being
Element of
AS st
(
a,
c // a',
c' &
b,
c // b',
c' )
theorem Th55: :: AFF_4:55
theorem :: AFF_4:56
theorem Th57: :: AFF_4:57
theorem Th58: :: AFF_4:58
theorem Th59: :: AFF_4:59
theorem Th60: :: AFF_4:60
theorem Th61: :: AFF_4:61
Lm13:
for AS being AffinSpace
for X, Y being Subset of AS st X is being_plane & Y is being_plane & X '||' Y & X <> Y holds
for a being Element of AS holds
( not a in X or not a in Y )
theorem :: AFF_4:62
theorem Th63: :: AFF_4:63
theorem :: AFF_4:64
theorem Th65: :: AFF_4:65
:: deftheorem Def6 defines + AFF_4:def 6 :
theorem :: AFF_4:66
theorem :: AFF_4:67
theorem :: AFF_4:68
theorem :: AFF_4:69