:: ANALMETR semantic presentation

E1: for b1 being RealLinearSpace
for b2, b3, b4, b5 being VECTOR of b1
for b6, b7, b8, b9 being Real holds
( ( b2 = (b6 * b3) + (b7 * b4) & b5 = (b8 * b3) + (b9 * b4) ) implies ( ( b2 + b5 = ((b6 + b8) * b3) + ((b7 + b9) * b4) & b2 - b5 = ((b6 - b8) * b3) + ((b7 - b9) * b4) ) ) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4, c5 be VECTOR of c1;
let c6, c7, c8, c9 be Real;
assume that
E2: c2 = (c6 * c3) + (c7 * c4) and
E3: c5 = (c8 * c3) + (c9 * c4) ;
thus c2 + c5 = (((c6 * c3) + (c7 * c4)) + (c8 * c3)) + (c9 * c4) by E2, E3, RLVECT_1:def 6
.= (((c6 * c3) + (c8 * c3)) + (c7 * c4)) + (c9 * c4) by RLVECT_1:def 6
.= (((c6 + c8) * c3) + (c7 * c4)) + (c9 * c4) by RLVECT_1:def 9
.= ((c6 + c8) * c3) + ((c7 * c4) + (c9 * c4)) by RLVECT_1:def 6
.= ((c6 + c8) * c3) + ((c7 + c9) * c4) by RLVECT_1:def 9 ;
thus c2 - c5 = ((c6 * c3) + (c7 * c4)) + (- ((c8 * c3) + (c9 * c4))) by E2, E3
.= ((c6 * c3) + (c7 * c4)) + ((- (c8 * c3)) + (- (c9 * c4))) by RLVECT_1:45
.= ((c6 * c3) + (c7 * c4)) + ((c8 * (- c3)) + (- (c9 * c4))) by RLVECT_1:39
.= ((c6 * c3) + (c7 * c4)) + ((c8 * (- c3)) + (c9 * (- c4))) by RLVECT_1:39
.= ((c6 * c3) + (c7 * c4)) + (((- c8) * c3) + (c9 * (- c4))) by RLVECT_1:38
.= ((c6 * c3) + (c7 * c4)) + (((- c8) * c3) + ((- c9) * c4)) by RLVECT_1:38
.= (((c6 * c3) + (c7 * c4)) + ((- c8) * c3)) + ((- c9) * c4) by RLVECT_1:def 6
.= (((c6 * c3) + ((- c8) * c3)) + (c7 * c4)) + ((- c9) * c4) by RLVECT_1:def 6
.= (((c6 + (- c8)) * c3) + (c7 * c4)) + ((- c9) * c4) by RLVECT_1:def 9
.= ((c6 + (- c8)) * c3) + ((c7 * c4) + ((- c9) * c4)) by RLVECT_1:def 6
.= ((c6 - c8) * c3) + ((c7 + (- c9)) * c4) by RLVECT_1:def 9
.= ((c6 - c8) * c3) + ((c7 - c9) * c4) ;
end;

E2: for b1 being RealLinearSpace
for b2, b3 being VECTOR of b1 holds (0 * b2) + (0 * b3) = 0. b1
proof
let c1 be RealLinearSpace;
let c2, c3 be VECTOR of c1;
thus (0 * c2) + (0 * c3) = (0. c1) + (0 * c3) by RLVECT_1:23
.= (0. c1) + (0. c1) by RLVECT_1:23
.= 0. c1 by RLVECT_1:10 ;
end;

E3: for b1 being RealLinearSpace
for b2, b3, b4 being VECTOR of b1
for b5, b6, b7 being Real holds
( b2 = (b5 * b3) + (b6 * b4) implies b7 * b2 = ((b7 * b5) * b3) + ((b7 * b6) * b4) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4 be VECTOR of c1;
let c5, c6, c7 be Real;
assume c2 = (c5 * c3) + (c6 * c4) ;
hence c7 * c2 = (c7 * (c5 * c3)) + (c7 * (c6 * c4)) by RLVECT_1:def 9
.= ((c7 * c5) * c3) + (c7 * (c6 * c4)) by RLVECT_1:def 9
.= ((c7 * c5) * c3) + ((c7 * c6) * c4) by RLVECT_1:def 9 ;

end;

definition
let c1 be RealLinearSpace;
let c2, c3 be VECTOR of c1;
pred Gen c2,c3 means :E4: :: ANALMETR:def 1
( ( for b1 being VECTOR of a1 holds
ex b2, b3 being Real st b1 = (b2 * a2) + (b3 * a3) ) & ( for b1, b2 being Real holds
( (b1 * a2) + (b2 * a3) = 0. a1 implies ( b1 = 0 & b2 = 0 ) ) ) );
end;

:: deftheorem E4 defines Gen ANALMETR:def 1 :
for b1 being RealLinearSpace
for b2, b3 being VECTOR of b1 holds
( Gen b2,b3 iff ( ( for b4 being VECTOR of b1 holds
ex b5, b6 being Real st b4 = (b5 * b2) + (b6 * b3) ) & ( for b4, b5 being Real holds
( (b4 * b2) + (b5 * b3) = 0. b1 implies ( b4 = 0 & b5 = 0 ) ) ) ) );

definition
let c1 be RealLinearSpace;
let c2, c3, c4, c5 be VECTOR of c1;
pred c2,c3 are_Ort_wrt c4,c5 means :E5: :: ANALMETR:def 2
ex b1, b2, b3, b4 being Real st
( a2 = (b1 * a4) + (b2 * a5) & a3 = (b3 * a4) + (b4 * a5) & (b1 * b3) + (b2 * b4) = 0 );
end;

:: deftheorem E5 defines are_Ort_wrt ANALMETR:def 2 :
for b1 being RealLinearSpace
for b2, b3, b4, b5 being VECTOR of b1 holds
( b2,b3 are_Ort_wrt b4,b5 iff ex b6, b7, b8, b9 being Real st
( b2 = (b6 * b4) + (b7 * b5) & b3 = (b8 * b4) + (b9 * b5) & (b6 * b8) + (b7 * b9) = 0 ) );

E6: for b1 being RealLinearSpace
for b2, b3 being VECTOR of b1
for b4, b5, b6, b7 being Real holds
( ( Gen b2,b3 & (b4 * b2) + (b5 * b3) = (b6 * b2) + (b7 * b3) ) implies ( ( b4 = b6 & b5 = b7 ) ) )
proof
let c1 be RealLinearSpace;
let c2, c3 be VECTOR of c1;
let c4, c5, c6, c7 be Real;
assume that
E7: Gen c2,c3 and
E8: (c4 * c2) + (c5 * c3) = (c6 * c2) + (c7 * c3) ;
0. c1 = ((c4 * c2) + (c5 * c3)) - ((c6 * c2) + (c7 * c3)) by E8, RLVECT_1:28
.= ((c4 - c6) * c2) + ((c5 - c7) * c3) by E1 ;
then ( (- c6) + c4 = 0 & (- c7) + c5 = 0 ) by E7, E4;
then ( c4 = - (- c6) & c5 = - (- c7) ) ;
hence ( c4 = c6 & c5 = c7 ) ;
end;

theorem :: ANALMETR:1
canceled;

theorem :: ANALMETR:2
canceled;

theorem :: ANALMETR:3
canceled;

theorem :: ANALMETR:4
canceled;

theorem E7: :: ANALMETR:5
for b1 being RealLinearSpace
for b2, b3, b4, b5 being VECTOR of b1 holds
( Gen b4,b5 implies ( b2,b3 are_Ort_wrt b4,b5 iff for b6, b7, b8, b9 being Real holds
( ( b2 = (b6 * b4) + (b7 * b5) & b3 = (b8 * b4) + (b9 * b5) ) implies ( (b6 * b8) + (b7 * b9) = 0 ) ) ) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4, c5 be VECTOR of c1;
assume E8: Gen c4,c5 ;
hereby
assume c2,c3 are_Ort_wrt c4,c5 ;
then consider c6, c7, c8, c9 being Real such that
E9: ( c2 = (c6 * c4) + (c7 * c5) & c3 = (c8 * c4) + (c9 * c5) ) and
E10: (c6 * c8) + (c7 * c9) = 0 by E5;
let c10, c11, c12, c13 be Real;
assume ( c2 = (c10 * c4) + (c11 * c5) & c3 = (c12 * c4) + (c13 * c5) ) ;
then ( c6 = c10 & c7 = c11 & c8 = c12 & c9 = c13 ) by E8, E9, E6;
hence 0 = (c10 * c12) + (c11 * c13) by E10;
end;
assume E9: for b1, b2, b3, b4 being Real holds
( ( c2 = (b1 * c4) + (b2 * c5) & c3 = (b3 * c4) + (b4 * c5) ) implies ( (b1 * b3) + (b2 * b4) = 0 ) ) ;
consider c6, c7 being Real such that
E10: c2 = (c6 * c4) + (c7 * c5) by E8, E4;
consider c8, c9 being Real such that
E11: c3 = (c8 * c4) + (c9 * c5) by E8, E4;
(c6 * c8) + (c7 * c9) = 0 by E9, E10, E11;
hence c2,c3 are_Ort_wrt c4,c5 by E10, E11, E5;
end;

E8: for b1 being RealLinearSpace
for b2, b3 being VECTOR of b1 holds
( Gen b2,b3 implies ( b2 <> 0. b1 & b3 <> 0. b1 ) )
proof
let c1 be RealLinearSpace;
let c2, c3 be VECTOR of c1;
assume E9: Gen c2,c3 ;
thus c2 <> 0. c1
proof
assume c2 = 0. c1 ;
then 0. c1 = 1 * c2 by RLVECT_1:def 9
.= (1 * c2) + (0. c1) by RLVECT_1:10
.= (1 * c2) + (0 * c3) by RLVECT_1:23 ;
hence not verum by E9, E4;
end;
thus c3 <> 0. c1
proof
assume c3 = 0. c1 ;
then 0. c1 = 1 * c3 by RLVECT_1:def 9
.= (0. c1) + (1 * c3) by RLVECT_1:10
.= (0 * c2) + (1 * c3) by RLVECT_1:23 ;
hence not verum by E9, E4;
end;
end;

theorem :: ANALMETR:6
for b1 being RealLinearSpace
for b2, b3 being VECTOR of b1 holds b2,b3 are_Ort_wrt b2,b3
proof
let c1 be RealLinearSpace;
let c2, c3 be VECTOR of c1;
E9: c2 = c2 + (0. c1) by RLVECT_1:10
.= (1 * c2) + (0. c1) by RLVECT_1:def 9
.= (1 * c2) + (0 * c3) by RLVECT_1:23 ;
E10: c3 = (0. c1) + c3 by RLVECT_1:10
.= (0. c1) + (1 * c3) by RLVECT_1:def 9
.= (0 * c2) + (1 * c3) by RLVECT_1:23 ;
(1 * 0) + (0 * 1) = 0 ;
hence c2,c3 are_Ort_wrt c2,c3 by E9, E10, E5;
end;

theorem E9: :: ANALMETR:7
ex b1 being RealLinearSpaceex b2, b3 being VECTOR of b1 st Gen b2,b3
proof
consider c1 being RealLinearSpace such that
E10: ex b1, b2 being VECTOR of c1 st
( ( for b3, b4 being Real holds
( (b3 * b1) + (b4 * b2) = 0. c1 implies ( b3 = 0 & b4 = 0 ) ) ) & ( for b3 being VECTOR of c1 holds
ex b4, b5 being Real st b3 = (b4 * b1) + (b5 * b2) ) ) by FUNCSDOM:37;
consider c2, c3 being VECTOR of c1 such that
E11: ( ( for b1, b2 being Real holds
( (b1 * c2) + (b2 * c3) = 0. c1 implies ( b1 = 0 & b2 = 0 ) ) ) & ( for b1 being VECTOR of c1 holds
ex b2, b3 being Real st b1 = (b2 * c2) + (b3 * c3) ) ) by E10;
take c1 ;
take c2 ;
take c3 ;
thus Gen c2,c3 by E11, E4;
end;

theorem E10: :: ANALMETR:8
for b1 being RealLinearSpace
for b2, b3, b4, b5 being VECTOR of b1 holds
( b2,b3 are_Ort_wrt b4,b5 implies b3,b2 are_Ort_wrt b4,b5 )
proof
let c1 be RealLinearSpace;
let c2, c3, c4, c5 be VECTOR of c1;
assume c2,c3 are_Ort_wrt c4,c5 ;
then consider c6, c7, c8, c9 being Real such that
E11: ( c2 = (c6 * c4) + (c7 * c5) & c3 = (c8 * c4) + (c9 * c5) ) and
E12: (c6 * c8) + (c7 * c9) = 0 by E5;
thus c3,c2 are_Ort_wrt c4,c5 by E11, E12, E5;
end;

theorem E11: :: ANALMETR:9
for b1 being RealLinearSpace
for b2, b3 being VECTOR of b1 holds
( Gen b2,b3 implies for b4, b5 being VECTOR of b1 holds
( b4, 0. b1 are_Ort_wrt b2,b3 & 0. b1,b5 are_Ort_wrt b2,b3 ) )
proof
let c1 be RealLinearSpace;
let c2, c3 be VECTOR of c1;
assume E12: Gen c2,c3 ;
let c4, c5 be VECTOR of c1;
consider c6, c7 being Real such that
E13: c4 = (c6 * c2) + (c7 * c3) by E12, E4;
consider c8, c9 being Real such that
E14: c5 = (c8 * c2) + (c9 * c3) by E12, E4;
E15: 0. c1 = (0. c1) + (0. c1) by RLVECT_1:10
.= (0 * c2) + (0. c1) by RLVECT_1:23
.= (0 * c2) + (0 * c3) by RLVECT_1:23 ;
(c6 * 0) + (c7 * 0) = 0 ;
hence c4, 0. c1 are_Ort_wrt c2,c3 by E13, E15, E5;
(0 * c8) + (0 * c9) = 0 ;
hence 0. c1,c5 are_Ort_wrt c2,c3 by E14, E15, E5;
end;

theorem E12: :: ANALMETR:10
for b1 being RealLinearSpace
for b2, b3, b4, b5 being VECTOR of b1
for b6, b7 being Real holds
( b2,b3 are_Ort_wrt b4,b5 implies b6 * b2,b7 * b3 are_Ort_wrt b4,b5 )
proof
let c1 be RealLinearSpace;
let c2, c3, c4, c5 be VECTOR of c1;
let c6, c7 be Real;
assume c2,c3 are_Ort_wrt c4,c5 ;
then consider c8, c9, c10, c11 being Real such that
E13: ( c2 = (c8 * c4) + (c9 * c5) & c3 = (c10 * c4) + (c11 * c5) ) and
E14: (c8 * c10) + (c9 * c11) = 0 by E5;
E15: c6 * c2 = (c6 * (c8 * c4)) + (c6 * (c9 * c5)) by E13, RLVECT_1:def 9
.= ((c6 * c8) * c4) + (c6 * (c9 * c5)) by RLVECT_1:def 9
.= ((c6 * c8) * c4) + ((c6 * c9) * c5) by RLVECT_1:def 9 ;
E16: c7 * c3 = (c7 * (c10 * c4)) + (c7 * (c11 * c5)) by E13, RLVECT_1:def 9
.= ((c7 * c10) * c4) + (c7 * (c11 * c5)) by RLVECT_1:def 9
.= ((c7 * c10) * c4) + ((c7 * c11) * c5) by RLVECT_1:def 9 ;
((c6 * c8) * (c7 * c10)) + ((c6 * c9) * (c7 * c11)) = ((c8 * c6) * (c10 * c7)) + ((c6 * c9) * (c11 * c7))
.= (((c8 * c6) * c10) * c7) + (((c6 * c9) * c11) * c7)
.= c7 * (((c8 * c6) * c10) + ((c6 * c9) * c11))
.= c7 * (((c6 * c8) * c10) + ((c6 * c9) * c11))
.= c7 * ((c6 * (c8 * c10)) + (c6 * (c9 * c11)))
.= (c7 * c6) * ((c8 * c10) + (c9 * c11))
.= c6 * (c7 * 0) by E14
.= 0 ;
hence c6 * c2,c7 * c3 are_Ort_wrt c4,c5 by E15, E16, E5;
end;

theorem E13: :: ANALMETR:11
for b1 being RealLinearSpace
for b2, b3, b4, b5 being VECTOR of b1
for b6, b7 being Real holds
( b2,b3 are_Ort_wrt b4,b5 implies ( b6 * b2,b3 are_Ort_wrt b4,b5 & b2,b7 * b3 are_Ort_wrt b4,b5 ) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4, c5 be VECTOR of c1;
let c6, c7 be Real;
assume E14: c2,c3 are_Ort_wrt c4,c5 ;
( c3 = 1 * c3 & c2 = 1 * c2 ) by RLVECT_1:def 9;
hence ( c6 * c2,c3 are_Ort_wrt c4,c5 & c2,c7 * c3 are_Ort_wrt c4,c5 ) by E14, E12;
end;

theorem E14: :: ANALMETR:12
for b1 being RealLinearSpace
for b2, b3 being VECTOR of b1 holds
( Gen b2,b3 implies for b4 being VECTOR of b1 holds
ex b5 being VECTOR of b1 st
( b4,b5 are_Ort_wrt b2,b3 & b5 <> 0. b1 ) )
proof
let c1 be RealLinearSpace;
let c2, c3 be VECTOR of c1;
assume E15: Gen c2,c3 ;
let c4 be VECTOR of c1;
consider c5, c6 being Real such that
E16: c4 = (c5 * c2) + (c6 * c3) by E15, E4;
E17: now
assume E18: c4 = 0. c1 ;
take c7 = c2;
thus c4,c7 are_Ort_wrt c2,c3 by E15, E18, E11;
thus c7 <> 0. c1 by E15, E8;
end;
now
assume E18: c4 <> 0. c1 ;
set c7 = (c6 * c2) + ((- c5) * c3);
E19: (c6 * c2) + ((- c5) * c3) <> 0. c1
proof
assume (c6 * c2) + ((- c5) * c3) = 0. c1 ;
then ( c6 = 0 & - c5 = 0 ) by E15, E4;
then c4 = (0 * c2) + (0 * c3) by E16
.= (0 * c2) + (0. c1) by RLVECT_1:23
.= 0 * c2 by RLVECT_1:10
.= 0. c1 by RLVECT_1:23 ;
hence not verum by E18;
end;
E20: (c5 * c6) + (c6 * (- c5)) = 0 ;
take c8 = (c6 * c2) + ((- c5) * c3);
thus c4,c8 are_Ort_wrt c2,c3 by E16, E20, E5;
thus c8 <> 0. c1 by E19;
end;
hence ex b1 being VECTOR of c1 st
( c4,b1 are_Ort_wrt c2,c3 & b1 <> 0. c1 ) by E17;
end;

theorem E15: :: ANALMETR:13
for b1 being RealLinearSpace
for b2, b3, b4, b5, b6 being VECTOR of b1 holds
not ( Gen b2,b3 & b4,b5 are_Ort_wrt b2,b3 & b4,b6 are_Ort_wrt b2,b3 & b4 <> 0. b1 & ( for b7, b8 being Real holds
not ( b7 * b5 = b8 * b6 & not ( not b7 <> 0 & not b8 <> 0 ) ) ) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4, c5, c6 be VECTOR of c1;
assume that
E16: Gen c2,c3 and
E17: c4,c5 are_Ort_wrt c2,c3 and
E18: c4,c6 are_Ort_wrt c2,c3 and
E19: c4 <> 0. c1 ;
consider c7, c8, c9, c10 being Real such that
E20: ( c4 = (c7 * c2) + (c8 * c3) & c5 = (c9 * c2) + (c10 * c3) ) and
E21: (c7 * c9) + (c8 * c10) = 0 by E17, E5;
consider c11, c12, c13, c14 being Real such that
E22: ( c4 = (c11 * c2) + (c12 * c3) & c6 = (c13 * c2) + (c14 * c3) ) and
E23: (c11 * c13) + (c12 * c14) = 0 by E18, E5;
E24: ( c7 = c11 & c8 = c12 ) by E16, E20, E22, E6;
E25: now
assume E26: c7 = 0 ;
then E27: c8 <> 0 by E19, E20, E2;
then E28: c14 = 0 by E23, E24, E26, XCMPLX_1:6;
c10 = 0 by E21, E26, E27, XCMPLX_1:6;
then E29: ( c5 = (c9 * c2) + (0. c1) & c6 = (c13 * c2) + (0. c1) ) by E20, E22, E28, RLVECT_1:23;
then E30: ( c5 = c9 * c2 & c6 = c13 * c2 ) by RLVECT_1:10;
E31: c13 * c5 = c13 * (c9 * c2) by E29, RLVECT_1:10
.= (c9 * c13) * c2 by RLVECT_1:def 9
.= c9 * c6 by E30, RLVECT_1:def 9 ;
now
assume c9 = 0 ;
then 1 * c5 = 0 * c2 by E30, RLVECT_1:def 9
.= 0. c1 by RLVECT_1:23
.= 0 * c6 by RLVECT_1:23 ;
hence ex b1, b2 being Real st
( b1 * c5 = b2 * c6 & not ( not b1 <> 0 & not b2 <> 0 ) ) ;
end;
hence ex b1, b2 being Real st
( b1 * c5 = b2 * c6 & not ( not b1 <> 0 & not b2 <> 0 ) ) by E31;
end;
now
assume E26: c7 <> 0 ;
E27: ( c7 * c9 = - (c8 * c10) & c7 * c13 = - (c8 * c14) ) by E21, E23, E24;
E28: c9 = 1 * c9
.= (c7 * (c7 " )) * c9 by E26, XCMPLX_0:def 7
.= (c7 * c9) * (c7 " )
.= ((- c8) * c10) * (c7 " ) by E27 ;
E29: c13 = 1 * c13
.= (c7 * (c7 " )) * c13 by E26, XCMPLX_0:def 7
.= (c7 * c13) * (c7 " )
.= ((- c8) * c14) * (c7 " ) by E27 ;
then E30: c10 * c6 = ((c10 * (((- c8) * c14) * (c7 " ))) * c2) + ((c10 * c14) * c3) by E22, E3;
E31: c14 * (((- c8) * c10) * (c7 " )) = c10 * (((- c8) * c14) * (c7 " )) ;
E32: now
assume E33: not ( not c14 <> 0 & not c10 <> 0 ) ;
take c15 = c14;
take c16 = c10;
thus ( c15 * c5 = c16 * c6 & not ( not c15 <> 0 & not c16 <> 0 ) ) by E20, E28, E30, E31, E33, E3;
end;
now
assume ( c10 = 0 & c14 = 0 ) ;
then 1 * c5 = 1 * c6 by E20, E22, E28, E29;
hence ex b1, b2 being Real st
( b1 * c5 = b2 * c6 & not ( not b1 <> 0 & not b2 <> 0 ) ) ;
end;
hence ex b1, b2 being Real st
( b1 * c5 = b2 * c6 & not ( not b1 <> 0 & not b2 <> 0 ) ) by E32;
end;
hence ex b1, b2 being Real st
( b1 * c5 = b2 * c6 & not ( not b1 <> 0 & not b2 <> 0 ) ) by E25;
end;

theorem E16: :: ANALMETR:14
for b1 being RealLinearSpace
for b2, b3, b4, b5, b6 being VECTOR of b1 holds
( ( Gen b2,b3 & b4,b5 are_Ort_wrt b2,b3 & b4,b6 are_Ort_wrt b2,b3 ) implies ( ( b4,b5 + b6 are_Ort_wrt b2,b3 & b4,b5 - b6 are_Ort_wrt b2,b3 ) ) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4, c5, c6 be VECTOR of c1;
assume that
E17: Gen c2,c3 and
E18: c4,c5 are_Ort_wrt c2,c3 and
E19: c4,c6 are_Ort_wrt c2,c3 ;
consider c7, c8, c9, c10 being Real such that
E20: ( c4 = (c7 * c2) + (c8 * c3) & c5 = (c9 * c2) + (c10 * c3) ) and
E21: (c7 * c9) + (c8 * c10) = 0 by E18, E5;
consider c11, c12, c13, c14 being Real such that
E22: ( c4 = (c11 * c2) + (c12 * c3) & c6 = (c13 * c2) + (c14 * c3) ) and
E23: (c11 * c13) + (c12 * c14) = 0 by E19, E5;
E24: ( c7 = c11 & c8 = c12 ) by E17, E20, E22, E6;
E25: c5 + c6 = ((c9 + c13) * c2) + ((c10 + c14) * c3) by E20, E22, E1;
(c7 * (c9 + c13)) + (c8 * (c10 + c14)) = (((c7 * c9) + (c8 * c10)) + (c7 * c13)) + (c8 * c14)
.= 0 by E21, E23, E24 ;
hence c4,c5 + c6 are_Ort_wrt c2,c3 by E20, E25, E5;
E26: c5 - c6 = ((c9 - c13) * c2) + ((c10 - c14) * c3) by E20, E22, E1;
(c7 * (c9 - c13)) + (c8 * (c10 - c14)) = 0 + ((- 1) * 0) by E21, E23, E24
.= 0 ;
hence c4,c5 - c6 are_Ort_wrt c2,c3 by E20, E26, E5;
end;

theorem E17: :: ANALMETR:15
for b1 being RealLinearSpace
for b2, b3, b4 being VECTOR of b1 holds
( ( Gen b2,b3 & b4,b4 are_Ort_wrt b2,b3 ) implies ( b4 = 0. b1 ) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4 be VECTOR of c1;
assume that
E18: Gen c2,c3 and
E19: c4,c4 are_Ort_wrt c2,c3 ;
consider c5, c6, c7, c8 being Real such that
E20: ( c4 = (c5 * c2) + (c6 * c3) & c4 = (c7 * c2) + (c8 * c3) ) and
E21: (c5 * c7) + (c6 * c8) = 0 by E19, E5;
E22: ( c5 = c7 & c6 = c8 ) by E18, E20, E6;
E23: now
let c9 be Real;
assume E24: c9 <> 0 ;
not ( 0 < c9 & not 0 < c9 * c9 ) by XREAL_1:131;
hence 0 < c9 * c9 by E24, XREAL_1:132;
end;
E24: c5 = 0
proof
assume c5 <> 0 ;
then 0 < c5 * c5 by E23;
then c6 * c6 < (c5 * c5) + (c6 * c6) by XREAL_1:31;
hence not verum by E21, E22, XREAL_1:65;
end;
c6 = 0
proof
assume c6 <> 0 ;
then E25: 0 < c6 * c6 by E23;
0 <= c5 * c5 by XREAL_1:65;
hence not verum by E21, E22, E25, XREAL_1:31;
end;
hence c4 = (0 * c2) + (0. c1) by E20, E24, RLVECT_1:23
.= 0 * c2 by RLVECT_1:10
.= 0. c1 by RLVECT_1:23 ;

end;

theorem E18: :: ANALMETR:16
for b1 being RealLinearSpace
for b2, b3, b4, b5, b6 being VECTOR of b1 holds
( ( Gen b2,b3 & b4,b5 - b6 are_Ort_wrt b2,b3 & b5,b6 - b4 are_Ort_wrt b2,b3 ) implies ( b6,b4 - b5 are_Ort_wrt b2,b3 ) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4, c5, c6 be VECTOR of c1;
assume that
E19: Gen c2,c3 and
E20: c4,c5 - c6 are_Ort_wrt c2,c3 and
E21: c5,c6 - c4 are_Ort_wrt c2,c3 ;
consider c7, c8 being Real such that
E22: c4 = (c7 * c2) + (c8 * c3) by E19, E4;
consider c9, c10 being Real such that
E23: c5 = (c9 * c2) + (c10 * c3) by E19, E4;
consider c11, c12 being Real such that
E24: c6 = (c11 * c2) + (c12 * c3) by E19, E4;
E25: ( c5 - c6 = ((c9 - c11) * c2) + ((c10 - c12) * c3) & c6 - c4 = ((c11 - c7) * c2) + ((c12 - c8) * c3) & c4 - c5 = ((c7 - c9) * c2) + ((c8 - c10) * c3) ) by E22, E23, E24, E1;
then ( (c7 * (c9 - c11)) + (c8 * (c10 - c12)) = 0 & (c9 * (c11 - c7)) + (c10 * (c12 - c8)) = 0 ) by E19, E20, E21, E22, E23, E7;
then E26: ( ((c7 * c9) + (c8 * c10)) + ((- 1) * ((c7 * c11) + (c8 * c12))) = 0 & ((c9 * c11) + (c10 * c12)) + ((- 1) * ((c9 * c7) + (c10 * c8))) = 0 ) ;
set c13 = (c7 * c9) + (c8 * c10);
set c14 = (c7 * c11) + (c8 * c12);
set c15 = (c9 * c11) + (c10 * c12);
0 = ((((- 1) * ((c7 * c11) + (c8 * c12))) + ((c7 * c9) + (c8 * c10))) + ((c9 * c11) + (c10 * c12))) + ((- 1) * ((c7 * c9) + (c8 * c10))) by E26
.= ((- 1) * ((c11 * c7) + (c12 * c8))) + ((c11 * c9) + (c12 * c10)) ;
then 0 = (- 1) * (((- 1) * ((c11 * c7) + (c12 * c8))) + ((c11 * c9) + (c12 * c10)))
.= (c11 * (c7 - c9)) + (c12 * (c8 - c10)) ;
hence c6,c4 - c5 are_Ort_wrt c2,c3 by E24, E25, E5;
end;

theorem E19: :: ANALMETR:17
for b1 being RealLinearSpace
for b2, b3, b4, b5 being VECTOR of b1 holds
not ( Gen b2,b3 & b4 <> 0. b1 & ( for b6 being Real holds
not b5 - (b6 * b4),b4 are_Ort_wrt b2,b3 ) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4, c5 be VECTOR of c1;
assume that
E20: Gen c2,c3 and
E21: c4 <> 0. c1 ;
consider c6, c7 being Real such that
E22: c4 = (c6 * c2) + (c7 * c3) by E20, E4;
consider c8, c9 being Real such that
E23: c5 = (c8 * c2) + (c9 * c3) by E20, E4;
set c10 = ((c8 * c6) + (c9 * c7)) * (((c6 * c6) + (c7 * c7)) " );
E24: (c6 * c6) + (c7 * c7) <> 0
proof
assume (c6 * c6) + (c7 * c7) = 0 ;
then c4,c4 are_Ort_wrt c2,c3 by E22, E5;
hence not verum by E20, E21, E17;
end;
(((c8 * c6) + (c9 * c7)) * (((c6 * c6) + (c7 * c7)) " )) * c4 = (((((c8 * c6) + (c9 * c7)) * (((c6 * c6) + (c7 * c7)) " )) * c6) * c2) + (((((c8 * c6) + (c9 * c7)) * (((c6 * c6) + (c7 * c7)) " )) * c7) * c3) by E22, E3;
then E25: c5 - ((((c8 * c6) + (c9 * c7)) * (((c6 * c6) + (c7 * c7)) " )) * c4) = ((c8 - ((((c8 * c6) + (c9 * c7)) * (((c6 * c6) + (c7 * c7))