let R be non empty right_complementable add-associative right_zeroed well-unital distributive left_zeroed Euclidian doubleLoopStr ; :: thesis: R is PID
let I be Ideal of R; :: according to IDEAL_1:def 29 :: thesis: I is principal

per cases ( I = {(0. R)} or I <> {(0. R)} ) ;

suppose A1: I = {(0. R)} ; :: thesis: I is principal

set e = 0. R;
take 0. R ; :: according to IDEAL_1:def 28 :: thesis: I = {(0. R)} -Ideal
thus I = {(0. R)} -Ideal by A1, Th44; :: thesis: verum

end;

suppose I <> {(0. R)} ; :: thesis: I is principal

then consider x being Element of R such that
A2: ( x <> 0. R & x in I ) by Th96;
set I9 = { y where y is Element of I : y <> 0. R } ;
A3: { y where y is Element of I : y <> 0. R } c= the carrier of R

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { y where y is Element of I : y <> 0. R } or x in the carrier of R )
assume x in { y where y is Element of I : y <> 0. R } ; :: thesis: x in the carrier of R
then ex y being Element of I st
( x = y & y <> 0. R ) ;
hence x in the carrier of R ; :: thesis: verum

end;

x in { y where y is Element of I : y <> 0. R } by A2;
then reconsider I9 = { y where y is Element of I : y <> 0. R } as non empty Subset of R by A3;
consider f being Function of the carrier of R,NAT such that
A4: for a, b being Element of R st b <> 0. R holds
ex q, r being Element of R st
( a = (q * b) + r & ( r = 0. R or f . r < f . b ) ) by INT_3:def 9;
set K = { (f . i) where i is Element of I9 : verum } ;
consider i being Element of I9;
A5: f . i in { (f . i) where i is Element of I9 : verum } ;
{ (f . i) where i is Element of I9 : verum } c= NAT

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (f . i) where i is Element of I9 : verum } or x in NAT )
assume x in { (f . i) where i is Element of I9 : verum } ; :: thesis: x in NAT
then ex e being Element of I9 st f . e = x ;
hence x in NAT ; :: thesis: verum

end;

then reconsider K = { (f . i) where i is Element of I9 : verum } as non empty Subset of NAT by A5;
set k = min K;
min K in K by XXREAL_2:def 7;
then consider e being Element of I9 such that
A6: f . e = min K ;
e in I9 ;
then A7: ex e9 being Element of I st
( e9 = e & e9 <> 0. R ) ;
reconsider e = e as Element of R ;
take e ; :: according to IDEAL_1:def 28 :: thesis: I = {e} -Ideal

now

let x be set ; :: thesis: ( ( x in I implies x in {e} -Ideal ) & ( x in {e} -Ideal implies x in I ) )
{e} c= I by A7, ZFMISC_1:37;
then A8: {e} -Ideal c= I by Def15;

hereby :: thesis: ( x in {e} -Ideal implies x in I )

assume A9: x in I ; :: thesis: x in {e} -Ideal
then reconsider x9 = x as Element of R ;
consider q, r being Element of R such that
A10: x9 = (q * e) + r and
A11: ( r = 0. R or f . r < min K ) by A4, A6, A7;

now

q * e in I by A7, Def2;
then A12: - (q * e) in I by Th13;
assume A13: r <> 0. R ; :: thesis: contradiction
(- (q * e)) + x9 = ((- (q * e)) + (q * e)) + r by A10, RLVECT_1:def 6
.= (0. R) + r by RLVECT_1:16
.= r by ALGSTR_1:def 5 ;
then r in I by A9, A12, Def1;
then r in I9 by A13;
then f . r in K ;
hence contradiction by A11, A13, XXREAL_2:def 7; :: thesis: verum

end;

then A14: x9 = q * e by A10, RLVECT_1:def 7;
( e in {e} & {e} c= {e} -Ideal ) by Def15, TARSKI:def 1;
hence x in {e} -Ideal by A14, Def2; :: thesis: verum

end;

assume x in {e} -Ideal ; :: thesis: x in I
hence x in I by A8; :: thesis: verum

end;

hence I = {e} -Ideal by TARSKI:2; :: thesis: verum

end;

end;