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

::

:: Received June 15, 1990

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

theorem Th1: :: ANPROJ_2:1

for V being RealLinearSpace

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

( a = 0 & b = 0 & c = 0 ) ) holds

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

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

( a = 0 & b = 0 & c = 0 ) ) holds

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

proof end;

Lm1: for V being RealLinearSpace

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

( a = 0 & b = 0 ) ) holds

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

proof end;

theorem Th2: :: ANPROJ_2:2

for V being RealLinearSpace

for u, v, u1, v1 being Element of V st ( for a, b, a1, b1 being Real st (((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1) = 0. V holds

( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) ) holds

( not u is zero & not v is zero & not are_Prop u,v & not u1 is zero & not v1 is zero & not are_Prop u1,v1 & not u,v,u1 are_LinDep & not u1,v1,u are_LinDep )

for u, v, u1, v1 being Element of V st ( for a, b, a1, b1 being Real st (((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1) = 0. V holds

( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) ) holds

( not u is zero & not v is zero & not are_Prop u,v & not u1 is zero & not v1 is zero & not are_Prop u1,v1 & not u,v,u1 are_LinDep & not u1,v1,u are_LinDep )

proof end;

Lm2: for V being RealLinearSpace

for u, v, w being Element of V

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

proof end;

Lm3: 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;

theorem Th3: :: ANPROJ_2:3

for V being RealLinearSpace

for p, q, r being Element of V st ( for w being Element of V ex a, b, c being Real st w = ((a * p) + (b * q)) + (c * r) ) & ( for a, b, c being Real st ((a * p) + (b * q)) + (c * r) = 0. V holds

( a = 0 & b = 0 & c = 0 ) ) holds

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

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

for p, q, r being Element of V st ( for w being Element of V ex a, b, c being Real st w = ((a * p) + (b * q)) + (c * r) ) & ( for a, b, c being Real st ((a * p) + (b * q)) + (c * r) = 0. V holds

( a = 0 & b = 0 & c = 0 ) ) holds

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

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

proof end;

Lm4: for V being RealLinearSpace

for u, v, w, y being Element of V

for a, b, c, d, d1 being Real holds a * ((((b * v) + (c * w)) + (d * u)) + (d1 * y)) = ((((a * b) * v) + ((a * c) * w)) + ((a * d) * u)) + ((a * d1) * y)

proof end;

Lm5: for V being RealLinearSpace

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

proof end;

Lm6: for V being RealLinearSpace

for u, v, w being Element of V

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

proof end;

Lm7: for V being RealLinearSpace

for p, q, r, w, y being Element of V

for a, b, c, a1, b1 being Real st y = (a1 * p) + (b1 * w) & w = ((a * p) + (b * q)) + (c * r) holds

y = (((a1 + (b1 * a)) * p) + ((b1 * b) * q)) + ((b1 * c) * r)

proof end;

theorem Th4: :: ANPROJ_2:4

for V being RealLinearSpace

for p, q, r, s being Element of V st ( for w being Element of V ex a, b, c, d being Real st w = (((a * p) + (b * q)) + (c * r)) + (d * s) ) & ( for a, b, c, d being Real st (((a * p) + (b * q)) + (c * r)) + (d * s) = 0. V holds

( a = 0 & b = 0 & c = 0 & d = 0 ) ) holds

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

ex y, w being Element of V st

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

for p, q, r, s being Element of V st ( for w being Element of V ex a, b, c, d being Real st w = (((a * p) + (b * q)) + (c * r)) + (d * s) ) & ( for a, b, c, d being Real st (((a * p) + (b * q)) + (c * r)) + (d * s) = 0. V holds

( a = 0 & b = 0 & c = 0 & d = 0 ) ) holds

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

ex y, w being Element of V st

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

proof end;

theorem Th5: :: ANPROJ_2:5

for V being RealLinearSpace

for u, v, u1, v1 being Element of V st ( for a, b, a1, b1 being Real st (((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1) = 0. V holds

( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) ) holds

for y being Element of V holds

( y is zero or not u,v,y are_LinDep or not u1,v1,y are_LinDep )

for u, v, u1, v1 being Element of V st ( for a, b, a1, b1 being Real st (((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1) = 0. V holds

( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) ) holds

for y being Element of V holds

( y is zero or not u,v,y are_LinDep or not u1,v1,y are_LinDep )

proof end;

:: deftheorem defines are_Prop_Vect ANPROJ_2:def 1 :

for V being RealLinearSpace

for u, v, w being Element of V holds

( u,v,w are_Prop_Vect iff ( not u is zero & not v is zero & not w is zero ) );

for V being RealLinearSpace

for u, v, w being Element of V holds

( u,v,w are_Prop_Vect iff ( not u is zero & not v is zero & not w is zero ) );

definition

let V be RealLinearSpace;

let u, v, w, u1, v1, w1 be Element of V;

end;
let u, v, w, u1, v1, w1 be Element of V;

pred u,v,w,u1,v1,w1 lie_on_a_triangle means :: ANPROJ_2:def 2

( u,v,w1 are_LinDep & u,w,v1 are_LinDep & v,w,u1 are_LinDep );

( u,v,w1 are_LinDep & u,w,v1 are_LinDep & v,w,u1 are_LinDep );

:: deftheorem defines lie_on_a_triangle ANPROJ_2:def 2 :

for V being RealLinearSpace

for u, v, w, u1, v1, w1 being Element of V holds

( u,v,w,u1,v1,w1 lie_on_a_triangle iff ( u,v,w1 are_LinDep & u,w,v1 are_LinDep & v,w,u1 are_LinDep ) );

for V being RealLinearSpace

for u, v, w, u1, v1, w1 being Element of V holds

( u,v,w,u1,v1,w1 lie_on_a_triangle iff ( u,v,w1 are_LinDep & u,w,v1 are_LinDep & v,w,u1 are_LinDep ) );

definition

let V be RealLinearSpace;

let o, u, v, w, u2, v2, w2 be Element of V;

end;
let o, u, v, w, u2, v2, w2 be Element of V;

pred o,u,v,w,u2,v2,w2 are_perspective means :: ANPROJ_2:def 3

( o,u,u2 are_LinDep & o,v,v2 are_LinDep & o,w,w2 are_LinDep );

( o,u,u2 are_LinDep & o,v,v2 are_LinDep & o,w,w2 are_LinDep );

:: deftheorem defines are_perspective ANPROJ_2:def 3 :

for V being RealLinearSpace

for o, u, v, w, u2, v2, w2 being Element of V holds

( o,u,v,w,u2,v2,w2 are_perspective iff ( o,u,u2 are_LinDep & o,v,v2 are_LinDep & o,w,w2 are_LinDep ) );

for V being RealLinearSpace

for o, u, v, w, u2, v2, w2 being Element of V holds

( o,u,v,w,u2,v2,w2 are_perspective iff ( o,u,u2 are_LinDep & o,v,v2 are_LinDep & o,w,w2 are_LinDep ) );

Lm8: for V being RealLinearSpace

for o being Element of V

for a being Real holds - (a * o) = (- a) * o

proof end;

theorem Th6: :: ANPROJ_2:6

for V being RealLinearSpace

for o, u, u2 being Element of V st o,u,u2 are_LinDep & not are_Prop o,u & not are_Prop o,u2 & not are_Prop u,u2 & o,u,u2 are_Prop_Vect holds

( ex a1, b1 being Real st

( b1 * u2 = o + (a1 * u) & a1 <> 0 & b1 <> 0 ) & ex a2, c2 being Real st

( u2 = (c2 * o) + (a2 * u) & c2 <> 0 & a2 <> 0 ) )

for o, u, u2 being Element of V st o,u,u2 are_LinDep & not are_Prop o,u & not are_Prop o,u2 & not are_Prop u,u2 & o,u,u2 are_Prop_Vect holds

( ex a1, b1 being Real st

( b1 * u2 = o + (a1 * u) & a1 <> 0 & b1 <> 0 ) & ex a2, c2 being Real st

( u2 = (c2 * o) + (a2 * u) & c2 <> 0 & a2 <> 0 ) )

proof end;

theorem Th7: :: ANPROJ_2:7

for V being RealLinearSpace

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

ex a, b being Real st r = (a * p) + (b * q)

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

ex a, b being Real st r = (a * p) + (b * q)

proof end;

Lm9: for V being RealLinearSpace

for u2, w2 being Element of V

for b1 being Real st b1 * u2 = w2 & b1 <> 0 holds

are_Prop u2,w2

proof end;

Lm10: for V being RealLinearSpace

for o, p, q, r, s being Element of V

for a, b being Real st q = o + (a * p) & r = o + (b * s) & are_Prop q,r & a <> 0 holds

o,p,s are_LinDep

proof end;

Lm11: for V being RealLinearSpace

for p, q being Element of V

for a being Real st a * p = q & a <> 0 & not p is zero holds

not q is zero

by RLVECT_1:11;

Lm12: for V being RealLinearSpace

for o, r, u, v, u2, v2 being Element of V

for a1, a2, A, B being Real st r = (A * u2) + (B * v2) & u2 = o + (a1 * u) & v2 = o + (a2 * v) holds

r = (((A + B) * o) + ((A * a1) * u)) + ((B * a2) * v)

proof end;

Lm13: for V being RealLinearSpace

for o, p, q, r being Element of V

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

r = ((0 * o) + (a * p)) + (b * q)

proof end;

Lm14: for V being RealLinearSpace

for p, q being Element of V holds (0 * p) + (0 * q) = 0. V

proof end;

Lm15: for V being RealLinearSpace

for o, v, w being Element of V

for b, a2, a3 being Real holds ((0 * o) + ((b * a2) * v)) + (((- b) * a3) * w) = b * ((a2 * v) - (a3 * w))

proof end;

theorem Th8: :: ANPROJ_2:8

for V being RealLinearSpace

for o, u, v, w, u1, v1, w1, u2, v2, w2 being Element of V st not o is zero & u,v,w are_Prop_Vect & u2,v2,w2 are_Prop_Vect & u1,v1,w1 are_Prop_Vect & o,u,v,w,u2,v2,w2 are_perspective & not are_Prop o,u2 & not are_Prop o,v2 & not are_Prop o,w2 & not are_Prop u,u2 & not are_Prop v,v2 & not are_Prop w,w2 & not o,u,v are_LinDep & not o,u,w are_LinDep & not o,v,w are_LinDep & u,v,w,u1,v1,w1 lie_on_a_triangle & u2,v2,w2,u1,v1,w1 lie_on_a_triangle holds

u1,v1,w1 are_LinDep

for o, u, v, w, u1, v1, w1, u2, v2, w2 being Element of V st not o is zero & u,v,w are_Prop_Vect & u2,v2,w2 are_Prop_Vect & u1,v1,w1 are_Prop_Vect & o,u,v,w,u2,v2,w2 are_perspective & not are_Prop o,u2 & not are_Prop o,v2 & not are_Prop o,w2 & not are_Prop u,u2 & not are_Prop v,v2 & not are_Prop w,w2 & not o,u,v are_LinDep & not o,u,w are_LinDep & not o,v,w are_LinDep & u,v,w,u1,v1,w1 lie_on_a_triangle & u2,v2,w2,u1,v1,w1 lie_on_a_triangle holds

u1,v1,w1 are_LinDep

proof end;

definition

let V be RealLinearSpace;

let o, u, v, w, u2, v2, w2 be Element of V;

end;
let o, u, v, w, u2, v2, w2 be Element of V;

pred o,u,v,w,u2,v2,w2 lie_on_an_angle means :: ANPROJ_2:def 4

( not o,u,u2 are_LinDep & o,u,v are_LinDep & o,u,w are_LinDep & o,u2,v2 are_LinDep & o,u2,w2 are_LinDep );

( not o,u,u2 are_LinDep & o,u,v are_LinDep & o,u,w are_LinDep & o,u2,v2 are_LinDep & o,u2,w2 are_LinDep );

:: deftheorem defines lie_on_an_angle ANPROJ_2:def 4 :

for V being RealLinearSpace

for o, u, v, w, u2, v2, w2 being Element of V holds

( o,u,v,w,u2,v2,w2 lie_on_an_angle iff ( not o,u,u2 are_LinDep & o,u,v are_LinDep & o,u,w are_LinDep & o,u2,v2 are_LinDep & o,u2,w2 are_LinDep ) );

for V being RealLinearSpace

for o, u, v, w, u2, v2, w2 being Element of V holds

( o,u,v,w,u2,v2,w2 lie_on_an_angle iff ( not o,u,u2 are_LinDep & o,u,v are_LinDep & o,u,w are_LinDep & o,u2,v2 are_LinDep & o,u2,w2 are_LinDep ) );

:: deftheorem defines are_half_mutually_not_Prop ANPROJ_2:def 5 :

for V being RealLinearSpace

for o, u, v, w, u2, v2, w2 being Element of V holds

( o,u,v,w,u2,v2,w2 are_half_mutually_not_Prop iff ( not are_Prop o,v & not are_Prop o,w & not are_Prop o,v2 & not are_Prop o,w2 & not are_Prop u,v & not are_Prop u,w & not are_Prop u2,v2 & not are_Prop u2,w2 & not are_Prop v,w & not are_Prop v2,w2 ) );

for V being RealLinearSpace

for o, u, v, w, u2, v2, w2 being Element of V holds

( o,u,v,w,u2,v2,w2 are_half_mutually_not_Prop iff ( not are_Prop o,v & not are_Prop o,w & not are_Prop o,v2 & not are_Prop o,w2 & not are_Prop u,v & not are_Prop u,w & not are_Prop u2,v2 & not are_Prop u2,w2 & not are_Prop v,w & not are_Prop v2,w2 ) );

Lm16: for V being RealLinearSpace

for u2, w2 being Element of V

for b1 being Real st b1 * u2 = w2 & b1 <> 0 holds

are_Prop u2,w2

proof end;

Lm17: for V being RealLinearSpace

for p, q, y being Element of V

for a being Real st not are_Prop p,q & y = a * q & a <> 0 holds

not are_Prop p,y

proof end;

Lm18: for V being RealLinearSpace

for o, u, w1, u2, v2 being Element of V

for a, b, c2 being Real st w1 = (a * u) + (b * v2) & v2 = o + (c2 * u2) holds

w1 = ((b * o) + (a * u)) + ((b * c2) * u2)

proof end;

Lm19: for V being RealLinearSpace

for o, u, v1, w1, u2 being Element of V

for a, b, a2 being Real st w1 = (a * u2) + (b * v1) & v1 = o + (a2 * u) holds

w1 = ((b * o) + ((b * a2) * u)) + (a * u2)

proof end;

Lm20: for V being RealLinearSpace

for p, q being Element of V

for a being Real st a * p = q & a <> 0 & not p is zero holds

not q is zero

by RLVECT_1:11;

Lm21: for V being RealLinearSpace

for p, q, s, y being Element of V

for a, b being Real st not are_Prop p,q & y = a * q & a <> 0 & s = b * p & b <> 0 holds

not are_Prop s,y

proof end;

Lm22: for V being RealLinearSpace

for o, r, u, v, u2, v2 being Element of V

for a1, a2, A, B being Real st r = (A * u2) + (B * v2) & u2 = o + (a1 * u) & v2 = o + (a2 * v) holds

r = (((A + B) * o) + ((A * a1) * u)) + ((B * a2) * v)

proof end;

Lm23: for a2, c2, a3 being Real st a2 <> a3 & c2 <> 0 holds

(a3 * c2) - (a2 * c2) <> 0

proof end;

Lm24: for a2, c2, a3, c3, A1, A19, B1, B19 being Real st A1 + B1 = A19 + B19 & A1 * a2 = A19 * a3 & B1 * c3 = B19 * c2 & a2 <> a3 & c2 <> 0 holds

A1 = (((a3 * c3) - (a3 * c2)) * (((a3 * c2) - (a2 * c2)) ")) * B1

proof end;

Lm25: for a2, c2, a3, B1 being Real st c2 <> 0 & a2 <> a3 & B1 <> 0 holds

B1 * (((a3 * c2) - (a2 * c2)) ") <> 0

proof end;

Lm26: for V being RealLinearSpace

for o, u, u1, u2 being Element of V

for a2, c2, a3, c3, A1, B1 being Real st A1 = (((a3 * c3) - (a3 * c2)) * (((a3 * c2) - (a2 * c2)) ")) * B1 & c2 <> 0 & a2 <> a3 & u1 = (((A1 + B1) * o) + ((A1 * a2) * u)) + ((B1 * c3) * u2) holds

u1 = (B1 * (((a3 * c2) - (a2 * c2)) ")) * (((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2))

proof end;

Lm27: for V being RealLinearSpace

for p, q, r, u, u1, u2 being Element of V holds ((p + q) + r) + ((u + u2) + u1) = ((p + u) + (q + u2)) + (r + u1)

proof end;

Lm28: for V being RealLinearSpace

for o, u, u1, v1, u2, w2 being Element of V

for a2, c2, a3, c3, C2, C3 being Real st u1 = ((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2) & v1 = (o + (a3 * u)) + (c3 * u2) & w2 = (o + (a2 * u)) + (c2 * u2) & C2 + C3 = (a2 * c2) - (a3 * c3) & (C2 * a3) + (C3 * a2) = (a2 * a3) * (c2 - c3) & (C2 * c3) + (C3 * c2) = (c2 * c3) * (a2 - a3) holds

((1 * u1) + (C2 * v1)) + (C3 * w2) = 0. V

proof end;

Lm29: for V being RealLinearSpace

for o, u, w1, u2, w2 being Element of V

for a2, c2, A3, A39, B3, B39 being Real st w2 = (o + (a2 * u)) + (c2 * u2) & w1 = ((B3 * o) + (A3 * u)) + ((B3 * c2) * u2) & B3 = B39 & A3 = B39 * a2 holds

w1 = B3 * w2

proof end;

theorem Th9: :: ANPROJ_2:9

for V being RealLinearSpace

for o, u, v, w, u1, v1, w1, u2, v2, w2 being Element of V st not o is zero & u,v,w are_Prop_Vect & u2,v2,w2 are_Prop_Vect & u1,v1,w1 are_Prop_Vect & o,u,v,w,u2,v2,w2 lie_on_an_angle & o,u,v,w,u2,v2,w2 are_half_mutually_not_Prop & u,v2,w1 are_LinDep & u2,v,w1 are_LinDep & u,w2,v1 are_LinDep & w,u2,v1 are_LinDep & v,w2,u1 are_LinDep & w,v2,u1 are_LinDep holds

u1,v1,w1 are_LinDep

for o, u, v, w, u1, v1, w1, u2, v2, w2 being Element of V st not o is zero & u,v,w are_Prop_Vect & u2,v2,w2 are_Prop_Vect & u1,v1,w1 are_Prop_Vect & o,u,v,w,u2,v2,w2 lie_on_an_angle & o,u,v,w,u2,v2,w2 are_half_mutually_not_Prop & u,v2,w1 are_LinDep & u2,v,w1 are_LinDep & u,w2,v1 are_LinDep & w,u2,v1 are_LinDep & v,w2,u1 are_LinDep & w,v2,u1 are_LinDep holds

u1,v1,w1 are_LinDep

proof end;

theorem Th10: :: ANPROJ_2:10

for A being non empty set

for x1 being Element of A ex f being Element of Funcs (A,REAL) st

( f . x1 = 1 & ( for z being set st z in A & z <> x1 holds

f . z = 0 ) )

for x1 being Element of A ex f being Element of Funcs (A,REAL) st

( f . x1 = 1 & ( for z being set st z in A & z <> x1 holds

f . z = 0 ) )

proof end;

theorem Th11: :: ANPROJ_2:11

for A being non empty set

for f, g, h being Element of Funcs (A,REAL)

for x1, x2, x3 being Element of A st x1 <> x2 & x1 <> x3 & x2 <> x3 & f . x1 = 1 & ( for z being set st z in A & z <> x1 holds

f . z = 0 ) & g . x2 = 1 & ( for z being set st z in A & z <> x2 holds

g . z = 0 ) & h . x3 = 1 & ( for z being set st z in A & z <> x3 holds

h . z = 0 ) holds

for a, b, c being Real st (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h])) = RealFuncZero A holds

( a = 0 & b = 0 & c = 0 )

for f, g, h being Element of Funcs (A,REAL)

for x1, x2, x3 being Element of A st x1 <> x2 & x1 <> x3 & x2 <> x3 & f . x1 = 1 & ( for z being set st z in A & z <> x1 holds

f . z = 0 ) & g . x2 = 1 & ( for z being set st z in A & z <> x2 holds

g . z = 0 ) & h . x3 = 1 & ( for z being set st z in A & z <> x3 holds

h . z = 0 ) holds

for a, b, c being Real st (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h])) = RealFuncZero A holds

( a = 0 & b = 0 & c = 0 )

proof end;

theorem :: ANPROJ_2:12

for A being non empty set

for x1, x2, x3 being Element of A st x1 <> x2 & x1 <> x3 & x2 <> x3 holds

ex f, g, h being Element of Funcs (A,REAL) st

for a, b, c being Real st (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h])) = RealFuncZero A holds

( a = 0 & b = 0 & c = 0 )

for x1, x2, x3 being Element of A st x1 <> x2 & x1 <> x3 & x2 <> x3 holds

ex f, g, h being Element of Funcs (A,REAL) st

for a, b, c being Real st (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h])) = RealFuncZero A holds

( a = 0 & b = 0 & c = 0 )

proof end;

theorem Th13: :: ANPROJ_2:13

for A being non empty set

for f, g, h being Element of Funcs (A,REAL)

for x1, x2, x3 being Element of A st A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 & f . x1 = 1 & ( for z being set st z in A & z <> x1 holds

f . z = 0 ) & g . x2 = 1 & ( for z being set st z in A & z <> x2 holds

g . z = 0 ) & h . x3 = 1 & ( for z being set st z in A & z <> x3 holds

h . z = 0 ) holds

for h9 being Element of Funcs (A,REAL) ex a, b, c being Real st h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))

for f, g, h being Element of Funcs (A,REAL)

for x1, x2, x3 being Element of A st A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 & f . x1 = 1 & ( for z being set st z in A & z <> x1 holds

f . z = 0 ) & g . x2 = 1 & ( for z being set st z in A & z <> x2 holds

g . z = 0 ) & h . x3 = 1 & ( for z being set st z in A & z <> x3 holds

h . z = 0 ) holds

for h9 being Element of Funcs (A,REAL) ex a, b, c being Real st h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))

proof end;

theorem :: ANPROJ_2:14

for A being non empty set

for x1, x2, x3 being Element of A st A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 holds

ex f, g, h being Element of Funcs (A,REAL) st

for h9 being Element of Funcs (A,REAL) ex a, b, c being Real st h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))

for x1, x2, x3 being Element of A st A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 holds

ex f, g, h being Element of Funcs (A,REAL) st

for h9 being Element of Funcs (A,REAL) ex a, b, c being Real st h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))

proof end;

theorem Th15: :: ANPROJ_2:15

for A being non empty set

for x1, x2, x3 being Element of A st A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 holds

ex f, g, h being Element of Funcs (A,REAL) st

( ( for a, b, c being Real st (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h])) = RealFuncZero A holds

( a = 0 & b = 0 & c = 0 ) ) & ( for h9 being Element of Funcs (A,REAL) ex a, b, c being Real st h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h])) ) )

for x1, x2, x3 being Element of A st A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 holds

ex f, g, h being Element of Funcs (A,REAL) st

( ( for a, b, c being Real st (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h])) = RealFuncZero A holds

( a = 0 & b = 0 & c = 0 ) ) & ( for h9 being Element of Funcs (A,REAL) ex a, b, c being Real st h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h])) ) )

proof end;

Lm30: ex A being non empty set ex x1, x2, x3 being Element of A st

( A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 )

proof end;

theorem Th16: :: ANPROJ_2:16

ex V being non trivial RealLinearSpace ex u, v, w being Element of V st

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

( a = 0 & b = 0 & c = 0 ) ) & ( for y being Element of V ex a, b, c being Real st y = ((a * u) + (b * v)) + (c * w) ) )

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

( a = 0 & b = 0 & c = 0 ) ) & ( for y being Element of V ex a, b, c being Real st y = ((a * u) + (b * v)) + (c * w) ) )

proof end;

theorem Th17: :: ANPROJ_2:17

for A being non empty set

for f, g, h, f1 being Element of Funcs (A,REAL)

for x1, x2, x3, x4 being Element of A st x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 & f . x1 = 1 & ( for z being set st z in A & z <> x1 holds

f . z = 0 ) & g . x2 = 1 & ( for z being set st z in A & z <> x2 holds

g . z = 0 ) & h . x3 = 1 & ( for z being set st z in A & z <> x3 holds

h . z = 0 ) & f1 . x4 = 1 & ( for z being set st z in A & z <> x4 holds

f1 . z = 0 ) holds

for a, b, c, d being Real st (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))),((RealFuncExtMult A) . [d,f1])) = RealFuncZero A holds

( a = 0 & b = 0 & c = 0 & d = 0 )

for f, g, h, f1 being Element of Funcs (A,REAL)

for x1, x2, x3, x4 being Element of A st x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 & f . x1 = 1 & ( for z being set st z in A & z <> x1 holds

f . z = 0 ) & g . x2 = 1 & ( for z being set st z in A & z <> x2 holds

g . z = 0 ) & h . x3 = 1 & ( for z being set st z in A & z <> x3 holds

h . z = 0 ) & f1 . x4 = 1 & ( for z being set st z in A & z <> x4 holds

f1 . z = 0 ) holds

for a, b, c, d being Real st (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))),((RealFuncExtMult A) . [d,f1])) = RealFuncZero A holds

( a = 0 & b = 0 & c = 0 & d = 0 )

proof end;

theorem :: ANPROJ_2:18

for A being non empty set

for x1, x2, x3, x4 being Element of A st x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 holds

ex f, g, h, f1 being Element of Funcs (A,REAL) st

for a, b, c, d being Real st (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))),((RealFuncExtMult A) . [d,f1])) = RealFuncZero A holds

( a = 0 & b = 0 & c = 0 & d = 0 )

for x1, x2, x3, x4 being Element of A st x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 holds

ex f, g, h, f1 being Element of Funcs (A,REAL) st

for a, b, c, d being Real st (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))),((RealFuncExtMult A) . [d,f1])) = RealFuncZero A holds

( a = 0 & b = 0 & c = 0 & d = 0 )

proof end;

theorem Th19: :: ANPROJ_2:19

for A being non empty set

for f, g, h, f1 being Element of Funcs (A,REAL)

for x1, x2, x3, x4 being Element of A st A = {x1,x2,x3,x4} & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 & f . x1 = 1 & ( for z being set st z in A & z <> x1 holds

f . z = 0 ) & g . x2 = 1 & ( for z being set st z in A & z <> x2 holds

g . z = 0 ) & h . x3 = 1 & ( for z being set st z in A & z <> x3 holds

h . z = 0 ) & f1 . x4 = 1 & ( for z being set st z in A & z <> x4 holds

f1 . z = 0 ) holds

for h9 being Element of Funcs (A,REAL) ex a, b, c, d being Real st h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))),((RealFuncExtMult A) . [d,f1]))

for f, g, h, f1 being Element of Funcs (A,REAL)

for x1, x2, x3, x4 being Element of A st A = {x1,x2,x3,x4} & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 & f . x1 = 1 & ( for z being set st z in A & z <> x1 holds

f . z = 0 ) & g . x2 = 1 & ( for z being set st z in A & z <> x2 holds

g . z = 0 ) & h . x3 = 1 & ( for z being set st z in A & z <> x3 holds

h . z = 0 ) & f1 . x4 = 1 & ( for z being set st z in A & z <> x4 holds

f1 . z = 0 ) holds

for h9 being Element of Funcs (A,REAL) ex a, b, c, d being Real st h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))),((RealFuncExtMult A) . [d,f1]))

proof end;

theorem :: ANPROJ_2:20

for A being non empty set

for x1, x2, x3, x4 being Element of A st A = {x1,x2,x3,x4} & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 holds

ex f, g, h, f1 being Element of Funcs (A,REAL) st

for h9 being Element of Funcs (A,REAL) ex a, b, c, d being Real st h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))),((RealFuncExtMult A) . [d,f1]))

for x1, x2, x3, x4 being Element of A st A = {x1,x2,x3,x4} & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 holds

ex f, g, h, f1 being Element of Funcs (A,REAL) st

for h9 being Element of Funcs (A,REAL) ex a, b, c, d being Real st h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))),((RealFuncExtMult A) . [d,f1]))

proof end;

theorem Th21: :: ANPROJ_2:21

for A being non empty set

for x1, x2, x3, x4 being Element of A st A = {x1,x2,x3,x4} & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 holds

ex f, g, h, f1 being Element of Funcs (A,REAL) st

( ( for a, b, c, d being Real st (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))),((RealFuncExtMult A) . [d,f1])) = RealFuncZero A holds

( a = 0 & b = 0 & c = 0 & d = 0 ) ) & ( for h9 being Element of Funcs (A,REAL) ex a, b, c, d being Real st h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))),((RealFuncExtMult A) . [d,f1])) ) )

for x1, x2, x3, x4 being Element of A st A = {x1,x2,x3,x4} & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 holds

ex f, g, h, f1 being Element of Funcs (A,REAL) st

( ( for a, b, c, d being Real st (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))),((RealFuncExtMult A) . [d,f1])) = RealFuncZero A holds

( a = 0 & b = 0 & c = 0 & d = 0 ) ) & ( for h9 being Element of Funcs (A,REAL) ex a, b, c, d being Real st h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))),((RealFuncExtMult A) . [d,f1])) ) )

proof end;

Lm31: ex A being non empty set ex x1, x2, x3, x4 being Element of A st

( A = {x1,x2,x3,x4} & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 )

proof end;

theorem Th22: :: ANPROJ_2:22

ex V being non trivial RealLinearSpace ex u, v, w, u1 being Element of V st

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

( a = 0 & b = 0 & c = 0 & d = 0 ) ) & ( for y being Element of V ex a, b, c, d being Real st y = (((a * u) + (b * v)) + (c * w)) + (d * u1) ) )

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

( a = 0 & b = 0 & c = 0 & d = 0 ) ) & ( for y being Element of V ex a, b, c, d being Real st y = (((a * u) + (b * v)) + (c * w)) + (d * u1) ) )

proof end;

:: deftheorem Def6 defines up-3-dimensional ANPROJ_2:def 6 :

for IT being RealLinearSpace holds

( IT is up-3-dimensional iff ex u, v, w1 being Element of IT st

for a, b, c being Real st ((a * u) + (b * v)) + (c * w1) = 0. IT holds

( a = 0 & b = 0 & c = 0 ) );

for IT being RealLinearSpace holds

( IT is up-3-dimensional iff ex u, v, w1 being Element of IT st

for a, b, c being Real st ((a * u) + (b * v)) + (c * w1) = 0. IT holds

( a = 0 & b = 0 & c = 0 ) );

registration

ex b_{1} being RealLinearSpace st b_{1} is up-3-dimensional
by Th16, Def6;

end;

cluster non empty V72() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital up-3-dimensional for RealLinearSpace;

existence ex b

registration

for b_{1} being RealLinearSpace st b_{1} is up-3-dimensional holds

not b_{1} is trivial
end;

cluster non empty V72() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital up-3-dimensional -> non trivial for RealLinearSpace;

coherence for b

not b

proof end;

definition

let CS be non empty CollStr ;

( CS is reflexive iff for p, q, r being Element of CS holds

( p,q,p are_collinear & p,p,q are_collinear & p,q,q are_collinear ) )

( CS is transitive iff for p, q, r, r1, r2 being Element of CS st p <> q & p,q,r are_collinear & p,q,r1 are_collinear & p,q,r2 are_collinear holds

r,r1,r2 are_collinear )

end;
redefine attr CS is reflexive means :Def7: :: ANPROJ_2:def 7

for p, q, r being Element of CS holds

( p,q,p are_collinear & p,p,q are_collinear & p,q,q are_collinear );

compatibility for p, q, r being Element of CS holds

( p,q,p are_collinear & p,p,q are_collinear & p,q,q are_collinear );

( CS is reflexive iff for p, q, r being Element of CS holds

( p,q,p are_collinear & p,p,q are_collinear & p,q,q are_collinear ) )

proof end;

redefine attr CS is transitive means :Def8: :: ANPROJ_2:def 8

for p, q, r, r1, r2 being Element of CS st p <> q & p,q,r are_collinear & p,q,r1 are_collinear & p,q,r2 are_collinear holds

r,r1,r2 are_collinear ;

compatibility for p, q, r, r1, r2 being Element of CS st p <> q & p,q,r are_collinear & p,q,r1 are_collinear & p,q,r2 are_collinear holds

r,r1,r2 are_collinear ;

( CS is transitive iff for p, q, r, r1, r2 being Element of CS st p <> q & p,q,r are_collinear & p,q,r1 are_collinear & p,q,r2 are_collinear holds

r,r1,r2 are_collinear )

proof end;

:: deftheorem Def7 defines reflexive ANPROJ_2:def 7 :

for CS being non empty CollStr holds

( CS is reflexive iff for p, q, r being Element of CS holds

( p,q,p are_collinear & p,p,q are_collinear & p,q,q are_collinear ) );

for CS being non empty CollStr holds

( CS is reflexive iff for p, q, r being Element of CS holds

( p,q,p are_collinear & p,p,q are_collinear & p,q,q are_collinear ) );

:: deftheorem Def8 defines transitive ANPROJ_2:def 8 :

for CS being non empty CollStr holds

( CS is transitive iff for p, q, r, r1, r2 being Element of CS st p <> q & p,q,r are_collinear & p,q,r1 are_collinear & p,q,r2 are_collinear holds

r,r1,r2 are_collinear );

for CS being non empty CollStr holds

( CS is transitive iff for p, q, r, r1, r2 being Element of CS st p <> q & p,q,r are_collinear & p,q,r1 are_collinear & p,q,r2 are_collinear holds

r,r1,r2 are_collinear );

definition

let IT be non empty CollStr ;

end;
attr IT is Vebleian means :Def9: :: ANPROJ_2:def 9

for p, p1, p2, r, r1 being Element of IT st p,p1,r are_collinear & p1,p2,r1 are_collinear holds

ex r2 being Element of IT st

( p,p2,r2 are_collinear & r,r1,r2 are_collinear );

for p, p1, p2, r, r1 being Element of IT st p,p1,r are_collinear & p1,p2,r1 are_collinear holds

ex r2 being Element of IT st

( p,p2,r2 are_collinear & r,r1,r2 are_collinear );

attr IT is at_least_3rank means :Def10: :: ANPROJ_2:def 10

for p, q being Element of IT ex r being Element of IT st

( p <> r & q <> r & p,q,r are_collinear );

for p, q being Element of IT ex r being Element of IT st

( p <> r & q <> r & p,q,r are_collinear );

:: deftheorem Def9 defines Vebleian ANPROJ_2:def 9 :

for IT being non empty CollStr holds

( IT is Vebleian iff for p, p1, p2, r, r1 being Element of IT st p,p1,r are_collinear & p1,p2,r1 are_collinear holds

ex r2 being Element of IT st

( p,p2,r2 are_collinear & r,r1,r2 are_collinear ) );

for IT being non empty CollStr holds

( IT is Vebleian iff for p, p1, p2, r, r1 being Element of IT st p,p1,r are_collinear & p1,p2,r1 are_collinear holds

ex r2 being Element of IT st

( p,p2,r2 are_collinear & r,r1,r2 are_collinear ) );

:: deftheorem Def10 defines at_least_3rank ANPROJ_2:def 10 :

for IT being non empty CollStr holds

( IT is at_least_3rank iff for p, q being Element of IT ex r being Element of IT st

( p <> r & q <> r & p,q,r are_collinear ) );

for IT being non empty CollStr holds

( IT is at_least_3rank iff for p, q being Element of IT ex r being Element of IT st

( p <> r & q <> r & p,q,r are_collinear ) );

theorem Th23: :: ANPROJ_2:23

for V being non trivial RealLinearSpace

for p, q, r being Element of (ProjectiveSpace V) holds

( p,q,r are_collinear iff ex u, v, w being Element of V st

( p = Dir u & q = Dir v & r = Dir w & not u is zero & not v is zero & not w is zero & u,v,w are_LinDep ) ) by ANPROJ_1:24, ANPROJ_1:25;

for p, q, r being Element of (ProjectiveSpace V) holds

( p,q,r are_collinear iff ex u, v, w being Element of V st

( p = Dir u & q = Dir v & r = Dir w & not u is zero & not v is zero & not w is zero & u,v,w are_LinDep ) ) by ANPROJ_1:24, ANPROJ_1:25;

Lm32: for V being non trivial RealLinearSpace holds ProjectiveSpace V is reflexive

proof end;

Lm33: for V being non trivial RealLinearSpace holds ProjectiveSpace V is transitive

proof end;

registration

let V be non trivial RealLinearSpace;

coherence

( ProjectiveSpace V is reflexive & ProjectiveSpace V is transitive ) by Lm32, Lm33;

end;
coherence

( ProjectiveSpace V is reflexive & ProjectiveSpace V is transitive ) by Lm32, Lm33;

theorem Th24: :: ANPROJ_2:24

for V being non trivial RealLinearSpace

for p, q, r being Element of (ProjectiveSpace V) st p,q,r are_collinear holds

( p,r,q are_collinear & q,p,r are_collinear & r,q,p are_collinear & r,p,q are_collinear & q,r,p are_collinear )

for p, q, r being Element of (ProjectiveSpace V) st p,q,r are_collinear holds

( p,r,q are_collinear & q,p,r are_collinear & r,q,p are_collinear & r,p,q are_collinear & q,r,p are_collinear )

proof end;

Lm34: for V being non trivial RealLinearSpace

for p, p1, p2, r, r1 being Element of (ProjectiveSpace V) st p,p1,p2 are_collinear & p,p1,r are_collinear & p1,p2,r1 are_collinear holds

ex r2 being Element of (ProjectiveSpace V) st

( p,p2,r2 are_collinear & r,r1,r2 are_collinear )

proof end;

Lm35: for V being non trivial RealLinearSpace

for p, p1, p2, r, r1 being Element of (ProjectiveSpace V) st not p,p1,p2 are_collinear & p,p1,r are_collinear & p1,p2,r1 are_collinear holds

ex r2 being Element of (ProjectiveSpace V) st

( p,p2,r2 are_collinear & r,r1,r2 are_collinear )

proof end;

Lm36: for V being non trivial RealLinearSpace holds ProjectiveSpace V is Vebleian

proof end;

registration
end;

Lm37: for V being non trivial RealLinearSpace st V is up-3-dimensional holds

ProjectiveSpace V is proper

proof end;

registration
end;

theorem Th25: :: ANPROJ_2:25

for V being non trivial RealLinearSpace st ex u, v being Element of V st

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

( a = 0 & b = 0 ) holds

ProjectiveSpace V is at_least_3rank

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

( a = 0 & b = 0 ) holds

ProjectiveSpace V is at_least_3rank

proof end;

Lm38: for V being non trivial RealLinearSpace st V is up-3-dimensional holds

ProjectiveSpace V is at_least_3rank

proof end;

registration
end;

registration

existence

ex b_{1} being non empty CollStr st

( b_{1} is transitive & b_{1} is reflexive & b_{1} is proper & b_{1} is Vebleian & b_{1} is at_least_3rank )

end;
ex b

( b

proof end;

definition
end;

definition

let IT be non empty CollStr ;

end;
attr IT is Fanoian means :: ANPROJ_2:def 11

for p1, r2, q, r1, q1, p, r being Element of IT st p1,r2,q are_collinear & r1,q1,q are_collinear & p1,r1,p are_collinear & r2,q1,p are_collinear & p1,q1,r are_collinear & r2,r1,r are_collinear & p,q,r are_collinear & not p1,r2,q1 are_collinear & not p1,r2,r1 are_collinear & not p1,r1,q1 are_collinear holds

r2,r1,q1 are_collinear ;

for p1, r2, q, r1, q1, p, r being Element of IT st p1,r2,q are_collinear & r1,q1,q are_collinear & p1,r1,p are_collinear & r2,q1,p are_collinear & p1,q1,r are_collinear & r2,r1,r are_collinear & p,q,r are_collinear & not p1,r2,q1 are_collinear & not p1,r2,r1 are_collinear & not p1,r1,q1 are_collinear holds

r2,r1,q1 are_collinear ;

attr IT is Desarguesian means :: ANPROJ_2:def 12

for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Element of IT st o <> q1 & p1 <> q1 & o <> q2 & p2 <> q2 & o <> q3 & p3 <> q3 & not o,p1,p2 are_collinear & not o,p1,p3 are_collinear & not o,p2,p3 are_collinear & p1,p2,r3 are_collinear & q1,q2,r3 are_collinear & p2,p3,r1 are_collinear & q2,q3,r1 are_collinear & p1,p3,r2 are_collinear & q1,q3,r2 are_collinear & o,p1,q1 are_collinear & o,p2,q2 are_collinear & o,p3,q3 are_collinear holds

r1,r2,r3 are_collinear ;

for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Element of IT st o <> q1 & p1 <> q1 & o <> q2 & p2 <> q2 & o <> q3 & p3 <> q3 & not o,p1,p2 are_collinear & not o,p1,p3 are_collinear & not o,p2,p3 are_collinear & p1,p2,r3 are_collinear & q1,q2,r3 are_collinear & p2,p3,r1 are_collinear & q2,q3,r1 are_collinear & p1,p3,r2 are_collinear & q1,q3,r2 are_collinear & o,p1,q1 are_collinear & o,p2,q2 are_collinear & o,p3,q3 are_collinear holds

r1,r2,r3 are_collinear ;

attr IT is Pappian means :: ANPROJ_2:def 13

for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Element of IT st o <> p2 & o <> p3 & p2 <> p3 & p1 <> p2 & p1 <> p3 & o <> q2 & o <> q3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not o,p1,q1 are_collinear & o,p1,p2 are_collinear & o,p1,p3 are_collinear & o,q1,q2 are_collinear & o,q1,q3 are_collinear & p1,q2,r3 are_collinear & q1,p2,r3 are_collinear & p1,q3,r2 are_collinear & p3,q1,r2 are_collinear & p2,q3,r1 are_collinear & p3,q2,r1 are_collinear holds

r1,r2,r3 are_collinear ;

for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Element of IT st o <> p2 & o <> p3 & p2 <> p3 & p1 <> p2 & p1 <> p3 & o <> q2 & o <> q3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not o,p1,q1 are_collinear & o,p1,p2 are_collinear & o,p1,p3 are_collinear & o,q1,q2 are_collinear & o,q1,q3 are_collinear & p1,q2,r3 are_collinear & q1,p2,r3 are_collinear & p1,q3,r2 are_collinear & p3,q1,r2 are_collinear & p2,q3,r1 are_collinear & p3,q2,r1 are_collinear holds

r1,r2,r3 are_collinear ;

:: deftheorem defines Fanoian ANPROJ_2:def 11 :

for IT being non empty CollStr holds

( IT is Fanoian iff for p1, r2, q, r1, q1, p, r being Element of IT st p1,r2,q are_collinear & r1,q1,q are_collinear & p1,r1,p are_collinear & r2,q1,p are_collinear & p1,q1,r are_collinear & r2,r1,r are_collinear & p,q,r are_collinear & not p1,r2,q1 are_collinear & not p1,r2,r1 are_collinear & not p1,r1,q1 are_collinear holds

r2,r1,q1 are_collinear );

for IT being non empty CollStr holds

( IT is Fanoian iff for p1, r2, q, r1, q1, p, r being Element of IT st p1,r2,q are_collinear & r1,q1,q are_collinear & p1,r1,p are_collinear & r2,q1,p are_collinear & p1,q1,r are_collinear & r2,r1,r are_collinear & p,q,r are_collinear & not p1,r2,q1 are_collinear & not p1,r2,r1 are_collinear & not p1,r1,q1 are_collinear holds

r2,r1,q1 are_collinear );

:: deftheorem defines Desarguesian ANPROJ_2:def 12 :

for IT being non empty CollStr holds

( IT is Desarguesian iff for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Element of IT st o <> q1 & p1 <> q1 & o <> q2 & p2 <> q2 & o <> q3 & p3 <> q3 & not o,p1,p2 are_collinear & not o,p1,p3 are_collinear & not o,p2,p3 are_collinear & p1,p2,r3 are_collinear & q1,q2,r3 are_collinear & p2,p3,r1 are_collinear & q2,q3,r1 are_collinear & p1,p3,r2 are_collinear & q1,q3,r2 are_collinear & o,p1,q1 are_collinear & o,p2,q2 are_collinear & o,p3,q3 are_collinear holds

r1,r2,r3 are_collinear );

for IT being non empty CollStr holds

( IT is Desarguesian iff for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Element of IT st o <> q1 & p1 <> q1 & o <> q2 & p2 <> q2 & o <> q3 & p3 <> q3 & not o,p1,p2 are_collinear & not o,p1,p3 are_collinear & not o,p2,p3 are_collinear & p1,p2,r3 are_collinear & q1,q2,r3 are_collinear & p2,p3,r1 are_collinear & q2,q3,r1 are_collinear & p1,p3,r2 are_collinear & q1,q3,r2 are_collinear & o,p1,q1 are_collinear & o,p2,q2 are_collinear & o,p3,q3 are_collinear holds

r1,r2,r3 are_collinear );

:: deftheorem defines Pappian ANPROJ_2:def 13 :

for IT being non empty CollStr holds

( IT is Pappian iff for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Element of IT st o <> p2 & o <> p3 & p2 <> p3 & p1 <> p2 & p1 <> p3 & o <> q2 & o <> q3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not o,p1,q1 are_collinear & o,p1,p2 are_collinear & o,p1,p3 are_collinear & o,q1,q2 are_collinear & o,q1,q3 are_collinear & p1,q2,r3 are_collinear & q1,p2,r3 are_collinear & p1,q3,r2 are_collinear & p3,q1,r2 are_collinear & p2,q3,r1 are_collinear & p3,q2,r1 are_collinear holds

r1,r2,r3 are_collinear );

for IT being non empty CollStr holds

( IT is Pappian iff for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Element of IT st o <> p2 & o <> p3 & p2 <> p3 & p1 <> p2 & p1 <> p3 & o <> q2 & o <> q3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not o,p1,q1 are_collinear & o,p1,p2 are_collinear & o,p1,p3 are_collinear & o,q1,q2 are_collinear & o,q1,q3 are_collinear & p1,q2,r3 are_collinear & q1,p2,r3 are_collinear & p1,q3,r2 are_collinear & p3,q1,r2 are_collinear & p2,q3,r1 are_collinear & p3,q2,r1 are_collinear holds

r1,r2,r3 are_collinear );

definition

let IT be CollProjectiveSpace;

end;
attr IT is 2-dimensional means :Def14: :: ANPROJ_2:def 14

for p, p1, q, q1 being Element of IT ex r being Element of IT st

( p,p1,r are_collinear & q,q1,r are_collinear );

for p, p1, q, q1 being Element of IT ex r being Element of IT st

( p,p1,r are_collinear & q,q1,r are_collinear );

:: deftheorem Def14 defines 2-dimensional ANPROJ_2:def 14 :

for IT being CollProjectiveSpace holds

( IT is 2-dimensional iff for p, p1, q, q1 being Element of IT ex r being Element of IT st

( p,p1,r are_collinear & q,q1,r are_collinear ) );

for IT being CollProjectiveSpace holds

( IT is 2-dimensional iff for p, p1, q, q1 being Element of IT ex r being Element of IT st

( p,p1,r are_collinear & q,q1,r are_collinear ) );

definition

let IT be CollProjectiveSpace;

end;
attr IT is at_most-3-dimensional means :: ANPROJ_2:def 15

for p, p1, q, q1, r2 being Element of IT ex r, r1 being Element of IT st

( p,q,r are_collinear & p1,q1,r1 are_collinear & r2,r,r1 are_collinear );

for p, p1, q, q1, r2 being Element of IT ex r, r1 being Element of IT st

( p,q,r are_collinear & p1,q1,r1 are_collinear & r2,r,r1 are_collinear );

:: deftheorem defines at_most-3-dimensional ANPROJ_2:def 15 :

for IT being CollProjectiveSpace holds

( IT is at_most-3-dimensional iff for p, p1, q, q1, r2 being Element of IT ex r, r1 being Element of IT st

( p,q,r are_collinear & p1,q1,r1 are_collinear & r2,r,r1 are_collinear ) );

for IT being CollProjectiveSpace holds

( IT is at_most-3-dimensional iff for p, p1, q, q1, r2 being Element of IT ex r, r1 being Element of IT st

( p,q,r are_collinear & p1,q1,r1 are_collinear & r2,r,r1 are_collinear ) );

theorem Th26: :: ANPROJ_2:26

for V being non trivial RealLinearSpace

for p, p1, q, q1, r, r1, r2 being Element of (ProjectiveSpace V) st p1,r2,q are_collinear & r1,q1,q are_collinear & p1,r1,p are_collinear & r2,q1,p are_collinear & p1,q1,r are_collinear & r2,r1,r are_collinear & p,q,r are_collinear & not p1,r2,q1 are_collinear & not p1,r2,r1 are_collinear & not p1,r1,q1 are_collinear holds

r2,r1,q1 are_collinear

for p, p1, q, q1, r, r1, r2 being Element of (ProjectiveSpace V) st p1,r2,q are_collinear & r1,q1,q are_collinear & p1,r1,p are_collinear & r2,q1,p are_collinear & p1,q1,r are_collinear & r2,r1,r are_collinear & p,q,r are_collinear & not p1,r2,q1 are_collinear & not p1,r2,r1 are_collinear & not p1,r1,q1 are_collinear holds

r2,r1,q1 are_collinear

proof end;

Lm39: for V being up-3-dimensional RealLinearSpace holds ProjectiveSpace V is Fanoian

by Th26;

Lm40: for V being up-3-dimensional RealLinearSpace holds ProjectiveSpace V is Desarguesian

proof end;

Lm41: for V being up-3-dimensional RealLinearSpace holds ProjectiveSpace V is Pappian

proof end;

registration

let V be up-3-dimensional RealLinearSpace;

coherence

( ProjectiveSpace V is Fanoian & ProjectiveSpace V is Desarguesian & ProjectiveSpace V is Pappian ) by Lm39, Lm40, Lm41;

end;
coherence

( ProjectiveSpace V is Fanoian & ProjectiveSpace V is Desarguesian & ProjectiveSpace V is Pappian ) by Lm39, Lm40, Lm41;

theorem Th27: :: ANPROJ_2:27

for V being non trivial RealLinearSpace st ex u, v, w being Element of V st

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

( a = 0 & b = 0 & c = 0 ) ) & ( for y being Element of V ex a, b, c being Real st y = ((a * u) + (b * v)) + (c * w) ) ) holds

ex x1, x2 being Element of (ProjectiveSpace V) st

( x1 <> x2 & ( for r1, r2 being Element of (ProjectiveSpace V) ex q being Element of (ProjectiveSpace V) st

( x1,x2,q are_collinear & r1,r2,q are_collinear ) ) )

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

( a = 0 & b = 0 & c = 0 ) ) & ( for y being Element of V ex a, b, c being Real st y = ((a * u) + (b * v)) + (c * w) ) ) holds

ex x1, x2 being Element of (ProjectiveSpace V) st

( x1 <> x2 & ( for r1, r2 being Element of (ProjectiveSpace V) ex q being Element of (ProjectiveSpace V) st

( x1,x2,q are_collinear & r1,r2,q are_collinear ) ) )

proof end;

theorem Th28: :: ANPROJ_2:28

for V being non trivial RealLinearSpace st ex x1, x2 being Element of (ProjectiveSpace V) st

( x1 <> x2 & ( for r1, r2 being Element of (ProjectiveSpace V) ex q being Element of (ProjectiveSpace V) st

( x1,x2,q are_collinear & r1,r2,q are_collinear ) ) ) holds

for p, p1, q, q1 being Element of (ProjectiveSpace V) ex r being Element of (ProjectiveSpace V) st

( p,p1,r are_collinear & q,q1,r are_collinear )

( x1 <> x2 & ( for r1, r2 being Element of (ProjectiveSpace V) ex q being Element of (ProjectiveSpace V) st

( x1,x2,q are_collinear & r1,r2,q are_collinear ) ) ) holds

for p, p1, q, q1 being Element of (ProjectiveSpace V) ex r being Element of (ProjectiveSpace V) st

( p,p1,r are_collinear & q,q1,r are_collinear )

proof end;

theorem Th29: :: ANPROJ_2:29

for V being non trivial RealLinearSpace st ex u, v, w being Element of V st

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

( a = 0 & b = 0 & c = 0 ) ) & ( for y being Element of V ex a, b, c being Real st y = ((a * u) + (b * v)) + (c * w) ) ) holds

ex CS being CollProjectiveSpace st

( CS = ProjectiveSpace V & CS is 2-dimensional )

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

( a = 0 & b = 0 & c = 0 ) ) & ( for y being Element of V ex a, b, c being Real st y = ((a * u) + (b * v)) + (c * w) ) ) holds

ex CS being CollProjectiveSpace st

( CS = ProjectiveSpace V & CS is 2-dimensional )

proof end;

Lm42: for V being non trivial RealLinearSpace st ex y, u, v, w being Element of V st

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

( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) holds

V is up-3-dimensional

proof end;

Lm43: for V being non trivial RealLinearSpace st ex y, u, v, w being Element of V st

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

( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) holds

( ProjectiveSpace V is proper & ProjectiveSpace V is at_least_3rank )

proof end;

theorem Th30: :: ANPROJ_2:30

for V being non trivial RealLinearSpace st ex y, u, v, w being Element of V st

( ( for w1 being Element of V ex a, b, a1, b1 being Real st w1 = (((a * y) + (b * u)) + (a1 * v)) + (b1 * w) ) & ( for a, b, a1, b1 being Real st (((a * y) + (b * u)) + (a1 * v)) + (b1 * w) = 0. V holds

( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) ) ) holds

ex p, q1, q2 being Element of (ProjectiveSpace V) st

( not p,q1,q2 are_collinear & ( for r1, r2 being Element of (ProjectiveSpace V) ex q3, r3 being Element of (ProjectiveSpace V) st

( r1,r2,r3 are_collinear & q1,q2,q3 are_collinear & p,r3,q3 are_collinear ) ) )

( ( for w1 being Element of V ex a, b, a1, b1 being Real st w1 = (((a * y) + (b * u)) + (a1 * v)) + (b1 * w) ) & ( for a, b, a1, b1 being Real st (((a * y) + (b * u)) + (a1 * v)) + (b1 * w) = 0. V holds

( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) ) ) holds

ex p, q1, q2 being Element of (ProjectiveSpace V) st

( not p,q1,q2 are_collinear & ( for r1, r2 being Element of (ProjectiveSpace V) ex q3, r3 being Element of (ProjectiveSpace V) st

( r1,r2,r3 are_collinear & q1,q2,q3 are_collinear & p,r3,q3 are_collinear ) ) )

proof end;

Lm44: for V being non trivial RealLinearSpace

for x, d, b, b9, d9, q being Element of (ProjectiveSpace V) st not q,b,d are_collinear & b,d,x are_collinear & q,b9,b are_collinear & q,d9,d are_collinear holds

ex o being Element of (ProjectiveSpace V) st

( b9,d9,o are_collinear & q,x,o are_collinear )

proof end;

theorem Th31: :: ANPROJ_2:31

for V being non trivial RealLinearSpace st ProjectiveSpace V is proper & ProjectiveSpace V is at_least_3rank & ex p, q1, q2 being Element of (ProjectiveSpace V) st

( not p,q1,q2 are_collinear & ( for r1, r2 being Element of (ProjectiveSpace V) ex q3, r3 being Element of (ProjectiveSpace V) st

( r1,r2,r3 are_collinear & q1,q2,q3 are_collinear & p,r3,q3 are_collinear ) ) ) holds

ex CS being CollProjectiveSpace st

( CS = ProjectiveSpace V & CS is at_most-3-dimensional )

( not p,q1,q2 are_collinear & ( for r1, r2 being Element of (ProjectiveSpace V) ex q3, r3 being Element of (ProjectiveSpace V) st

( r1,r2,r3 are_collinear & q1,q2,q3 are_collinear & p,r3,q3 are_collinear ) ) ) holds

ex CS being CollProjectiveSpace st

( CS = ProjectiveSpace V & CS is at_most-3-dimensional )

proof end;

theorem Th32: :: ANPROJ_2:32

for V being non trivial RealLinearSpace st ex y, u, v, w being Element of V st

( ( for w1 being Element of V ex a, b, c, c1 being Real st w1 = (((a * y) + (b * u)) + (c * v)) + (c1 * w) ) & ( for a, b, a1, b1 being Real st (((a * y) + (b * u)) + (a1 * v)) + (b1 * w) = 0. V holds

( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) ) ) holds

ex CS being CollProjectiveSpace st

( CS = ProjectiveSpace V & CS is at_most-3-dimensional )

( ( for w1 being Element of V ex a, b, c, c1 being Real st w1 = (((a * y) + (b * u)) + (c * v)) + (c1 * w) ) & ( for a, b, a1, b1 being Real st (((a * y) + (b * u)) + (a1 * v)) + (b1 * w) = 0. V holds

( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) ) ) holds

ex CS being CollProjectiveSpace st

( CS = ProjectiveSpace V & CS is at_most-3-dimensional )

proof end;

theorem Th33: :: ANPROJ_2:33

for V being non trivial RealLinearSpace st ex u, v, u1, v1 being Element of V st

for a, b, a1, b1 being Real st (((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1) = 0. V holds

( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) holds

ex CS being CollProjectiveSpace st

( CS = ProjectiveSpace V & not CS is 2-dimensional )

for a, b, a1, b1 being Real st (((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1) = 0. V holds

( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) holds

ex CS being CollProjectiveSpace st

( CS = ProjectiveSpace V & not CS is 2-dimensional )

proof end;

theorem Th34: :: ANPROJ_2:34

for V being non trivial RealLinearSpace st ex u, v, u1, v1 being Element of V st

( ( for w being Element of V ex a, b, a1, b1 being Real st w = (((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1) ) & ( for a, b, a1, b1 being Real st (((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1) = 0. V holds

( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) ) ) holds

ex CS being CollProjectiveSpace st

( CS = ProjectiveSpace V & CS is up-3-dimensional & CS is at_most-3-dimensional )

( ( for w being Element of V ex a, b, a1, b1 being Real st w = (((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1) ) & ( for a, b, a1, b1 being Real st (((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1) = 0. V holds

( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) ) ) holds

ex CS being CollProjectiveSpace st

( CS = ProjectiveSpace V & CS is up-3-dimensional & CS is at_most-3-dimensional )

proof end;

registration

ex b_{1} being CollProjectiveSpace st

( b_{1} is strict & b_{1} is Fanoian & b_{1} is Desarguesian & b_{1} is Pappian & b_{1} is 2-dimensional )

ex b_{1} being CollProjectiveSpace st

( b_{1} is strict & b_{1} is Fanoian & b_{1} is Desarguesian & b_{1} is Pappian & b_{1} is at_most-3-dimensional & b_{1} is up-3-dimensional )
end;

cluster non empty strict reflexive transitive proper Vebleian at_least_3rank Fanoian Desarguesian Pappian 2-dimensional for CollProjectiveSpace;

existence ex b

( b

proof end;

cluster non empty strict reflexive transitive proper Vebleian at_least_3rank Fanoian Desarguesian Pappian up-3-dimensional at_most-3-dimensional for CollProjectiveSpace;

existence ex b

( b

proof end;

theorem :: ANPROJ_2:35

for CS being non empty CollStr holds

( CS is 2-dimensional CollProjectiveSpace iff ( CS is proper at_least_3rank CollSp & ( for p, p1, q, q1 being Element of CS ex r being Element of CS st

( p,p1,r are_collinear & q,q1,r are_collinear ) ) ) )

( CS is 2-dimensional CollProjectiveSpace iff ( CS is proper at_least_3rank CollSp & ( for p, p1, q, q1 being Element of CS ex r being Element of CS st

( p,p1,r are_collinear & q,q1,r are_collinear ) ) ) )

proof end;