let R be comRing; :: thesis: for a being Element of R holds
( a is Unit of R iff {a} -Ideal = [#] R )
let a be Element of R; :: thesis: ( a is Unit of R iff {a} -Ideal = [#] R )
set A = {a} -Ideal ;
B: now :: thesis: ( a is Unit of R implies {a} -Ideal = [#] R )
assume a is Unit of R ; :: thesis: {a} -Ideal = [#] R
then a divides 1. R by GCD_1:def 2;
then consider c being Element of R such that
A1: a * c = 1. R ;
now :: thesis: for x being object holds
( x in {a} -Ideal iff x in the carrier of R )
let x be object ; :: thesis: ( x in {a} -Ideal iff x in the carrier of R )
now :: thesis: ( x in the carrier of R implies x in {a} -Ideal )
assume x in the carrier of R ; :: thesis: x in {a} -Ideal
then reconsider x1 = x as Element of R ;
x = x1 * (c * a) by A1
.= a * (x1 * c) by GROUP_1:def 3 ;
then x in { (a * r) where r is Element of R : verum } ;
hence x in {a} -Ideal by IDEAL_1:64; :: thesis: verum
end;
hence ( x in {a} -Ideal iff x in the carrier of R ) ; :: thesis: verum
end;
hence {a} -Ideal = [#] R by TARSKI:2; :: thesis: verum
end;
now :: thesis: ( {a} -Ideal = [#] R implies a is Unit of R )
assume {a} -Ideal = [#] R ; :: thesis: a is Unit of R
then a is unital by div0;
hence a is Unit of R ; :: thesis: verum
end;
hence ( a is Unit of R iff {a} -Ideal = [#] R ) by B; :: thesis: verum