:: ANALOAF semantic presentation

definition
let c1 be RealLinearSpace;
let c2, c3, c4, c5 be VECTOR of c1;
pred a2,a3 // a4,a5 means :E1: :: 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 E1 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) ) ) );

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

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

theorem :: ANALOAF:1
canceled;

theorem :: ANALOAF:2
canceled;

theorem :: ANALOAF:3
canceled;

theorem E4: :: 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 :: ANALOAF:5
canceled;

theorem E5: :: ANALOAF:6
for b1 being RealLinearSpace
for b2, b3, b4 being VECTOR of b1 holds b2 - (b3 - b4) = b2 + (b4 - b3)
proof
let c1 be RealLinearSpace;
let c2, c3, c4 be VECTOR of c1;
thus c2 - (c3 - c4) = c2 + (- (c3 - c4)) by RLVECT_1:def 11
.= c2 + (c4 - c3) by VECTSP_1:81 ;
end;

theorem :: ANALOAF:7
canceled;

theorem :: ANALOAF:8
canceled;

theorem E6: :: 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
.= (c2 + (c3 + (- c3))) - c5 by RLVECT_1:def 11
.= ((c4 + c5) + (- c3)) - c5 by E7, RLVECT_1:def 6
.= ((- c3) + (c4 + c5)) + (- c5) by RLVECT_1:def 11
.= (- c3) + ((c4 + c5) + (- c5)) by RLVECT_1:def 6
.= (- c3) + ((c4 + c5) - c5) by RLVECT_1:def 11
.= c4 + (- c3) by RLSUB_2:78
.= c4 - c3 by RLVECT_1:def 11 ;
end;

theorem E7: :: 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 VECTSP_1:81
.= (c4 * (c3 - c2)) + (- (c4 * (c3 - c2))) by RLVECT_1:39
.= (c4 * (c3 - c2)) - (c4 * (c3 - c2)) by RLVECT_1:def 11
.= 0. c1 by RLVECT_1:28 ;
hence c4 * (c2 - c3) = - (c4 * (c3 - c2)) by RLVECT_1:def 10;
end;

theorem E8: :: 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 VECTSP_1:81
.= (c5 - c4) * (c3 - c2) by RLVECT_1:40 ;
end;

theorem E9: :: ANALOAF:12
for b1 being RealLinearSpace
for b2, b3 being VECTOR of b1
for b4 being Real holds
( ( b4 * b2 = b3 ) implies ( not b4 <> 0 or 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 E10: :: ANALOAF:13
for b1 being RealLinearSpace
for b2, b3 being VECTOR of b1
for b4 being Real holds
( ( ( b4 * b2 = b3 ) implies ( not b4 <> 0 or b2 = (b4 " ) * b3 ) ) & ( ( b2 = (b4 " ) * b3 ) implies ( not b4 <> 0 or 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, E9
.= c4 * c2 ;

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

theorem :: ANALOAF:14
canceled;

theorem :: ANALOAF:15
canceled;

theorem E11: :: 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, E1;
hence ex b1, b2 being Real st
( b1 * (c3 - c2) = b2 * (c5 - c4) & 0 < b1 & 0 < b2 ) by E13;
end;

theorem E12: :: 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 E1;
end;

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

theorem E13: :: 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, E11;
c4 * (c3 - c2) = - (c5 * (c3 - c2)) by E16, E7;
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, E2, RLVECT_1:def 11;
then c3 = - (- c2) by RLVECT_1:def 10
.= c2 by RLVECT_1:30 ;
hence not verum by E15;
end;

theorem E14: :: ANALOAF:20
for b1 being RealLinearSpace
for b2, b3, b4, b5, b6, b7 being VECTOR of b1 holds
( ( b2,b3 // b4,b5 & b2,b3 // b6,b7 ) implies ( not b2 <> b3 or 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, E11;
consider c10, c11 being Real such that
E20: ( c10 * (c3 - c2) = c11 * (c7 - c6) & 0 < c10 & 0 < c11 ) by E15, E17, E18, E11;
E21: c3 - c2 = (c8 " ) * (c9 * (c5 - c4)) by E19, E10
.= ((c8 " ) * c9) * (c5 - c4) by RLVECT_1:def 9 ;
E22: c3 - c2 = (c10 " ) * (c11 * (c7 - c6)) by E20, E10
.= ((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, E1;
end;
hence c4,c5 // c6,c7 by E1;
end;

theorem E15: :: 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, E11;
c6 * (c2 - c3) = - (c7 * (c5 - c4)) by E17, E7
.= c7 * (c4 - c5) by E7 ;
hence ( c3,c2 // c5,c4 & c4,c5 // c2,c3 ) by E17, E1;
end;
hence ( c3,c2 // c5,c4 & c4,c5 // c2,c3 ) by E1;
end;

theorem E16: :: 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, E11;
E19: c6 * (c4 - c2) = c6 * ((c4 - c3) + (c3 - c2)) by E4
.= (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, E2;
hence c2,c3 // c2,c4 by E18, E19, E1;
end;
hence c2,c3 // c2,c4 by E1, E12;
end;

theorem E17: :: 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, E11;
c3 - c4 = (c3 - c2) + (c2 - c4) by E4
.= (c3 - c2) - (c4 - c2) by E5 ;
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 E8 ;
c4 - c3 = (c4 - c2) + (c2 - c3) by E4
.= (c4 - c2) - (c3 - c2) by E5 ;
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 E8 ;
E22: now
assume E23: c5 = c6 ;
(- c2) + c3 = c3 - c2 by RLVECT_1:def 11
.= c4 - c2 by E19, E23, RLVECT_1:50
.= (- c2) + c4 by RLVECT_1:def 11 ;
then c3 = c4 by RLVECT_1:21;
hence not ( not c2,c3 // c3,c4 & not c2,c4 // c4,c3 ) by E1;
end;
now
assume c5 <> c6 ;
then not ( not 0 < c5 - c6 & not 0 < c6 - c5 ) by E3;
then ( c3,c2 // c4,c3 or c4,c2 // c3,c4 ) by E19, E20, E21, E1;
hence not ( not c2,c3 // c3,c4 & not c2,c4 // c4,c3 ) by E15;
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 E1;
end;

theorem E18: :: 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 E1;
end;

theorem E19: :: 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 E6;
hence ( c2 = (c3 + c4) - c5 implies ( c5,c3 // c4,c2 & c5,c4 // c3,c2 ) ) by E18;
end;

theorem E20: :: 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 E1;
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, E1;
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 E19;
now
assume c5 = c7 ;
then c5 = c5 + (c6 - c4) by RLVECT_1:42;
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 E21: :: 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, E1;
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, E11;
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, E1;
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 E4
.= (c2 - c5) - (c2 - c3) by E5 ;
E30: ((((c7 " ) * c6) * (c2 - c5)) + c2) - c4 = (((((c7 " ) * c6) * (c2 - c5)) + c2) - c2) + (c2 - c4) by E4
.= (((((c7 " ) * c6) * (c2 - c5)) + c2) - c2) - (c4 - c2) by E5 ;
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, E10
.= c7 * (((((c7 " ) * c6) * (c2 - c5)) + c2) - c4) by E30, RLVECT_1:48 ;
then c5,c3 // c4,(((c7 " ) * c6) * (c2 - c5)) + c2 by E25, E1;
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 E22: :: 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 by RLVECT_1:def 11;
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 E23: :: 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, E22;
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, E1;
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:def 11
.= (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, E1;
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;

E24: 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 E1;
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 E1;
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, E1;
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 VECTSP_1:81 ;
hence c3,c2 // c4,c5 by E32, E1;
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 VECTSP_1:81
.= c7 * (- (c5 - c4)) by RLVECT_1:39
.= (- c7) * (c5 - c4) by RLVECT_1:38 ;
hence c3,c2 // c4,c5 by E32, E1;
end;
hence not ( not c3,c2 // c4,c5 & not c3,c2 // c5,c4 ) by E25, E29, E30, E31, E1;
end;
hence not ( not c3,c2 // c4,c5 & not c3,c2 // c5,c4 ) by E27, E28;
end;

theorem :: ANALOAF:30
canceled;

theorem E25: :: 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, E1;
end;
then E37: c10 = 0 by E33, E35, XCMPLX_1:6;
E38: c11 <> 0
proof
assume c11 = 0 ;
then c7 - c6 = (0. c1) + (0 * c3) by E29, E37, RLVECT_1:23
.= (0. c1) + (0. c1) by RLVECT_1:23
.= 0. c1 by RLVECT_1:10 ;
then c7 = c6 by RLVECT_1:35;
hence not verum by E27, E1;
end;
E39: c5 - c4 = (0. c1) + (c9 * c3) by E28, E35, RLVECT_1:23
.= c9 * c3 by RLVECT_1:10 ;
E40: c7 - c6 = (0. c1) + (c11 * c3) by E29, E37, RLVECT_1:23
.= c11 * c3 by RLVECT_1:10 ;
E41: (c9 " ) * (c5 - c4) = ((c9 " ) * c9) * c3 by E39, RLVECT_1:def 9
.= 1 * c3 by E36, XCMPLX_0:def 7
.= c3 by RLVECT_1:def 9 ;
(c11 " ) * (c7 - c6) = ((c11 " ) * c11) * c3 by E40, RLVECT_1:def 9
.= 1 * c3 by E38, XCMPLX_0:def 7
.= c3 by RLVECT_1:def 9 ;
then ( (c9 " ) * (c5 - c4) = (c11 " ) * (c7 - c6) & c9 " <> 0 & c11 " <> 0 ) by E36, E38, E41, XCMPLX_1:203;
hence not verum by E27, E24;
end;
E35: now
assume E36: ( c8 <> 0 & c10 = 0 ) ;
c11 <> 0
proof
assume c11 = 0 ;
then c7 - c6 = (0. c1) + (0 * c3) by E29, E36, RLVECT_1:23
.= (0. c1) + (0. c1) by RLVECT_1:23
.= 0. c1 by RLVECT_1:10 ;
then c7 = c6 by RLVECT_1:35;
hence not verum by E27, E1;
end;
hence not verum by E32, E36, XCMPLX_1:6;
end;
E36: now
assume E37: ( c8 <> 0 & c10 <> 0 & c9 = 0 ) ;
then E38: c11 = 0 by E32, XCMPLX_1:6;
E39: c5 - c4 = (c8 * c2) + (0. c1) by E28, E37, RLVECT_1:23
.= c8 * c2 by RLVECT_1:10 ;
E40: c7 - c6 = (c10 * c2) + (0. c1) by E29, E38, RLVECT_1:23
.= c10 * c2 by RLVECT_1:10 ;
E41: (c8 " ) * (c5 - c4) = ((c8 " ) * c8) * c2 by E39, RLVECT_1:def 9
.= 1 * c2 by E37, XCMPLX_0:def 7
.= c2 by RLVECT_1:def 9 ;
(c10 " ) * (c7 - c6) = ((c10 " ) * c10) * c2 by E40, RLVECT_1:def 9
.= 1 * c2 by E37, XCMPLX_0:def 7
.= c2 by RLVECT_1:def 9 ;
then ( (c8 " ) * (c5 - c4) = (c10 " ) * (c7 - c6) & c8 " <> 0 & c10 " <> 0 ) by E37, E41,