:: ANPROJ_1 semantic presentation

begin


definition
let V be RealLinearSpace;
let p, q be Element of V;
pred are_Prop p,q means :Def1: :: ANPROJ_1:def 1
 ex a, b being Real st
( a * p = b * q & a <> 0 & b <> 0 );
reflexivity
 for p being Element of V ex a, b being Real st
( a * p = b * p & a <> 0 & b <> 0 )
proof
let p be Element of V; ::_thesis: ex a, b being Real st
( a * p = b * p & a <> 0 & b <> 0 )
 1 * p = 1 * p ;
hence  ex a, b being Real st
( a * p = b * p & a <> 0 & b <> 0 ) ; ::_thesis: verum
end;
symmetry
 for p, q being Element of V st ex a, b being Real st
( a * p = b * q & a <> 0 & b <> 0 ) holds
ex a, b being Real st
( a * q = b * p & a <> 0 & b <> 0 ) ;
end;

:: deftheorem Def1 defines are_Prop ANPROJ_1:def_1_:_
 for V being RealLinearSpace
for p, q being Element of V holds
( are_Prop p,q iff ex a, b being Real st
( a * p = b * q & a <> 0 & b <> 0 ) );

theorem Th1: :: ANPROJ_1:1
for V being RealLinearSpace
for p, q being Element of V holds
( are_Prop p,q iff ex a being Real st
( a <> 0 & p = a * q ) )
proof
let V be RealLinearSpace; ::_thesis: for p, q being Element of V holds
( are_Prop p,q iff ex a being Real st
( a <> 0 & p = a * q ) )
let p, q be Element of V; ::_thesis: ( are_Prop p,q iff ex a being Real st
( a <> 0 & p = a * q ) )
A1: now__::_thesis:_(_are_Prop_p,q_implies_ex_a_being_Real_st_
(_a_<>_0_&_p_=_a_*_q_)_)
assume  are_Prop p,q ; ::_thesis: ex a being Real st
( a <> 0 & p = a * q )
then consider a, b being Real such that
A2: a * p = b * q and
A3: a <> 0 and
A4: b <> 0 by Def1;
A5: a " <> 0 by A3, XCMPLX_1:202;
p = 1 * p by RLVECT_1:def_8
.= ((a ") * a) * p by A3, XCMPLX_0:def_7
.= (a ") * (b * q) by A2, RLVECT_1:def_7
.= ((a ") * b) * q by RLVECT_1:def_7 ;
hence  ex a being Real st
( a <> 0 & p = a * q ) by A4, A5, XCMPLX_1:6; ::_thesis: verum
end;
now__::_thesis:_(_ex_a_being_Real_st_
(_a_<>_0_&_p_=_a_*_q_)_implies_are_Prop_p,q_)
given a being Real such that A6: a <> 0 and
A7: p = a * q ; ::_thesis: are_Prop p,q
 1 * p = a * q by A7, RLVECT_1:def_8;
hence  are_Prop p,q by A6, Def1; ::_thesis: verum
end;
hence  ( are_Prop p,q iff ex a being Real st
( a <> 0 & p = a * q ) ) by A1; ::_thesis: verum
end;

theorem Th2: :: ANPROJ_1:2
for V being RealLinearSpace
for p, u, q being Element of V st are_Prop p,u & are_Prop u,q holds
are_Prop p,q
proof
let V be RealLinearSpace; ::_thesis: for p, u, q being Element of V st are_Prop p,u & are_Prop u,q holds
are_Prop p,q
let p, u, q be Element of V; ::_thesis: ( are_Prop p,u & are_Prop u,q implies are_Prop p,q )
assume that
A1: are_Prop p,u and
A2: are_Prop u,q ; ::_thesis: are_Prop p,q
consider a, b being Real such that
A3: a * p = b * u and
A4: a <> 0 and
A5: b <> 0 by A1, Def1;
consider c, d being Real such that
A6: c * u = d * q and
A7: c <> 0 and
A8: d <> 0 by A2, Def1;
 b " <> 0 by A5, XCMPLX_1:202;
then  (b ") * a <> 0 by A4, XCMPLX_1:6;
then A9: c * ((b ") * a) <> 0 by A7, XCMPLX_1:6;
((b ") * a) * p = (b ") * (b * u) by A3, RLVECT_1:def_7
.= ((b ") * b) * u by RLVECT_1:def_7
.= 1 * u by A5, XCMPLX_0:def_7
.= u by RLVECT_1:def_8 ;
then  d * q = (c * ((b ") * a)) * p by A6, RLVECT_1:def_7;
hence  are_Prop p,q by A8, A9, Def1; ::_thesis: verum
end;

theorem Th3: :: ANPROJ_1:3
for V being RealLinearSpace
for p being Element of V holds
( are_Prop p, 0. V iff p = 0. V )
proof
let V be RealLinearSpace; ::_thesis: for p being Element of V holds
( are_Prop p, 0. V iff p = 0. V )
let p be Element of V; ::_thesis: ( are_Prop p, 0. V iff p = 0. V )
now__::_thesis:_(_are_Prop_p,_0._V_implies_p_=_0._V_)
assume  are_Prop p, 0. V ; ::_thesis: p = 0. V
then consider a, b being Real such that
A1: a * p = b * (0. V) and
A2: a <> 0 and
 b <> 0 by Def1;
 0. V = a * p by A1, RLVECT_1:10;
hence  p = 0. V by A2, RLVECT_1:11; ::_thesis: verum
end;
hence  ( are_Prop p, 0. V iff p = 0. V ) ; ::_thesis: verum
end;

definition
let V be RealLinearSpace;
let u, v, w be Element of V;
predu,v,w are_LinDep  means :Def2: :: ANPROJ_1:def 2
 ex a, b, c being Real st
( ((a * u) + (b * v)) + (c * w) = 0. V & ( a <> 0 or b <> 0 or c <> 0 ) );
end;

:: deftheorem Def2 defines are_LinDep ANPROJ_1:def_2_:_
 for V being RealLinearSpace
for u, v, w being Element of V holds
( u,v,w are_LinDep iff ex a, b, c being Real st
( ((a * u) + (b * v)) + (c * w) = 0. V & ( a <> 0 or b <> 0 or c <> 0 ) ) );

theorem Th4: :: ANPROJ_1:4
for V being RealLinearSpace
for u, u1, v, v1, w, w1 being Element of V st are_Prop u,u1 & are_Prop v,v1 & are_Prop w,w1 & u,v,w are_LinDep holds
u1,v1,w1 are_LinDep
proof
let V be RealLinearSpace; ::_thesis: for u, u1, v, v1, w, w1 being Element of V st are_Prop u,u1 & are_Prop v,v1 & are_Prop w,w1 & u,v,w are_LinDep holds
u1,v1,w1 are_LinDep
let u, u1, v, v1, w, w1 be Element of V; ::_thesis: ( are_Prop u,u1 & are_Prop v,v1 & are_Prop w,w1 & u,v,w are_LinDep implies u1,v1,w1 are_LinDep )
assume that
A1: are_Prop u,u1 and
A2: are_Prop v,v1 and
A3: are_Prop w,w1 and
A4: u,v,w are_LinDep ; ::_thesis: u1,v1,w1 are_LinDep
consider b being Real such that
A5: b <> 0 and
A6: v = b * v1 by A2, Th1;
consider a being Real such that
A7: a <> 0 and
A8: u = a * u1 by A1, Th1;
consider d1, d2, d3 being Real such that
A9: ((d1 * u) + (d2 * v)) + (d3 * w) = 0. V and
A10: ( d1 <> 0 or d2 <> 0 or d3 <> 0 ) by A4, Def2;
consider c being Real such that
A11: c <> 0 and
A12: w = c * w1 by A3, Th1;
A13: ( d1 * a <> 0 or d2 * b <> 0 or d3 * c <> 0 ) by A7, A5, A11, A10, XCMPLX_1:6;
0. V = (((d1 * a) * u1) + (d2 * (b * v1))) + (d3 * (c * w1)) by A8, A6, A12, A9, RLVECT_1:def_7
.= (((d1 * a) * u1) + ((d2 * b) * v1)) + (d3 * (c * w1)) by RLVECT_1:def_7
.= (((d1 * a) * u1) + ((d2 * b) * v1)) + ((d3 * c) * w1) by RLVECT_1:def_7 ;
hence  u1,v1,w1 are_LinDep by A13, Def2; ::_thesis: verum
end;

theorem Th5: :: ANPROJ_1:5
for V being RealLinearSpace
for u, v, w being Element of V st u,v,w are_LinDep holds
( u,w,v are_LinDep & v,u,w are_LinDep & w,v,u are_LinDep & w,u,v are_LinDep & v,w,u are_LinDep )
proof
let V be RealLinearSpace; ::_thesis: for u, v, w being Element of V st u,v,w are_LinDep holds
( u,w,v are_LinDep & v,u,w are_LinDep & w,v,u are_LinDep & w,u,v are_LinDep & v,w,u are_LinDep )
let u, v, w be Element of V; ::_thesis: ( u,v,w are_LinDep implies ( u,w,v are_LinDep & v,u,w are_LinDep & w,v,u are_LinDep & w,u,v are_LinDep & v,w,u are_LinDep ) )
assume  u,v,w are_LinDep ; ::_thesis: ( u,w,v are_LinDep & v,u,w are_LinDep & w,v,u are_LinDep & w,u,v are_LinDep & v,w,u are_LinDep )
then consider a, b, c being Real such that
A1: ((a * u) + (b * v)) + (c * w) = 0. V and
A2: ( a <> 0 or b <> 0 or c <> 0 ) by Def2;
 ( ((a * u) + (c * w)) + (b * v) = 0. V & ((b * v) + (c * w)) + (a * u) = 0. V ) by A1, RLVECT_1:def_3;
hence  ( u,w,v are_LinDep & v,u,w are_LinDep & w,v,u are_LinDep & w,u,v are_LinDep & v,w,u are_LinDep ) by A1, A2, Def2; ::_thesis: verum
end;

Lm1:  for V being RealLinearSpace
for v, w being Element of V
for a, b being Real st (a * v) + (b * w) = 0. V holds
a * v = (- b) * w
proof
let V be RealLinearSpace; ::_thesis: for v, w being Element of V
for a, b being Real st (a * v) + (b * w) = 0. V holds
a * v = (- b) * w
let v, w be Element of V; ::_thesis: for a, b being Real st (a * v) + (b * w) = 0. V holds
a * v = (- b) * w
let a, b be Real; ::_thesis: ( (a * v) + (b * w) = 0. V implies a * v = (- b) * w )
assume  (a * v) + (b * w) = 0. V ; ::_thesis: a * v = (- b) * w
then a * v = - (b * w) by RLVECT_1:6
.= b * (- w) by RLVECT_1:25 ;
hence  a * v = (- b) * w by RLVECT_1:24; ::_thesis: verum
end;

Lm2:  for V being RealLinearSpace
for u, v, w being Element of V
for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V & a <> 0 holds
u = ((- ((a ") * b)) * v) + ((- ((a ") * c)) * w)
proof
let V be RealLinearSpace; ::_thesis: for u, v, w being Element of V
for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V & a <> 0 holds
u = ((- ((a ") * b)) * v) + ((- ((a ") * c)) * w)
let u, v, w be Element of V; ::_thesis: for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V & a <> 0 holds
u = ((- ((a ") * b)) * v) + ((- ((a ") * c)) * w)
let a, b, c be Real; ::_thesis: ( ((a * u) + (b * v)) + (c * w) = 0. V & a <> 0 implies u = ((- ((a ") * b)) * v) + ((- ((a ") * c)) * w) )
assume that
A1: ((a * u) + (b * v)) + (c * w) = 0. V and
A2: a <> 0 ; ::_thesis: u = ((- ((a ") * b)) * v) + ((- ((a ") * c)) * w)
 ((a * u) + (b * v)) + (c * w) = (a * u) + ((b * v) + (c * w)) by RLVECT_1:def_3;
then a * u = - ((b * v) + (c * w)) by A1, RLVECT_1:6
.= (- (b * v)) + (- (c * w)) by RLVECT_1:31
.= (b * (- v)) + (- (c * w)) by RLVECT_1:25
.= (b * (- v)) + (c * (- w)) by RLVECT_1:25
.= ((- b) * v) + (c * (- w)) by RLVECT_1:24
.= ((- b) * v) + ((- c) * w) by RLVECT_1:24 ;
hence u = (a ") * (((- b) * v) + ((- c) * w)) by A2, ANALOAF:5
.= ((a ") * ((- b) * v)) + ((a ") * ((- c) * w)) by RLVECT_1:def_5
.= (((a ") * (- b)) * v) + ((a ") * ((- c) * w)) by RLVECT_1:def_7
.= ((- ((a ") * b)) * v) + (((a ") * (- c)) * w) by RLVECT_1:def_7
.= ((- ((a ") * b)) * v) + ((- ((a ") * c)) * w) ;
::_thesis: verum
end;

theorem Th6: :: ANPROJ_1:6
for V being RealLinearSpace
for v, w, u being Element of V st not v is zero & not w is zero & not are_Prop v,w holds
( v,w,u are_LinDep iff ex a, b being Real st u = (a * v) + (b * w) )
proof
let V be RealLinearSpace; ::_thesis: for v, w, u being Element of V st not v is zero & not w is zero & not are_Prop v,w holds
( v,w,u are_LinDep iff ex a, b being Real st u = (a * v) + (b * w) )
let v, w, u be Element of V; ::_thesis: ( not v is zero & not w is zero & not are_Prop v,w implies ( v,w,u are_LinDep iff ex a, b being Real st u = (a * v) + (b * w) ) )
assume that
A1: not v is zero and
A2: not w is zero and
A3: not are_Prop v,w ; ::_thesis: ( v,w,u are_LinDep iff ex a, b being Real st u = (a * v) + (b * w) )
A4: w <> 0. V by A2;
A5: v <> 0. V by A1;
A6: ( v,w,u are_LinDep implies ex a, b being Real st u = (a * v) + (b * w) )
proof
assume  v,w,u are_LinDep ; ::_thesis: ex a, b being Real st u = (a * v) + (b * w)
then  u,v,w are_LinDep by Th5;
then consider a, b, c being Real such that
A7: ((a * u) + (b * v)) + (c * w) = 0. V and
A8: ( a <> 0 or b <> 0 or c <> 0 ) by Def2;
 a <> 0
proof
assume A9: a = 0 ; ::_thesis: contradiction
then A10: 0. V = ((0. V) + (b * v)) + (c * w) by A7, RLVECT_1:10
.= (b * v) + (c * w) by RLVECT_1:4 ;
A11: b <> 0
proof
assume A12: b = 0 ; ::_thesis: contradiction
then  0. V = (0. V) + (c * w) by A10, RLVECT_1:10
.= c * w by RLVECT_1:4 ;
hence  contradiction by A4, A8, A9, A12, RLVECT_1:11; ::_thesis: verum
end;
A13: c <> 0
proof
assume A14: c = 0 ; ::_thesis: contradiction
then  0. V = (b * v) + (0. V) by A10, RLVECT_1:10
.= b * v by RLVECT_1:4 ;
hence  contradiction by A5, A8, A9, A14, RLVECT_1:11; ::_thesis: verum
end;
 b * v = (- c) * w by A10, Lm1;
then  ( b = 0 or - c = 0 ) by A3, Def1;
hence  contradiction by A11, A13; ::_thesis: verum
end;
then  u = ((- ((a ") * b)) * v) + ((- ((a ") * c)) * w) by A7, Lm2;
hence  ex a, b being Real st u = (a * v) + (b * w) ; ::_thesis: verum
end;
 ( ex a, b being Real st u = (a * v) + (b * w) implies v,w,u are_LinDep )
proof
given a, b being Real such that A15: u = (a * v) + (b * w) ; ::_thesis: v,w,u are_LinDep
0. V = ((a * v) + (b * w)) + (- u) by A15, RLVECT_1:5
.= ((a * v) + (b * w)) + ((- 1) * u) by RLVECT_1:16 ;
hence  v,w,u are_LinDep by Def2; ::_thesis: verum
end;
hence  ( v,w,u are_LinDep iff ex a, b being Real st u = (a * v) + (b * w) ) by A6; ::_thesis: verum
end;

Lm3:  for V being RealLinearSpace
for p being Element of V
for a, b, c being Real holds ((a + b) + c) * p = ((a * p) + (b * p)) + (c * p)
proof
let V be RealLinearSpace; ::_thesis: for p being Element of V
for a, b, c being Real holds ((a + b) + c) * p = ((a * p) + (b * p)) + (c * p)
let p be Element of V; ::_thesis: for a, b, c being Real holds ((a + b) + c) * p = ((a * p) + (b * p)) + (c * p)
let a, b, c be Real; ::_thesis: ((a + b) + c) * p = ((a * p) + (b * p)) + (c * p)
thus ((a + b) + c) * p = ((a + b) * p) + (c * p) by RLVECT_1:def_6
.= ((a * p) + (b * p)) + (c * p) by RLVECT_1:def_6 ; ::_thesis: verum
end;

Lm4:  for V being RealLinearSpace
for u, v, w, u1, v1, w1 being Element of V holds ((u + v) + w) + ((u1 + v1) + w1) = ((u + u1) + (v + v1)) + (w + w1)
proof
let V be RealLinearSpace; ::_thesis: for u, v, w, u1, v1, w1 being Element of V holds ((u + v) + w) + ((u1 + v1) + w1) = ((u + u1) + (v + v1)) + (w + w1)
let u, v, w, u1, v1, w1 be Element of V; ::_thesis: ((u + v) + w) + ((u1 + v1) + w1) = ((u + u1) + (v + v1)) + (w + w1)
thus ((u + u1) + (v + v1)) + (w + w1) = (u1 + (u + (v + v1))) + (w + w1) by RLVECT_1:def_3
.= (u1 + (v1 + (u + v))) + (w + w1) by RLVECT_1:def_3
.= ((u1 + v1) + (u + v)) + (w + w1) by RLVECT_1:def_3
.= (u1 + v1) + ((u + v) + (w + w1)) by RLVECT_1:def_3
.= (u1 + v1) + (w1 + ((u + v) + w)) by RLVECT_1:def_3
.= ((u + v) + w) + ((u1 + v1) + w1) by RLVECT_1:def_3 ; ::_thesis: verum
end;

Lm5:  for V being RealLinearSpace
for p, q being Element of V
for a, a1, b1 being Real holds ((a * a1) * p) + ((a * b1) * q) = a * ((a1 * p) + (b1 * q))
proof
let V be RealLinearSpace; ::_thesis: for p, q being Element of V
for a, a1, b1 being Real holds ((a * a1) * p) + ((a * b1) * q) = a * ((a1 * p) + (b1 * q))
let p, q be Element of V; ::_thesis: for a, a1, b1 being Real holds ((a * a1) * p) + ((a * b1) * q) = a * ((a1 * p) + (b1 * q))
let a, a1, b1 be Real; ::_thesis: ((a * a1) * p) + ((a * b1) * q) = a * ((a1 * p) + (b1 * q))
thus ((a * a1) * p) + ((a * b1) * q) = (a * (a1 * p)) + ((a * b1) * q) by RLVECT_1:def_7
.= (a * (a1 * p)) + (a * (b1 * q)) by RLVECT_1:def_7
.= a * ((a1 * p) + (b1 * q)) by RLVECT_1:def_5 ; ::_thesis: verum
end;

theorem :: ANPROJ_1:7
for V being RealLinearSpace
for p, q being Element of V
for a1, b1, a2, b2 being Real st not are_Prop p,q & (a1 * p) + (b1 * q) = (a2 * p) + (b2 * q) & not p is zero & not q is zero holds
( a1 = a2 & b1 = b2 )
proof
let V be RealLinearSpace; ::_thesis: for p, q being Element of V
for a1, b1, a2, b2 being Real st not are_Prop p,q & (a1 * p) + (b1 * q) = (a2 * p) + (b2 * q) & not p is zero & not q is zero holds
( a1 = a2 & b1 = b2 )
let p, q be Element of V; ::_thesis: for a1, b1, a2, b2 being Real st not are_Prop p,q & (a1 * p) + (b1 * q) = (a2 * p) + (b2 * q) & not p is zero & not q is zero holds
( a1 = a2 & b1 = b2 )
let a1, b1, a2, b2 be Real; ::_thesis: ( not are_Prop p,q & (a1 * p) + (b1 * q) = (a2 * p) + (b2 * q) & not p is zero & not q is zero implies ( a1 = a2 & b1 = b2 ) )
assume that
A1: not are_Prop p,q and
A2: (a1 * p) + (b1 * q) = (a2 * p) + (b2 * q) and
A3: not p is zero and
A4: not q is zero ; ::_thesis: ( a1 = a2 & b1 = b2 )
((a2 * p) + (b2 * q)) + (- (b1 * q)) = (a1 * p) + ((b1 * q) + (- (b1 * q))) by A2, RLVECT_1:def_3
.= (a1 * p) + (0. V) by RLVECT_1:5
.= a1 * p by RLVECT_1:4 ;
then a1 * p = ((b2 * q) + (- (b1 * q))) + (a2 * p) by RLVECT_1:def_3
.= ((b2 * q) - (b1 * q)) + (a2 * p) by RLVECT_1:def_11
.= ((b2 - b1) * q) + (a2 * p) by RLVECT_1:35 ;
then (a1 * p) + (- (a2 * p)) = ((b2 - b1) * q) + ((a2 * p) + (- (a2 * p))) by RLVECT_1:def_3
.= ((b2 - b1) * q) + (0. V) by RLVECT_1:5
.= (b2 - b1) * q by RLVECT_1:4 ;
then A5: (b2 - b1) * q = (a1 * p) - (a2 * p) by RLVECT_1:def_11
.= (a1 - a2) * p by RLVECT_1:35 ;
A6: q <> 0. V by A4;
A7: now__::_thesis:_(_a1_-_a2_=_0_implies_(_a1_=_a2_&_b1_=_b2_)_)
assume A8: a1 - a2 = 0 ; ::_thesis: ( a1 = a2 & b1 = b2 )
then  (b2 - b1) * q = 0. V by A5, RLVECT_1:10;
then  b2 - b1 = 0 by A6, RLVECT_1:11;
hence  ( a1 = a2 & b1 = b2 ) by A8; ::_thesis: verum
end;
A9: p <> 0. V by A3;
now__::_thesis:_(_b2_-_b1_=_0_implies_(_a1_=_a2_&_b1_=_b2_)_)
assume A10: b2 - b1 = 0 ; ::_thesis: ( a1 = a2 & b1 = b2 )
then  (a1 - a2) * p = 0. V by A5, RLVECT_1:10;
then  a1 - a2 = 0 by A9, RLVECT_1:11;
hence  ( a1 = a2 & b1 = b2 ) by A10; ::_thesis: verum
end;
hence  ( a1 = a2 & b1 = b2 ) by A1, A5, A7, Def1; ::_thesis: verum
end;

Lm6:  for V being RealLinearSpace
for p, v, q being Element of V
for a, b being Real st p + (a * v) = q + (b * v) holds
((a - b) * v) + p = q
proof
let V be RealLinearSpace; ::_thesis: for p, v, q being Element of V
for a, b being Real st p + (a * v) = q + (b * v) holds
((a - b) * v) + p = q
let p, v, q be Element of V; ::_thesis: for a, b being Real st p + (a * v) = q + (b * v) holds
((a - b) * v) + p = q
let a, b be Real; ::_thesis: ( p + (a * v) = q + (b * v) implies ((a - b) * v) + p = q )
assume  p + (a * v) = q + (b * v) ; ::_thesis: ((a - b) * v) + p = q
then (p + (a * v)) + (- (b * v)) = q + ((b * v) + (- (b * v))) by RLVECT_1:def_3
.= q + (0. V) by RLVECT_1:5
.= q by RLVECT_1:4 ;
then q = p + ((a * v) + (- (b * v))) by RLVECT_1:def_3
.= p + ((a * v) - (b * v)) by RLVECT_1:def_11
.= p + ((a - b) * v) by RLVECT_1:35 ;
hence  ((a - b) * v) + p = q ; ::_thesis: verum
end;

theorem :: ANPROJ_1:8
for V being RealLinearSpace
for u, v, w being Element of V
for a1, b1, c1, a2, b2, c2 being Real st not u,v,w are_LinDep & ((a1 * u) + (b1 * v)) + (c1 * w) = ((a2 * u) + (b2 * v)) + (c2 * w) holds
( a1 = a2 & b1 = b2 & c1 = c2 )
proof
let V be RealLinearSpace; ::_thesis: for u, v, w being Element of V
for a1, b1, c1, a2, b2, c2 being Real st not u,v,w are_LinDep & ((a1 * u) + (b1 * v)) + (c1 * w) = ((a2 * u) + (b2 * v)) + (c2 * w) holds
( a1 = a2 & b1 = b2 & c1 = c2 )
let u, v, w be Element of V; ::_thesis: for a1, b1, c1, a2, b2, c2 being Real st not u,v,w are_LinDep & ((a1 * u) + (b1 * v)) + (c1 * w) = ((a2 * u) + (b2 * v)) + (c2 * w) holds
( a1 = a2 & b1 = b2 & c1 = c2 )
let a1, b1, c1, a2, b2, c2 be Real; ::_thesis: ( not u,v,w are_LinDep & ((a1 * u) + (b1 * v)) + (c1 * w) = ((a2 * u) + (b2 * v)) + (c2 * w) implies ( a1 = a2 & b1 = b2 & c1 = c2 ) )
A1: ( ((a1 * u) + (b1 * v)) + (c1 * w) = ((a2 * u) + (b2 * v)) + (c2 * w) implies (((a1 - a2) * u) + ((b1 - b2) * v)) + ((c1 - c2) * w) = 0. V )
proof
assume  ((a1 * u) + (b1 * v)) + (c1 * w) = ((a2 * u) + (b2 * v)) + (c2 * w) ; ::_thesis: (((a1 - a2) * u) + ((b1 - b2) * v)) + ((c1 - c2) * w) = 0. V
then  ((c1 - c2) * w) + ((a1 * u) + (b1 * v)) = (a2 * u) + (b2 * v) by Lm6;
then  (((c1 - c2) * w) + (a1 * u)) + (b1 * v) = (a2 * u) + (b2 * v) by RLVECT_1:def_3;
then  ((b1 - b2) * v) + (((c1 - c2) * w) + (a1 * u)) = a2 * u by Lm6;
then  (((b1 - b2) * v) + ((c1 - c2) * w)) + (a1 * u) = a2 * u by RLVECT_1:def_3;
then  (((b1 - b2) * v) + ((c1 - c2) * w)) + (a1 * u) = (0. V) + (a2 * u) by RLVECT_1:4;
then  ((a1 - a2) * u) + (((b1 - b2) * v) + ((c1 - c2) * w)) = 0. V by Lm6;
hence  (((a1 - a2) * u) + ((b1 - b2) * v)) + ((c1 - c2) * w) = 0. V by RLVECT_1:def_3; ::_thesis: verum
end;
assume A2: ( not u,v,w are_LinDep & ((a1 * u) + (b1 * v)) + (c1 * w) = ((a2 * u) + (b2 * v)) + (c2 * w) ) ; ::_thesis: ( a1 = a2 & b1 = b2 & c1 = c2 )
then A3: c1 - c2 = 0 by A1, Def2;
 ( a1 - a2 = 0 & b1 - b2 = 0 ) by A2, A1, Def2;
hence  ( a1 = a2 & b1 = b2 & c1 = c2 ) by A3; ::_thesis: verum
end;

theorem Th9: :: ANPROJ_1:9
for V being RealLinearSpace
for p, q, u, v being Element of V
for a1, b1, a2, b2 being Real st not are_Prop p,q & u = (a1 * p) + (b1 * q) & v = (a2 * p) + (b2 * q) & (a1 * b2) - (a2 * b1) = 0 & not p is zero & not q is zero & not are_Prop u,v & not u = 0. V holds
v = 0. V
proof
let V be RealLinearSpace; ::_thesis: for p, q, u, v being Element of V
for a1, b1, a2, b2 being Real st not are_Prop p,q & u = (a1 * p) + (b1 * q) & v = (a2 * p) + (b2 * q) & (a1 * b2) - (a2 * b1) = 0 & not p is zero & not q is zero & not are_Prop u,v & not u = 0. V holds
v = 0. V
let p, q, u, v be Element of V; ::_thesis: for a1, b1, a2, b2 being Real st not are_Prop p,q & u = (a1 * p) + (b1 * q) & v = (a2 * p) + (b2 * q) & (a1 * b2) - (a2 * b1) = 0 & not p is zero & not q is zero & not are_Prop u,v & not u = 0. V holds
v = 0. V
let a1, b1, a2, b2 be Real; ::_thesis: ( not are_Prop p,q & u = (a1 * p) + (b1 * q) & v = (a2 * p) + (b2 * q) & (a1 * b2) - (a2 * b1) = 0 & not p is zero & not q is zero & not are_Prop u,v & not u = 0. V implies v = 0. V )
assume that
A1: not are_Prop p,q and
A2: u = (a1 * p) + (b1 * q) and
A3: v = (a2 * p) + (b2 * q) and
A4: (a1 * b2) - (a2 * b1) = 0 and
A5: ( not p is zero & not q is zero ) ; ::_thesis: ( are_Prop u,v or u = 0. V or v = 0. V )
now__::_thesis:_(_u_<>_0._V_&_v_<>_0._V_&_not_are_Prop_u,v_&_not_u_=_0._V_implies_v_=_0._V_)
assume that
 u <> 0. V and
 v <> 0. V ; ::_thesis: ( are_Prop u,v or u = 0. V or v = 0. V )
A6: for p, q, u, v being Element of V
for a1, a2, b1, b2 being Real st not are_Prop p,q & u = (a1 * p) + (b1 * q) & v = (a2 * p) + (b2 * q) & (a1 * b2) - (a2 * b1) = 0 & not p is zero & not q is zero & a1 = 0 & u <> 0. V & v <> 0. V holds
are_Prop u,v
proof
let p, q, u, v be Element of V; ::_thesis: for a1, a2, b1, b2 being Real st not are_Prop p,q & u = (a1 * p) + (b1 * q) & v = (a2 * p) + (b2 * q) & (a1 * b2) - (a2 * b1) = 0 & not p is zero & not q is zero & a1 = 0 & u <> 0. V & v <> 0. V holds
are_Prop u,v
let a1, a2, b1, b2 be Real; ::_thesis: ( not are_Prop p,q & u = (a1 * p) + (b1 * q) & v = (a2 * p) + (b2 * q) & (a1 * b2) - (a2 * b1) = 0 & not p is zero & not q is zero & a1 = 0 & u <> 0. V & v <> 0. V implies are_Prop u,v )
assume that
 not are_Prop p,q and
A7: u = (a1 * p) + (b1 * q) and
A8: v = (a2 * p) + (b2 * q) and
A9: (a1 * b2) - (a2 * b1) = 0 and
 not p is zero and
 not q is zero and
A10: a1 = 0 and
A11: u <> 0. V and
A12: v <> 0. V ; ::_thesis: are_Prop u,v
 0 = (- a2) * b1 by A9, A10;
then A13: ( - a2 = 0 or b1 = 0 ) by XCMPLX_1:6;
A14: now__::_thesis:_not_b1_=_0
assume  b1 = 0 ; ::_thesis: contradiction
then u = (0. V) + (0 * q) by A7, A10, RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10 ;
hence  contradiction by A11, RLVECT_1:4; ::_thesis: verum
end;
then A15: b1 " <> 0 by XCMPLX_1:202;
A16: now__::_thesis:_not_b2_*_(b1_")_=_0
assume  b2 * (b1 ") = 0 ; ::_thesis: contradiction
then  b2 = 0 by A15, XCMPLX_1:6;
then v = (0. V) + (0 * q) by A8, A13, A14, RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10 ;
hence  contradiction by A12, RLVECT_1:4; ::_thesis: verum
end;
 u = (0. V) + (b1 * q) by A7, A10, RLVECT_1:10;
then A17: u = b1 * q by RLVECT_1:4;
 v = (0. V) + (b2 * q) by A8, A13, A14, RLVECT_1:10;
then  v = b2 * q by RLVECT_1:4;
then  v = b2 * ((b1 ") * u) by A14, A17, ANALOAF:5;
then  v = (b2 * (b1 ")) * u by RLVECT_1:def_7;
then  1 * v = (b2 * (b1 ")) * u by RLVECT_1:def_8;
hence  are_Prop u,v by A16, Def1; ::_thesis: verum
end;
now__::_thesis:_(_a1_<>_0_&_a2_<>_0_&_not_are_Prop_u,v_&_not_u_=_0._V_implies_v_=_0._V_)
assume that
A18: a1 <> 0 and
A19: a2 <> 0 ; ::_thesis: ( are_Prop u,v or u = 0. V or v = 0. V )
A20: now__::_thesis:_(_b1_=_0_implies_are_Prop_u,v_)
 a1 " <> 0 by A18, XCMPLX_1:202;
then A21: a2 * (a1 ") <> 0 by A19, XCMPLX_1:6;
assume A22: b1 = 0 ; ::_thesis: are_Prop u,v
then  b2 = 0 by A4, A18, XCMPLX_1:6;
then  v = (a2 * p) + (0. V) by A3, RLVECT_1:10;
then A23: v = a2 * p by RLVECT_1:4;
 u = (a1 * p) + (0. V) by A2, A22, RLVECT_1:10;
then  u = a1 * p by RLVECT_1:4;
then v = a2 * ((a1 ") * u) by A18, A23, ANALOAF:5
.= (a2 * (a1 ")) * u by RLVECT_1:def_7 ;
then  1 * v = (a2 * (a1 ")) * u by RLVECT_1:def_8;
hence  are_Prop u,v by A21, Def1; ::_thesis: verum
end;
now__::_thesis:_(_b1_<>_0_implies_are_Prop_u,v_)
A24: ( b2 * u = ((a1 * b2) * p) + ((b2 * b1) * q) & b1 * v = ((a2 * b1) * p) + ((b1 * b2) * q) ) by A2, A3, Lm5;
assume A25: b1 <> 0 ; ::_thesis: are_Prop u,v
then  b2 <> 0 by A4, A19, XCMPLX_1:6;
hence  are_Prop u,v by A4, A25, A24, Def1; ::_thesis: verum
end;
hence  ( are_Prop u,v or u = 0. V or v = 0. V ) by A20; ::_thesis: verum
end;
hence  ( are_Prop u,v or u = 0. V or v = 0. V ) by A1, A2, A3, A4, A5, A6; ::_thesis: verum
end;
hence  ( are_Prop u,v or u = 0. V or v = 0. V ) ; ::_thesis: verum
end;

theorem Th10: :: ANPROJ_1:10
for V being RealLinearSpace
for u, v, w being Element of V st ( u = 0. V or v = 0. V or w = 0. V ) holds
u,v,w are_LinDep
proof
let V be RealLinearSpace; ::_thesis: for u, v, w being Element of V st ( u = 0. V or v = 0. V or w = 0. V ) holds
u,v,w are_LinDep
let u, v, w be Element of V; ::_thesis: ( ( u = 0. V or v = 0. V or w = 0. V ) implies u,v,w are_LinDep )
A1: for u, v, w being Element of V st u = 0. V holds
u,v,w are_LinDep
proof
let u, v, w be Element of V; ::_thesis: ( u = 0. V implies u,v,w are_LinDep )
assume A2: u = 0. V ; ::_thesis: u,v,w are_LinDep
0. V = (0. V) + (0. V) by RLVECT_1:4
.= (1 * u) + (0. V) by A2, RLVECT_1:10
.= (1 * u) + (0 * v) by RLVECT_1:10
.= ((1 * u) + (0 * v)) + (0. V) by RLVECT_1:4
.= ((1 * u) + (0 * v)) + (0 * w) by RLVECT_1:10 ;
hence  u,v,w are_LinDep by Def2; ::_thesis: verum
end;
A3: now__::_thesis:_(_v_=_0._V_&_(_u_=_0._V_or_v_=_0._V_or_w_=_0._V_)_implies_u,v,w_are_LinDep_)
assume  v = 0. V ; ::_thesis: ( ( u = 0. V or v = 0. V or w = 0. V ) implies u,v,w are_LinDep )
then  v,w,u are_LinDep by A1;
hence  ( ( u = 0. V or v = 0. V or w = 0. V ) implies u,v,w are_LinDep ) by Th5; ::_thesis: verum
end;
A4: now__::_thesis:_(_w_=_0._V_&_(_u_=_0._V_or_v_=_0._V_or_w_=_0._V_)_implies_u,v,w_are_LinDep_)
assume  w = 0. V ; ::_thesis: ( ( u = 0. V or v = 0. V or w = 0. V ) implies u,v,w are_LinDep )
then  w,u,v are_LinDep by A1;
hence  ( ( u = 0. V or v = 0. V or w = 0. V ) implies u,v,w are_LinDep ) by Th5; ::_thesis: verum
end;
assume  ( u = 0. V or v = 0. V or w = 0. V ) ; ::_thesis: u,v,w are_LinDep
hence  u,v,w are_LinDep by A1, A3, A4; ::_thesis: verum
end;

theorem Th11: :: ANPROJ_1:11
for V being RealLinearSpace
for u, v, w being Element of V st ( are_Prop u,v or are_Prop w,u or are_Prop v,w ) holds
w,u,v are_LinDep
proof
let V be RealLinearSpace; ::_thesis: for u, v, w being Element of V st ( are_Prop u,v or are_Prop w,u or are_Prop v,w ) holds
w,u,v are_LinDep
let u, v, w be Element of V; ::_thesis: ( ( are_Prop u,v or are_Prop w,u or are_Prop v,w ) implies w,u,v are_LinDep )
A1: for u, v, w being Element of V st are_Prop u,v holds
w,u,v are_LinDep
proof
let u, v, w be Element of V; ::_thesis: ( are_Prop u,v implies w,u,v are_LinDep )
A2: 0 * w = 0. V by RLVECT_1:10;
assume  are_Prop u,v ; ::_thesis: w,u,v are_LinDep
then consider a, b being Real such that
A3: a * u = b * v and
A4: a <> 0 and
 b <> 0 by Def1;
0. V = (a * u) + (- (b * v)) by A3, RLVECT_1:5
.= (a * u) + ((- 1) * (b * v)) by RLVECT_1:16
.= (a * u) + (((- 1) * b) * v) by RLVECT_1:def_7 ;
then  0. V = ((0 * w) + (a * u)) + (((- 1) * b) * v) by A2, RLVECT_1:4;
hence  w,u,v are_LinDep by A4, Def2; ::_thesis: verum
end;
A5: now__::_thesis:_(_are_Prop_w,u_&_(_are_Prop_u,v_or_are_Prop_w,u_or_are_Prop_v,w_)_implies_w,u,v_are_LinDep_)
assume  are_Prop w,u ; ::_thesis: ( ( are_Prop u,v or are_Prop w,u or are_Prop v,w ) implies w,u,v are_LinDep )
then  v,w,u are_LinDep by A1;
hence  ( ( are_Prop u,v or are_Prop w,u or are_Prop v,w ) implies w,u,v are_LinDep ) by Th5; ::_thesis: verum
end;
A6: now__::_thesis:_(_are_Prop_v,w_&_(_are_Prop_u,v_or_are_Prop_w,u_or_are_Prop_v,w_)_implies_w,u,v_are_LinDep_)
assume  are_Prop v,w ; ::_thesis: ( ( are_Prop u,v or are_Prop w,u or are_Prop v,w ) implies w,u,v are_LinDep )
then  u,v,w are_LinDep by A1;
hence  ( ( are_Prop u,v or are_Prop w,u or are_Prop v,w ) implies w,u,v are_LinDep ) by Th5; ::_thesis: verum
end;
assume  ( are_Prop u,v or are_Prop w,u or are_Prop v,w ) ; ::_thesis: w,u,v are_LinDep
hence  w,u,v are_LinDep by A1, A5, A6; ::_thesis: verum
end;

theorem Th12: :: ANPROJ_1:12
for V being RealLinearSpace
for u, v, w being Element of V st not u,v,w are_LinDep holds
( not u is zero & not v is zero & not w is zero & not are_Prop u,v & not are_Prop v,w & not are_Prop w,u )
proof
let V be RealLinearSpace; ::_thesis: for u, v, w being Element of V st not u,v,w are_LinDep holds
( not u is zero & not v is zero & not w is zero & not are_Prop u,v & not are_Prop v,w & not are_Prop w,u )
let u, v, w be Element of V; ::_thesis: ( not u,v,w are_LinDep implies ( not u is zero & not v is zero & not w is zero & not are_Prop u,v & not are_Prop v,w & not are_Prop w,u ) )
assume A1: not u,v,w are_LinDep ; ::_thesis: ( not u is zero & not v is zero & not w is zero & not are_Prop u,v & not are_Prop v,w & not are_Prop w,u )
then A2: w <> 0. V by Th10;
 ( u <> 0. V & v <> 0. V ) by A1, Th10;
hence  ( not u is zero & not v is zero & not w is zero ) by A2, STRUCT_0:def_12; ::_thesis: ( not are_Prop u,v & not are_Prop v,w & not are_Prop w,u )
thus  ( not are_Prop u,v & not are_Prop v,w & not are_Prop w,u ) by A1, Th11; ::_thesis: verum
end;

theorem Th13: :: ANPROJ_1:13
for V being RealLinearSpace
for p, q being Element of V st p + q = 0. V holds
are_Prop p,q
proof
let V be RealLinearSpace; ::_thesis: for p, q being Element of V st p + q = 0. V holds
are_Prop p,q
let p, q be Element of V; ::_thesis: ( p + q = 0. V implies are_Prop p,q )
assume  p + q = 0. V ; ::_thesis: are_Prop p,q
then  q = - p by RLVECT_1:def_10;
then  q = (- 1) * p by RLVECT_1:16;
hence  are_Prop p,q by Th1; ::_thesis: verum
end;

theorem Th14: :: ANPROJ_1:14
for V being RealLinearSpace
for p, q, u, v, w being Element of V st not are_Prop p,q & p,q,u are_LinDep & p,q,v are_LinDep & p,q,w are_LinDep & not p is zero & not q is zero holds
u,v,w are_LinDep
proof
let V be RealLinearSpace; ::_thesis: for p, q, u, v, w being Element of V st not are_Prop p,q & p,q,u are_LinDep & p,q,v are_LinDep & p,q,w are_LinDep & not p is zero & not q is zero holds
u,v,w are_LinDep
let p, q, u, v, w be Element of V; ::_thesis: ( not are_Prop p,q & p,q,u are_LinDep & p,q,v are_LinDep & p,q,w are_LinDep & not p is zero & not q is zero implies u,v,w are_LinDep )
assume that
A1: not are_Prop p,q and
A2: p,q,u are_LinDep and
A3: p,q,v are_LinDep and
A4: p,q,w are_LinDep and
A5: ( not p is zero & not q is zero ) ; ::_thesis: u,v,w are_LinDep
consider a1, b1 being Real such that
A6: u = (a1 * p) + (b1 * q) by A1, A2, A5, Th6;
consider a3, b3 being Real such that
A7: w = (a3 * p) + (b3 * q) by A1, A4, A5, Th6;
consider a2, b2 being Real such that
A8: v = (a2 * p) + (b2 * q) by A1, A3, A5, Th6;
set a = (a2 * b3) - (a3 * b2);
set b = (- (a1 * b3)) + (a3 * b1);
set c = (a1 * b2) - (a2 * b1);
A9: now__::_thesis:_(_(a2_*_b3)_-_(a3_*_b2)_=_0_&_(-_(a1_*_b3))_+_(a3_*_b1)_=_0_&_(a1_*_b2)_-_(a2_*_b1)_=_0_implies_u,v,w_are_LinDep_)
A10: ( w = 0. V & v = 0. V & ( are_Prop v,w or v = 0. V or w = 0. V ) implies u,v,w are_LinDep ) by Th10;
A11: ( w = 0. V & u = 0. V & ( are_Prop v,w or v = 0. V or w = 0. V ) implies u,v,w are_LinDep ) by Th10;
A12: ( u = 0. V & v = 0. V & ( are_Prop v,w or v = 0. V or w = 0. V ) implies u,v,w are_LinDep ) by Th10;
A13: ( ( ( w = 0. V & are_Prop u,v & w = 0. V ) or ( u = 0. V & u = 0. V & are_Prop v,w ) or ( are_Prop w,u & v = 0. V & v = 0. V ) ) implies u,v,w are_LinDep ) by Th11;
A14: ( are_Prop w,u & are_Prop u,v & are_Prop v,w implies u,v,w are_LinDep ) by Th11;
assume that
A15: (a2 * b3) - (a3 * b2) = 0 and
A16: (- (a1 * b3)) + (a3 * b1) = 0 and
A17: (a1 * b2) - (a2 * b1) = 0 ; ::_thesis: u,v,w are_LinDep
 0 = (a3 * b1) - (a1 * b3) by A16;
hence  u,v,w are_LinDep by A1, A5, A6, A8, A7, A15, A17, A14, A13, A11, A10, A12, Th9; ::_thesis: verum
end;
 ( 0. V = (((((a2 * b3) - (a3 * b2)) * a1) + (((- (a1 * b3)) + (a3 * b1)) * a2)) + (((a1 * b2) - (a2 * b1)) * a3)) * p & 0. V = (((((a2 * b3) - (a3 * b2)) * b1) + (((- (a1 * b3)) + (a3 * b1)) * b2)) + (((a1 * b2) - (a2 * b1)) * b3)) * q ) by RLVECT_1:10;
then A18: 0. V = ((((((a2 * b3) - (a3 * b2)) * a1) + (((- (a1 * b3)) + (a3 * b1)) * a2)) + (((a1 * b2) - (a2 * b1)) * a3)) * p) + ((((((a2 * b3) - (a3 * b2)) * b1) + (((- (a1 * b3)) + (a3 * b1)) * b2)) + (((a1 * b2) - (a2 * b1)) * b3)) * q) by RLVECT_1:4;
 (((((a2 * b3) - (a3 * b2)) * a1) + (((- (a1 * b3)) + (a3 * b1)) * a2)) + (((a1 * b2) - (a2 * b1)) * a3)) * p = (((((a2 * b3) - (a3 * b2)) * a1) * p) + ((((- (a1 * b3)) + (a3 * b1)) * a2) * p)) + ((((a1 * b2) - (a2 * b1)) * a3) * p) by Lm3;
then  0. V = ((((((a2 * b3) - (a3 * b2)) * a1) * p) + ((((- (a1 * b3)) + (a3 * b1)) * a2) * p)) + ((((a1 * b2) - (a2 * b1)) * a3) * p)) + ((((((a2 * b3) - (a3 * b2)) * b1) * q) + ((((- (a1 * b3)) + (a3 * b1)) * b2) * q)) + ((((a1 * b2) - (a2 * b1)) * b3) * q)) by A18, Lm3;
then A19: 0. V = ((((((a2 * b3) - (a3 * b2)) * a1) * p) + ((((a2 * b3) - (a3 * b2)) * b1) * q)) + (((((- (a1 * b3)) + (a3 * b1)) * a2) * p) + ((((- (a1 * b3)) + (a3 * b1)) * b2) * q))) + (((((a1 * b2) - (a2 * b1)) * a3) * p) + ((((a1 * b2) - (a2 * b1)) * b3) * q)) by Lm4;
A20: ((((a1 * b2) - (a2 * b1)) * a3) * p) + ((((a1 * b2) - (a2 * b1)) * b3) * q) = ((a1 * b2) - (a2 * b1)) * ((a3 * p) + (b3 * q)) by Lm5;
 ( ((((a2 * b3) - (a3 * b2)) * a1) * p) + ((((a2 * b3) - (a3 * b2)) * b1) * q) = ((a2 * b3) - (a3 * b2)) * ((a1 * p) + (b1 * q)) & ((((- (a1 * b3)) + (a3 * b1)) * a2) * p) + ((((- (a1 * b3)) + (a3 * b1)) * b2) * q) = ((- (a1 * b3)) + (a3 * b1)) * ((a2 * p) + (b2 * q)) ) by Lm5;
hence  u,v,w are_LinDep by A6, A8, A7, A19, A20, A9, Def2; ::_thesis: verum
end;

Lm7:  for V being RealLinearSpace
for v, w being Element of V
for a, b, c being Real holds a * ((b * v) + (c * w)) = ((a * b) * v) + ((a * c) * w)
proof
let V be RealLinearSpace; ::_thesis: for v, w being Element of V
for a, b, c being Real holds a * ((b * v) + (c * w)) = ((a * b) * v) + ((a * c) * w)
let v, w be Element of V; ::_thesis: for a, b, c being Real holds a * ((b * v) + (c * w)) = ((a * b) * v) + ((a * c) * w)
let a, b, c be Real; ::_thesis: a * ((b * v) + (c * w)) = ((a * b) * v) + ((a * c) * w)
thus ((a * b) * v) + ((a * c) * w) = (a * (b * v)) + ((a * c) * w) by RLVECT_1:def_7
.= (a * (b * v)) + (a * (c * w)) by RLVECT_1:def_7
.= a * ((b * v) + (c * w)) by RLVECT_1:def_5 ; ::_thesis: verum
end;

theorem :: ANPROJ_1:15
for V being RealLinearSpace
for u, v, w, p, q being Element of V st not u,v,w are_LinDep & u,v,p are_LinDep & v,w,q are_LinDep holds
ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero )
proof
let V be RealLinearSpace; ::_thesis: for u, v, w, p, q being Element of V st not u,v,w are_LinDep & u,v,p are_LinDep & v,w,q are_LinDep holds
ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero )
let u, v, w, p, q be Element of V; ::_thesis: ( not u,v,w are_LinDep & u,v,p are_LinDep & v,w,q are_LinDep implies ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) )
assume that
A1: not u,v,w are_LinDep and
A2: u,v,p are_LinDep and
A3: v,w,q are_LinDep ; ::_thesis: ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero )
A4: not v is zero by A1, Th12;
A5: not w is zero by A1, Th12;
A6: now__::_thesis:_(_(_are_Prop_p,q_or_p_is_zero_or_q_is_zero_)_implies_ex_y_being_Element_of_V_st_
(_u,w,y_are_LinDep_&_p,q,y_are_LinDep_&_not_y_is_zero_)_)
A7: now__::_thesis:_(_q_is_zero_implies_ex_y_being_Element_of_V_st_
(_u,w,y_are_LinDep_&_p,q,y_are_LinDep_&_not_y_is_zero_)_)
assume  q is zero ; ::_thesis: ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero )
then  q = 0. V by STRUCT_0:def_12;
then A8: p,q,w are_LinDep by Th10;
 u,w,w are_LinDep by Th11;
hence  ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) by A5, A8; ::_thesis: verum
end;
A9: now__::_thesis:_(_p_is_zero_implies_ex_y_being_Element_of_V_st_
(_u,w,y_are_LinDep_&_p,q,y_are_LinDep_&_not_y_is_zero_)_)
assume  p is zero ; ::_thesis: ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero )
then  p = 0. V by STRUCT_0:def_12;
then A10: p,q,w are_LinDep by Th10;
 u,w,w are_LinDep by Th11;
hence  ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) by A5, A10; ::_thesis: verum
end;
A11: now__::_thesis:_(_are_Prop_p,q_implies_ex_y_being_Element_of_V_st_
(_u,w,y_are_LinDep_&_p,q,y_are_LinDep_&_not_y_is_zero_)_)
assume  are_Prop p,q ; ::_thesis: ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero )
then A12: p,q,w are_LinDep by Th11;
 u,w,w are_LinDep by Th11;
hence  ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) by A5, A12; ::_thesis: verum
end;
assume  ( are_Prop p,q or p is zero or q is zero ) ; ::_thesis: ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero )
hence  ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) by A11, A9, A7; ::_thesis: verum
end;
A13: not u is zero by A1, Th12;
 not are_Prop u,v by A1, Th12;
then consider a1, b1 being Real such that
A14: p = (a1 * u) + (b1 * v) by A2, A13, A4, Th6;
A15: not are_Prop w,u by A1, Th12;
 not are_Prop v,w by A1, Th12;
then consider a2, b2 being Real such that
A16: q = (a2 * v) + (b2 * w) by A3, A4, A5, Th6;
A17: for c, d being Real holds (c * p) + (d * q) = (((c * a1) * u) + (((c * b1) + (d * a2)) * v)) + ((d * b2) * w)
proof
let c, d be Real; ::_thesis: (c * p) + (d * q) = (((c * a1) * u) + (((c * b1) + (d * a2)) * v)) + ((d * b2) * w)
thus (c * p) + (d * q) = (((c * a1) * u) + ((c * b1) * v)) + (d * ((a2 * v) + (b2 * w))) by A14, A16, Lm7
.= (((c * a1) * u) + ((c * b1) * v)) + (((d * a2) * v) + ((d * b2) * w)) by Lm7
.= ((((c * a1) * u) + ((c * b1) * v)) + ((d * a2) * v)) + ((d * b2) * w) by RLVECT_1:def_3
.= (((c * a1) * u) + (((c * b1) * v) + ((d * a2) * v))) + ((d * b2) * w) by RLVECT_1:def_3
.= (((c * a1) * u) + (((c * b1) + (d * a2)) * v)) + ((d * b2) * w) by RLVECT_1:def_6 ; ::_thesis: verum
end;
A18: now__::_thesis:_(_not_are_Prop_p,q_&_not_p_is_zero_&_not_q_is_zero_&_b1_<>_0_implies_ex_y_being_Element_of_V_st_
(_u,w,y_are_LinDep_&_p,q,y_are_LinDep_&_not_y_is_zero_)_)
assume that
A19: not are_Prop p,q and
A20: not p is zero and
A21: not q is zero and
A22: b1 <> 0 ; ::_thesis: ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero )
A23: now__::_thesis:_(_a2_<>_0_implies_ex_y_being_Element_of_V_st_
(_u,w,y_are_LinDep_&_p,q,y_are_LinDep_&_not_y_is_zero_)_)
set c = 1;
set d = - (b1 * (a2 "));
set y = (1 * p) + ((- (b1 * (a2 "))) * q);
assume A24: a2 <> 0 ; ::_thesis: ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero )
then  a2 " <> 0 by XCMPLX_1:202;
then A25: b1 * (a2 ") <> 0 by A22, XCMPLX_1:6;
A26: not (1 * p) + ((- (b1 * (a2 "))) * q) is zero
proof
assume  (1 * p) + ((- (b1 * (a2 "))) * q) is zero ; ::_thesis: contradiction
then  0. V = (1 * p) + ((- (b1 * (a2 "))) * q) by STRUCT_0:def_12
.= (1 * p) + ((b1 * (a2 ")) * (- q)) by RLVECT_1:24
.= (1 * p) + (- ((b1 * (a2 ")) * q)) by RLVECT_1:25 ;
then  - (1 * p) = - ((b1 * (a2 ")) * q) by RLVECT_1:def_10;
then  1 * p = (b1 * (a2 ")) * q by RLVECT_1:18;
hence  contradiction by A19, A25, Def1; ::_thesis: verum
end;
(1 * b1) + ((- (b1 * (a2 "))) * a2) = b1 + ((- b1) * ((a2 ") * a2))
.= b1 + ((- b1) * 1) by A24, XCMPLX_0:def_7
.= 0 ;
then (1 * p) + ((- (b1 * (a2 "))) * q) = (((1 * a1) * u) + (0 * v)) + (((- (b1 * (a2 "))) * b2) * w) by A17
.= (((1 * a1) * u) + (0. V)) + (((- (b1 * (a2 "))) * b2) * w) by RLVECT_1:10
.= ((1 * a1) * u) + (((- (b1 * (a2 "))) * b2) * w) by RLVECT_1:4 ;
then A27: u,w,(1 * p) + ((- (b1 * (a2 "))) * q) are_LinDep by A15, A13, A5, Th6;
 p,q,(1 * p) + ((- (b1 * (a2 "))) * q) are_LinDep by A19, A20, A21, Th6;
hence  ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) by A26, A27; ::_thesis: verum
end;
now__::_thesis:_(_a2_=_0_implies_ex_y_being_Element_of_V_st_
(_u,w,y_are_LinDep_&_p,q,y_are_LinDep_&_not_y_is_zero_)_)
set c = 0 ;
set d = 1;
set y = (0 * p) + (1 * q);
A28: (0 * p) + (1 * q) = (0. V) + (1 * q) by RLVECT_1:10
.= (0. V) + q by RLVECT_1:def_8
.= q by RLVECT_1:4 ;
assume  a2 = 0 ; ::_thesis: ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero )
then  (0 * b1) + (1 * a2) = 0 ;
then (0 * p) + (1 * q) = (((0 * a1) * u) + (0 * v)) + ((1 * b2) * w) by A17
.= (((0 * a1) * u) + (0. V)) + ((1 * b2) * w) by RLVECT_1:10
.= ((0 * a1) * u) + ((1 * b2) * w) by RLVECT_1:4 ;
then A29: u,w,(0 * p) + (1 * q) are_LinDep by A15, A13, A5, Th6;
 p,q,(0 * p) + (1 * q) are_LinDep by A19, A20, A21, Th6;
hence  ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) by A21, A28, A29; ::_thesis: verum
end;
hence  ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) by A23; ::_thesis: verum
end;
now__::_thesis:_(_not_are_Prop_p,q_&_not_p_is_zero_&_not_q_is_zero_&_b1_=_0_implies_ex_y_being_Element_of_V_st_
(_u,w,y_are_LinDep_&_p,q,y_are_LinDep_&_not_y_is_zero_)_)
assume that
A30: not are_Prop p,q and
A31: not p is zero and
A32: not q is zero and
A33: b1 = 0 ; ::_thesis: ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero )
now__::_thesis:_ex_y_being_Element_of_V_st_
(_u,w,y_are_LinDep_&_p,q,y_are_LinDep_&_not_y_is_zero_)
set c = 1;
set d = 0 ;
set y = (1 * p) + (0 * q);
A34: (1 * p) + (0 * q) = p + (0 * q) by RLVECT_1:def_8
.= p + (0. V) by RLVECT_1:10
.= p by RLVECT_1:4 ;
 (1 * b1) + (0 * a2) = 0 by A33;
then (1 * p) + (0 * q) = (((1 * a1) * u) + (0 * v)) + ((0 * b2) * w) by A17
.= (((1 * a1) * u) + (0. V)) + ((0 * b2) * w) by RLVECT_1:10
.= ((1 * a1) * u) + ((0 * b2) * w) by RLVECT_1:4 ;
then A35: u,w,(1 * p) + (0 * q) are_LinDep by A15, A13, A5, Th6;
 p,q,(1 * p) + (0 * q) are_LinDep by A30, A31, A32, Th6;
hence  ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) by A31, A34, A35; ::_thesis: verum
end;
hence  ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) ; ::_thesis: verum
end;
hence  ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero ) by A6, A18; ::_thesis: verum
end;

theorem :: ANPROJ_1:16
for V being RealLinearSpace
for p, q being Element of V st not are_Prop p,q & not p is zero & not q is zero holds
for u, v being Element of V ex y being Element of V st
( not y is zero & u,v,y are_LinDep & not are_Prop u,y & not are_Prop v,y )
proof
let V be RealLinearSpace; ::_thesis: for p, q being Element of V st not are_Prop p,q & not p is zero & not q is zero holds
for u, v being Element of V ex y being Element of V st
( not y is zero & u,v,y are_LinDep & not are_Prop u,y & not are_Prop v,y )
let p, q be Element of V; ::_thesis: ( not are_Prop p,q & not p is zero & not q is zero implies for u, v being Element of V ex y being Element of V st
( not y is zero & u,v,y are_LinDep & not are_Prop u,y & not are_Prop v,y ) )
assume that
A1: not are_Prop p,q and
A2: not p is zero and
A3: not q is zero ; ::_thesis: for u, v being Element of V ex y being Element of V st
( not y is zero & u,v,y are_LinDep & not are_Prop u,y & not are_Prop v,y )
let u, v be Element of V; ::_thesis: ex y being Element of V st
( not y is zero & u,v,y are_LinDep & not are_Prop u,y & not are_Prop v,y )
A4: now__::_thesis:_(_not_are_Prop_u,v_&_u_is_zero_implies_ex_y_being_Element_of_V_st_
(_not_y_is_zero_&_u,v,y_are_LinDep_&_not_are_Prop_u,y_&_not_are_Prop_v,y_)_)
assume that
 not are_Prop u,v and
A5: u is zero ; ::_thesis: ex y being Element of V st
( not y is zero & u,v,y are_LinDep & not are_Prop u,y & not are_Prop v,y )
A6: u = 0. V by A5, STRUCT_0:def_12;
then A7: ( not are_Prop v,q implies ( not are_Prop v,q & not q is zero & u,v,q are_LinDep & not are_Prop u,q ) ) by A3, Th3, Th10;
 ( not are_Prop v,p implies ( not are_Prop v,p & not p is zero & u,v,p are_LinDep & not are_Prop u,p ) ) by A2, A6, Th3, Th10;
hence  ex y being Element of V st
( not y is zero & u,v,y are_LinDep & not are_Prop u,y & not are_Prop v,y ) by A1, A7, Th2; ::_thesis: verum
end;
A8: now__::_thesis:_(_not_are_Prop_u,v_&_not_u_is_zero_&_not_v_is_zero_implies_(_not_u_+_v_is_zero_&_u,v,u_+_v_are_LinDep_&_not_are_Prop_u,u_+_v_&_not_are_Prop_v,u_+_v_)_)
set y = u + v;
assume that
A9: not are_Prop u,v and
A10: not u is zero and
A11: not v is zero ; ::_thesis: ( not u + v is zero & u,v,u + v are_LinDep & not are_Prop u,u + v & not are_Prop v,u + v )
 u + v <> 0. V by A9, Th13;
hence  not u + v is zero by STRUCT_0:def_12; ::_thesis: ( u,v,u + v are_LinDep & not are_Prop u,u + v & not are_Prop v,u + v )
((1 * u) + (1 * v)) + ((- 1) * (u + v)) = (u + (1 * v)) + ((- 1) * (u + v)) by RLVECT_1:def_8
.= (u + v) + ((- 1) * (u + v)) by RLVECT_1:def_8
.= (u + v) + (- (u + v)) by RLVECT_1:16
.= (v + u) + ((- u) + (- v)) by RLVECT_1:31
.= v + (u + ((- u) + (- v))) by RLVECT_1:def_3
.= v + ((u + (- u)) + (- v)) by RLVECT_1:def_3
.= v + ((0. V) + (- v)) by RLVECT_1:5
.= v + (- v) by RLVECT_1:4
.= 0. V by RLVECT_1:5 ;
hence  u,v,u + v are_LinDep by Def2; ::_thesis: ( not are_Prop u,u + v & not are_Prop v,u + v )
A12: v <> 0. V by A11;
now__::_thesis:_for_a,_b_being_Real_holds_
(_not_a_*_u_=_b_*_(u_+_v)_or_a_=_0_or_b_=_0_)
let a, b be Real; ::_thesis: ( not a * u = b * (u + v) or a = 0 or b = 0 )
assume  a * u = b * (u + v) ; ::_thesis: ( a = 0 or b = 0 )
then (- (b * u)) + (a * u) = (- (b * u)) + ((b * u) + (b * v)) by RLVECT_1:def_5
.= ((b * u) + (- (b * u))) + (b * v) by RLVECT_1:def_3
.= (0. V) + (b * v) by RLVECT_1:5
.= b * v by RLVECT_1:4 ;
then A13: b * v = (a * u) + (b * (- u)) by RLVECT_1:25
.= (a * u) + ((- b) * u) by RLVECT_1:24
.= (a + (- b)) * u by RLVECT_1:def_6 ;
now__::_thesis:_(_a_+_(-_b)_=_0_implies_b_=_0_)
assume  a + (- b) = 0 ; ::_thesis: b = 0
then  b * v = 0. V by A13, RLVECT_1:10;
hence  b = 0 by A12, RLVECT_1:11; ::_thesis: verum
end;
hence  ( a = 0 or b = 0 ) by A9, A13, Def1; ::_thesis: verum
end;
hence  not are_Prop u,u + v by Def1; ::_thesis: not are_Prop v,u + v
A14: u <> 0. V by A10;
now__::_thesis:_for_a,_b_being_Real_holds_
(_not_a_*_v_=_b_*_(u_+_v)_or_a_=_0_or_b_=_0_)
let a, b be Real; ::_thesis: ( not a * v = b * (u + v) or a = 0 or b = 0 )
assume  a * v = b * (u + v) ; ::_thesis: ( a = 0 or b = 0 )
then (a * v) + (- (b * v)) = ((b * u) + (b * v)) + (- (b * v)) by RLVECT_1:def_5
.= (b * u) + ((b * v) + (- (b * v))) by RLVECT_1:def_3
.= (b * u) + (0. V) by RLVECT_1:5
.= b * u by RLVECT_1:4 ;
then A15: b * u = (a * v) + (b * (- v)) by RLVECT_1:25
.= (a * v) + ((- b) * v) by RLVECT_1:24
.= (a + (- b)) * v by RLVECT_1:def_6 ;
now__::_thesis:_(_a_+_(-_b)_=_0_implies_b_=_0_)
assume  a + (- b) = 0 ; ::_thesis: b = 0
then  b * u = 0. V by A15, RLVECT_1:10;
hence  b = 0 by A14, RLVECT_1:11; ::_thesis: verum
end;
hence  ( a = 0 or b = 0 ) by A9, A15, Def1; ::_thesis: verum
end;
hence  not are_Prop v,u + v by Def1; ::_thesis: verum
end;
A16: now__::_thesis:_(_not_are_Prop_u,v_&_v_is_zero_implies_ex_y_being_Element_of_V_st_
(_not_y_is_zero_&_u,v,y_are_LinDep_&_not_are_Prop_u,y_&_not_are_Prop_v,y_)_)
assume that
 not are_Prop u,v and
A17: v is zero ; ::_thesis: ex y being Element of V st
( not y is zero & u,v,y are_LinDep & not are_Prop u,y & not are_Prop v,y )
A18: v = 0. V by A17, STRUCT_0:def_12;
then A19: ( not are_Prop u,q implies ( not q is zero & u,v,q are_LinDep & not are_Prop u,q & not are_Prop v,q ) ) by A3, Th3, Th10;
 ( not are_Prop u,p implies ( not p is zero & u,v,p are_LinDep & not are_Prop u,p & not are_Prop v,p ) ) by A2, A18, Th3, Th10;
hence  ex y being Element of V st
( not y is zero & u,v,y are_LinDep & not are_Prop u,y & not are_Prop v,y ) by A1, A19, Th2; ::_thesis: verum
end;
now__::_thesis:_(_are_Prop_u,v_implies_ex_y_being_Element_of_V_st_
(_not_y_is_zero_&_u,v,y_are_LinDep_&_not_are_Prop_u,y_&_not_are_Prop_v,y_)_)
assume A20: are_Prop u,v ; ::_thesis: ex y being Element of V st
( not y is zero & u,v,y are_LinDep & not are_Prop u,y & not are_Prop v,y )
then A21: ( not are_Prop u,q implies ( not q is zero & u,v,q are_LinDep & not are_Prop u,q & not are_Prop v,q ) ) by A3, Th2, Th11;
 ( not are_Prop u,p implies ( not p is zero & u,v,p are_LinDep & not are_Prop u,p & not are_Prop v,p ) ) by A2, A20, Th2, Th11;
hence  ex y being Element of V st
( not y is zero & u,v,y are_LinDep & not are_Prop u,y & not are_Prop v,y ) by A1, A21, Th2; ::_thesis: verum
end;
hence  ex y being Element of V st
( not y is zero & u,v,y are_LinDep & not are_Prop u,y & not are_Prop v,y ) by A8, A4, A16; ::_thesis: verum
end;

Lm8:  for V being RealLinearSpace
for p, q, r being Element of V st not p,q,r are_LinDep holds
for u, v being Element of V st not u is zero & not v is zero & not are_Prop u,v holds
ex y being Element of V st not u,v,y are_LinDep
proof
let V be RealLinearSpace; ::_thesis: for p, q, r being Element of V st not p,q,r are_LinDep holds
for u, v being Element of V st not u is zero & not v is zero & not are_Prop u,v holds
ex y being Element of V st not u,v,y are_LinDep
let p, q, r be Element of V; ::_thesis: ( not p,q,r are_LinDep implies for u, v being Element of V st not u is zero & not v is zero & not are_Prop u,v holds
ex y being Element of V st not u,v,y are_LinDep )
assume A1: not p,q,r are_LinDep ; ::_thesis: for u, v being Element of V st not u is zero & not v is zero & not are_Prop u,v holds
ex y being Element of V st not u,v,y are_LinDep
let u, v be Element of V; ::_thesis: ( not u is zero & not v is zero & not are_Prop u,v implies ex y being Element of V st not u,v,y are_LinDep )
assume A2: ( not u is zero & not v is zero & not are_Prop u,v ) ; ::_thesis: not for y being Element of V holds u,v,y are_LinDep
assume A3: for y being Element of V holds u,v,y are_LinDep ; ::_thesis: contradiction
then A4: u,v,r are_LinDep ;
 ( u,v,p are_LinDep & u,v,q are_LinDep ) by A3;
hence  contradiction by A1, A2, A4, Th14; ::_thesis: verum
end;

theorem :: ANPROJ_1:17
for V being RealLinearSpace
for p, q, r being Element of V st not p,q,r are_LinDep holds
for u, v being Element of V st not u is zero & not v is zero & not are_Prop u,v holds
ex y being Element of V st
( not y is zero & not u,v,y are_LinDep )
proof
let V be RealLinearSpace; ::_thesis: for p, q, r being Element of V st not p,q,r are_LinDep holds
for u, v being Element of V st not u is zero & not v is zero & not are_Prop u,v holds
ex y being Element of V st
( not y is zero & not u,v,y are_LinDep )
let p, q, r be Element of V; ::_thesis: ( not p,q,r are_LinDep implies for u, v being Element of V st not u is zero & not v is zero & not are_Prop u,v holds
ex y being Element of V st
( not y is zero & not u,v,y are_LinDep ) )
assume A1: not p,q,r are_LinDep ; ::_thesis: for u, v being Element of V st not u is zero & not v is zero & not are_Prop u,v holds
ex y being Element of V st
( not y is zero & not u,v,y are_LinDep )
let u, v be Element of V; ::_thesis: ( not u is zero & not v is zero & not are_Prop u,v implies ex y being Element of V st
( not y is zero & not u,v,y are_LinDep ) )
assume  ( not u is zero & not v is zero & not are_Prop u,v ) ; ::_thesis: ex y being Element of V st
( not y is zero & not u,v,y are_LinDep )
then consider y being Element of V such that
A2: not u,v,y are_LinDep by A1, Lm8;
take  y ; ::_thesis: ( not y is zero & not u,v,y are_LinDep )
thus  not y is zero by A2, Th12; ::_thesis: not u,v,y are_LinDep
thus  not u,v,y are_LinDep by A2; ::_thesis: verum
end;

Lm9:  for V being RealLinearSpace
for u, w, y being Element of V
for a, b, c, d, e, f, A, B, C being Real holds ((A * ((a * u) + (b * w))) + (B * ((c * w) + (d * y)))) + (C * ((e * u) + (f * y))) = ((((A * a) + (C * e)) * u) + (((A * b) + (B * c)) * w)) + (((B * d) + (C * f)) * y)
proof
let V be RealLinearSpace; ::_thesis: for u, w, y being Element of V
for a, b, c, d, e, f, A, B, C being Real holds ((A * ((a * u) + (b * w))) + (B * ((c * w) + (d * y)))) + (C * ((e * u) + (f * y))) = ((((A * a) + (C * e)) * u) + (((A * b) + (B * c)) * w)) + (((B * d) + (C * f)) * y)
let u, w, y be Element of V; ::_thesis: for a, b, c, d, e, f, A, B, C being Real holds ((A * ((a * u) + (b * w))) + (B * ((c * w) + (d * y)))) + (C * ((e * u) + (f * y))) = ((((A * a) + (C * e)) * u) + (((A * b) + (B * c)) * w)) + (((B * d) + (C * f)) * y)
let a, b, c, d, e, f be Real; ::_thesis: for A, B, C being Real holds ((A * ((a * u) + (b * w))) + (B * ((c * w) + (d * y)))) + (C * ((e * u) + (f * y))) = ((((A * a) + (C * e)) * u) + (((A * b) + (B * c)) * w)) + (((B * d) + (C * f)) * y)
let A, B, C be Real; ::_thesis: ((A * ((a * u) + (b * w))) + (B * ((c * w) + (d * y)))) + (C * ((e * u) + (f * y))) = ((((A * a) + (C * e)) * u) + (((A * b) + (B * c)) * w)) + (((B * d) + (C * f)) * y)
A1: C * ((e * u) + (f * y)) = ((C * e) * u) + ((C * f) * y) by Lm7;
 ( A * ((a * u) + (b * w)) = ((A * a) * u) + ((A * b) * w) & B * ((c * w) + (d * y)) = ((B * c) * w) + ((B * d) * y) ) by Lm7;
hence ((A * ((a * u) + (b * w))) + (B * ((c * w) + (d * y)))) + (C * ((e * u) + (f * y))) = (((((A * a) * u) + ((A * b) * w)) + ((B * c) * w)) + ((B * d) * y)) + (((C * e) * u) + ((C * f) * y)) by A1, RLVECT_1:def_3
.= ((((A * a) * u) + (((A * b) * w) + ((B * c) * w))) + ((B * d) * y)) + (((C * e) * u) + ((C * f) * y)) by RLVECT_1:def_3
.= ((((A * a) * u) + (((A * b) + (B * c)) * w)) + ((B * d) * y)) + (((C * e) * u) + ((C * f) * y)) by RLVECT_1:def_6
.= (((A * a) * u) + (((A * b) + (B * c)) * w)) + (((B * d) * y) + (((C * f) * y) + ((C * e) * u))) by RLVECT_1:def_3
.= (((A * a) * u) + (((A * b) + (B * c)) * w)) + ((((B * d) * y) + ((C * f) * y)) + ((C * e) * u)) by RLVECT_1:def_3
.= (((A * a) * u) + (((A * b) + (B * c)) * w)) + ((((B * d) + (C * f)) * y) + ((C * e) * u)) by RLVECT_1:def_6
.= ((A * a) * u) + ((((A * b) + (B * c)) * w) + ((((B * d) + (C * f)) * y) + ((C * e) * u))) by RLVECT_1:def_3
.= ((A * a) * u) + (((C * e) * u) + ((((A * b) + (B * c)) * w) + (((B * d) + (C * f)) * y))) by RLVECT_1:def_3
.= (((A * a) * u) + ((C * e) * u)) + ((((A * b) + (B * c)) * w) + (((B * d) + (C * f)) * y)) by RLVECT_1:def_3
.= (((A * a) + (C * e)) * u) + ((((A * b) + (B * c)) * w) + (((B * d) + (C * f)) * y)) by RLVECT_1:def_6
.= ((((A * a) + (C * e)) * u) + (((A * b) + (B * c)) * w)) + (((B * d) + (C * f)) * y) by RLVECT_1:def_3 ;
::_thesis: verum
end;

theorem :: ANPROJ_1:18
for V being RealLinearSpace
for u, v, q, w, y, p, r being Element of V st u,v,q are_LinDep & w,y,q are_LinDep & u,w,p are_LinDep & v,y,p are_LinDep & u,y,r are_LinDep & v,w,r are_LinDep & p,q,r are_LinDep & not p is zero & not q is zero & not r is zero & not u,v,y are_LinDep & not u,v,w are_LinDep & not u,w,y are_LinDep holds
v,w,y are_LinDep
proof
let V be RealLinearSpace; ::_thesis: for u, v, q, w, y, p, r being Element of V st u,v,q are_LinDep & w,y,q are_LinDep & u,w,p are_LinDep & v,y,p are_LinDep & u,y,r are_LinDep & v,w,r are_LinDep & p,q,r are_LinDep & not p is zero & not q is zero & not r is zero & not u,v,y are_LinDep & not u,v,w are_LinDep & not u,w,y are_LinDep holds
v,w,y are_LinDep
let u, v, q, w, y, p, r be Element of V; ::_thesis: ( u,v,q are_LinDep & w,y,q are_LinDep & u,w,p are_LinDep & v,y,p are_LinDep & u,y,r are_LinDep & v,w,r are_LinDep & p,q,r are_LinDep & not p is zero & not q is zero & not r is zero & not u,v,y are_LinDep & not u,v,w are_LinDep & not u,w,y are_LinDep implies v,w,y are_LinDep )
assume that
A1: u,v,q are_LinDep and
A2: w,y,q are_LinDep and
A3: u,w,p are_LinDep and
A4: v,y,p are_LinDep and
A5: u,y,r are_LinDep and
A6: v,w,r are_LinDep and
A7: p,q,r are_LinDep and
A8: not p is zero and
A9: not q is zero and
A10: not r is zero ; ::_thesis: ( u,v,y are_LinDep or u,v,w are_LinDep or u,w,y are_LinDep or v,w,y are_LinDep )
assume A11: ( not u,v,y are_LinDep & not u,v,w are_LinDep & not u,w,y are_LinDep & not v,w,y are_LinDep ) ; ::_thesis: contradiction
then A12: not v is zero by Th12;
A13: not w is zero by A11, Th12;
A14: not y is zero by A11, Th12;
A15: not u is zero by A11, Th12;
 not are_Prop v,y by A11, Th12;
then consider a19, b19 being Real such that
A16: p = (a19 * v) + (b19 * y) by A4, A12, A14, Th6;
 not are_Prop u,v by A11, Th12;
then consider a2, b2 being Real such that
A17: q = (a2 * u) + (b2 * v) by A1, A15, A12, Th6;
 not are_Prop v,w by A11, Th12;
then consider a39, b39 being Real such that
A18: r = (a39 * v) + (b39 * w) by A6, A12, A13, Th6;
 not are_Prop u,w by A11, Th12;
then consider a1, b1 being Real such that
A19: p = (a1 * u) + (b1 * w) by A3, A15, A13, Th6;
 not are_Prop w,y by A11, Th12;
then consider a29, b29 being Real such that
A20: q = (a29 * w) + (b29 * y) by A2, A13, A14, Th6;
 not are_Prop y,u by A11, Th12;
then consider a3, b3 being Real such that
A21: r = (a3 * u) + (b3 * y) by A5, A15, A14, Th6;
consider A, B, C being Real such that
A22: ((A * p) + (B * q)) + (C * r) = 0. V and
A23: ( A <> 0 or B <> 0 or C <> 0 ) by A7, Def2;
A24: 0. V = ((((A * a1) + (C * a3)) * u) + (((A * b1) + (B * a29)) * w)) + (((B * b29) + (C * b3)) * y) by A19, A20, A21, A22, Lm9;
then A25: (A * a1) + (C * a3) = 0 by A11, Def2;
A26: 0. V = ((C * ((a39 * v) + (b39 * w))) + (B * ((a29 * w) + (b29 * y)))) + (A * ((a19 * v) + (b19 * y))) by A16, A20, A18, A22, RLVECT_1:def_3
.= ((((C * a39) + (A * a19)) * v) + (((C * b39) + (B * a29)) * w)) + (((B * b29) + (A * b19)) * y) by Lm9 ;
then A27: (C * a39) + (A * a19) = 0 by A11, Def2;
A28: 0. V = ((((B * a2) + (C * a3)) * u) + (((B * b2) + (A * a19)) * v)) + (((A * b19) + (C * b3)) * y) by A16, A17, A21, A22, Lm9;
then A29: (B * a2) + (C * a3) = 0 by A11, Def2;
A30: 0. V = ((((B * a2) + (A * a1)) * u) + (((B * b2) + (C * a39)) * v)) + (((C * b39) + (A * b1)) * w) by A19, A17, A18, A22, Lm9;
then A31: (B * a2) + (A * a1) = 0 by A11, Def2;
A32: (C * b39) + (B * a29) = 0 by A11, A26, Def2;
A33: (C * b39) + (A * b1) = 0 by A11, A30, Def2;
A34: (B * b29) + (A * b19) = 0 by A11, A26, Def2;
A35: (A * b19) + (C * b3) = 0 by A11, A28, Def2;
A36: (B * b29) + (C * b3) = 0 by A11, A24, Def2;
A37: now__::_thesis:_not_C_<>_0
assume A38: C <> 0 ; ::_thesis: contradiction
then  a3 = 0 by A25, A29, A31, XCMPLX_1:6;
then r = (0 * u) + (0 * y) by A21, A36, A35, A34, A38, XCMPLX_1:6
.= (0. V) + (0 * y) by RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
hence  contradiction by A10; ::_thesis: verum
end;
A39: (B * b2) + (C * a39) = 0 by A11, A30, Def2;
A40: (B * b2) + (A * a19) = 0 by A11, A28, Def2;
A41: now__::_thesis:_not_B_<>_0
assume A42: B <> 0 ; ::_thesis: contradiction
then  a2 = 0 by A25, A29, A31, XCMPLX_1:6;
then q = (0 * u) + (0 * v) by A17, A40, A39, A27, A42, XCMPLX_1:6
.= (0. V) + (0 * v) by RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
hence  contradiction by A9; ::_thesis: verum
end;
A43: (A * b1) + (B * a29) = 0 by A11, A24, Def2;
now__::_thesis:_not_A_<>_0
assume A44: A <> 0 ; ::_thesis: contradiction
then  a1 = 0 by A25, A29, A31, XCMPLX_1:6;
then p = (0 * u) + (0 * w) by A19, A43, A33, A32, A44, XCMPLX_1:6
.= (0. V) + (0 * w) by RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
hence  contradiction by A8; ::_thesis: verum
end;
hence  contradiction by A23, A41, A37; ::_thesis: verum
end;


definition
let V be RealLinearSpace;
func Proportionality_as_EqRel_of V ->  Equivalence_Relation of (NonZero V) means :Def3: :: ANPROJ_1:def 3
 for x, y being set holds
( [x,y] in it iff ( x in NonZero V & y in NonZero V & ex u, v being Element of V st
( x = u & y = v & are_Prop u,v ) ) );
existence
 ex b1 being Equivalence_Relation of (NonZero V) st
for x, y being set holds
( [x,y] in b1 iff ( x in NonZero V & y in NonZero V & ex u, v being Element of V st
( x = u & y = v & are_Prop u,v ) ) )
proof
defpred S1[ set , set ] means  ex u, v being Element of V st
( $1 = u & $2 = v & are_Prop u,v );
A1: for x being set st x in NonZero V holds
S1[x,x] ;
A2: for x, y being set st S1[x,y] holds
S1[y,x] ;
A3: for x, y, z being set st S1[x,y] & S1[y,z] holds
S1[x,z] by Th2;
consider R being Equivalence_Relation of (NonZero V) such that
A4: for x, y being set holds
( [x,y] in R iff ( x in NonZero V & y in NonZero V & S1[x,y] ) ) from EQREL_1:sch_1(A1, A2, A3);
take  R ; ::_thesis: for x, y being set holds
( [x,y] in R iff ( x in NonZero V & y in NonZero V & ex u, v being Element of V st
( x = u & y = v & are_Prop u,v ) ) )
thus  for x, y being set holds
( [x,y] in R iff ( x in NonZero V & y in NonZero V & ex u, v being Element of V st
( x = u & y = v & are_Prop u,v ) ) ) by A4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Equivalence_Relation of (NonZero V) st ( for x, y being set holds
( [x,y] in b1 iff ( x in NonZero V & y in NonZero V & ex u, v being Element of V st
( x = u & y = v & are_Prop u,v ) ) ) ) & ( for x, y being set holds
( [x,y] in b2 iff ( x in NonZero V & y in NonZero V & ex u, v being Element of V st
( x = u & y = v & are_Prop u,v ) ) ) ) holds
b1 = b2
proof
let R1, R2 be Equivalence_Relation of (NonZero V); ::_thesis: ( ( for x, y being set holds
( [x,y] in R1 iff ( x in NonZero V & y in NonZero V & ex u, v being Element of V st
( x = u & y = v & are_Prop u,v ) ) ) ) & ( for x, y being set holds
( [x,y] in R2 iff ( x in NonZero V & y in NonZero V & ex u, v being Element of V st
( x = u & y = v & are_Prop u,v ) ) ) ) implies R1 = R2 )
assume that
A5: for x, y being set holds
( [x,y] in R1 iff ( x in NonZero V & y in NonZero V & ex u, v being Element of V st
( x = u & y = v & are_Prop u,v ) ) ) and
A6: for x, y being set holds
( [x,y] in R2 iff ( x in NonZero V & y in NonZero V & ex u, v being Element of V st
( x = u & y = v & are_Prop u,v ) ) ) ; ::_thesis: R1 = R2
 for x, y being set holds
( [x,y] in R1 iff [x,y] in R2 )
proof
let x, y be set ; ::_thesis: ( [x,y] in R1 iff [x,y] in R2 )
A7: now__::_thesis:_(_[x,y]_in_R2_implies_[x,y]_in_R1_)
assume A8: [x,y] in R2 ; ::_thesis: [x,y] in R1
then A9: ex u, v being Element of V st
( x = u & y = v & are_Prop u,v ) by A6;
 ( x in NonZero V & y in NonZero V ) by A6, A8;
hence  [x,y] in R1 by A5, A9; ::_thesis: verum
end;
now__::_thesis:_(_[x,y]_in_R1_implies_[x,y]_in_R2_)
assume A10: [x,y] in R1 ; ::_thesis: [x,y] in R2
then A11: ex u, v being Element of V st
( x = u & y = v & are_Prop u,v ) by A5;
 ( x in NonZero V & y in NonZero V ) by A5, A10;
hence  [x,y] in R2 by A6, A11; ::_thesis: verum
end;
hence  ( [x,y] in R1 iff [x,y] in R2 ) by A7; ::_thesis: verum
end;
hence  R1 = R2 by RELAT_1:def_2; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines Proportionality_as_EqRel_of ANPROJ_1:def_3_:_
 for V being RealLinearSpace
for b2 being Equivalence_Relation of (NonZero V) holds
( b2 = Proportionality_as_EqRel_of V iff for x, y being set holds
( [x,y] in b2 iff ( x in NonZero V & y in NonZero V & ex u, v being Element of V st
( x = u & y = v & are_Prop u,v ) ) ) );

theorem :: ANPROJ_1:19
for V being RealLinearSpace
for x, y being set st [x,y] in Proportionality_as_EqRel_of V holds
( x is Element of V & y is Element of V )
proof
let V be RealLinearSpace; ::_thesis: for x, y being set st [x,y] in Proportionality_as_EqRel_of V holds
( x is Element of V & y is Element of V )
let x, y be set ; ::_thesis: ( [x,y] in Proportionality_as_EqRel_of V implies ( x is Element of V & y is Element of V ) )
assume  [x,y] in Proportionality_as_EqRel_of V ; ::_thesis: ( x is Element of V & y is Element of V )
then  ex u, v being Element of V st
( x = u & y = v & are_Prop u,v ) by Def3;
then reconsider x = x, y = y as Element of V ;
 ( x is Element of V & y is Element of V ) ;
hence  ( x is Element of V & y is Element of V ) ; ::_thesis: verum
end;

theorem Th20: :: ANPROJ_1:20
for V being RealLinearSpace
for u, v being Element of V holds
( [u,v] in Proportionality_as_EqRel_of V iff ( not u is zero & not v is zero & are_Prop u,v ) )
proof
let V be RealLinearSpace; ::_thesis: for u, v being Element of V holds
( [u,v] in Proportionality_as_EqRel_of V iff ( not u is zero & not v is zero & are_Prop u,v ) )
let u, v be Element of V; ::_thesis: ( [u,v] in Proportionality_as_EqRel_of V iff ( not u is zero & not v is zero & are_Prop u,v ) )
A1: now__::_thesis:_(_[u,v]_in_Proportionality_as_EqRel_of_V_implies_(_not_u_is_zero_&_not_v_is_zero_&_are_Prop_u,v_)_)
assume A2: [u,v] in Proportionality_as_EqRel_of V ; ::_thesis: ( not u is zero & not v is zero & are_Prop u,v )
then  ( u in NonZero V & v in NonZero V ) by Def3;
hence  ( not u is zero & not v is zero ) by STRUCT_0:1; ::_thesis: are_Prop u,v
 ex u1, v1 being Element of V st
( u = u1 & v = v1 & are_Prop u1,v1 ) by A2, Def3;
hence  are_Prop u,v ; ::_thesis: verum
end;
now__::_thesis:_(_not_u_is_zero_&_not_v_is_zero_&_are_Prop_u,v_implies_[u,v]_in_Proportionality_as_EqRel_of_V_)
assume that
A3: ( not u is zero & not v is zero ) and
A4: are_Prop u,v ; ::_thesis: [u,v] in Proportionality_as_EqRel_of V
 ( u in NonZero V & v in NonZero V ) by A3, STRUCT_0:1;
hence  [u,v] in Proportionality_as_EqRel_of V by A4, Def3; ::_thesis: verum
end;
hence  ( [u,v] in Proportionality_as_EqRel_of V iff ( not u is zero & not v is zero & are_Prop u,v ) ) by A1; ::_thesis: verum
end;

definition
let V be RealLinearSpace;
let v be Element of V;
func Dir v ->  Subset of (NonZero V) equals :: ANPROJ_1:def 4
 Class ((Proportionality_as_EqRel_of V),v);
correctness
coherence
Class ((Proportionality_as_EqRel_of V),v) is Subset of (NonZero V);
;
end;

:: deftheorem  defines Dir ANPROJ_1:def_4_:_
 for V being RealLinearSpace
for v being Element of V holds Dir v = Class ((Proportionality_as_EqRel_of V),v);

definition
let V be RealLinearSpace;
func ProjectivePoints V ->  set  means :Def5: :: ANPROJ_1:def 5
 ex Y being Subset-Family of (NonZero V) st
( Y = Class (Proportionality_as_EqRel_of V) & it = Y );
correctness
existence
ex b1 being set ex Y being Subset-Family of (NonZero V) st
( Y = Class (Proportionality_as_EqRel_of V) & b1 = Y );
uniqueness
for b1, b2 being set st ex Y being Subset-Family of (NonZero V) st
( Y = Class (Proportionality_as_EqRel_of V) & b1 = Y ) & ex Y being Subset-Family of (NonZero V) st
( Y = Class (Proportionality_as_EqRel_of V) & b2 = Y ) holds
b1 = b2;
;
end;

:: deftheorem Def5 defines ProjectivePoints ANPROJ_1:def_5_:_
 for V being RealLinearSpace
for b2 being set holds
( b2 = ProjectivePoints V iff ex Y being Subset-Family of (NonZero V) st
( Y = Class (Proportionality_as_EqRel_of V) & b2 = Y ) );

registration
cluster non empty non trivial V79() V80() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() for RLSStruct ;
existence
 ex b1 being RealLinearSpace st
( b1 is strict & not b1 is trivial )
proof
consider V being strict RealLinearSpace such that
A1: 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 ) ) & ( for w being Element of V ex a, b being Real st w = (a * u) + (b * v) ) ) by FUNCSDOM:23;
consider u, v being Element of V such that
A2: for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) and
 for w being Element of V ex a, b being Real st w = (a * u) + (b * v) by A1;
 u <> 0. V
proof
assume A3: u = 0. V ; ::_thesis: contradiction
0. V = (0. V) + (0. V) by RLVECT_1:4
.= (1 * u) + (0. V) by A3, RLVECT_1:def_8
.= (1 * u) + (0 * v) by RLVECT_1:10 ;
hence  contradiction by A2; ::_thesis: verum
end;
then  not V is trivial by STRUCT_0:def_18;
hence  ex b1 being RealLinearSpace st
( b1 is strict & not b1 is trivial ) ; ::_thesis: verum
end;
end;


registration
let V be non trivial RealLinearSpace;
cluster ProjectivePoints V ->  non empty ;
coherence
 not ProjectivePoints V is empty
proof
consider u being Element of V such that
A1: u <> 0. V by STRUCT_0:def_18;
set Y = Dir u;
consider Z being Subset-Family of (NonZero V) such that
A2: Z = Class (Proportionality_as_EqRel_of V) and
A3: ProjectivePoints V = Z by Def5;
 u in NonZero V by A1, ZFMISC_1:56;
then  Dir u in Z by A2, EQREL_1:def_3;
hence  not ProjectivePoints V is empty by A3; ::_thesis: verum
end;
end;

theorem Th21: :: ANPROJ_1:21
for V being non trivial RealLinearSpace
for p being Element of V st not p is zero holds
Dir p is Element of ProjectivePoints V
proof
let V be non trivial RealLinearSpace; ::_thesis: for p being Element of V st not p is zero holds
Dir p is Element of ProjectivePoints V
let p be Element of V; ::_thesis: ( not p is zero implies Dir p is Element of ProjectivePoints V )
assume  not p is zero ; ::_thesis: Dir p is Element of ProjectivePoints V
then  p in NonZero V by STRUCT_0:1;
then  Dir p in Class (Proportionality_as_EqRel_of V) by EQREL_1:def_3;
hence  Dir p is Element of ProjectivePoints V by Def5; ::_thesis: verum
end;

theorem Th22: :: ANPROJ_1:22
for V being non trivial RealLinearSpace
for p, q being Element of V st not p is zero & not q is zero holds
( Dir p = Dir q iff are_Prop p,q )
proof
let V be non trivial RealLinearSpace; ::_thesis: for p, q being Element of V st not p is zero & not q is zero holds
( Dir p = Dir q iff are_Prop p,q )
let p, q be Element of V; ::_thesis: ( not p is zero & not q is zero implies ( Dir p = Dir q iff are_Prop p,q ) )
assume that
A1: not p is zero and
A2: not q is zero ; ::_thesis: ( Dir p = Dir q iff are_Prop p,q )
A3: p in NonZero V by A1, STRUCT_0:1;
A4: now__::_thesis:_(_Dir_p_=_Dir_q_implies_are_Prop_p,q_)
assume  Dir p = Dir q ; ::_thesis: are_Prop p,q
then  [p,q] in Proportionality_as_EqRel_of V by A3, EQREL_1:35;
hence  are_Prop p,q by Th20; ::_thesis: verum
end;
now__::_thesis:_(_are_Prop_p,q_implies_Dir_p_=_Dir_q_)
assume  are_Prop p,q ; ::_thesis: Dir p = Dir q
then  [p,q] in Proportionality_as_EqRel_of V by A1, A2, Th20;
hence  Dir p = Dir q by A3, EQREL_1:35; ::_thesis: verum
end;
hence  ( Dir p = Dir q iff are_Prop p,q ) by A4; ::_thesis: verum
end;

definition
let V be non trivial RealLinearSpace;
func ProjectiveCollinearity V ->  Relation3 of ProjectivePoints V means :Def6: :: ANPROJ_1:def 6
 for x, y, z being set holds
( [x,y,z] in it iff ex p, q, r being Element of V st
( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) );
existence
 ex b1 being Relation3 of ProjectivePoints V st
for x, y, z being set holds
( [x,y,z] in b1 iff ex p, q, r being Element of V st
( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) )
proof
defpred S1[ set ] means  ex p, q, r being Element of V st
( $1 = [(Dir p),(Dir q),(Dir r)] & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep );
set D = ProjectivePoints V;
set XXX = [:(ProjectivePoints V),(ProjectivePoints V),(ProjectivePoints V):];
consider R being set  such that
A1: for xyz being set holds
( xyz in R iff ( xyz in [:(ProjectivePoints V),(ProjectivePoints V),(ProjectivePoints V):] & S1[xyz] ) ) from XBOOLE_0:sch_1();
 for x being set st x in R holds
x in [:(ProjectivePoints V),(ProjectivePoints V),(ProjectivePoints V):] by A1;
then  R c= [:(ProjectivePoints V),(ProjectivePoints V),(ProjectivePoints V):] by TARSKI:def_3;
then reconsider R9 = R as Relation3 of ProjectivePoints V by COLLSP:def_1;
take  R9 ; ::_thesis: for x, y, z being set holds
( [x,y,z] in R9 iff ex p, q, r being Element of V st
( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) )
let x, y, z be set ; ::_thesis: ( [x,y,z] in R9 iff ex p, q, r being Element of V st
( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) )
A2: now__::_thesis:_(_ex_p,_q,_r_being_Element_of_V_st_
(_x_=_Dir_p_&_y_=_Dir_q_&_z_=_Dir_r_&_not_p_is_zero_&_not_q_is_zero_&_not_r_is_zero_&_p,q,r_are_LinDep_)_implies_[x,y,z]_in_R9_)
set xyz = [x,y,z];
given p, q, r being Element of V such that A3: ( x = Dir p & y = Dir q & z = Dir r ) and
A4: ( not p is zero & not q is zero ) and
A5: not r is zero and
A6: p,q,r are_LinDep ; ::_thesis: [x,y,z] in R9
A7: Dir r is Element of ProjectivePoints V by A5, Th21;
 ( Dir p is Element of ProjectivePoints V & Dir q is Element of ProjectivePoints V ) by A4, Th21;
then  [x,y,z] in [:(ProjectivePoints V),(ProjectivePoints V),(ProjectivePoints V):] by A3, A7, MCART_1:69;
hence  [x,y,z] in R9 by A1, A3, A4, A5, A6; ::_thesis: verum
end;
now__::_thesis:_(_[x,y,z]_in_R9_implies_ex_p,_q,_r_being_Element_of_V_st_
(_x_=_Dir_p_&_y_=_Dir_q_&_z_=_Dir_r_&_not_p_is_zero_&_not_q_is_zero_&_not_r_is_zero_&_p,q,r_are_LinDep_)_)
assume  [x,y,z] in R9 ; ::_thesis: ex p, q, r being Element of V st
( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep )
then consider p, q, r being Element of V such that
A8: [x,y,z] = [(Dir p),(Dir q),(Dir r)] and
A9: ( not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) by A1;
A10: z = Dir r by A8, XTUPLE_0:3;
 ( x = Dir p & y = Dir q ) by A8, XTUPLE_0:3;
hence  ex p, q, r being Element of V st
( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) by A9, A10; ::_thesis: verum
end;
hence  ( [x,y,z] in R9 iff ex p, q, r being Element of V st
( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) ) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Relation3 of ProjectivePoints V st ( for x, y, z being set holds
( [x,y,z] in b1 iff ex p, q, r being Element of V st
( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) ) ) & ( for x, y, z being set holds
( [x,y,z] in b2 iff ex p, q, r being Element of V st
( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) ) ) holds
b1 = b2
proof
set X = ProjectivePoints V;
set XXX = [:(ProjectivePoints V),(ProjectivePoints V),(ProjectivePoints V):];
let R1, R2 be Relation3 of ProjectivePoints V; ::_thesis: ( ( for x, y, z being set holds
( [x,y,z] in R1 iff ex p, q, r being Element of V st
( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) ) ) & ( for x, y, z being set holds
( [x,y,z] in R2 iff ex p, q, r being Element of V st
( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) ) ) implies R1 = R2 )
assume that
A11: for x, y, z being set holds
( [x,y,z] in R1 iff ex p, q, r being Element of V st
( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) ) and
A12: for x, y, z being set holds
( [x,y,z] in R2 iff ex p, q, r being Element of V st
( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) ) ; ::_thesis: R1 = R2
A13: R2 c= [:(ProjectivePoints V),(ProjectivePoints V),(ProjectivePoints V):] by COLLSP:def_1;
A14: R1 c= [:(ProjectivePoints V),(ProjectivePoints V),(ProjectivePoints V):] by COLLSP:def_1;
now__::_thesis:_for_u_being_set_holds_
(_u_in_R1_iff_u_in_R2_)
let u be set ; ::_thesis: ( u in R1 iff u in R2 )
A15: now__::_thesis:_(_u_in_R2_implies_u_in_R1_)
assume A16: u in R2 ; ::_thesis: u in R1
then consider x, y, z being Element of ProjectivePoints V such that
A17: u = [x,y,z] by A13, DOMAIN_1:3;
 ex p, q, r being Element of V st
( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) by A12, A16, A17;
hence  u in R1 by A11, A17; ::_thesis: verum
end;
now__::_thesis:_(_u_in_R1_implies_u_in_R2_)
assume A18: u in R1 ; ::_thesis: u in R2
then consider x, y, z being Element of ProjectivePoints V such that
A19: u = [x,y,z] by A14, DOMAIN_1:3;
 ex p, q, r being Element of V st
( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) by A11, A18, A19;
hence  u in R2 by A12, A19; ::_thesis: verum
end;
hence  ( u in R1 iff u in R2 ) by A15; ::_thesis: verum
end;
hence  R1 = R2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines ProjectiveCollinearity ANPROJ_1:def_6_:_
 for V being non trivial RealLinearSpace
for b2 being Relation3 of ProjectivePoints V holds
( b2 = ProjectiveCollinearity V iff for x, y, z being set holds
( [x,y,z] in b2 iff ex p, q, r being Element of V st
( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) ) );

definition
let V be non trivial RealLinearSpace;
func ProjectiveSpace V ->  strict CollStr  equals :: ANPROJ_1:def 7
 CollStr(# (ProjectivePoints V),(ProjectiveCollinearity V) #);
correctness
coherence
CollStr(# (ProjectivePoints V),(ProjectiveCollinearity V) #) is strict CollStr ;
;
end;

:: deftheorem  defines ProjectiveSpace ANPROJ_1:def_7_:_
 for V being non trivial RealLinearSpace holds ProjectiveSpace V = CollStr(# (ProjectivePoints V),(ProjectiveCollinearity V) #);

registration
let V be non trivial RealLinearSpace;
cluster ProjectiveSpace V ->  non empty strict ;
coherence
 not ProjectiveSpace V is empty ;
end;

theorem :: ANPROJ_1:23
for V being non trivial RealLinearSpace holds
( the carrier of (ProjectiveSpace V) = ProjectivePoints V & the Collinearity of (ProjectiveSpace V) = ProjectiveCollinearity V ) ;

theorem :: ANPROJ_1:24
for x, y, z being set
for V being non trivial RealLinearSpace st [x,y,z] in the Collinearity of (ProjectiveSpace V) holds
ex p, q, r being Element of V st
( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) by Def6;

theorem :: ANPROJ_1:25
for V being non trivial RealLinearSpace
for u, v, w being Element of V st not u is zero & not v is zero & not w is zero holds
( [(Dir u),(Dir v),(Dir w)] in the Collinearity of (ProjectiveSpace V) iff u,v,w are_LinDep )
proof
let V be non trivial RealLinearSpace; ::_thesis: for u, v, w being Element of V st not u is zero & not v is zero & not w is zero holds
( [(Dir u),(Dir v),(Dir w)] in the Collinearity of (ProjectiveSpace V) iff u,v,w are_LinDep )
let u, v, w be Element of V; ::_thesis: ( not u is zero & not v is zero & not w is zero implies ( [(Dir u),(Dir v),(Dir w)] in the Collinearity of (ProjectiveSpace V) iff u,v,w are_LinDep ) )
assume that
A1: ( not u is zero & not v is zero ) and
A2: not w is zero ; ::_thesis: ( [(Dir u),(Dir v),(Dir w)] in the Collinearity of (ProjectiveSpace V) iff u,v,w are_LinDep )
now__::_thesis:_(_[(Dir_u),(Dir_v),(Dir_w)]_in_the_Collinearity_of_(ProjectiveSpace_V)_implies_u,v,w_are_LinDep_)
reconsider du = Dir u, dv = Dir v, dw = Dir w as set ;
assume  [(Dir u),(Dir v),(Dir w)] in the Collinearity of (ProjectiveSpace V) ; ::_thesis: u,v,w are_LinDep
then consider p, q, r being Element of V such that
A3: ( du = Dir p & dv = Dir q ) and
A4: dw = Dir r and
A5: ( not p is zero & not q is zero ) and
A6: not r is zero and
A7: p,q,r are_LinDep by Def6;
A8: are_Prop r,w by A2, A4, A6, Th22;
 ( are_Prop p,u & are_Prop q,v ) by A1, A3, A5, Th22;
hence  u,v,w are_LinDep by A7, A8, Th4; ::_thesis: verum
end;
hence  ( [(Dir u),(Dir v),(Dir w)] in the Collinearity of (ProjectiveSpace V) iff u,v,w are_LinDep ) by A1, A2, Def6; ::_thesis: verum
end;

theorem :: ANPROJ_1:26
for x being set
for V being non trivial RealLinearSpace holds
( x is Element of (ProjectiveSpace V) iff ex u being Element of V st
( not u is zero & x = Dir u ) )
proof
let x be set ; ::_thesis: for V being non trivial RealLinearSpace holds
( x is Element of (ProjectiveSpace V) iff ex u being Element of V st
( not u is zero & x = Dir u ) )
let V be non trivial RealLinearSpace; ::_thesis: ( x is Element of (ProjectiveSpace V) iff ex u being Element of V st
( not u is zero & x = Dir u ) )
now__::_thesis:_(_x_is_Element_of_(ProjectiveSpace_V)_implies_ex_y_being_Element_of_V_st_
(_not_y_is_zero_&_x_=_Dir_y_)_)
assume A1: x is Element of (ProjectiveSpace V) ; ::_thesis: ex y being Element of V st
( not y is zero & x = Dir y )
A2: ex Y being Subset-Family of (NonZero V) st
( Y = Class (Proportionality_as_EqRel_of V) & ProjectivePoints V = Y ) by Def5;
then reconsider x9 = x as Subset of (NonZero V) by A1, TARSKI:def_3;
consider y being set  such that
A3: y in NonZero V and
A4: x9 = Class ((Proportionality_as_EqRel_of V),y) by A1, A2, EQREL_1:def_3;
A5: y <> 0. V by A3, ZFMISC_1:56;
reconsider y = y as Element of V by A3;
take y = y; ::_thesis: ( not y is zero & x = Dir y )
thus  not y is zero by A5, STRUCT_0:def_12; ::_thesis: x = Dir y
thus  x = Dir y by A4; ::_thesis: verum
end;
hence  ( x is Element of (ProjectiveSpace V) iff ex u being Element of V st
( not u is zero & x = Dir u ) ) by Th21; ::_thesis: verum
end;