let R be domRing; :: thesis: ( R is Field iff for a being NonUnit of R holds a = 0. R )
A: now :: thesis: ( R is Field implies for a being NonUnit of R holds a = 0. R )
assume R is Field ; :: thesis: for a being NonUnit of R holds a = 0. R
then B: R is almost_left_invertible ;
let a be NonUnit of R; :: thesis: a = 0. R
now :: thesis: not a <> 0. R
assume a <> 0. R ; :: thesis: contradiction
then consider b being Element of R such that
C: b * a = 1. R by B, ALGSTR_0:def 27;
a divides 1. R by C;
hence contradiction by GCD_1:def 2; :: thesis: verum
end;
hence a = 0. R ; :: thesis: verum
end;
now :: thesis: ( ( for a being NonUnit of R holds a = 0. R ) implies R is Field )
assume B: for a being NonUnit of R holds a = 0. R ; :: thesis: R is Field
now :: thesis: for a being Element of R st a <> 0. R holds
a is left_invertible
let a be Element of R; :: thesis: ( a <> 0. R implies a is left_invertible )
assume a <> 0. R ; :: thesis: a is left_invertible
then a is Unit of R by B;
then a divides 1. R by GCD_1:def 2;
then consider b being Element of R such that
C: a * b = 1. R ;
thus a is left_invertible by C; :: thesis: verum
end;
then R is almost_left_invertible ;
hence R is Field ; :: thesis: verum
end;
hence ( R is Field iff for a being NonUnit of R holds a = 0. R ) by A; :: thesis: verum