let V be RealLinearSpace; :: thesis: for u, v, w, u1, v1, w1 being Element of V st are_Prop u,u1 & are_Prop v,v1 & are_Prop w,w1 & u,v,w are_LinDep holds

u1,v1,w1 are_LinDep

let u, v, w, u1, v1, w1 be Element of V; :: thesis: ( are_Prop u,u1 & are_Prop v,v1 & are_Prop w,w1 & u,v,w are_LinDep implies u1,v1,w1 are_LinDep )

assume that

A1: are_Prop u,u1 and

A2: are_Prop v,v1 and

A3: are_Prop w,w1 and

A4: u,v,w are_LinDep ; :: thesis: u1,v1,w1 are_LinDep

consider b being Real such that

A5: b <> 0 and

A6: v = b * v1 by A2, Th1;

consider a being Real such that

A7: a <> 0 and

A8: u = a * u1 by A1, Th1;

consider d1, d2, d3 being Real such that

A9: ((d1 * u) + (d2 * v)) + (d3 * w) = 0. V and

A10: ( d1 <> 0 or d2 <> 0 or d3 <> 0 ) by A4;

consider c being Real such that

A11: c <> 0 and

A12: w = c * w1 by A3, Th1;

A13: ( d1 * a <> 0 or d2 * b <> 0 or d3 * c <> 0 ) by A7, A5, A11, A10, XCMPLX_1:6;

0. V = (((d1 * a) * u1) + (d2 * (b * v1))) + (d3 * (c * w1)) by A8, A6, A12, A9, RLVECT_1:def 7

.= (((d1 * a) * u1) + ((d2 * b) * v1)) + (d3 * (c * w1)) by RLVECT_1:def 7

.= (((d1 * a) * u1) + ((d2 * b) * v1)) + ((d3 * c) * w1) by RLVECT_1:def 7 ;

hence u1,v1,w1 are_LinDep by A13; :: thesis: verum

u1,v1,w1 are_LinDep

let u, v, w, u1, v1, w1 be Element of V; :: thesis: ( are_Prop u,u1 & are_Prop v,v1 & are_Prop w,w1 & u,v,w are_LinDep implies u1,v1,w1 are_LinDep )

assume that

A1: are_Prop u,u1 and

A2: are_Prop v,v1 and

A3: are_Prop w,w1 and

A4: u,v,w are_LinDep ; :: thesis: u1,v1,w1 are_LinDep

consider b being Real such that

A5: b <> 0 and

A6: v = b * v1 by A2, Th1;

consider a being Real such that

A7: a <> 0 and

A8: u = a * u1 by A1, Th1;

consider d1, d2, d3 being Real such that

A9: ((d1 * u) + (d2 * v)) + (d3 * w) = 0. V and

A10: ( d1 <> 0 or d2 <> 0 or d3 <> 0 ) by A4;

consider c being Real such that

A11: c <> 0 and

A12: w = c * w1 by A3, Th1;

A13: ( d1 * a <> 0 or d2 * b <> 0 or d3 * c <> 0 ) by A7, A5, A11, A10, XCMPLX_1:6;

0. V = (((d1 * a) * u1) + (d2 * (b * v1))) + (d3 * (c * w1)) by A8, A6, A12, A9, RLVECT_1:def 7

.= (((d1 * a) * u1) + ((d2 * b) * v1)) + (d3 * (c * w1)) by RLVECT_1:def 7

.= (((d1 * a) * u1) + ((d2 * b) * v1)) + ((d3 * c) * w1) by RLVECT_1:def 7 ;

hence u1,v1,w1 are_LinDep by A13; :: thesis: verum