let x be Element of F_Complex; :: thesis: ( x is algebraic implies FQ_Ring x is Field )
assume A1: x is algebraic ; :: thesis: FQ_Ring x is Field
for a being Element of (FQ_Ring x) st a <> 0. (FQ_Ring x) holds
a is left_invertible
proof
let a be Element of (FQ_Ring x); :: thesis: ( a <> 0. (FQ_Ring x) implies a is left_invertible )
assume a <> 0. (FQ_Ring x) ; :: thesis: a is left_invertible
then A4: a <> 0. F_Complex by SUBSET_1:def 8;
a in FQ x ;
then reconsider y = a as Element of F_Complex ;
consider b being Element of F_Complex such that
A5: b in the carrier of (FQ_Ring x) and
A6: y * b = 1. F_Complex by A1, A4, Th85;
reconsider a1 = y, b1 = b as Element of (FQ_Ring x) by A5;
b1 * a1 = 1. F_Complex by A6, Th50
.= 1. (FQ_Ring x) by Lm52 ;
hence a is left_invertible ; :: thesis: verum
end;
then FQ_Ring x is almost_left_invertible ;
hence FQ_Ring x is Field ; :: thesis: verum