let N be non empty ConjNormAlgStr ; :: thesis: for a, b being Element of N st <%a,b%> is left_complementable & <%a,b%> is right_add-cancelable holds
- <%a,b%> = <%(- a),(- b)%>
let a, b be Element of N; :: thesis: ( <%a,b%> is left_complementable & <%a,b%> is right_add-cancelable implies - <%a,b%> = <%(- a),(- b)%> )
assume A1: ( <%a,b%> is left_complementable & <%a,b%> is right_add-cancelable ) ; :: thesis: - <%a,b%> = <%(- a),(- b)%>
then ( a is left_complementable & b is left_complementable & a is right_add-cancelable & b is right_add-cancelable ) by Th15, Th23;
then A2: ( (- a) + a = 0. N & (- b) + b = 0. N ) by ALGSTR_0:def 13;
<%(- a),(- b)%> + <%a,b%> = <%((- a) + a),((- b) + b)%> by Def9
.= 0. (Cayley-Dickson N) by A2, Def9 ;
hence - <%a,b%> = <%(- a),(- b)%> by A1, ALGSTR_0:def 13; :: thesis: verum