let x, y, z be Real; :: thesis: - |[x,y,z]| = ((- (x * <e1>)) - (y * <e2>)) - (z * <e3>)
- |[x,y,z]| = ((((- 1) * x) * <e1>) + (((- 1) * y) * <e2>)) + (((- 1) * z) * <e3>) by Th32
.= ((- (x * <e1>)) + (((- 1) * y) * <e2>)) + ((- z) * <e3>) by RVSUM_1:49
.= ((- (x * <e1>)) + (- (y * <e2>))) + (((- 1) * z) * <e3>) by RVSUM_1:49
.= ((- (x * <e1>)) - (y * <e2>)) - (z * <e3>) by RVSUM_1:49 ;
hence - |[x,y,z]| = ((- (x * <e1>)) - (y * <e2>)) - (z * <e3>) ; :: thesis: verum