let x, y, z be Element of REAL ; :: thesis: - |[x,y,z]| = ((- (x * <e1> )) - (y * <e2> )) - (z * <e3> )
- 1 in REAL by XREAL_0:def 1;
then - |[x,y,z]| = ((((- 1) * x) * <e1> ) + (((- 1) * y) * <e2> )) + (((- 1) * z) * <e3> ) by ThA8
.= ((- (x * <e1> )) + (((- 1) * y) * <e2> )) + ((- z) * <e3> ) by RVSUM_1:71
.= ((- (x * <e1> )) + (- (y * <e2> ))) + (((- 1) * z) * <e3> ) by RVSUM_1:71
.= ((- (x * <e1> )) - (y * <e2> )) - (z * <e3> ) by RVSUM_1:71 ;
hence - |[x,y,z]| = ((- (x * <e1> )) - (y * <e2> )) - (z * <e3> ) ; :: thesis: verum