:: by Wojciech Leo\'nczuk and Krzysztof Pra\.zmowski

::

:: Received June 15, 1990

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

definition

let V be RealLinearSpace;

let p, q be Element of V;

for p being Element of V ex a, b being Real st

( a * p = b * p & a <> 0 & b <> 0 )

for p, q being Element of V st ex a, b being Real st

( a * p = b * q & a <> 0 & b <> 0 ) holds

ex a, b being Real st

( a * q = b * p & a <> 0 & b <> 0 ) ;

end;
let p, q be Element of V;

pred are_Prop p,q means :Def1: :: ANPROJ_1:def 1

ex a, b being Real st

( a * p = b * q & a <> 0 & b <> 0 );

reflexivity ex a, b being Real st

( a * p = b * q & a <> 0 & b <> 0 );

for p being Element of V ex a, b being Real st

( a * p = b * p & a <> 0 & b <> 0 )

proof end;

symmetry for p, q being Element of V st ex a, b being Real st

( a * p = b * q & a <> 0 & b <> 0 ) holds

ex a, b being Real st

( a * q = b * p & a <> 0 & b <> 0 ) ;

:: deftheorem Def1 defines are_Prop ANPROJ_1:def 1 :

for V being RealLinearSpace

for p, q being Element of V holds

( are_Prop p,q iff ex a, b being Real st

( a * p = b * q & a <> 0 & b <> 0 ) );

for V being RealLinearSpace

for p, q being Element of V holds

( are_Prop p,q iff ex a, b being Real st

( a * p = b * q & a <> 0 & b <> 0 ) );

theorem Th1: :: ANPROJ_1:1

for V being RealLinearSpace

for p, q being Element of V holds

( are_Prop p,q iff ex a being Real st

( a <> 0 & p = a * q ) )

for p, q being Element of V holds

( are_Prop p,q iff ex a being Real st

( a <> 0 & p = a * q ) )

proof end;

theorem Th2: :: ANPROJ_1:2

for V being RealLinearSpace

for p, u, q being Element of V st are_Prop p,u & are_Prop u,q holds

are_Prop p,q

for p, u, q being Element of V st are_Prop p,u & are_Prop u,q holds

are_Prop p,q

proof end;

:: deftheorem Def2 defines are_LinDep ANPROJ_1:def 2 :

for V being RealLinearSpace

for u, v, w being Element of V holds

( u,v,w are_LinDep iff ex a, b, c being Real st

( ((a * u) + (b * v)) + (c * w) = 0. V & ( a <> 0 or b <> 0 or c <> 0 ) ) );

for V being RealLinearSpace

for u, v, w being Element of V holds

( u,v,w are_LinDep iff ex a, b, c being Real st

( ((a * u) + (b * v)) + (c * w) = 0. V & ( a <> 0 or b <> 0 or c <> 0 ) ) );

theorem Th4: :: ANPROJ_1:4

for V being RealLinearSpace

for u, u1, v, v1, w, w1 being Element of V st are_Prop u,u1 & are_Prop v,v1 & are_Prop w,w1 & u,v,w are_LinDep holds

u1,v1,w1 are_LinDep

for u, u1, v, v1, w, w1 being Element of V st are_Prop u,u1 & are_Prop v,v1 & are_Prop w,w1 & u,v,w are_LinDep holds

u1,v1,w1 are_LinDep

proof end;

theorem Th5: :: ANPROJ_1:5

for V being RealLinearSpace

for u, v, w being Element of V st u,v,w are_LinDep holds

( u,w,v are_LinDep & v,u,w are_LinDep & w,v,u are_LinDep & w,u,v are_LinDep & v,w,u are_LinDep )

for u, v, w being Element of V st u,v,w are_LinDep holds

( u,w,v are_LinDep & v,u,w are_LinDep & w,v,u are_LinDep & w,u,v are_LinDep & v,w,u are_LinDep )

proof end;

Lm1: for V being RealLinearSpace

for v, w being Element of V

for a, b being Real st (a * v) + (b * w) = 0. V holds

a * v = (- b) * w

proof end;

Lm2: for V being RealLinearSpace

for u, v, w being Element of V

for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V & a <> 0 holds

u = ((- ((a ") * b)) * v) + ((- ((a ") * c)) * w)

proof end;

theorem Th6: :: ANPROJ_1:6

for V being RealLinearSpace

for v, w, u being Element of V st not v is zero & not w is zero & not are_Prop v,w holds

( v,w,u are_LinDep iff ex a, b being Real st u = (a * v) + (b * w) )

for v, w, u being Element of V st not v is zero & not w is zero & not are_Prop v,w holds

( v,w,u are_LinDep iff ex a, b being Real st u = (a * v) + (b * w) )

proof end;

Lm3: for V being RealLinearSpace

for p being Element of V

for a, b, c being Real holds ((a + b) + c) * p = ((a * p) + (b * p)) + (c * p)

proof end;

Lm4: for V being RealLinearSpace

for u, v, w, u1, v1, w1 being Element of V holds ((u + v) + w) + ((u1 + v1) + w1) = ((u + u1) + (v + v1)) + (w + w1)

proof end;

Lm5: for V being RealLinearSpace

for p, q being Element of V

for a, a1, b1 being Real holds ((a * a1) * p) + ((a * b1) * q) = a * ((a1 * p) + (b1 * q))

proof end;

theorem :: ANPROJ_1:7

for V being RealLinearSpace

for p, q being Element of V

for a1, b1, a2, b2 being Real st not are_Prop p,q & (a1 * p) + (b1 * q) = (a2 * p) + (b2 * q) & not p is zero & not q is zero holds

( a1 = a2 & b1 = b2 )

for p, q being Element of V

for a1, b1, a2, b2 being Real st not are_Prop p,q & (a1 * p) + (b1 * q) = (a2 * p) + (b2 * q) & not p is zero & not q is zero holds

( a1 = a2 & b1 = b2 )

proof end;

Lm6: for V being RealLinearSpace

for p, v, q being Element of V

for a, b being Real st p + (a * v) = q + (b * v) holds

((a - b) * v) + p = q

proof end;

theorem :: ANPROJ_1:8

for V being RealLinearSpace

for u, v, w being Element of V

for a1, b1, c1, a2, b2, c2 being Real st not u,v,w are_LinDep & ((a1 * u) + (b1 * v)) + (c1 * w) = ((a2 * u) + (b2 * v)) + (c2 * w) holds

( a1 = a2 & b1 = b2 & c1 = c2 )

for u, v, w being Element of V

for a1, b1, c1, a2, b2, c2 being Real st not u,v,w are_LinDep & ((a1 * u) + (b1 * v)) + (c1 * w) = ((a2 * u) + (b2 * v)) + (c2 * w) holds

( a1 = a2 & b1 = b2 & c1 = c2 )

proof end;

theorem Th9: :: ANPROJ_1:9

for V being RealLinearSpace

for p, q, u, v being Element of V

for a1, b1, a2, b2 being Real st not are_Prop p,q & u = (a1 * p) + (b1 * q) & v = (a2 * p) + (b2 * q) & (a1 * b2) - (a2 * b1) = 0 & not p is zero & not q is zero & not are_Prop u,v & not u = 0. V holds

v = 0. V

for p, q, u, v being Element of V

for a1, b1, a2, b2 being Real st not are_Prop p,q & u = (a1 * p) + (b1 * q) & v = (a2 * p) + (b2 * q) & (a1 * b2) - (a2 * b1) = 0 & not p is zero & not q is zero & not are_Prop u,v & not u = 0. V holds

v = 0. V

proof end;

theorem Th10: :: ANPROJ_1:10

for V being RealLinearSpace

for u, v, w being Element of V st ( u = 0. V or v = 0. V or w = 0. V ) holds

u,v,w are_LinDep

for u, v, w being Element of V st ( u = 0. V or v = 0. V or w = 0. V ) holds

u,v,w are_LinDep

proof end;

theorem Th11: :: ANPROJ_1:11

for V being RealLinearSpace

for u, v, w being Element of V st ( are_Prop u,v or are_Prop w,u or are_Prop v,w ) holds

w,u,v are_LinDep

for u, v, w being Element of V st ( are_Prop u,v or are_Prop w,u or are_Prop v,w ) holds

w,u,v are_LinDep

proof end;

theorem Th12: :: ANPROJ_1:12

for V being RealLinearSpace

for u, v, w being Element of V st not u,v,w are_LinDep holds

( not u is zero & not v is zero & not w is zero & not are_Prop u,v & not are_Prop v,w & not are_Prop w,u )

for u, v, w being Element of V st not u,v,w are_LinDep holds

( not u is zero & not v is zero & not w is zero & not are_Prop u,v & not are_Prop v,w & not are_Prop w,u )

proof end;

theorem Th14: :: ANPROJ_1:14

for V being RealLinearSpace

for p, q, u, v, w being Element of V st not are_Prop p,q & p,q,u are_LinDep & p,q,v are_LinDep & p,q,w are_LinDep & not p is zero & not q is zero holds

u,v,w are_LinDep

for p, q, u, v, w being Element of V st not are_Prop p,q & p,q,u are_LinDep & p,q,v are_LinDep & p,q,w are_LinDep & not p is zero & not q is zero holds

u,v,w are_LinDep

proof end;

Lm7: for V being RealLinearSpace

for v, w being Element of V

for a, b, c being Real holds a * ((b * v) + (c * w)) = ((a * b) * v) + ((a * c) * w)

proof end;

theorem :: ANPROJ_1:15

for V being RealLinearSpace

for u, v, w, p, q being Element of V st not u,v,w are_LinDep & u,v,p are_LinDep & v,w,q are_LinDep holds

ex y being Element of V st

( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero )

for u, v, w, p, q being Element of V st not u,v,w are_LinDep & u,v,p are_LinDep & v,w,q are_LinDep holds

ex y being Element of V st

( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero )

proof end;

theorem :: ANPROJ_1:16

for V being RealLinearSpace

for p, q being Element of V st not are_Prop p,q & not p is zero & not q is zero holds

for u, v being Element of V ex y being Element of V st

( not y is zero & u,v,y are_LinDep & not are_Prop u,y & not are_Prop v,y )

for p, q being Element of V st not are_Prop p,q & not p is zero & not q is zero holds

for u, v being Element of V ex y being Element of V st

( not y is zero & u,v,y are_LinDep & not are_Prop u,y & not are_Prop v,y )

proof end;

Lm8: for V being RealLinearSpace

for p, q, r being Element of V st not p,q,r are_LinDep holds

for u, v being Element of V st not u is zero & not v is zero & not are_Prop u,v holds

ex y being Element of V st not u,v,y are_LinDep

proof end;

theorem :: ANPROJ_1:17

for V being RealLinearSpace

for p, q, r being Element of V st not p,q,r are_LinDep holds

for u, v being Element of V st not u is zero & not v is zero & not are_Prop u,v holds

ex y being Element of V st

( not y is zero & not u,v,y are_LinDep )

for p, q, r being Element of V st not p,q,r are_LinDep holds

for u, v being Element of V st not u is zero & not v is zero & not are_Prop u,v holds

ex y being Element of V st

( not y is zero & not u,v,y are_LinDep )

proof end;

Lm9: for V being RealLinearSpace

for u, w, y being Element of V

for a, b, c, d, e, f, A, B, C being Real holds ((A * ((a * u) + (b * w))) + (B * ((c * w) + (d * y)))) + (C * ((e * u) + (f * y))) = ((((A * a) + (C * e)) * u) + (((A * b) + (B * c)) * w)) + (((B * d) + (C * f)) * y)

proof end;

theorem :: ANPROJ_1:18

for V being RealLinearSpace

for u, v, q, w, y, p, r being Element of V st u,v,q are_LinDep & w,y,q are_LinDep & u,w,p are_LinDep & v,y,p are_LinDep & u,y,r are_LinDep & v,w,r are_LinDep & p,q,r are_LinDep & not p is zero & not q is zero & not r is zero & not u,v,y are_LinDep & not u,v,w are_LinDep & not u,w,y are_LinDep holds

v,w,y are_LinDep

for u, v, q, w, y, p, r being Element of V st u,v,q are_LinDep & w,y,q are_LinDep & u,w,p are_LinDep & v,y,p are_LinDep & u,y,r are_LinDep & v,w,r are_LinDep & p,q,r are_LinDep & not p is zero & not q is zero & not r is zero & not u,v,y are_LinDep & not u,v,w are_LinDep & not u,w,y are_LinDep holds

v,w,y are_LinDep

proof end;

definition

let V be RealLinearSpace;

ex b_{1} being Equivalence_Relation of (NonZero V) st

for x, y being set holds

( [x,y] in b_{1} iff ( x in NonZero V & y in NonZero V & ex u, v being Element of V st

( x = u & y = v & are_Prop u,v ) ) )

for b_{1}, b_{2} being Equivalence_Relation of (NonZero V) st ( for x, y being set holds

( [x,y] in b_{1} iff ( x in NonZero V & y in NonZero V & ex u, v being Element of V st

( x = u & y = v & are_Prop u,v ) ) ) ) & ( for x, y being set holds

( [x,y] in b_{2} iff ( x in NonZero V & y in NonZero V & ex u, v being Element of V st

( x = u & y = v & are_Prop u,v ) ) ) ) holds

b_{1} = b_{2}

end;
func Proportionality_as_EqRel_of V -> Equivalence_Relation of (NonZero V) means :Def3: :: ANPROJ_1:def 3

for x, y being set holds

( [x,y] in it iff ( x in NonZero V & y in NonZero V & ex u, v being Element of V st

( x = u & y = v & are_Prop u,v ) ) );

existence for x, y being set holds

( [x,y] in it iff ( x in NonZero V & y in NonZero V & ex u, v being Element of V st

( x = u & y = v & are_Prop u,v ) ) );

ex b

for x, y being set holds

( [x,y] in b

( x = u & y = v & are_Prop u,v ) ) )

proof end;

uniqueness for b

( [x,y] in b

( x = u & y = v & are_Prop u,v ) ) ) ) & ( for x, y being set holds

( [x,y] in b

( x = u & y = v & are_Prop u,v ) ) ) ) holds

b

proof end;

:: deftheorem Def3 defines Proportionality_as_EqRel_of ANPROJ_1:def 3 :

for V being RealLinearSpace

for b_{2} being Equivalence_Relation of (NonZero V) holds

( b_{2} = Proportionality_as_EqRel_of V iff for x, y being set holds

( [x,y] in b_{2} iff ( x in NonZero V & y in NonZero V & ex u, v being Element of V st

( x = u & y = v & are_Prop u,v ) ) ) );

for V being RealLinearSpace

for b

( b

( [x,y] in b

( x = u & y = v & are_Prop u,v ) ) ) );

theorem :: ANPROJ_1:19

for V being RealLinearSpace

for x, y being set st [x,y] in Proportionality_as_EqRel_of V holds

( x is Element of V & y is Element of V )

for x, y being set st [x,y] in Proportionality_as_EqRel_of V holds

( x is Element of V & y is Element of V )

proof end;

theorem Th20: :: ANPROJ_1:20

for V being RealLinearSpace

for u, v being Element of V holds

( [u,v] in Proportionality_as_EqRel_of V iff ( not u is zero & not v is zero & are_Prop u,v ) )

for u, v being Element of V holds

( [u,v] in Proportionality_as_EqRel_of V iff ( not u is zero & not v is zero & are_Prop u,v ) )

proof end;

definition

let V be RealLinearSpace;

let v be Element of V;

coherence

Class ((Proportionality_as_EqRel_of V),v) is Subset of (NonZero V);

;

end;
let v be Element of V;

func Dir v -> Subset of (NonZero V) equals :: ANPROJ_1:def 4

Class ((Proportionality_as_EqRel_of V),v);

correctness Class ((Proportionality_as_EqRel_of V),v);

coherence

Class ((Proportionality_as_EqRel_of V),v) is Subset of (NonZero V);

;

:: deftheorem defines Dir ANPROJ_1:def 4 :

for V being RealLinearSpace

for v being Element of V holds Dir v = Class ((Proportionality_as_EqRel_of V),v);

for V being RealLinearSpace

for v being Element of V holds Dir v = Class ((Proportionality_as_EqRel_of V),v);

definition

let V be RealLinearSpace;

existence

ex b_{1} being set ex Y being Subset-Family of (NonZero V) st

( Y = Class (Proportionality_as_EqRel_of V) & b_{1} = Y );

uniqueness

for b_{1}, b_{2} being set st ex Y being Subset-Family of (NonZero V) st

( Y = Class (Proportionality_as_EqRel_of V) & b_{1} = Y ) & ex Y being Subset-Family of (NonZero V) st

( Y = Class (Proportionality_as_EqRel_of V) & b_{2} = Y ) holds

b_{1} = b_{2};

;

end;
func ProjectivePoints V -> set means :Def5: :: ANPROJ_1:def 5

ex Y being Subset-Family of (NonZero V) st

( Y = Class (Proportionality_as_EqRel_of V) & it = Y );

correctness ex Y being Subset-Family of (NonZero V) st

( Y = Class (Proportionality_as_EqRel_of V) & it = Y );

existence

ex b

( Y = Class (Proportionality_as_EqRel_of V) & b

uniqueness

for b

( Y = Class (Proportionality_as_EqRel_of V) & b

( Y = Class (Proportionality_as_EqRel_of V) & b

b

;

:: deftheorem Def5 defines ProjectivePoints ANPROJ_1:def 5 :

for V being RealLinearSpace

for b_{2} being set holds

( b_{2} = ProjectivePoints V iff ex Y being Subset-Family of (NonZero V) st

( Y = Class (Proportionality_as_EqRel_of V) & b_{2} = Y ) );

for V being RealLinearSpace

for b

( b

( Y = Class (Proportionality_as_EqRel_of V) & b

registration

ex b_{1} being RealLinearSpace st

( b_{1} is strict & not b_{1} is trivial )
end;

cluster non empty non trivial V79() V80() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() for RLSStruct ;

existence ex b

( b

proof end;

registration
end;

theorem Th21: :: ANPROJ_1:21

for V being non trivial RealLinearSpace

for p being Element of V st not p is zero holds

Dir p is Element of ProjectivePoints V

for p being Element of V st not p is zero holds

Dir p is Element of ProjectivePoints V

proof end;

theorem Th22: :: ANPROJ_1:22

for V being non trivial RealLinearSpace

for p, q being Element of V st not p is zero & not q is zero holds

( Dir p = Dir q iff are_Prop p,q )

for p, q being Element of V st not p is zero & not q is zero holds

( Dir p = Dir q iff are_Prop p,q )

proof end;

definition

let V be non trivial RealLinearSpace;

ex b_{1} being Relation3 of ProjectivePoints V st

for x, y, z being set holds

( [x,y,z] in b_{1} iff ex p, q, r being Element of V st

( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) )

for b_{1}, b_{2} being Relation3 of ProjectivePoints V st ( for x, y, z being set holds

( [x,y,z] in b_{1} iff ex p, q, r being Element of V st

( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) ) ) & ( for x, y, z being set holds

( [x,y,z] in b_{2} iff ex p, q, r being Element of V st

( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) ) ) holds

b_{1} = b_{2}

end;
func ProjectiveCollinearity V -> Relation3 of ProjectivePoints V means :Def6: :: ANPROJ_1:def 6

for x, y, z being set holds

( [x,y,z] in it iff ex p, q, r being Element of V st

( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) );

existence for x, y, z being set holds

( [x,y,z] in it iff ex p, q, r being Element of V st

( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) );

ex b

for x, y, z being set holds

( [x,y,z] in b

( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) )

proof end;

uniqueness for b

( [x,y,z] in b

( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) ) ) & ( for x, y, z being set holds

( [x,y,z] in b

( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) ) ) holds

b

proof end;

:: deftheorem Def6 defines ProjectiveCollinearity ANPROJ_1:def 6 :

for V being non trivial RealLinearSpace

for b_{2} being Relation3 of ProjectivePoints V holds

( b_{2} = ProjectiveCollinearity V iff for x, y, z being set holds

( [x,y,z] in b_{2} iff ex p, q, r being Element of V st

( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) ) );

for V being non trivial RealLinearSpace

for b

( b

( [x,y,z] in b

( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) ) );

definition

let V be non trivial RealLinearSpace;

coherence

CollStr(# (ProjectivePoints V),(ProjectiveCollinearity V) #) is strict CollStr ;

;

end;
func ProjectiveSpace V -> strict CollStr equals :: ANPROJ_1:def 7

CollStr(# (ProjectivePoints V),(ProjectiveCollinearity V) #);

correctness CollStr(# (ProjectivePoints V),(ProjectiveCollinearity V) #);

coherence

CollStr(# (ProjectivePoints V),(ProjectiveCollinearity V) #) is strict CollStr ;

;

:: deftheorem defines ProjectiveSpace ANPROJ_1:def 7 :

for V being non trivial RealLinearSpace holds ProjectiveSpace V = CollStr(# (ProjectivePoints V),(ProjectiveCollinearity V) #);

for V being non trivial RealLinearSpace holds ProjectiveSpace V = CollStr(# (ProjectivePoints V),(ProjectiveCollinearity V) #);

theorem :: ANPROJ_1:23

for V being non trivial RealLinearSpace holds

( the carrier of (ProjectiveSpace V) = ProjectivePoints V & the Collinearity of (ProjectiveSpace V) = ProjectiveCollinearity V ) ;

( the carrier of (ProjectiveSpace V) = ProjectivePoints V & the Collinearity of (ProjectiveSpace V) = ProjectiveCollinearity V ) ;

theorem :: ANPROJ_1:24

for x, y, z being set

for V being non trivial RealLinearSpace st [x,y,z] in the Collinearity of (ProjectiveSpace V) holds

ex p, q, r being Element of V st

( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) by Def6;

for V being non trivial RealLinearSpace st [x,y,z] in the Collinearity of (ProjectiveSpace V) holds

ex p, q, r being Element of V st

( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) by Def6;

theorem :: ANPROJ_1:25

for V being non trivial RealLinearSpace

for u, v, w being Element of V st not u is zero & not v is zero & not w is zero holds

( [(Dir u),(Dir v),(Dir w)] in the Collinearity of (ProjectiveSpace V) iff u,v,w are_LinDep )

for u, v, w being Element of V st not u is zero & not v is zero & not w is zero holds

( [(Dir u),(Dir v),(Dir w)] in the Collinearity of (ProjectiveSpace V) iff u,v,w are_LinDep )

proof end;

theorem :: ANPROJ_1:26

for x being set

for V being non trivial RealLinearSpace holds

( x is Element of (ProjectiveSpace V) iff ex u being Element of V st

( not u is zero & x = Dir u ) )

for V being non trivial RealLinearSpace holds

( x is Element of (ProjectiveSpace V) iff ex u being Element of V st

( not u is zero & x = Dir u ) )

proof end;