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 J' = opp J;
set L' = opp L;

A1: now

assume J is linear ; :: thesis: opp J is antilinear
then A2: ( J is additive & J is multiplicative & J is unity-preserving ) by RINGCAT1:def 2;
A3: for x, y being Scalar of K holds (opp J) . (x + y) = ((opp J) . x) + ((opp J) . y)

proof

let x, y be Scalar of K; :: thesis: (opp J) . (x + y) = ((opp J) . x) + ((opp J) . y)
thus (opp J) . (x + y) = (J . x) + (J . y) by A2, GRCAT_1:def 13
.= ((opp J) . x) + ((opp J) . y) ; :: thesis: verum

end;

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

proof

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 7
.= ((opp J) . y) * ((opp J) . x) by Lm3 ; :: thesis: verum

end;

(opp J) . (1_ K) = 1_ L by A2, GROUP_1:def 17
.= 1_ (opp L) ;
then ( opp J is additive & opp J is antimultiplicative & opp J is unity-preserving ) by A3, A4, Def6, GRCAT_1:def 13, GROUP_1:def 17;
hence opp J is antilinear ; :: thesis: verum

end;

now

assume opp J is antilinear ; :: thesis: J is linear
then A5: ( opp J is additive & opp J is antimultiplicative & opp J is unity-preserving ) ;
A6: for x, y being Scalar of K holds J . (x + y) = (J . x) + (J . y)

proof

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 A5, GRCAT_1:def 13
.= (J . x) + (J . y) ; :: thesis: verum

end;

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

proof

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 A5, Def6
.= (J . x) * (J . y) by Lm3 ; :: thesis: verum

end;

J . (1_ K) = 1_ (opp L) by A5, GROUP_1:def 17
.= 1_ L ;
then ( J is additive & J is multiplicative & J is unity-preserving ) by A6, A7, GRCAT_1:def 13, GROUP_1:def 17, GROUP_6:def 7;
hence J is linear by RINGCAT1:def 2; :: thesis: verum

end;

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