let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ; :: thesis: for L being non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr

for J being Function of K,L holds

( J is linear iff opp J is antilinear )

let L be non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr ; :: thesis: for J being Function of K,L holds

( J is linear iff opp J is antilinear )

let J be Function of K,L; :: thesis: ( J is linear iff opp J is antilinear )

set J9 = opp J;

set L9 = opp L;

for J being Function of K,L holds

( J is linear iff opp J is antilinear )

let L be non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr ; :: thesis: for J being Function of K,L holds

( J is linear iff opp J is antilinear )

let J be Function of K,L; :: thesis: ( J is linear iff opp J is antilinear )

set J9 = opp J;

set L9 = opp L;

A1: now :: thesis: ( J is linear implies opp J is antilinear )

assume A2:
J is linear
; :: thesis: opp J is antilinear

A3: for x, y being Scalar of K holds (opp J) . (x * y) = ((opp J) . y) * ((opp J) . x)

.= 1_ (opp L) ;

then ( opp J is additive & opp J is antimultiplicative & opp J is unity-preserving ) by Lm12, A3, A2;

hence opp J is antilinear ; :: thesis: verum

end;A3: for x, y being Scalar of K holds (opp J) . (x * y) = ((opp J) . y) * ((opp J) . x)

proof

(opp J) . (1_ K) =
1_ L
by A2, GROUP_1:def 13
let x, y be Scalar of K; :: thesis: (opp J) . (x * y) = ((opp J) . y) * ((opp J) . x)

thus (opp J) . (x * y) = (J . x) * (J . y) by A2, GROUP_6:def 6

.= ((opp J) . y) * ((opp J) . x) by Lm3 ; :: thesis: verum

end;thus (opp J) . (x * y) = (J . x) * (J . y) by A2, GROUP_6:def 6

.= ((opp J) . y) * ((opp J) . x) by Lm3 ; :: thesis: verum

.= 1_ (opp L) ;

then ( opp J is additive & opp J is antimultiplicative & opp J is unity-preserving ) by Lm12, A3, A2;

hence opp J is antilinear ; :: thesis: verum

now :: thesis: ( opp J is antilinear implies J is linear )

hence
( J is linear iff opp J is antilinear )
by A1; :: thesis: verumassume A4:
opp J is antilinear
; :: thesis: J is linear

A5: for x, y being Scalar of K holds J . (x + y) = (J . x) + (J . y)

.= 1_ L ;

then ( J is additive & J is multiplicative & J is unity-preserving ) by A5, A6;

hence J is linear ; :: thesis: verum

end;A5: for x, y being Scalar of K holds J . (x + y) = (J . x) + (J . y)

proof

A6:
for x, y being Scalar of K holds J . (x * y) = (J . x) * (J . y)
let x, y be Scalar of K; :: thesis: J . (x + y) = (J . x) + (J . y)

thus J . (x + y) = ((opp J) . x) + ((opp J) . y) by A4, VECTSP_1:def 20

.= (J . x) + (J . y) ; :: thesis: verum

end;thus J . (x + y) = ((opp J) . x) + ((opp J) . y) by A4, VECTSP_1:def 20

.= (J . x) + (J . y) ; :: thesis: verum

proof

J . (1_ K) =
1_ (opp L)
by A4, GROUP_1:def 13
let x, y be Scalar of K; :: thesis: J . (x * y) = (J . x) * (J . y)

thus J . (x * y) = ((opp J) . y) * ((opp J) . x) by A4, Def6

.= (J . x) * (J . y) by Lm3 ; :: thesis: verum

end;thus J . (x * y) = ((opp J) . y) * ((opp J) . x) by A4, Def6

.= (J . x) * (J . y) by Lm3 ; :: thesis: verum

.= 1_ L ;

then ( J is additive & J is multiplicative & J is unity-preserving ) by A5, A6;

hence J is linear ; :: thesis: verum