:: ANPROJ_1 semantic presentation

notation
let c1 be RealLinearSpace;
let c2 be Element of c1;
end;

definition
let c1 be RealLinearSpace;
let c2, c3 be Element of c1;
canceled;
pred are_Prop a2,a3 means :E1: :: ANPROJ_1:def 2
ex b1, b2 being Real st
( b1 * a2 = b2 * a3 & b1 <> 0 & b2 <> 0 );
reflexivity
for b1 being Element of c1 holds
ex b2, b3 being Real st
( b2 * b1 = b3 * b1 & b2 <> 0 & b3 <> 0 )
proof
let c4 be Element of c1;
( 1 <> 0 & 1 * c4 = 1 * c4 ) ;
hence ex b1, b2 being Real st
( b1 * c4 = b2 * c4 & b1 <> 0 & b2 <> 0 ) ;
end;
symmetry
for b1, b2 being Element of c1 holds
not ( ex b3, b4 being Real st
( b3 * b1 = b4 * b2 & b3 <> 0 & b4 <> 0 ) & for b3, b4 being Real holds
not ( b3 * b2 = b4 * b1 & b3 <> 0 & b4 <> 0 ) ) ;
end;

:: deftheorem ANPROJ_1:def 1 :
canceled;

:: deftheorem E1 defines are_Prop ANPROJ_1:def 2 :
for b1 being RealLinearSpace
for b2, b3 being Element of b1 holds
( are_Prop b2,b3 iff ex b4, b5 being Real st
( b4 * b2 = b5 * b3 & b4 <> 0 & b5 <> 0 ) );

theorem :: ANPROJ_1:1
canceled;

theorem :: ANPROJ_1:2
canceled;

theorem :: ANPROJ_1:3
canceled;

theorem :: ANPROJ_1:4
canceled;

theorem E2: :: ANPROJ_1:5
for b1 being RealLinearSpace
for b2, b3 being Element of b1 holds
( are_Prop b2,b3 iff ex b4 being Real st
( b4 <> 0 & b2 = b4 * b3 ) )
proof
let c1 be RealLinearSpace;
let c2, c3 be Element of c1;
E3: now
assume are_Prop c2,c3 ;
then consider c4, c5 being Real such that
E4: ( c4 * c2 = c5 * c3 & c4 <> 0 & c5 <> 0 ) by E1;
E5: c2 = 1 * c2 by RLVECT_1:def 9
.= ((c4 " ) * c4) * c2 by E4, XCMPLX_0:def 7
.= (c4 " ) * (c5 * c3) by E4, RLVECT_1:def 9
.= ((c4 " ) * c5) * c3 by RLVECT_1:def 9 ;
c4 " <> 0 by E4, XCMPLX_1:203;
then (c4 " ) * c5 <> 0 by E4, XCMPLX_1:6;
hence ex b1 being Real st
( b1 <> 0 & c2 = b1 * c3 ) by E5;
end;
now
given c4 being Real such that E4: ( c4 <> 0 & c2 = c4 * c3 ) ;
1 * c2 = c4 * c3 by E4, RLVECT_1:def 9;
hence are_Prop c2,c3 by E4, E1;
end;
hence ( are_Prop c2,c3 iff ex b1 being Real st
( b1 <> 0 & c2 = b1 * c3 ) ) by E3;
end;

theorem E3: :: ANPROJ_1:6
for b1 being RealLinearSpace
for b2, b3, b4 being Element of b1 holds
( ( are_Prop b2,b3 & are_Prop b3,b4 ) implies ( are_Prop b2,b4 ) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4 be Element of c1;
assume that E4: are_Prop c2,c3
and E5: are_Prop c3,c4 ;
consider c5, c6 being Real such that
E6: ( c5 * c2 = c6 * c3 & c5 <> 0 & c6 <> 0 ) by E4, E1;
consider c7, c8 being Real such that
E7: ( c7 * c3 = c8 * c4 & c7 <> 0 & c8 <> 0 ) by E5, E1;
((c6 " ) * c5) * c2 = (c6 " ) * (c6 * c3) by E6, RLVECT_1:def 9
.= ((c6 " ) * c6) * c3 by RLVECT_1:def 9
.= 1 * c3 by E6, XCMPLX_0:def 7
.= c3 by RLVECT_1:def 9 ;
then E8: c8 * c4 = (c7 * ((c6 " ) * c5)) * c2 by E7, RLVECT_1:def 9;
c6 " <> 0 by E6, XCMPLX_1:203;
then (c6 " ) * c5 <> 0 by E6, XCMPLX_1:6;
then c7 * ((c6 " ) * c5) <> 0 by E7, XCMPLX_1:6;
hence are_Prop c2,c4 by E7, E8, E1;
end;

theorem E4: :: ANPROJ_1:7
for b1 being RealLinearSpace
for b2 being Element of b1 holds
( are_Prop b2, 0. b1 iff b2 = 0. b1 )
proof
let c1 be RealLinearSpace;
let c2 be Element of c1;
now
assume are_Prop c2, 0. c1 ;
then consider c3, c4 being Real such that
E5: ( c3 * c2 = c4 * (0. c1) & c3 <> 0 & c4 <> 0 ) by E1;
0. c1 = c3 * c2 by E5, RLVECT_1:23;
hence c2 = 0. c1 by E5, RLVECT_1:24;
end;
hence ( are_Prop c2, 0. c1 iff c2 = 0. c1 ) ;
end;

definition
let c1 be RealLinearSpace;
let c2, c3, c4 be Element of c1;
pred a2,a3,a4 are_LinDep means :E5: :: ANPROJ_1:def 3
ex b1, b2, b3 being Real st
( ((b1 * a2) + (b2 * a3)) + (b3 * a4) = 0. a1 & not ( not b1 <> 0 & not b2 <> 0 & not b3 <> 0 ) );
end;

:: deftheorem E5 defines are_LinDep ANPROJ_1:def 3 :
for b1 being RealLinearSpace
for b2, b3, b4 being Element of b1 holds
( b2,b3,b4 are_LinDep iff ex b5, b6, b7 being Real st
( ((b5 * b2) + (b6 * b3)) + (b7 * b4) = 0. b1 & not ( not b5 <> 0 & not b6 <> 0 & not b7 <> 0 ) ) );

theorem :: ANPROJ_1:8
canceled;

theorem E6: :: ANPROJ_1:9
for b1 being RealLinearSpace
for b2, b3, b4, b5, b6, b7 being Element of b1 holds
( ( are_Prop b2,b3 & are_Prop b4,b5 & are_Prop b6,b7 & b2,b4,b6 are_LinDep ) implies ( b3,b5,b7 are_LinDep ) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4, c5, c6, c7 be Element of c1;
assume that E7: ( are_Prop c2,c3 & are_Prop c4,c5 & are_Prop c6,c7 )
and E8: c2,c4,c6 are_LinDep ;
consider c8 being Real such that
E9: ( c8 <> 0 & c2 = c8 * c3 ) by E7, E2;
consider c9 being Real such that
E10: ( c9 <> 0 & c4 = c9 * c5 ) by E7, E2;
consider c10 being Real such that
E11: ( c10 <> 0 & c6 = c10 * c7 ) by E7, E2;
consider c11, c12, c13 being Real such that
E12: ( ((c11 * c2) + (c12 * c4)) + (c13 * c6) = 0. c1 & not ( not c11 <> 0 & not c12 <> 0 & not c13 <> 0 ) ) by E8, E5;
E13: 0. c1 = (((c11 * c8) * c3) + (c12 * (c9 * c5))) + (c13 * (c10 * c7)) by E9, E10, E11, E12, RLVECT_1:def 9
.= (((c11 * c8) * c3) + ((c12 * c9) * c5)) + (c13 * (c10 * c7)) by RLVECT_1:def 9
.= (((c11 * c8) * c3) + ((c12 * c9) * c5)) + ((c13 * c10) * c7) by RLVECT_1:def 9 ;
not ( not c11 * c8 <> 0 & not c12 * c9 <> 0 & not c13 * c10 <> 0 ) by E9, E10, E11, E12, XCMPLX_1:6;
hence c3,c5,c7 are_LinDep by E13, E5;
end;

theorem E7: :: ANPROJ_1:10
for b1 being RealLinearSpace
for b2, b3, b4 being Element of b1 holds
( b2,b3,b4 are_LinDep implies ( b2,b4,b3 are_LinDep & b3,b2,b4 are_LinDep & b4,b3,b2 are_LinDep & b4,b2,b3 are_LinDep & b3,b4,b2 are_LinDep ) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4 be Element of c1;
assume c2,c3,c4 are_LinDep ;
then consider c5, c6, c7 being Real such that
E8: ((c5 * c2) + (c6 * c3)) + (c7 * c4) = 0. c1
and E9: not ( not c5 <> 0 & not c6 <> 0 & not c7 <> 0 ) by E5;
E10: ((c5 * c2) + (c7 * c4)) + (c6 * c3) = 0. c1 by E8, RLVECT_1:def 6;
((c6 * c3) + (c7 * c4)) + (c5 * c2) = 0. c1 by E8, RLVECT_1:def 6;
hence ( c2,c4,c3 are_LinDep & c3,c2,c4 are_LinDep & c4,c3,c2 are_LinDep & c4,c2,c3 are_LinDep & c3,c4,c2 are_LinDep ) by E8, E9, E10, E5;
end;

E8: for b1 being RealLinearSpace
for b2, b3 being Element of b1
for b4, b5 being Real holds
( (b4 * b2) + (b5 * b3) = 0. b1 implies b4 * b2 = (- b5) * b3 )
proof
let c1 be RealLinearSpace;
let c2, c3 be Element of c1;
let c4, c5 be Real;
assume (c4 * c2) + (c5 * c3) = 0. c1 ;
then c4 * c2 = - (c5 * c3) by RLVECT_1:19
.= c5 * (- c3) by RLVECT_1:39 ;
hence c4 * c2 = (- c5) * c3 by RLVECT_1:38;
end;

E9: for b1 being RealLinearSpace
for b2, b3, b4 being Element of b1
for b5, b6, b7 being Real holds
( ( ((b5 * b2) + (b6 * b3)) + (b7 * b4) = 0. b1 ) implies ( not b5 <> 0 or b2 = ((- ((b5 " ) * b6)) * b3) + ((- ((b5 " ) * b7)) * b4) ) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4 be Element of c1;
let c5, c6, c7 be Real;
assume that E10: ((c5 * c2) + (c6 * c3)) + (c7 * c4) = 0. c1
and E11: c5 <> 0 ;
((c5 * c2) + (c6 * c3)) + (c7 * c4) = (c5 * c2) + ((c6 * c3) + (c7 * c4)) by RLVECT_1:def 6;
then c5 * c2 = - ((c6 * c3) + (c7 * c4)) by E10, RLVECT_1:19
.= (- (c6 * c3)) + (- (c7 * c4)) by RLVECT_1:45
.= (c6 * (- c3)) + (- (c7 * c4)) by RLVECT_1:39
.= (c6 * (- c3)) + (c7 * (- c4)) by RLVECT_1:39
.= ((- c6) * c3) + (c7 * (- c4)) by RLVECT_1:38
.= ((- c6) * c3) + ((- c7) * c4) by RLVECT_1:38 ;
hence c2 = (c5 " ) * (((- c6) * c3) + ((- c7) * c4)) by E11, ANALOAF:12
.= ((c5 " ) * ((- c6) * c3)) + ((c5 " ) * ((- c7) * c4)) by RLVECT_1:def 9
.= (((c5 " ) * (- c6)) * c3) + ((c5 " ) * ((- c7) * c4)) by RLVECT_1:def 9
.= ((- ((c5 " ) * c6)) * c3) + (((c5 " ) * (- c7)) * c4) by RLVECT_1:def 9
.= ((- ((c5 " ) * c6)) * c3) + ((- ((c5 " ) * c7)) * c4) ;

end;

theorem E10: :: ANPROJ_1:11
for b1 being RealLinearSpace
for b2, b3, b4 being Element of b1 holds
( ( b2 is is_Prop_Vect & b3 is is_Prop_Vect ) implies ( are_Prop b2,b3 or ( b2,b3,b4 are_LinDep iff ex b5, b6 being Real st b4 = (b5 * b2) + (b6 * b3) ) ) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4 be Element of c1;
assume that E11: ( c2 is is_Prop_Vect & c3 is is_Prop_Vect )
and E12: not are_Prop c2,c3 ;
E13: ( c2 <> 0. c1 & c3 <> 0. c1 ) by E11, RLVECT_1:def 13;
E14: not ( c2,c3,c4 are_LinDep & for b1, b2 being Real holds
not c4 = (b1 * c2) + (b2 * c3) )
proof
assume c2,c3,c4 are_LinDep ;
then c4,c2,c3 are_LinDep by E7;
then consider c5, c6, c7 being Real such that
E15: ((c5 * c4) + (c6 * c2)) + (c7 * c3) = 0. c1
and E16: not ( not c5 <> 0 & not c6 <> 0 & not c7 <> 0 ) by E5;
c5 <> 0
proof
assume E17: c5 = 0 ;
then E18: 0. c1 = ((0. c1) + (c6 * c2)) + (c7 * c3) by E15, RLVECT_1:23
.= (c6 * c2) + (c7 * c3) by RLVECT_1:10 ;
then c6 * c2 = (- c7) * c3 by E8;
then E19: ( c6 = 0 or - c7 = 0 ) by E12, E1;
E20: c6 <> 0
proof
assume E21: c6 = 0 ;
then 0. c1 = (0. c1) + (c7 * c3) by E18, RLVECT_1:23
.= c7 * c3 by RLVECT_1:10 ;
hence not verum by E13, E16, E17, E21, RLVECT_1:24;
end;
c7 <> 0
proof
assume E21: c7 = 0 ;
then 0. c1 = (c6 * c2) + (0. c1) by E18, RLVECT_1:23
.= c6 * c2 by RLVECT_1:10 ;
hence not verum by E13, E16, E17, E21, RLVECT_1:24;
end;
hence not verum by E19, E20;
end;
then c4 = ((- ((c5 " ) * c6)) * c2) + ((- ((c5 " ) * c7)) * c3) by E15, E9;
hence ex b1, b2 being Real st c4 = (b1 * c2) + (b2 * c3) ;
end;
( ex b1, b2 being Real st c4 = (b1 * c2) + (b2 * c3) implies c2,c3,c4 are_LinDep )
proof
given c5, c6 being Real such that E15: c4 = (c5 * c2) + (c6 * c3) ;
0. c1 = ((c5 * c2) + (c6 * c3)) + (- c4) by E15, RLVECT_1:16
.= ((c5 * c2) + (c6 * c3)) + ((- 1) * c4) by RLVECT_1:29 ;
hence c2,c3,c4 are_LinDep by E5;
end;
hence ( c2,c3,c4 are_LinDep iff ex b1, b2 being Real st c4 = (b1 * c2) + (b2 * c3) ) by E14;
end;

E11: for b1 being RealLinearSpace
for b2 being Element of b1
for b3, b4, b5 being Real holds ((b3 + b4) + b5) * b2 = ((b3 * b2) + (b4 * b2)) + (b5 * b2)
proof
let c1 be RealLinearSpace;
let c2 be Element of c1;
let c3, c4, c5 be Real;
thus ((c3 + c4) + c5) * c2 = ((c3 + c4) * c2) + (c5 * c2) by RLVECT_1:def 9
.= ((c3 * c2) + (c4 * c2)) + (c5 * c2) by RLVECT_1:def 9 ;
end;

E12: for b1 being RealLinearSpace
for b2, b3, b4, b5, b6, b7 being Element of b1 holds ((b2 + b3) + b4) + ((b5 + b6) + b7) = ((b2 + b5) + (b3 + b6)) + (b4 + b7)
proof
let c1 be RealLinearSpace;
let c2, c3, c4, c5, c6, c7 be Element of c1;
thus ((c2 + c5) + (c3 + c6)) + (c4 + c7) = (c5 + (c2 + (c3 + c6))) + (c4 + c7) by RLVECT_1:def 6
.= (c5 + (c6 + (c2 + c3))) + (c4 + c7) by RLVECT_1:def 6
.= ((c5 + c6) + (c2 + c3)) + (c4 + c7) by RLVECT_1:def 6
.= (c5 + c6) + ((c2 + c3) + (c4 + c7)) by RLVECT_1:def 6
.= (c5 + c6) + (c7 + ((c2 + c3) + c4)) by RLVECT_1:def 6
.= ((c2 + c3) + c4) + ((c5 + c6) + c7) by RLVECT_1:def 6 ;
end;

E13: for b1 being RealLinearSpace
for b2, b3 being Element of b1
for b4, b5, b6 being Real holds ((b4 * b5) * b2) + ((b4 * b6) * b3) = b4 * ((b5 * b2) + (b6 * b3))
proof
let c1 be RealLinearSpace;
let c2, c3 be Element of c1;
let c4, c5, c6 be Real;
thus ((c4 * c5) * c2) + ((c4 * c6) * c3) = (c4 * (c5 * c2)) + ((c4 * c6) * c3) by RLVECT_1:def 9
.= (c4 * (c5 * c2)) + (c4 * (c6 * c3)) by RLVECT_1:def 9
.= c4 * ((c5 * c2) + (c6 * c3)) by RLVECT_1:def 9 ;
end;

theorem :: ANPROJ_1:12
for b1 being RealLinearSpace
for b2, b3 being Element of b1
for b4, b5, b6, b7 being Real holds
( ( (b4 * b2) + (b5 * b3) = (b6 * b2) + (b7 * b3) & b2 is is_Prop_Vect & b3 is is_Prop_Vect ) implies ( are_Prop b2,b3 or ( b4 = b6 & b5 = b7 ) ) )
proof
let c1 be RealLinearSpace;
let c2, c3 be Element of c1;
let c4, c5, c6, c7 be Real;
assume E14: ( not are_Prop c2,c3 & (c4 * c2) + (c5 * c3) = (c6 * c2) + (c7 * c3) & c2 is is_Prop_Vect & c3 is is_Prop_Vect ) ;
then E15: ( c2 <> 0. c1 & c3 <> 0. c1 ) by RLVECT_1:def 13;
E16: (c4 - c6) * c2 = (c7 - c5) * c3
proof
((c6 * c2) + (c7 * c3)) + (- (c5 * c3)) = (c4 * c2) + ((c5 * c3) + (- (c5 * c3))) by E14, RLVECT_1:def 6
.= (c4 * c2) + (0. c1) by RLVECT_1:16
.= c4 * c2 by RLVECT_1:10 ;
then c4 * c2 = ((c7 * c3) + (- (c5 * c3))) + (c6 * c2) by RLVECT_1:def 6
.= ((c7 * c3) - (c5 * c3)) + (c6 * c2) by RLVECT_1:def 11
.= ((c7 - c5) * c3) + (c6 * c2) by RLVECT_1:49 ;
then (c4 * c2) + (- (c6 * c2)) = ((c7 - c5) * c3) + ((c6 * c2) + (- (c6 * c2))) by RLVECT_1:def 6
.= ((c7 - c5) * c3) + (0. c1) by RLVECT_1:16
.= (c7 - c5) * c3 by RLVECT_1:10 ;
hence (c7 - c5) * c3 = (c4 * c2) - (c6 * c2) by RLVECT_1:def 11
.= (c4 - c6) * c2 by RLVECT_1:49 ;

end;
E17: now
assume E18: c4 - c6 = 0 ;
then (c7 - c5) * c3 = 0. c1 by E16, RLVECT_1:23;
then c7 - c5 = 0 by E15, RLVECT_1:24;
hence ( c4 = c6 & c5 = c7 ) by E18;
end;
now
assume E18: c7 - c5 = 0 ;
then (c4 - c6) * c2 = 0. c1 by E16, RLVECT_1:23;
then c4 - c6 = 0 by E15, RLVECT_1:24;
hence ( c4 = c6 & c5 = c7 ) by E18;
end;
hence ( c4 = c6 & c5 = c7 ) by E14, E16, E17, E1;
end;

E14: for b1 being RealLinearSpace
for b2, b3, b4 being Element of b1
for b5, b6 being Real holds
( b2 + (b5 * b3) = b4 + (b6 * b3) implies ((b5 - b6) * b3) + b2 = b4 )
proof
let c1 be RealLinearSpace;
let c2, c3, c4 be Element of c1;
let c5, c6 be Real;
assume c2 + (c5 * c3) = c4 + (c6 * c3) ;
then (c2 + (c5 * c3)) + (- (c6 * c3)) = c4 + ((c6 * c3) + (- (c6 * c3))) by RLVECT_1:def 6
.= c4 + (0. c1) by RLVECT_1:16
.= c4 by RLVECT_1:10 ;
then c4 = c2 + ((c5 * c3) + (- (c6 * c3))) by RLVECT_1:def 6
.= c2 + ((c5 * c3) - (c6 * c3)) by RLVECT_1:def 11
.= c2 + ((c5 - c6) * c3) by RLVECT_1:49 ;
hence ((c5 - c6) * c3) + c2 = c4 ;
end;

theorem :: ANPROJ_1:13
for b1 being RealLinearSpace
for b2, b3, b4 being Element of b1
for b5, b6, b7, b8, b9, b10 being Real holds
( ( ((b5 * b2) + (b6 * b3)) + (b7 * b4) = ((b8 * b2) + (b9 * b3)) + (b10 * b4) ) implies ( b2,b3,b4 are_LinDep or ( b5 = b8 & b6 = b9 & b7 = b10 ) ) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4 be Element of c1;
let c5, c6, c7, c8, c9, c10 be Real;
assume that E15: not c2,c3,c4 are_LinDep
and E16: ((c5 * c2) + (c6 * c3)) + (c7 * c4) = ((c8 * c2) + (c9 * c3)) + (c10 * c4) ;
( ((c5 * c2) + (c6 * c3)) + (c7 * c4) = ((c8 * c2) + (c9 * c3)) + (c10 * c4) implies (((c5 - c8) * c2) + ((c6 - c9) * c3)) + ((c7 - c10) * c4) = 0. c1 )
proof
assume ((c5 * c2) + (c6 * c3)) + (c7 * c4) = ((c8 * c2) + (c9 * c3)) + (c10 * c4) ;
then ((c7 - c10) * c4) + ((c5 * c2) + (c6 * c3)) = (c8 * c2) + (c9 * c3) by E14;
then (((c7 - c10) * c4) + (c5 * c2)) + (c6 * c3) = (c8 * c2) + (c9 * c3) by RLVECT_1:def 6;
then ((c6 - c9) * c3) + (((c7 - c10) * c4) + (c5 * c2)) = c8 * c2 by E14;
then (((c6 - c9) * c3) + ((c7 - c10) * c4)) + (c5 * c2) = c8 * c2 by RLVECT_1:def 6;
then (((c6 - c9) * c3) + ((c7 - c10) * c4)) + (c5 * c2) = (0. c1) + (c8 * c2) by RLVECT_1:10;
then ((c5 - c8) * c2) + (((c6 - c9) * c3) + ((c7 - c10) * c4)) = 0. c1 by E14;
hence (((c5 - c8) * c2) + ((c6 - c9) * c3)) + ((c7 - c10) * c4) = 0. c1 by RLVECT_1:def 6;
end;
then ( c5 - c8 = 0 & c6 - c9 = 0 & c7 - c10 = 0 ) by E15, E16, E5;
hence ( c5 = c8 & c6 = c9 & c7 = c10 ) ;
end;

theorem E15: :: ANPROJ_1:14
for b1 being RealLinearSpace
for b2, b3, b4, b5 being Element of b1
for b6, b7, b8, b9 being Real holds
not ( not are_Prop b2,b3 & b4 = (b6 * b2) + (b7 * b3) & b5 = (b8 * b2) + (b9 * b3) & (b6 * b9) - (b8 * b7) = 0 & b2 is is_Prop_Vect & b3 is is_Prop_Vect & not are_Prop b4,b5 & not b4 = 0. b1 & not b5 = 0. b1 )
proof
let c1 be RealLinearSpace;
let c2, c3, c4, c5 be Element of c1;
let c6, c7, c8, c9 be Real;
assume E16: ( not are_Prop c2,c3 & c4 = (c6 * c2) + (c7 * c3) & c5 = (c8 * c2) + (c9 * c3) & (c6 * c9) - (c8 * c7) = 0 & c2 is is_Prop_Vect & c3 is is_Prop_Vect ) ;
then E17: c6 * c9 = c8 * c7 ;
now
assume ( c4 <> 0. c1 & c5 <> 0. c1 ) ;
E18: for b1, b2, b3, b4 being Element of c1
for b5, b6, b7, b8 being Real holds
( ( b3 = (b5 * b1) + (b7 * b2) & b4 = (b6 * b1) + (b8 * b2) & (b5 * b8) - (b6 * b7) = 0 & b1 is is_Prop_Vect & b2 is is_Prop_Vect & b5 = 0 ) implies ( are_Prop b1,b2 or not b3 <> 0. c1 or not b4 <> 0. c1 or are_Prop b3,b4 ) )
proof
let c10, c11, c12, c13 be Element of c1;
let c14, c15, c16, c17 be Real;
assume that E19: ( not are_Prop c10,c11 & c12 = (c14 * c10) + (c16 * c11) & c13 = (c15 * c10) + (c17 * c11) & (c14 * c17) - (c15 * c16) = 0 & c10 is is_Prop_Vect & c11 is is_Prop_Vect )
and E20: c14 = 0
and E21: ( c12 <> 0. c1 & c13 <> 0. c1 ) ;
0 = - (c15 * c16) by E19, E20
.= (- c15) * c16 ;
then E22: ( - c15 = 0 or c16 = 0 ) by XCMPLX_1:6;
E23: now
assume c16 = 0 ;
then c12 = (0. c1) + (0 * c11) by E19, E20, RLVECT_1:23
.= (0. c1) + (0. c1) by RLVECT_1:23 ;
hence not verum by E21, RLVECT_1:10;
end;
then E24: ( c15 = 0 & c16 <> 0 ) by E22;
E25: c16 " <> 0 by E23, XCMPLX_1:203;
( c12 = (0. c1) + (c16 * c11) & c13 = (0. c1) + (c17 * c11) ) by E19, E20, E24, RLVECT_1:23;
then ( c12 = c16 * c11 & c13 = c17 * c11 ) by RLVECT_1:10;
then c13 = c17 * ((c16 " ) * c12) by E23, ANALOAF:12;
then c13 = (c17 * (c16 " )) * c12 by RLVECT_1:def 9;
then E26: ( 1 * c13 = (c17 * (c16 " )) * c12 & 1 <> 0 ) by RLVECT_1:def 9;
now
assume c17 * (c16 " ) = 0 ;
then c17 = 0 by E25, XCMPLX_1:6;
then c13 = (0. c1) + (0 * c11) by E19, E24, RLVECT_1:23
.= (0. c1) + (0. c1) by RLVECT_1:23 ;
hence not verum by E21, RLVECT_1:10;
end;
hence are_Prop c12,c13 by E26, E1;
end;
now
assume E19: ( c6 <> 0 & c8 <> 0 ) ;
E20: now
assume E21: c7 = 0 ;
then c9 = 0 by E16, E19, XCMPLX_1:6;
then ( c4 = (c6 * c2) + (0. c1) & c5 = (c8 * c2) + (0. c1) ) by E16, E21, RLVECT_1:23;
then E22: ( c4 = c6 * c2 & c5 = c8 * c2 & c6 " <> 0 ) by E19, RLVECT_1:10, XCMPLX_1:203;
then c5 = c8 * ((c6 " ) * c4) by E19, ANALOAF:12
.= (c8 * (c6 " )) * c4 by RLVECT_1:def 9 ;
then ( 1 * c5 = (c8 * (c6 " )) * c4 & c8 * (c6 " ) <> 0 & 1 <> 0 ) by E19, E22, RLVECT_1:def 9, XCMPLX_1:6;
hence are_Prop c4,c5 by E1;
end;
now
assume E21: c7 <> 0 ;
E22: ( c9 * c4 = ((c6 * c9) * c2) + ((c9 * c7) * c3) & c7 * c5 = ((c8 * c7) * c2) + ((c7 * c9) * c3) ) by E16, E13;
c9 <> 0 by E17, E19, E21, XCMPLX_1:6;
hence are_Prop c4,c5 by E17, E21, E22, E1;
end;
hence not ( not are_Prop c4,c5 & not c4 = 0. c1 & not c5 = 0. c1 ) by E20;
end;
hence not ( not are_Prop c4,c5 & not c4 = 0. c1 & not c5 = 0. c1 ) by E16, E18;
end;
hence not ( not are_Prop c4,c5 & not c4 = 0. c1 & not c5 = 0. c1 ) ;
end;

theorem E16: :: ANPROJ_1:15
for b1 being RealLinearSpace
for b2, b3, b4 being Element of b1 holds
( not ( not b2 = 0. b1 & not b3 = 0. b1 & not b4 = 0. b1 ) implies b2,b3,b4 are_LinDep )
proof
let c1 be RealLinearSpace;
let c2, c3, c4 be Element of c1;
assume E17: not ( not c2 = 0. c1 & not c3 = 0. c1 & not c4 = 0. c1 ) ;
E18: for b1, b2, b3 being Element of c1 holds
( b1 = 0. c1 implies b1,b2,b3 are_LinDep )
proof
let c5, c6, c7 be Element of c1;
assume E19: c5 = 0. c1 ;
0. c1 = (0. c1) + (0. c1) by RLVECT_1:10
.= (1 * c5) + (0. c1) by E19, RLVECT_1:23
.= (1 * c5) + (0 * c6) by RLVECT_1:23
.= ((1 * c5) + (0 * c6)) + (0. c1) by RLVECT_1:10
.= ((1 * c5) + (0 * c6)) + (0 * c7) by RLVECT_1:23 ;
hence c5,c6,c7 are_LinDep by E5;
end;
E19: now
assume c3 = 0. c1 ;
then c3,c4,c2 are_LinDep by E18;
hence c2,c3,c4 are_LinDep by E7;
end;
now
assume c4 = 0. c1 ;
then c4,c2,c3 are_LinDep by E18;
hence c2,c3,c4 are_LinDep by E7;
end;
hence c2,c3,c4 are_LinDep by E17, E18, E19;
end;

theorem E17: :: ANPROJ_1:16
for b1 being RealLinearSpace
for b2, b3, b4 being Element of b1 holds
( not ( not are_Prop b2,b3 & not are_Prop b4,b2 & not are_Prop b3,b4 ) implies b4,b2,b3 are_LinDep )
proof
let c1 be RealLinearSpace;
let c2, c3, c4 be Element of c1;
assume E18: not ( not are_Prop c2,c3 & not are_Prop c4,c2 & not are_Prop c3,c4 ) ;
E19: for b1, b2, b3 being Element of c1 holds
( are_Prop b1,b2 implies b3,b1,b2 are_LinDep )
proof
let c5, c6, c7 be Element of c1;
assume are_Prop c5,c6 ;
then consider c8, c9 being Real such that
E20: ( c8 * c5 = c9 * c6 & c8 <> 0 & c9 <> 0 ) by E1;
E21: 0. c1 = (c8 * c5) + (- (c9 * c6)) by E20, RLVECT_1:16
.= (c8 * c5) + ((- 1) * (c9 * c6)) by RLVECT_1:29
.= (c8 * c5) + (((- 1) * c9) * c6) by RLVECT_1:def 9 ;
0 * c7 = 0. c1 by RLVECT_1:23;
then 0. c1 = ((0 * c7) + (c8 * c5)) + (((- 1) * c9) * c6) by E21, RLVECT_1:10;
hence c7,c5,c6 are_LinDep by E20, E5;
end;
E20: now
assume are_Prop c4,c2 ;
then c3,c4,c2 are_LinDep by E19;
hence c4,c2,c3 are_LinDep by E7;
end;
now
assume are_Prop c3,c4 ;
then c2,c3,c4 are_LinDep by E19;
hence c4,c2,c3 are_LinDep by E7;
end;
hence c4,c2,c3 are_LinDep by E18, E19, E20;
end;

theorem E18<