let p be Element of REAL 3; :: thesis: - p = ((- ((p . 1) * <e1> )) - ((p . 2) * <e2> )) - ((p . 3) * <e3> )
set r = - 1;
- 1 is Element of REAL by XREAL_0:def 1;
then - p = ((((- 1) * (p . 1)) * <e1> ) + (((- 1) * (p . 2)) * <e2> )) + (((- 1) * (p . 3)) * <e3> ) by ThA7
.= ((- ((p . 1) * <e1> )) + (((- 1) * (p . 2)) * <e2> )) + ((- (p . 3)) * <e3> ) by RVSUM_1:71
.= ((- ((p . 1) * <e1> )) + (- ((p . 2) * <e2> ))) + (((- 1) * (p . 3)) * <e3> ) by RVSUM_1:71
.= ((- ((p . 1) * <e1> )) - ((p . 2) * <e2> )) - ((p . 3) * <e3> ) by RVSUM_1:71 ;
hence - p = ((- ((p . 1) * <e1> )) - ((p . 2) * <e2> )) - ((p . 3) * <e3> ) ; :: thesis: verum