let K be Ring; :: thesis: ( id K is antiisomorphism iff K is comRing )

set J = id K;

set J = id K;

A1: now :: thesis: ( K is comRing implies id K is antiisomorphism )

assume A2:
K is comRing
; :: thesis: id K is antiisomorphism

A3: for x, y being Scalar of K holds (id K) . (x * y) = ((id K) . y) * ((id K) . x) by A2, Lm5;

(id K) . (1_ K) = 1_ K ;

hence id K is antiisomorphism by A3, Th22; :: thesis: verum

end;A3: for x, y being Scalar of K holds (id K) . (x * y) = ((id K) . y) * ((id K) . x) by A2, Lm5;

(id K) . (1_ K) = 1_ K ;

hence id K is antiisomorphism by A3, Th22; :: thesis: verum

now :: thesis: ( id K is antiisomorphism implies K is comRing )

hence
( id K is antiisomorphism iff K is comRing )
by A1; :: thesis: verumassume A4:
id K is antiisomorphism
; :: thesis: K is comRing

for x, y being Element of K holds x * y = y * x

end;for x, y being Element of K holds x * y = y * x

proof

hence
K is comRing
by GROUP_1:def 12; :: thesis: verum
let x, y be Element of K; :: thesis: x * y = y * x

A5: (id K) . y = y ;

( (id K) . (x * y) = x * y & (id K) . x = x ) ;

hence x * y = y * x by A4, A5, Th22; :: thesis: verum

end;A5: (id K) . y = y ;

( (id K) . (x * y) = x * y & (id K) . x = x ) ;

hence x * y = y * x by A4, A5, Th22; :: thesis: verum