let p be Element of REAL 3; :: thesis: - p = ((- ((p . 1) * <e1>)) - ((p . 2) * <e2>)) - ((p . 3) * <e3>)
- p = ((((- 1) * (p . 1)) * <e1>) + (((- 1) * (p . 2)) * <e2>)) + (((- 1) * (p . 3)) * <e3>) by Th30
.= ((- ((p . 1) * <e1>)) + (((- 1) * (p . 2)) * <e2>)) + ((- (p . 3)) * <e3>) by RVSUM_1:49
.= ((- ((p . 1) * <e1>)) + (- ((p . 2) * <e2>))) + (((- 1) * (p . 3)) * <e3>) by RVSUM_1:49
.= ((- ((p . 1) * <e1>)) - ((p . 2) * <e2>)) - ((p . 3) * <e3>) by RVSUM_1:49 ;
hence - p = ((- ((p . 1) * <e1>)) - ((p . 2) * <e2>)) - ((p . 3) * <e3>) ; :: thesis: verum