let A be domRing; :: thesis: Total-Quotient-Ring A is Field
set S = Non_ZeroDiv_Set A;
A0: Non_ZeroDiv_Set A = ([#] A) \ {(0. A)} by Th4;
for x being Element of ((Non_ZeroDiv_Set A) ~ A) st x <> 0. ((Non_ZeroDiv_Set A) ~ A) holds
x is left_invertible
proof
let x be Element of ((Non_ZeroDiv_Set A) ~ A); :: thesis: ( x <> 0. ((Non_ZeroDiv_Set A) ~ A) implies x is left_invertible )
assume A1: x <> 0. ((Non_ZeroDiv_Set A) ~ A) ; :: thesis: x is left_invertible
consider a1, s1 being Element of A such that
A2: s1 in Non_ZeroDiv_Set A and
A3: x = Class ((EqRel (Non_ZeroDiv_Set A)),[a1,s1]) by Th46;
reconsider as1 = [a1,s1] as Element of Frac (Non_ZeroDiv_Set A) by A2, Def3;
a1 <> 0. A
proof
assume A5: a1 = 0. A ; :: thesis: contradiction
reconsider t = 1. A as Element of A ;
t in Non_ZeroDiv_Set A by C0SP1:def 4;
then as1, 0. (A,(Non_ZeroDiv_Set A)) Fr_Eq Non_ZeroDiv_Set A by A5;
then x = Class ((EqRel (Non_ZeroDiv_Set A)),(0. (A,(Non_ZeroDiv_Set A)))) by A3, Th26
.= 0. ((Non_ZeroDiv_Set A) ~ A) by Def6 ;
hence contradiction by A1; :: thesis: verum
end;
then not a1 in {(0. A)} by TARSKI:def 1;
then as1 `1 in Non_ZeroDiv_Set A by A0, XBOOLE_0:def 5;
then Class ((EqRel (Non_ZeroDiv_Set A)),as1) is Unit of ((Non_ZeroDiv_Set A) ~ A) by Lm45;
then x in Unit_Set ((Non_ZeroDiv_Set A) ~ A) by A3;
then (x ["]) * x = 1. ((Non_ZeroDiv_Set A) ~ A) by Def2;
hence x is left_invertible ; :: thesis: verum
end;
then (Non_ZeroDiv_Set A) ~ A is almost_left_invertible ;
hence Total-Quotient-Ring A is Field ; :: thesis: verum