:: Projective Spaces
:: by Wojciech Leo\'nczuk and Krzysztof Pra\.zmowski
::
:: Received June 15, 1990
:: Copyright (c) 1990 Association of Mizar Users

:: ANPROJ_2 semantic presentation

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
( u is_Prop_Vect & v is_Prop_Vect & w is_Prop_Vect & 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
( u is_Prop_Vect & v is_Prop_Vect & 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
( u is_Prop_Vect & v is_Prop_Vect & not are_Prop u,v & u1 is_Prop_Vect & v1 is_Prop_Vect & 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 v, w, u 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 & y is_Prop_Vect )
proof end;

Lm4: for V being RealLinearSpace
for v, w, u, 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, u1, v1, w1, y1 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 v, w, u 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 y, p, w, q, r being Element of V
for a1, b1, a, b, c 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 u is_Prop_Vect & v is_Prop_Vect holds
ex y, w being Element of V st
( u,v,w are_LinDep & q,r,y are_LinDep & p,w,y are_LinDep & y is_Prop_Vect & w is_Prop_Vect )
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
( not y is_Prop_Vect or not u,v,y are_LinDep or not u1,v1,y are_LinDep )
proof end;

definition
let V be RealLinearSpace;
let u, v, w be Element of V;
pred u,v,w are_Prop_Vect means :Def1: :: ANPROJ_2:def 1
( u is_Prop_Vect & v is_Prop_Vect & w is_Prop_Vect );
end;

:: deftheorem Def1 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 ( u is_Prop_Vect & v is_Prop_Vect & w is_Prop_Vect ) );

definition
let V be RealLinearSpace;
let u, v, w, u1, v1, w1 be Element of V;
pred u,v,w,u1,v1,w1 lie_on_a_triangle means :Def2: :: ANPROJ_2:def 2
( u,v,w1 are_LinDep & u,w,v1 are_LinDep & v,w,u1 are_LinDep );
end;

:: deftheorem Def2 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 ) );

definition
let V be RealLinearSpace;
let o, u, v, w, u2, v2, w2 be Element of V;
pred o,u,v,w,u2,v2,w2 are_perspective means :Def3: :: ANPROJ_2:def 3
( o,u,u2 are_LinDep & o,v,v2 are_LinDep & o,w,w2 are_LinDep );
end;

:: deftheorem Def3 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 ) );

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 ) )
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)
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 q, o, p, 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 & p is_Prop_Vect holds
q is_Prop_Vect
proof end;

Lm12: for V being RealLinearSpace
for r, u2, v2, o, u, v 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 r, p, q, o 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, u2, v2, w2, u1, v1, w1 being Element of V st o is_Prop_Vect & 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;
pred o,u,v,w,u2,v2,w2 lie_on_an_angle means :Def4: :: 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 );
end;

:: deftheorem Def4 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 ) );

definition
let V be RealLinearSpace;
let o, u, v, w, u2, v2, w2 be Element of V;
pred o,u,v,w,u2,v2,w2 are_half_mutually_not_Prop means :Def5: :: ANPROJ_2:def 5
( 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 );
end;

:: deftheorem Def5 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 ) );

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 w1, u, v2, o, u2 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 w1, u2, v1, o, u 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 & p is_Prop_Vect holds
q is_Prop_Vect
proof end;

Lm21: for V being RealLinearSpace
for p, q, y, s 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 r, u2, v2, o, u, v 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, a3, c2 being Real st a2 <> a3 & c2 <> 0 holds
(a3 * c2) - (a2 * c2) <> 0
proof end;

Lm24: for a2, a3, c3, c2, A1, A1', B1, B1' being Real st A1 + B1 = A1' + B1' & A1 * a2 = A1' * a3 & B1 * c3 = B1' * c2 & a2 <> a3 & c2 <> 0 holds
A1 = (((a3 * c3) - (a3 * c2)) * (((a3 * c2) - (a2 * c2)) " )) * B1
proof end;

Lm25: for c2, a2, 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 u1, o, u, u2 being Element of V
for a3, c3, c2, a2, 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, u2, u1 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 u1, o, u, u2, v1, w2 being Element of V
for a3, c3, a2, c2, 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 w2, o, u, u2, w1 being Element of V
for a2, c2, A3, A3', B3, B3' being Real st w2 = (o + (a2 * u)) + (c2 * u2) & w1 = ((B3 * o) + (A3 * u)) + ((B3 * c2) * u2) & B3 = B3' & A3 =