let V be RealLinearSpace; :: thesis: for u, v, w being Element of V st ( u = 0. V or v = 0. V or w = 0. V ) holds

u,v,w are_LinDep

let u, v, w be Element of V; :: thesis: ( ( u = 0. V or v = 0. V or w = 0. V ) implies u,v,w are_LinDep )

A1: for u, v, w being Element of V st u = 0. V holds

u,v,w are_LinDep

hence u,v,w are_LinDep by A1, A3, A4; :: thesis: verum

u,v,w are_LinDep

let u, v, w be Element of V; :: thesis: ( ( u = 0. V or v = 0. V or w = 0. V ) implies u,v,w are_LinDep )

A1: for u, v, w being Element of V st u = 0. V holds

u,v,w are_LinDep

proof

let u, v, w be Element of V; :: thesis: ( u = 0. V implies u,v,w are_LinDep )

assume A2: u = 0. V ; :: thesis: u,v,w are_LinDep

0. V = (0. V) + (0. V)

.= (1 * u) + (0. V) by A2

.= (1 * u) + (0 * v) by RLVECT_1:10

.= ((1 * u) + (0 * v)) + (0. V)

.= ((1 * u) + (0 * v)) + (0 * w) by RLVECT_1:10 ;

hence u,v,w are_LinDep ; :: thesis: verum

end;assume A2: u = 0. V ; :: thesis: u,v,w are_LinDep

0. V = (0. V) + (0. V)

.= (1 * u) + (0. V) by A2

.= (1 * u) + (0 * v) by RLVECT_1:10

.= ((1 * u) + (0 * v)) + (0. V)

.= ((1 * u) + (0 * v)) + (0 * w) by RLVECT_1:10 ;

hence u,v,w are_LinDep ; :: thesis: verum

A3: now :: thesis: ( v = 0. V & ( u = 0. V or v = 0. V or w = 0. V ) implies u,v,w are_LinDep )

assume
v = 0. V
; :: thesis: ( ( u = 0. V or v = 0. V or w = 0. V ) implies u,v,w are_LinDep )

then v,w,u are_LinDep by A1;

hence ( ( u = 0. V or v = 0. V or w = 0. V ) implies u,v,w are_LinDep ) by Th5; :: thesis: verum

end;then v,w,u are_LinDep by A1;

hence ( ( u = 0. V or v = 0. V or w = 0. V ) implies u,v,w are_LinDep ) by Th5; :: thesis: verum

A4: now :: thesis: ( w = 0. V & ( u = 0. V or v = 0. V or w = 0. V ) implies u,v,w are_LinDep )

assume
( u = 0. V or v = 0. V or w = 0. V )
; :: thesis: u,v,w are_LinDep assume
w = 0. V
; :: thesis: ( ( u = 0. V or v = 0. V or w = 0. V ) implies u,v,w are_LinDep )

then w,u,v are_LinDep by A1;

hence ( ( u = 0. V or v = 0. V or w = 0. V ) implies u,v,w are_LinDep ) by Th5; :: thesis: verum

end;then w,u,v are_LinDep by A1;

hence ( ( u = 0. V or v = 0. V or w = 0. V ) implies u,v,w are_LinDep ) by Th5; :: thesis: verum

hence u,v,w are_LinDep by A1, A3, A4; :: thesis: verum