let R be commutative domRing-like Ring; :: thesis: for Amp being AmpleSet of R st Amp is multiplicative holds
for x, y being Element of Amp st y divides x & y <> 0. R holds
x / y in Amp
let Amp be AmpleSet of R; :: thesis: ( Amp is multiplicative implies for x, y being Element of Amp st y divides x & y <> 0. R holds
x / y in Amp )
assume A1: Amp is multiplicative ; :: thesis: for x, y being Element of Amp st y divides x & y <> 0. R holds
x / y in Amp
let x, y be Element of Amp; :: thesis: ( y divides x & y <> 0. R implies x / y in Amp )
assume that
A2: y divides x and
A3: y <> 0. R ; :: thesis: x / y in Amp
now :: thesis: ( ( x <> 0. R & x / y in Amp ) or ( x = 0. R & x / y in Amp ) )
per cases ( x <> 0. R or x = 0. R ) ;
case A4: x <> 0. R ; :: thesis: x / y in Amp
set d = x / y;
consider d9 being Element of Amp such that
A5: d9 is_associated_to x / y by Th22;
consider u being Element of R such that
A6: u is unital and
A7: (x / y) * u = d9 by A5, Th18;
x = y * (x / y) by A2, A3, Def4;
then A8: u * x = y * d9 by A7, GROUP_1:def 3;
A9: x is_associated_to u * x
proof
u divides 1. R by A6;
then consider e being Element of R such that
A10: u * e = 1. R ;
A11: x divides u * x ;
(u * x) * e = (e * u) * x by GROUP_1:def 3
.= x by A10 ;
then u * x divides x ;
hence x is_associated_to u * x by A11; :: thesis: verum
end;
A12: y * d9 in Amp by A1;
(1. R) * x = x
.= u * x by A8, A12, A9, Th22 ;
then u = 1. R by A4, Th1;
then d9 = x / y by A7;
hence x / y in Amp ; :: thesis: verum
end;
case A13: x = 0. R ; :: thesis: x / y in Amp
set d = x / y;
x = y * (x / y) by A2, A3, Def4;
then A14: x / y = 0. R by A3, A13, VECTSP_2:def 1;
0. R is Element of Amp by Th24;
hence x / y in Amp by A14; :: thesis: verum
end;
end;
end;
hence x / y in Amp ; :: thesis: verum