let V be non trivial RealLinearSpace; :: thesis: ( 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 ) implies ex CS being CollProjectiveSpace st
( CS = ProjectiveSpace V & not CS is 2-dimensional ) )
given u, v, u1, v1 being Element of V such that A1:
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 )
; :: thesis: ex CS being CollProjectiveSpace st
( CS = ProjectiveSpace V & not CS is 2-dimensional )
A2:
( not u is zero & not v is zero & not u1 is zero & not v1 is zero )
by A1, Th2;
V is up-3-dimensional
by A1, Lm43;
then reconsider CS = ProjectiveSpace V as CollProjectiveSpace ;
take
CS
; :: thesis: ( CS = ProjectiveSpace V & not CS is 2-dimensional )
thus
CS = ProjectiveSpace V
; :: thesis: not CS is 2-dimensional
reconsider p = Dir u, p1 = Dir v, q = Dir u1, q1 = Dir v1 as Element of CS by A2, ANPROJ_1:42;
take
p
; :: according to ANPROJ_2:def 14 :: thesis: ex p1, q, q1 being Element of CS st
for r being Element of CS holds
( not p,p1,r is_collinear or not q,q1,r is_collinear )
take
p1
; :: thesis: ex q, q1 being Element of CS st
for r being Element of CS holds
( not p,p1,r is_collinear or not q,q1,r is_collinear )
take
q
; :: thesis: ex q1 being Element of CS st
for r being Element of CS holds
( not p,p1,r is_collinear or not q,q1,r is_collinear )
take
q1
; :: thesis: for r being Element of CS holds
( not p,p1,r is_collinear or not q,q1,r is_collinear )
thus
for r being Element of CS holds
( not p,p1,r is_collinear or not q,q1,r is_collinear )
:: thesis: verumproof
assume
ex
r being
Element of
CS st
(
p,
p1,
r is_collinear &
q,
q1,
r is_collinear )
;
:: thesis: contradiction
then consider r being
Element of
CS such that A3:
(
p,
p1,
r is_collinear &
q,
q1,
r is_collinear )
;
A4:
(
[p,p1,r] in the
Collinearity of
(ProjectiveSpace V) &
[q,q1,r] in the
Collinearity of
(ProjectiveSpace V) )
by A3, COLLSP:def 2;
consider y being
Element of
V such that A5:
( not
y is
zero &
r = Dir y )
by ANPROJ_1:42;
(
u,
v,
y are_LinDep &
u1,
v1,
y are_LinDep )
by A2, A4, A5, ANPROJ_1:41;
hence
contradiction
by A1, A5, Th5;
:: thesis: verum
end;