:: ANALOAF semantic presentation

definition
let c1 be RealLinearSpace;
let c2, c3, c4, c5 be VECTOR of c1;
pred c2,c3 // c4,c5 means :Def1: :: ANALOAF:def 1
not ( not a2 = a3 & not a4 = a5 & ( for b1, b2 being Real holds
not ( 0 < b1 & 0 < b2 & b1 * (a3 - a2) = b2 * (a5 - a4) ) ) );
end;

:: deftheorem Def1 defines // ANALOAF:def 1 :
for b1 being RealLinearSpace
for b2, b3, b4, b5 being VECTOR of b1 holds
( b2,b3 // b4,b5 iff not ( not b2 = b3 & not b4 = b5 & ( for b6, b7 being Real holds
not ( 0 < b6 & 0 < b7 & b6 * (b3 - b2) = b7 * (b5 - b4) ) ) ) );

Lemma2: for b1, b2 being Real holds
not ( 0 < b1 & 0 < b2 & not 0 < b1 + b2 )
by XREAL_1:36;

Lemma3: for b1, b2 being Real holds
not ( b1 <> b2 & not 0 < b1 - b2 & not 0 < b2 - b1 )
by XREAL_1:57;

theorem Th1: :: ANALOAF:1
canceled;

theorem Th2: :: ANALOAF:2
canceled;

theorem Th3: :: ANALOAF:3
canceled;

theorem Th4: :: ANALOAF:4
for b1 being RealLinearSpace
for b2, b3, b4 being VECTOR of b1 holds (b2 - b3) + (b3 - b4) = b2 - b4
proof
let c1 be RealLinearSpace;
let c2, c3, c4 be VECTOR of c1;
thus (c2 - c3) + (c3 - c4) = c2 - (c3 - (c3 - c4)) by RLVECT_1:43
.= c2 - ((c3 - c3) + c4) by RLVECT_1:43
.= c2 - ((0. c1) + c4) by RLVECT_1:28
.= c2 - c4 by RLVECT_1:10 ;
end;

theorem Th5: :: ANALOAF:5
canceled;

theorem Th6: :: ANALOAF:6
for b1 being RealLinearSpace
for b2, b3, b4 being VECTOR of b1 holds b2 - (b3 - b4) = b2 + (b4 - b3) by RLVECT_1:47;

theorem Th7: :: ANALOAF:7
canceled;

theorem Th8: :: ANALOAF:8
canceled;

theorem Th9: :: ANALOAF:9
for b1 being RealLinearSpace
for b2, b3, b4, b5 being VECTOR of b1 holds
( b2 + b3 = b4 + b5 implies b2 - b5 = b4 - b3 )
proof
let c1 be RealLinearSpace;
let c2, c3, c4, c5 be VECTOR of c1;
assume E7: c2 + c3 = c4 + c5 ;
thus c2 - c5 = (c2 + (0. c1)) - c5 by RLVECT_1:10
.= (c2 + (c3 - c3)) - c5 by RLVECT_1:28
.= ((c4 + c5) + (- c3)) - c5 by E7, RLVECT_1:def 6
.= (- c3) + ((c4 + c5) - c5) by RLVECT_1:def 6
.= c4 - c3 by RLSUB_2:78 ;
end;

theorem Th10: :: ANALOAF:10
for b1 being RealLinearSpace
for b2, b3 being VECTOR of b1
for b4 being Real holds b4 * (b2 - b3) = - (b4 * (b3 - b2))
proof
let c1 be RealLinearSpace;
let c2, c3 be VECTOR of c1;
let c4 be Real;
(c4 * (c3 - c2)) + (c4 * (c2 - c3)) = (c4 * (c3 - c2)) + (c4 * (- (c3 - c2))) by RLVECT_1:47
.= (c4 * (c3 - c2)) - (c4 * (c3 - c2)) by RLVECT_1:39
.= 0. c1 by RLVECT_1:28 ;
hence c4 * (c2 - c3) = - (c4 * (c3 - c2)) by RLVECT_1:def 10;
end;

theorem Th11: :: ANALOAF:11
for b1 being RealLinearSpace
for b2, b3 being VECTOR of b1
for b4, b5 being Real holds (b4 - b5) * (b2 - b3) = (b5 - b4) * (b3 - b2)
proof
let c1 be RealLinearSpace;
let c2, c3 be VECTOR of c1;
let c4, c5 be Real;
thus (c4 - c5) * (c2 - c3) = (- (c5 - c4)) * (- (c3 - c2)) by RLVECT_1:47
.= (c5 - c4) * (c3 - c2) by RLVECT_1:40 ;
end;

theorem Th12: :: ANALOAF:12
for b1 being RealLinearSpace
for b2, b3 being VECTOR of b1
for b4 being Real holds
( b4 <> 0 & b4 * b2 = b3 implies b2 = (b4 " ) * b3 )
proof
let c1 be RealLinearSpace;
let c2, c3 be VECTOR of c1;
let c4 be Real;
assume that
E10: c4 <> 0 and
E11: c4 * c2 = c3 ;
thus c2 = 1 * c2 by RLVECT_1:def 9
.= ((c4 " ) * c4) * c2 by E10, XCMPLX_0:def 7
.= (c4 " ) * c3 by E11, RLVECT_1:def 9 ;
end;

theorem Th13: :: ANALOAF:13
for b1 being RealLinearSpace
for b2, b3 being VECTOR of b1
for b4 being Real holds
( ( b4 <> 0 & b4 * b2 = b3 implies b2 = (b4 " ) * b3 ) & ( b4 <> 0 & b2 = (b4 " ) * b3 implies b4 * b2 = b3 ) )
proof
let c1 be RealLinearSpace;
let c2, c3 be VECTOR of c1;
let c4 be Real;
now
assume that
E11: c4 <> 0 and
E12: c2 = (c4 " ) * c3 ;
c4 " <> 0 by E11, XCMPLX_1:203;
hence c3 = ((c4 " ) " ) * c2 by E12, Th12
.= c4 * c2 ;

end;
hence ( ( c4 <> 0 & c4 * c2 = c3 implies c2 = (c4 " ) * c3 ) & ( c4 <> 0 & c2 = (c4 " ) * c3 implies c4 * c2 = c3 ) ) by Th12;
end;

theorem Th14: :: ANALOAF:14
canceled;

theorem Th15: :: ANALOAF:15
canceled;

theorem Th16: :: ANALOAF:16
for b1 being RealLinearSpace
for b2, b3, b4, b5 being VECTOR of b1 holds
not ( b2,b3 // b4,b5 & b2 <> b3 & b4 <> b5 & ( for b6, b7 being Real holds
not ( b6 * (b3 - b2) = b7 * (b5 - b4) & 0 < b6 & 0 < b7 ) ) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4, c5 be VECTOR of c1;
assume that
E12: c2,c3 // c4,c5 and
E13: ( c2 <> c3 & c4 <> c5 ) ;
not ( not c2 = c3 & not c4 = c5 & ( for b1, b2 being Real holds
not ( 0 < b1 & 0 < b2 & b1 * (c3 - c2) = b2 * (c5 - c4) ) ) ) by E12, Def1;
hence ex b1, b2 being Real st
( b1 * (c3 - c2) = b2 * (c5 - c4) & 0 < b1 & 0 < b2 ) by E13;
end;

theorem Th17: :: ANALOAF:17
for b1 being RealLinearSpace
for b2, b3 being VECTOR of b1 holds b2,b3 // b2,b3
proof
let c1 be RealLinearSpace;
let c2, c3 be VECTOR of c1;
( 1 * (c3 - c2) = 1 * (c3 - c2) & 0 < 1 ) ;
hence c2,c3 // c2,c3 by Def1;
end;

theorem Th18: :: ANALOAF:18
for b1 being RealLinearSpace
for b2, b3, b4 being VECTOR of b1 holds
( b2,b3 // b4,b4 & b2,b2 // b3,b4 ) by Def1;

theorem Th19: :: ANALOAF:19
for b1 being RealLinearSpace
for b2, b3 being VECTOR of b1 holds
( b2,b3 // b3,b2 implies b2 = b3 )
proof
let c1 be RealLinearSpace;
let c2, c3 be VECTOR of c1;
assume E14: c2,c3 // c3,c2 ;
assume E15: c2 <> c3 ;
then consider c4, c5 being Real such that
E16: ( c4 * (c3 - c2) = c5 * (c2 - c3) & 0 < c4 & 0 < c5 ) by E14, Th16;
c4 * (c3 - c2) = - (c5 * (c3 - c2)) by E16, Th10;
then (c5 * (c3 - c2)) + (c4 * (c3 - c2)) = 0. c1 by RLVECT_1:16;
then (c5 + c4) * (c3 - c2) = 0. c1 by RLVECT_1:def 9;
then ( c3 - c2 = 0. c1 or c5 + c4 = 0 ) by RLVECT_1:24;
then 0. c1 = (- c2) + c3 by E16, Lemma2;
then c3 = - (- c2) by RLVECT_1:def 10
.= c2 by RLVECT_1:30 ;
hence not verum by E15;
end;

theorem Th20: :: ANALOAF:20
for b1 being RealLinearSpace
for b2, b3, b4, b5, b6, b7 being VECTOR of b1 holds
( b2 <> b3 & b2,b3 // b4,b5 & b2,b3 // b6,b7 implies b4,b5 // b6,b7 )
proof
let c1 be RealLinearSpace;
let c2, c3, c4, c5, c6, c7 be VECTOR of c1;
assume that
E15: c2 <> c3 and
E16: c2,c3 // c4,c5 and
E17: c2,c3 // c6,c7 ;
now
assume E18: ( c4 <> c5 & c6 <> c7 ) ;
then consider c8, c9 being Real such that
E19: ( c8 * (c3 - c2) = c9 * (c5 - c4) & 0 < c8 & 0 < c9 ) by E15, E16, Th16;
consider c10, c11 being Real such that
E20: ( c10 * (c3 - c2) = c11 * (c7 - c6) & 0 < c10 & 0 < c11 ) by E15, E17, E18, Th16;
E21: c3 - c2 = (c8 " ) * (c9 * (c5 - c4)) by E19, Th13
.= ((c8 " ) * c9) * (c5 - c4) by RLVECT_1:def 9 ;
E22: c3 - c2 = (c10 " ) * (c11 * (c7 - c6)) by E20, Th13
.= ((c10 " ) * c11) * (c7 - c6) by RLVECT_1:def 9 ;
( 0 < c8 " & 0 < c10 " ) by E19, E20, XREAL_1:124;
then ( 0 < (c8 " ) * c9 & 0 < (c10 " ) * c11 ) by E19, E20, XREAL_1:131;
hence c4,c5 // c6,c7 by E21, E22, Def1;
end;
hence c4,c5 // c6,c7 by Def1;
end;

theorem Th21: :: ANALOAF:21
for b1 being RealLinearSpace
for b2, b3, b4, b5 being VECTOR of b1 holds
( b2,b3 // b4,b5 implies ( b3,b2 // b5,b4 & b4,b5 // b2,b3 ) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4, c5 be VECTOR of c1;
assume E16: c2,c3 // c4,c5 ;
now
assume ( c2 <> c3 & c4 <> c5 ) ;
then consider c6, c7 being Real such that
E17: ( c6 * (c3 - c2) = c7 * (c5 - c4) & 0 < c6 & 0 < c7 ) by E16, Th16;
c6 * (c2 - c3) = - (c7 * (c5 - c4)) by E17, Th10
.= c7 * (c4 - c5) by Th10 ;
hence ( c3,c2 // c5,c4 & c4,c5 // c2,c3 ) by E17, Def1;
end;
hence ( c3,c2 // c5,c4 & c4,c5 // c2,c3 ) by Def1;
end;

theorem Th22: :: ANALOAF:22
for b1 being RealLinearSpace
for b2, b3, b4 being VECTOR of b1 holds
( b2,b3 // b3,b4 implies b2,b3 // b2,b4 )
proof
let c1 be RealLinearSpace;
let c2, c3, c4 be VECTOR of c1;
assume E17: c2,c3 // c3,c4 ;
now
assume ( c2 <> c3 & c3 <> c4 ) ;
then consider c5, c6 being Real such that
E18: ( c5 * (c3 - c2) = c6 * (c4 - c3) & 0 < c5 & 0 < c6 ) by E17, Th16;
E19: c6 * (c4 - c2) = c6 * ((c4 - c3) + (c3 - c2)) by Th4
.= (c5 * (c3 - c2)) + (c6 * (c3 - c2)) by E18, RLVECT_1:def 9
.= (c5 + c6) * (c3 - c2) by RLVECT_1:def 9 ;
0 < c5 + c6 by E18, Lemma2;
hence c2,c3 // c2,c4 by E18, E19, Def1;
end;
hence c2,c3 // c2,c4 by Def1, Th17;
end;

theorem Th23: :: ANALOAF:23
for b1 being RealLinearSpace
for b2, b3, b4 being VECTOR of b1 holds
not ( b2,b3 // b2,b4 & not b2,b3 // b3,b4 & not b2,b4 // b4,b3 )
proof
let c1 be RealLinearSpace;
let c2, c3, c4 be VECTOR of c1;
assume E18: c2,c3 // c2,c4 ;
now
assume ( c2 <> c3 & c2 <> c4 ) ;
then consider c5, c6 being Real such that
E19: ( c5 * (c3 - c2) = c6 * (c4 - c2) & 0 < c5 & 0 < c6 ) by E18, Th16;
c3 - c4 = (c3 - c2) + (c2 - c4) by Th4
.= (c3 - c2) - (c4 - c2) by Th6 ;
then E20: c6 * (c3 - c4) = (c6 * (c3 - c2)) - (c5 * (c3 - c2)) by E19, RLVECT_1:48
.= (c6 - c5) * (c3 - c2) by RLVECT_1:49
.= (c5 - c6) * (c2 - c3) by Th11 ;
c4 - c3 = (c4 - c2) + (c2 - c3) by Th4
.= (c4 - c2) - (c3 - c2) by Th6 ;
then E21: c5 * (c4 - c3) = (c5 * (c4 - c2)) - (c6 * (c4 - c2)) by E19, RLVECT_1:48
.= (c5 - c6) * (c4 - c2) by RLVECT_1:49
.= (c6 - c5) * (c2 - c4) by Th11 ;
E22: now
assume E23: c5 = c6 ;
(- c2) + c3 = (- c2) + c4 by E19, E23, RLVECT_1:50;
then c3 = c4 by RLVECT_1:21;
hence not ( not c2,c3 // c3,c4 & not c2,c4 // c4,c3 ) by Def1;
end;
now
assume c5 <> c6 ;
then not ( not 0 < c5 - c6 & not 0 < c6 - c5 ) by Lemma3;
then ( c3,c2 // c4,c3 or c4,c2 // c3,c4 ) by E19, E20, E21, Def1;
hence not ( not c2,c3 // c3,c4 & not c2,c4 // c4,c3 ) by Th21;
end;
hence not ( not c2,c3 // c3,c4 & not c2,c4 // c4,c3 ) by E22;
end;
hence not ( not c2,c3 // c3,c4 & not c2,c4 // c4,c3 ) by Def1;
end;

theorem Th24: :: ANALOAF:24
for b1 being RealLinearSpace
for b2, b3, b4, b5 being VECTOR of b1 holds
( b2 - b3 = b4 - b5 implies b3,b2 // b5,b4 )
proof
let c1 be RealLinearSpace;
let c2, c3, c4, c5 be VECTOR of c1;
assume c2 - c3 = c4 - c5 ;
then 1 * (c2 - c3) = 1 * (c4 - c5) ;
hence c3,c2 // c5,c4 by Def1;
end;

theorem Th25: :: ANALOAF:25
for b1 being RealLinearSpace
for b2, b3, b4, b5 being VECTOR of b1 holds
( b2 = (b3 + b4) - b5 implies ( b5,b3 // b4,b2 & b5,b4 // b3,b2 ) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4, c5 be VECTOR of c1;
set c6 = (c3 + c4) - c5;
( ((c3 + c4) - c5) + c5 = c3 + c4 & ((c3 + c4) - c5) + c5 = c4 + c3 ) by RLSUB_2:78;
then ( ((c3 + c4) - c5) - c3 = c4 - c5 & ((c3 + c4) - c5) - c4 = c3 - c5 ) by Th9;
hence ( c2 = (c3 + c4) - c5 implies ( c5,c3 // c4,c2 & c5,c4 // c3,c2 ) ) by Th24;
end;

theorem Th26: :: ANALOAF:26
for b1 being RealLinearSpace holds
( not for b2, b3 being VECTOR of b1 holds not b2 <> b3 implies for b2, b3, b4 being VECTOR of b1 holds
ex b5 being VECTOR of b1 st
( b2,b3 // b4,b5 & b2,b4 // b3,b5 & b3 <> b5 ) )
proof
let c1 be RealLinearSpace;
given c2, c3 being VECTOR of c1 such that E21: c2 <> c3 ;
let c4, c5, c6 be VECTOR of c1;
E22: now
assume E23: c4 = c6 ;
then E24: ( c4,c5 // c6,c4 & c4,c6 // c5,c4 ) by Def1;
now
assume c4 = c5 ;
then ( not ( not c5 <> c2 & not c5 <> c3 ) & c4,c5 // c6,c2 & c4,c6 // c5,c2 & c4,c5 // c6,c3 & c4,c6 // c5,c3 ) by E21, E23, Def1;
hence ex b1 being VECTOR of c1 st
( c4,c5 // c6,b1 & c4,c6 // c5,b1 & c5 <> b1 ) ;
end;
hence ex b1 being VECTOR of c1 st
( c4,c5 // c6,b1 & c4,c6 // c5,b1 & c5 <> b1 ) by E24;
end;
now
assume E23: c4 <> c6 ;
take c7 = (c5 + c6) - c4;
E24: ( c4,c5 // c6,c7 & c4,c6 // c5,c7 ) by Th25;
now
assume c5 = c7 ;
then c5 = c5 + (c6 - c4) by RLVECT_1:def 6;
then c6 - c4 = 0. c1 by RLVECT_1:22;
hence not verum by E23, RLVECT_1:35;
end;
hence ex b1 being VECTOR of c1 st
( c4,c5 // c6,b1 & c4,c6 // c5,b1 & c5 <> b1 ) by E24;
end;
hence ex b1 being VECTOR of c1 st
( c4,c5 // c6,b1 & c4,c6 // c5,b1 & c5 <> b1 ) by E22;
end;

theorem Th27: :: ANALOAF:27
for b1 being RealLinearSpace
for b2, b3, b4, b5 being VECTOR of b1 holds
not ( b2 <> b3 & b3,b2 // b2,b4 & ( for b6 being VECTOR of b1 holds
not ( b5,b2 // b2,b6 & b5,b3 // b4,b6 ) ) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4, c5 be VECTOR of c1;
assume that
E22: c2 <> c3 and
E23: c3,c2 // c2,c4 ;
E24: now
assume E25: c2 = c4 ;
take c6 = c2;
thus ( c5,c2 // c2,c6 & c5,c3 // c4,c6 ) by E25, Def1;
end;
now
assume c2 <> c4 ;
then consider c6, c7 being Real such that
E25: ( c6 * (c2 - c3) = c7 * (c4 - c2) & 0 < c6 & 0 < c7 ) by E22, E23, Th16;
set c8 = (((c7 " ) * c6) * (c2 - c5)) + c2;
E26: 1 * (((((c7 " ) * c6) * (c2 - c5)) + c2) - c2) = ((((c7 " ) * c6) * (c2 - c5)) + c2) - c2 by RLVECT_1:def 9
.= ((c7 " ) * c6) * (c2 - c5) by RLSUB_2:78 ;
0 < c7 " by E25, XREAL_1:124;
then ( 0 < (c7 " ) * c6 & 0 < 1 ) by E25, XREAL_1:131;
then E27: c5,c2 // c2,(((c7 " ) * c6) * (c2 - c5)) + c2 by E26, Def1;
E28: ((((c7 " ) * c6) * (c2 - c5)) + c2) - c2 = ((c7 " ) * c6) * (c2 - c5) by RLSUB_2:78
.= (c7 " ) * (c6 * (c2 - c5)) by RLVECT_1:def 9 ;
E29: c3 - c5 = (c2 - c5) + (c3 - c2) by Th4
.= (c2 - c5) - (c2 - c3) by Th6 ;
E30: ((((c7 " ) * c6) * (c2 - c5)) + c2) - c4 = (((((c7 " ) * c6) * (c2 - c5)) + c2) - c2) + (c2 - c4) by Th4
.= (((((c7 " ) * c6) * (c2 - c5)) + c2) - c2) - (c4 - c2) by Th6 ;
c6 * (c3 - c5) = (c6 * (c2 - c5)) - (c6 * (c2 - c3)) by E29, RLVECT_1:48
.= (c7 * (((((c7 " ) * c6) * (c2 - c5)) + c2) - c2)) - (c7 * (c4 - c2)) by E25, E28, Th13
.= c7 * (((((c7 " ) * c6) * (c2 - c5)) + c2) - c4) by E30, RLVECT_1:48 ;
then c5,c3 // c4,(((c7 " ) * c6) * (c2 - c5)) + c2 by E25, Def1;
hence ex b1 being VECTOR of c1 st
( c5,c2 // c2,b1 & c5,c3 // c4,b1 ) by E27;
end;
hence ex b1 being VECTOR of c1 st
( c5,c2 // c2,b1 & c5,c3 // c4,b1 ) by E24;
end;

theorem Th28: :: ANALOAF:28
for b1 being RealLinearSpace
for b2, b3 being VECTOR of b1 holds
( ( for b4, b5 being Real holds
( (b4 * b2) + (b5 * b3) = 0. b1 implies ( b4 = 0 & b5 = 0 ) ) ) implies ( b2 <> b3 & b2 <> 0. b1 & b3 <> 0. b1 ) )
proof
let c1 be RealLinearSpace;
let c2, c3 be VECTOR of c1;
assume E23: for b1, b2 being Real holds
( (b1 * c2) + (b2 * c3) = 0. c1 implies ( b1 = 0 & b2 = 0 ) ) ;
thus c2 <> c3
proof
assume c2 = c3 ;
then c2 - c3 = 0. c1 by RLVECT_1:28;
then c2 + (- c3) = 0. c1 ;
then (1 * c2) + (- c3) = 0. c1 by RLVECT_1:def 9;
then ( (1 * c2) + ((- 1) * c3) = 0. c1 & 1 <> 0 ) by RLVECT_1:29;
hence not verum by E23;
end;
thus c2 <> 0. c1
proof
assume c2 = 0. c1 ;
then 1 * c2 = 0. c1 by RLVECT_1:23;
then (1 * c2) + (0. c1) = 0. c1 by RLVECT_1:10;
then ( (1 * c2) + (0 * c3) = 0. c1 & 1 <> 0 ) by RLVECT_1:23;
hence not verum by E23;
end;
thus c3 <> 0. c1
proof
assume c3 = 0. c1 ;
then 1 * c3 = 0. c1 by RLVECT_1:23;
then (0. c1) + (1 * c3) = 0. c1 by RLVECT_1:10;
then ( (0 * c2) + (1 * c3) = 0. c1 & 1 <> 0 ) by RLVECT_1:23;
hence not verum by E23;
end;
end;

theorem Th29: :: ANALOAF:29
for b1 being RealLinearSpace holds
not ( ex b2, b3 being VECTOR of b1 st
for b4, b5 being Real holds
( (b4 * b2) + (b5 * b3) = 0. b1 implies ( b4 = 0 & b5 = 0 ) ) & ( for b2, b3, b4, b5 being VECTOR of b1 holds
not ( not b2,b3 // b4,b5 & not b2,b3 // b5,b4 ) ) )
proof
let c1 be RealLinearSpace;
given c2, c3 being VECTOR of c1 such that E24: for b1, b2 being Real holds
( (b1 * c2) + (b2 * c3) = 0. c1 implies ( b1 = 0 & b2 = 0 ) ) ;
E25: ( c2 <> c3 & c2 <> 0. c1 & c3 <> 0. c1 ) by E24, Th28;
E26: not 0. c1,c2 // c3, 0. c1
proof
assume E27: 0. c1,c2 // c3, 0. c1 ;
now
given c4, c5 being Real such that E28: ( 0 < c4 & 0 < c5 & c4 * (c2 - (0. c1)) = c5 * ((0. c1) - c3) ) ;
( c4 * c2 = c4 * (c2 - (0. c1)) & c5 * ((0. c1) - c3) = c5 * (- c3) ) by RLVECT_1:26, RLVECT_1:27;
then c4 * c2 = - (c5 * c3) by E28, RLVECT_1:39;
then (c4 * c2) + (c5 * c3) = 0. c1 by RLVECT_1:16;
hence not verum by E24, E28;
end;
hence not verum by E25, E27, Def1;
end;
not 0. c1,c2 // 0. c1,c3
proof
assume E27: 0. c1,c2 // 0. c1,c3 ;
now
given c4, c5 being Real such that E28: ( 0 < c4 & 0 < c5 & c4 * (c2 - (0. c1)) = c5 * (c3 - (0. c1)) ) ;
( c4 * c2 = c4 * (c2 - (0. c1)) & c5 * (c3 - (0. c1)) = c5 * c3 ) by RLVECT_1:26;
then 0. c1 = (c4 * c2) - (c5 * c3) by E28, RLVECT_1:28
.= (c4 * c2) + (c5 * (- c3)) by RLVECT_1:39
.= (c4 * c2) + ((- c5) * c3) by RLVECT_1:38 ;
hence not verum by E24, E28;
end;
hence not verum by E25, E27, Def1;
end;
hence ex b1, b2, b3, b4 being VECTOR of c1 st
( not b1,b2 // b3,b4 & not b1,b2 // b4,b3 ) by E26;
end;

Lemma24: for b1 being RealLinearSpace
for b2, b3, b4, b5 being VECTOR of b1
for b6, b7 being Real holds
not ( b6 * (b2 - b3) = b7 * (b4 - b5) & not ( not b6 <> 0 & not b7 <> 0 ) & not b3,b2 // b4,b5 & not b3,b2 // b5,b4 )
proof
let c1 be RealLinearSpace;
let c2, c3, c4, c5 be VECTOR of c1;
let c6, c7 be Real;
assume that
E25: c6 * (c2 - c3) = c7 * (c4 - c5) and
E26: not ( not c6 <> 0 & not c7 <> 0 ) ;
E27: now
assume E28: c6 = 0 ;
then 0. c1 = c7 * (c4 - c5) by E25, RLVECT_1:23;
then c4 - c5 = 0. c1 by E26, E28, RLVECT_1:24;
then c4 = c5 by RLVECT_1:35;
hence c3,c2 // c4,c5 by Def1;
end;
E28: now
assume E29: c7 = 0 ;
then 0. c1 = c6 * (c2 - c3) by E25, RLVECT_1:23;
then c2 - c3 = 0. c1 by E26, E29, RLVECT_1:24;
then c3 = c2 by RLVECT_1:35;
hence c3,c2 // c4,c5 by Def1;
end;
now
assume E29: ( c6 <> 0 & c7 <> 0 ) ;
E30: now
assume ( c6 < 0 & c7 < 0 ) ;
then E31: ( 0 < - c6 & 0 < - c7 ) by XREAL_1:60;
(- c6) * (c2 - c3) = c6 * (- (c2 - c3)) by RLVECT_1:38
.= - (c7 * (c4 - c5)) by E25, RLVECT_1:39
.= c7 * (- (c4 - c5)) by RLVECT_1:39
.= (- c7) * (c4 - c5) by RLVECT_1:38 ;
hence c3,c2 // c5,c4 by E31, Def1;
end;
E31: now
assume ( c6 < 0 & 0 < c7 ) ;
then E32: ( 0 < - c6 & 0 < c7 ) by XREAL_1:60;
(- c6) * (c2 - c3) = c6 * (- (c2 - c3)) by RLVECT_1:38
.= - (c7 * (c4 - c5)) by E25, RLVECT_1:39
.= c7 * (- (c4 - c5)) by RLVECT_1:39
.= c7 * (c5 - c4) by RLVECT_1:47 ;
hence c3,c2 // c4,c5 by E32, Def1;
end;
now
assume ( 0 < c6 & c7 < 0 ) ;
then E32: ( 0 < c6 & 0 < - c7 ) by XREAL_1:60;
c6 * (c2 - c3) = - (- (c7 * (c4 - c5))) by E25, RLVECT_1:30
.= - (c7 * (- (c4 - c5))) by RLVECT_1:39
.= - (c7 * (c5 - c4)) by RLVECT_1:47
.= c7 * (- (c5 - c4)) by RLVECT_1:39
.= (- c7) * (c5 - c4) by RLVECT_1:38 ;
hence c3,c2 // c4,c5 by E32, Def1;
end;
hence not ( not c3,c2 // c4,c5 & not c3,c2 // c5,c4 ) by E25, E29, E30, E31, Def1;
end;
hence not ( not c3,c2 // c4,c5 & not c3,c2 // c5,c4 ) by E27, E28;
end;

theorem Th30: :: ANALOAF:30
canceled;

theorem Th31: :: ANALOAF:31
for b1 being RealLinearSpace holds
( ex b2, b3 being VECTOR of b1 st
for b4 being VECTOR of b1 holds
ex b5, b6 being Real st (b5 * b2) + (b6 * b3) = b4 implies for b2, b3, b4, b5 being VECTOR of b1 holds
not ( not b2,b3 // b4,b5 & not b2,b3 // b5,b4 & ( for b6 being VECTOR of b1 holds
not ( ( b2,b3 // b2,b6 or b2,b3 // b6,b2 ) & ( b4,b5 // b4,b6 or b4,b5 // b6,b4 ) ) ) ) )
proof
let c1 be RealLinearSpace;
given c2, c3 being VECTOR of c1 such that E26: for b1 being VECTOR of c1 holds
ex b2, b3 being Real st (b2 * c2) + (b3 * c3) = b1 ;
let c4, c5, c6, c7 be VECTOR of c1;
assume E27: ( not c4,c5 // c6,c7 & not c4,c5 // c7,c6 ) ;
consider c8, c9 being Real such that
E28: (c8 * c2) + (c9 * c3) = c5 - c4 by E26;
consider c10, c11 being Real such that
E29: (c10 * c2) + (c11 * c3) = c7 - c6 by E26;
consider c12, c13 being Real such that
E30: (c12 * c2) + (c13 * c3) = c4 - c6 by E26;
set c14 = (c8 * c11) - (c10 * c9);
E31: now
assume E32: (c8 * c11) - (c10 * c9) = 0 ;
then E33: c8 * c11 = c10 * c9 ;
E34: now
assume E35: c8 = 0 ;
E36: c9 <> 0
proof
assume c9 = 0 ;
then c5 - c4 = (0. c1) + (0 * c3) by E28, E35, RLVECT_1:23
.= (0. c1) + (0. c1) by RLVECT_1:23
.= 0. c1 by RLVECT_1:10 ;
then c4 = c5 by RLVECT_1:35;
hence not verum by E27, Def1;
end;
then E37: c10 = 0 by E33, E35, XCMPLX_1:6;
E38: c11 <> 0
proof
assume