let a1, a2, b1, b2 be Real; :: thesis: for n being Nat
for y2, x1, x2, y1, y1 being Element of REAL n st y1,y2 are_lindependent2 & y1 = (a1 * x1) + (a2 * x2) & y2 = (b1 * x1) + (b2 * x2) holds
ex c1, c2, d1, d2 being Real st
( x1 = (c1 * y1) + (c2 * y2) & x2 = (d1 * y1) + (d2 * y2) )
let n be Nat; :: thesis: for y2, x1, x2, y1, y1 being Element of REAL n st y1,y2 are_lindependent2 & y1 = (a1 * x1) + (a2 * x2) & y2 = (b1 * x1) + (b2 * x2) holds
ex c1, c2, d1, d2 being Real st
( x1 = (c1 * y1) + (c2 * y2) & x2 = (d1 * y1) + (d2 * y2) )
let y2, x1, x2, y1, y1 be Element of REAL n; :: thesis: ( y1,y2 are_lindependent2 & y1 = (a1 * x1) + (a2 * x2) & y2 = (b1 * x1) + (b2 * x2) implies ex c1, c2, d1, d2 being Real st
( x1 = (c1 * y1) + (c2 * y2) & x2 = (d1 * y1) + (d2 * y2) ) )
assume A1: y1,y2 are_lindependent2 ; :: thesis: ( not y1 = (a1 * x1) + (a2 * x2) or not y2 = (b1 * x1) + (b2 * x2) or ex c1, c2, d1, d2 being Real st
( x1 = (c1 * y1) + (c2 * y2) & x2 = (d1 * y1) + (d2 * y2) ) )
assume that
A2: y1 = (a1 * x1) + (a2 * x2) and
A3: y2 = (b1 * x1) + (b2 * x2) ; :: thesis: ex c1, c2, d1, d2 being Real st
( x1 = (c1 * y1) + (c2 * y2) & x2 = (d1 * y1) + (d2 * y2) )
A4: (- (b1 * y1)) + (a1 * y2) = ((- b1) * ((a1 * x1) + (a2 * x2))) + (a1 * ((b1 * x1) + (b2 * x2))) by A2, A3, Th3
.= ((((- b1) * a1) * x1) + (((- b1) * a2) * x2)) + (a1 * ((b1 * x1) + (b2 * x2))) by Th21
.= (((- (a1 * b1)) * x1) + ((- (a2 * b1)) * x2)) + (((a1 * b1) * x1) + ((a1 * b2) * x2)) by Th21
.= (((- (a1 * b1)) + (a1 * b1)) * x1) + (((- (a2 * b1)) + (a1 * b2)) * x2) by Th23
.= (0* n) + (((- (a2 * b1)) + (a1 * b2)) * x2) by EUCLID_4:3
.= ((a1 * b2) - (a2 * b1)) * x2 by EUCLID_4:1 ;
A5: (b2 * y1) - (a2 * y2) = (((a1 * b2) * x1) + ((a2 * b2) * x2)) - (a2 * ((b1 * x1) + (b2 * x2))) by A2, A3, Th21
.= (((a1 * b2) * x1) + ((a2 * b2) * x2)) - (((a2 * b1) * x1) + ((a2 * b2) * x2)) by Th21
.= (((a1 * b2) - (a2 * b1)) * x1) + (((a2 * b2) - (a2 * b2)) * x2) by Th25
.= (((a1 * b2) - (a2 * b1)) * x1) + (0* n) by EUCLID_4:3
.= ((a1 * b2) - (a2 * b1)) * x1 by EUCLID_4:1 ;
A6: (a1 * b2) - (a2 * b1) <> 0
proof
assume not (a1 * b2) - (a2 * b1) <> 0 ; :: thesis: contradiction
then A7: (b2 * y1) + ((- a2) * y2) = 0 * x1 by A5, Th3
.= 0* n by EUCLID_4:3 ;
then A8: y2 = (b1 * x1) + (0 * x2) by A1, A3
.= (b1 * x1) + (0* n) by EUCLID_4:3
.= b1 * x1 by EUCLID_4:1 ;
A9: - a2 = 0 by A1, A7;
then y1 = (a1 * x1) + (0* n) by A2, EUCLID_4:3
.= a1 * x1 by EUCLID_4:1 ;
then (b1 * y1) + ((- a1) * y2) = ((a1 * b1) * x1) + ((- a1) * (b1 * x1)) by A8, EUCLID_4:4
.= ((a1 * b1) * x1) + (((- a1) * b1) * x1) by EUCLID_4:4
.= ((a1 * b1) + ((- a1) * b1)) * x1 by EUCLID_4:7
.= 0* n by EUCLID_4:3 ;
then - a1 = 0 by A1;
then y1 = (0* n) + (0 * x2) by A2, A9, EUCLID_4:3
.= (0* n) + (0* n) by EUCLID_4:3
.= 0* n by EUCLID_4:1 ;
hence contradiction by A1, Lm2; :: thesis: verum
end;
A10: x2 = 1 * x2 by EUCLID_4:3
.= ((1 / ((a1 * b2) - (a2 * b1))) * ((a1 * b2) - (a2 * b1))) * x2 by A6, XCMPLX_1:106
.= (1 / ((a1 * b2) - (a2 * b1))) * (((a1 * b2) - (a2 * b1)) * x2) by EUCLID_4:4
.= ((1 / ((a1 * b2) - (a2 * b1))) * (- (b1 * y1))) + ((1 / ((a1 * b2) - (a2 * b1))) * (a1 * y2)) by A4, EUCLID_4:6
.= ((1 / ((a1 * b2) - (a2 * b1))) * ((- b1) * y1)) + ((1 / ((a1 * b2) - (a2 * b1))) * (a1 * y2)) by Th3
.= (((- b1) / ((a1 * b2) - (a2 * b1))) * y1) + ((1 / ((a1 * b2) - (a2 * b1))) * (a1 * y2)) by Th1
.= (((- b1) / ((a1 * b2) - (a2 * b1))) * y1) + ((a1 / ((a1 * b2) - (a2 * b1))) * y2) by Th1 ;
set d2 = a1 / ((a1 * b2) - (a2 * b1));
set d1 = (- b1) / ((a1 * b2) - (a2 * b1));
set c2 = (- a2) / ((a1 * b2) - (a2 * b1));
set c1 = b2 / ((a1 * b2) - (a2 * b1));
take b2 / ((a1 * b2) - (a2 * b1)) ; :: thesis: ex c2, d1, d2 being Real st
( x1 = ((b2 / ((a1 * b2) - (a2 * b1))) * y1) + (c2 * y2) & x2 = (d1 * y1) + (d2 * y2) )
take (- a2) / ((a1 * b2) - (a2 * b1)) ; :: thesis: ex d1, d2 being Real st
( x1 = ((b2 / ((a1 * b2) - (a2 * b1))) * y1) + (((- a2) / ((a1 * b2) - (a2 * b1))) * y2) & x2 = (d1 * y1) + (d2 * y2) )
take (- b1) / ((a1 * b2) - (a2 * b1)) ; :: thesis: ex d2 being Real st
( x1 = ((b2 / ((a1 * b2) - (a2 * b1))) * y1) + (((- a2) / ((a1 * b2) - (a2 * b1))) * y2) & x2 = (((- b1) / ((a1 * b2) - (a2 * b1))) * y1) + (d2 * y2) )
take a1 / ((a1 * b2) - (a2 * b1)) ; :: thesis: ( x1 = ((b2 / ((a1 * b2) - (a2 * b1))) * y1) + (((- a2) / ((a1 * b2) - (a2 * b1))) * y2) & x2 = (((- b1) / ((a1 * b2) - (a2 * b1))) * y1) + ((a1 / ((a1 * b2) - (a2 * b1))) * y2) )
x1 = 1 * x1 by EUCLID_4:3
.= ((1 / ((a1 * b2) - (a2 * b1))) * ((a1 * b2) - (a2 * b1))) * x1 by A6, XCMPLX_1:106
.= (1 / ((a1 * b2) - (a2 * b1))) * (((a1 * b2) - (a2 * b1)) * x1) by EUCLID_4:4
.= ((1 / ((a1 * b2) - (a2 * b1))) * (b2 * y1)) - ((1 / ((a1 * b2) - (a2 * b1))) * (a2 * y2)) by A5, Th12
.= ((b2 / ((a1 * b2) - (a2 * b1))) * y1) - ((1 / ((a1 * b2) - (a2 * b1))) * (a2 * y2)) by Th1
.= ((b2 / ((a1 * b2) - (a2 * b1))) * y1) + (- (((1 / ((a1 * b2) - (a2 * b1))) * a2) * y2)) by EUCLID_4:4
.= ((b2 / ((a1 * b2) - (a2 * b1))) * y1) + ((- ((1 / ((a1 * b2) - (a2 * b1))) * a2)) * y2) by Th3
.= ((b2 / ((a1 * b2) - (a2 * b1))) * y1) + (((1 / ((a1 * b2) - (a2 * b1))) * (- a2)) * y2)
.= ((b2 / ((a1 * b2) - (a2 * b1))) * y1) + (((- a2) / ((a1 * b2) - (a2 * b1))) * y2) by XCMPLX_1:99 ;
hence ( x1 = ((b2 / ((a1 * b2) - (a2 * b1))) * y1) + (((- a2) / ((a1 * b2) - (a2 * b1))) * y2) & x2 = (((- b1) / ((a1 * b2) - (a2 * b1))) * y1) + ((a1 / ((a1 * b2) - (a2 * b1))) * y2) ) by A10; :: thesis: verum