let n be Nat; :: thesis: for x, y being Element of REAL n st x _|_ y holds
x,y are_lindependent2
let x, y be Element of REAL n; :: thesis: ( x _|_ y implies x,y are_lindependent2 )
assume A1: x _|_ y ; :: thesis: x,y are_lindependent2
then x,y are_orthogonal ;
then A2: |(x,y)| = 0 by RVSUM_1:def 17;
x <> 0* n by A1;
then |(x,x)| <> 0 by EUCLID_4:17;
then A3: |(x,x)| > 0 by RVSUM_1:119;
y <> 0* n by A1;
then A4: |(y,y)| <> 0 by EUCLID_4:17;
then A5: |(y,y)| > 0 by RVSUM_1:119;
for a, b being Real st (a * x) + (b * y) = 0* n holds
( a = 0 & b = 0 )
proof
let a, b be Real; :: thesis: ( (a * x) + (b * y) = 0* n implies ( a = 0 & b = 0 ) )
assume (a * x) + (b * y) = 0* n ; :: thesis: ( a = 0 & b = 0 )
then A6: 0 = |(((a * x) + (b * y)),((a * x) + (b * y)))| by EUCLID_4:17
.= (|((a * x),(a * x))| + (2 * |((a * x),(b * y))|)) + |((b * y),(b * y))| by EUCLID_4:32
.= ((a * |(x,(a * x))|) + (2 * |((a * x),(b * y))|)) + |((b * y),(b * y))| by EUCLID_4:21
.= ((a * |(x,(a * x))|) + (2 * (a * |(x,(b * y))|))) + |((b * y),(b * y))| by EUCLID_4:21
.= ((a * |(x,(a * x))|) + ((2 * a) * |(x,(b * y))|)) + (b * |(y,(b * y))|) by EUCLID_4:21
.= ((a * (a * |(x,x)|)) + ((2 * a) * |(x,(b * y))|)) + (b * |(y,(b * y))|) by EUCLID_4:22
.= (((a * a) * |(x,x)|) + ((2 * a) * (b * |(x,y)|))) + (b * |(y,(b * y))|) by EUCLID_4:22
.= (((a * a) * |(x,x)|) + (((2 * a) * b) * |(x,y)|)) + (b * (b * |(y,y)|)) by EUCLID_4:22
.= ((a * a) * |(x,x)|) + ((b * b) * |(y,y)|) by A2 ;
A7: b * b >= 0 by XREAL_1:63;
A8: a * a = 0
proof
assume a * a <> 0 ; :: thesis: contradiction
then a * a > 0 by XREAL_1:63;
then (a * a) * |(x,x)| > 0 by A3, XREAL_1:129;
hence contradiction by A5, A6, A7; :: thesis: verum
end;
then b * b = 0 by A4, A6, XCMPLX_1:6;
hence ( a = 0 & b = 0 ) by A8, XCMPLX_1:6; :: thesis: verum
end;
hence x,y are_lindependent2 ; :: thesis: verum