let N be non degenerated right_complementable almost_right_cancelable almost_left_invertible Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative discerning reflexive RealNormSpace-like well-unital distributive associative Banach_Algebra-like_2 Banach_Algebra-like_3 well-conjugated add-conjugative ConjNormAlgStr ; :: thesis: for a, b being Element of N st ( not a is zero or not b is zero ) & <%a,b%> is right_mult-cancelable & <%a,b%> is left_invertible holds
/ <%a,b%> = <%((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * (a *')),((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * (- b))%>
let a, b be Element of N; :: thesis: ( ( not a is zero or not b is zero ) & <%a,b%> is right_mult-cancelable & <%a,b%> is left_invertible implies / <%a,b%> = <%((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * (a *')),((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * (- b))%> )
assume that
A1: ( not a is zero or not b is zero ) and
A2: ( <%a,b%> is right_mult-cancelable & <%a,b%> is left_invertible ) ; :: thesis: / <%a,b%> = <%((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * (a *')),((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * (- b))%>
set C = Cayley-Dickson N;
set m = 1 / ((||.a.|| ^2) + (||.b.|| ^2));
A3: (b *') * (- b) = - ((b *') * b) by VECTSP_1:8;
A4: (a *') * a = (||.a.|| ^2) * (1. N) by Th9;
A5: (b *') * b = (||.b.|| ^2) * (1. N) by Th9;
(b *') * ((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * (- b)) = (1 / ((||.a.|| ^2) + (||.b.|| ^2))) * ((b *') * (- b)) by LOPBAN_2:def 11;
then A6: (((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * (a *')) * a) - ((b *') * ((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * (- b))) = (((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * (a *')) * a) - (- ((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * ((b *') * b))) by A3, RLVECT_1:25
.= (((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * (a *')) * a) + ((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * ((b *') * b))
.= ((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * ((a *') * a)) + ((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * ((b *') * b)) by FUNCSDOM:def 9
.= (1 / ((||.a.|| ^2) + (||.b.|| ^2))) * (((a *') * a) + ((b *') * b)) by RLVECT_1:def 5
.= (1 / ((||.a.|| ^2) + (||.b.|| ^2))) * (((||.a.|| ^2) + (||.b.|| ^2)) * (1. N)) by A4, A5, RLVECT_1:def 6
.= ((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * ((||.a.|| ^2) + (||.b.|| ^2))) * (1. N) by RLVECT_1:def 7
.= 1 * (1. N) by A1, XCMPLX_1:106
.= 1. N by RLVECT_1:def 8 ;
((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * (- b)) * (a *') = (1 / ((||.a.|| ^2) + (||.b.|| ^2))) * ((- b) * (a *')) by FUNCSDOM:def 9
.= (- b) * ((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * (a *')) by LOPBAN_2:def 11
.= - (b * ((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * (a *'))) by VECTSP_1:9 ;
then A7: (b * ((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * (a *'))) + (((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * (- b)) * (a *')) = 0. N by RLVECT_1:def 10;
<%((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * (a *')),((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * (- b))%> * <%a,b%> = <%((((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * (a *')) * a) - ((b *') * ((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * (- b)))),((b * ((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * (a *'))) + (((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * (- b)) * (a *')))%> by Def9
.= 1. (Cayley-Dickson N) by A6, A7, Def9 ;
hence / <%a,b%> = <%((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * (a *')),((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * (- b))%> by A2, ALGSTR_0:def 30; :: thesis: verum