let K be comRing; :: thesis: for a1, a2 being Element of K holds (a1 - a2) * (((a1 |^ 2) + (a1 * a2)) + (a2 |^ 2)) = (a1 |^ 3) - (a2 |^ 3)
let a1, a2 be Element of K; :: thesis: (a1 - a2) * (((a1 |^ 2) + (a1 * a2)) + (a2 |^ 2)) = (a1 |^ 3) - (a2 |^ 3)
thus (a1 - a2) * (((a1 |^ 2) + (a1 * a2)) + (a2 |^ 2)) = (a1 * (((a1 |^ 2) + (a1 * a2)) + (a2 |^ 2))) - (a2 * (((a1 |^ 2) + (a1 * a2)) + (a2 |^ 2))) by VECTSP_1:13
.= ((a1 * ((a1 |^ 2) + (a1 * a2))) + (a1 * (a2 |^ 2))) - (a2 * (((a1 |^ 2) + (a1 * a2)) + (a2 |^ 2))) by VECTSP_1:def 7
.= (((a1 * (a1 |^ 2)) + (a1 * (a1 * a2))) + (a1 * (a2 |^ 2))) - (a2 * (((a1 |^ 2) + (a1 * a2)) + (a2 |^ 2))) by VECTSP_1:def 7
.= ((((a1 |^ 2) * a1) + ((a1 * a1) * a2)) + (a1 * (a2 |^ 2))) - (a2 * (((a1 |^ 2) + (a1 * a2)) + (a2 |^ 2))) by GROUP_1:def 3
.= ((((a1 |^ 2) * a1) + ((a1 * a1) * a2)) + (a1 * (a2 |^ 2))) - ((a2 * ((a1 |^ 2) + (a1 * a2))) + (a2 * (a2 |^ 2))) by VECTSP_1:def 7
.= (((a1 |^ (2 + 1)) + ((a1 * a1) * a2)) + (a1 * (a2 |^ 2))) - ((a2 * ((a1 |^ 2) + (a1 * a2))) + ((a2 |^ 2) * a2)) by EC_PF_1:24
.= (((a1 |^ 3) + ((a1 * a1) * a2)) + (a1 * (a2 |^ 2))) - (((a2 * (a1 |^ 2)) + (a2 * (a1 * a2))) + ((a2 |^ 2) * a2)) by VECTSP_1:def 7
.= (((a1 |^ 3) + ((a1 |^ 2) * a2)) + (a1 * (a2 |^ 2))) - (((a2 * (a1 |^ 2)) + (a2 * (a1 * a2))) + ((a2 |^ 2) * a2)) by GROUP_1:51
.= (((a1 |^ 3) + ((a1 |^ 2) * a2)) + (a1 * (a2 |^ 2))) - (((a2 * (a1 |^ 2)) + (a2 * (a1 * a2))) + (a2 |^ (2 + 1))) by EC_PF_1:24
.= ((((a1 |^ 3) + ((a1 |^ 2) * a2)) + (a1 * (a2 |^ 2))) - ((a2 * (a1 |^ 2)) + (a2 * (a1 * a2)))) - (a2 |^ 3) by VECTSP_1:17
.= (((a1 |^ 3) + (((a1 |^ 2) * a2) + (a1 * (a2 |^ 2)))) - ((a2 * (a1 |^ 2)) + (a2 * (a1 * a2)))) - (a2 |^ 3) by ALGSTR_1:7
.= ((a1 |^ 3) + ((((a1 |^ 2) * a2) + (a1 * (a2 |^ 2))) - ((a2 * (a1 |^ 2)) + (a2 * (a1 * a2))))) - (a2 |^ 3) by ALGSTR_1:7
.= ((a1 |^ 3) + ((((a1 |^ 2) * a2) + (a1 * (a2 |^ 2))) + ((- (a2 * (a1 * a2))) - (a2 * (a1 |^ 2))))) - (a2 |^ 3) by VECTSP_1:17
.= ((a1 |^ 3) + ((((a1 |^ 2) * a2) + (a1 * (a2 |^ 2))) + ((- (a1 * (a2 * a2))) - ((a1 |^ 2) * a2)))) - (a2 |^ 3) by GROUP_1:def 3
.= ((a1 |^ 3) + ((((a1 |^ 2) * a2) + (a1 * (a2 |^ 2))) + ((- (a1 * (a2 |^ 2))) - ((a1 |^ 2) * a2)))) - (a2 |^ 3) by GROUP_1:51
.= ((a1 |^ 3) + (((((a1 |^ 2) * a2) + (a1 * (a2 |^ 2))) - (a1 * (a2 |^ 2))) - ((a1 |^ 2) * a2))) - (a2 |^ 3) by ALGSTR_1:7
.= ((a1 |^ 3) + ((((a1 |^ 2) * a2) + ((a1 * (a2 |^ 2)) - (a1 * (a2 |^ 2)))) - ((a1 |^ 2) * a2))) - (a2 |^ 3) by ALGSTR_1:7
.= ((a1 |^ 3) + ((((a1 |^ 2) * a2) + (0. K)) - ((a1 |^ 2) * a2))) - (a2 |^ 3) by VECTSP_1:19
.= ((a1 |^ 3) + (0. K)) - (a2 |^ 3) by VECTSP_1:19, ALGSTR_1:7
.= (a1 |^ 3) - (a2 |^ 3) by ALGSTR_1:7 ; :: thesis: verum