let N be non empty ConjNormAlgStr ; for a being Element of N st N is well-conjugated & N is reflexive & N is discerning & N is RealNormSpace-like & N is vector-distributive & N is scalar-distributive & N is scalar-associative & N is scalar-unital & N is Abelian & N is add-associative & N is right_zeroed & N is right_complementable & N is associative & N is distributive & N is well-unital & not N is degenerated & N is almost_left_invertible holds
(- a) *' = - (a *')
let a be Element of N; ( N is well-conjugated & N is reflexive & N is discerning & N is RealNormSpace-like & N is vector-distributive & N is scalar-distributive & N is scalar-associative & N is scalar-unital & N is Abelian & N is add-associative & N is right_zeroed & N is right_complementable & N is associative & N is distributive & N is well-unital & not N is degenerated & N is almost_left_invertible implies (- a) *' = - (a *') )
assume that
A1:
N is well-conjugated
and
A2:
( N is reflexive & N is discerning & N is RealNormSpace-like & N is vector-distributive & N is scalar-distributive & N is scalar-associative & N is scalar-unital & N is Abelian & N is add-associative & N is right_zeroed & N is right_complementable )
and
A3:
N is associative
and
A4:
N is distributive
and
A5:
N is well-unital
and
A6:
( not N is degenerated & N is almost_left_invertible )
; (- a) *' = - (a *')
per cases
( not a is zero or a is zero )
;
suppose A7:
not
a is
zero
;
(- a) *' = - (a *')then A8:
(a *') * a = (||.a.|| ^2) * (1. N)
by A1, Def3;
A9:
((- a) *') * (- a) = (||.(- a).|| ^2) * (1. N)
by A1, A2, A6, A7, Def3;
A10:
||.(- a).|| = ||.a.||
by A2, NORMSP_1:2;
A11:
a <> 0. N
by A7;
A12:
a * (/ a) = 1. N
by A2, A3, A4, A5, A6, A11, VECTSP_2:9;
then A13:
(- a) * (- (/ a)) = 1. N
by A2, A4, VECTSP_1:10;
A14:
a * (- (/ a)) = - (1. N)
by A2, A4, A12, VECTSP_1:8;
thus (- a) *' =
((- a) *') * (1. N)
by A5
.=
(((- a) *') * (- a)) * (- (/ a))
by A13, A3
.=
(a *') * (a * (- (/ a)))
by A8, A9, A10, A3
.=
- (a *')
by A2, A14, A4, A5, VECTSP_2:28
;
verum end;