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 antilinear iff opp J is linear )

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 antilinear iff opp J is linear )

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

set J9 = opp J;

set L9 = opp L;

for J being Function of K,L holds

( J is antilinear iff opp J is linear )

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 antilinear iff opp J is linear )

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

set J9 = opp J;

set L9 = opp L;

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

assume A4:
( opp J is additive & opp J is multiplicative & opp J is unity-preserving )
; :: according to RINGCAT1:def 1 :: thesis: J is antilinear assume A1:
J is antilinear
; :: thesis: opp J is linear

A2: opp J is additive

.= 1_ (opp L) ;

then opp J is unity-preserving ;

hence opp J is linear by A2, A3; :: thesis: verum

end;A2: opp J is additive

proof

A3:
opp J is multiplicative
let x, y be Scalar of K; :: according to VECTSP_1:def 19 :: thesis: (opp J) . (x + y) = ((opp J) . x) + ((opp J) . y)

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

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

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

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

proof

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

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

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

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

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

.= 1_ (opp L) ;

then opp J is unity-preserving ;

hence opp J is linear by A2, A3; :: thesis: verum

hereby :: according to VECTSP_1:def 19,MOD_4:def 7 :: thesis: ( J is antimultiplicative & J is unity-preserving )

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

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

end;thus J . (x + y) = ((opp J) . x) + ((opp J) . y) by A4

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

hereby :: according to MOD_4:def 6 :: thesis: J is unity-preserving

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

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

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

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

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