:: Projective Spaces
:: by Wojciech Leo\'nczuk and Krzysztof Pra\.zmowski
::
:: Received June 15, 1990
:: Copyright (c) 1990-2021 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 )
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 )
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 )
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 )
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 )
proof end;

definition
let V be RealLinearSpace;
let u, v, w be Element of V;
pred u,v,w are_Prop_Vect means :: ANPROJ_2:def 1
( not u is zero & not v is zero & not w is zero );
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 ) );

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 :: ANPROJ_2:def 2
( u,v,w1 are_LinDep & u,w,v1 are_LinDep & v,w,u1 are_LinDep );
end;

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

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 :: ANPROJ_2:def 3
( o,u,u2 are_LinDep & o,v,v2 are_LinDep & o,w,w2 are_LinDep );
end;

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

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 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
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 :: 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 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 :: 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 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 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
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 ) )
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 )
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 )
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]))
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]))
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])) ) )
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) ) )
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 )
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 )
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]))
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]))
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])) ) )
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) ) )
proof end;

definition
let IT be RealLinearSpace;
attr IT is up-3-dimensional means :Def6: :: ANPROJ_2:def 6
 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 );
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 ) );

registration
cluster non empty V72() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital up-3-dimensional for RLSStruct ;
existence
ex b1 being RealLinearSpace st b1 is up-3-dimensional by Th16, Def6;
end;

registration
cluster non empty V72() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital up-3-dimensional -> non trivial for RLSStruct ;
coherence
for b1 being RealLinearSpace st b1 is up-3-dimensional holds
not b1 is trivial
proof end;
end;

definition
let CS be non empty CollStr ;
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
( 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
( 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;
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 ) );

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

definition
let IT be non empty CollStr ;
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 );
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 );
end;

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

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

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;

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;
cluster ProjectiveSpace V -> reflexive transitive ;
coherence
( ProjectiveSpace V is reflexive & ProjectiveSpace V is transitive ) by Lm32, Lm33;
end;

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 )
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
let V be non trivial RealLinearSpace;
cluster ProjectiveSpace V -> Vebleian ;
coherence
ProjectiveSpace V is Vebleian by Lm36;
end;

Lm37: for V being non trivial RealLinearSpace st V is up-3-dimensional holds
ProjectiveSpace V is proper
proof end;

registration
let V be up-3-dimensional RealLinearSpace;
cluster ProjectiveSpace V -> proper ;
coherence
ProjectiveSpace V is proper by Lm37;
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
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
let V be up-3-dimensional RealLinearSpace;
cluster ProjectiveSpace V -> at_least_3rank ;
coherence
ProjectiveSpace V is at_least_3rank by Lm38;
end;

registration
cluster non empty reflexive transitive proper Vebleian at_least_3rank for CollStr ;
existence
ex b1 being non empty CollStr st
( b1 is transitive & b1 is reflexive & b1 is proper & b1 is Vebleian & b1 is at_least_3rank )
proof end;
end;

definition
mode CollProjectiveSpace is non empty reflexive transitive proper Vebleian at_least_3rank CollStr ;
end;

definition
let IT be non empty CollStr ;
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 ;
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 ;
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 ;
end;

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

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

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

definition
let IT be CollProjectiveSpace;
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 );
end;

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

notation
let IT be CollProjectiveSpace;
antonym up-3-dimensional IT for 2-dimensional ;
end;

definition
let IT be CollProjectiveSpace;
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 );
end;

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

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
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;
cluster ProjectiveSpace V -> Fanoian Desarguesian Pappian ;
coherence
( ProjectiveSpace V is Fanoian & ProjectiveSpace V is Desarguesian & ProjectiveSpace V is Pappian ) by Lm39, Lm40, Lm41;
end;

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 ) ) )
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 )
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 )
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 ) ) )
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 )
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 )
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 )
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 )
proof end;

registration
cluster non empty strict reflexive transitive proper Vebleian at_least_3rank Fanoian Desarguesian Pappian 2-dimensional for CollStr ;
existence
ex b1 being CollProjectiveSpace st
( b1 is strict & b1 is Fanoian & b1 is Desarguesian & b1 is Pappian & b1 is 2-dimensional )
proof end;
cluster non empty strict reflexive transitive proper Vebleian at_least_3rank Fanoian Desarguesian Pappian up-3-dimensional at_most-3-dimensional for CollStr ;
existence
ex b1 being CollProjectiveSpace st
( b1 is strict & b1 is Fanoian & b1 is Desarguesian & b1 is Pappian & b1 is at_most-3-dimensional & b1 is up-3-dimensional )
proof end;
end;

definition
mode CollProjectivePlane is 2-dimensional CollProjectiveSpace;
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 ) ) ) )
proof end;