let R be commutative domRing-like Ring; :: thesis: for a, b being Element of R holds
( a is_associated_to b iff ex c being Element of R st
( c is unital & a * c = b ) )
A1: for a, b being Element of R st a is_associated_to b holds
ex c being Element of R st
( c is unital & a * c = b )
proof
let A, B be Element of R; :: thesis: ( A is_associated_to B implies ex c being Element of R st
( c is unital & A * c = B ) )
assume A2: A is_associated_to B ; :: thesis: ex c being Element of R st
( c is unital & A * c = B )
then A divides B ;
then consider C being Element of R such that
A3: B = A * C ;
B divides A by A2;
then consider D being Element of R such that
A4: A = B * D ;
now :: thesis: ( ( A <> 0. R & ex c being Element of R st
( c is unital & A * c = B ) ) or ( A = 0. R & ex c being Element of R st
( c is unital & A * c = B ) ) )
per cases ( A <> 0. R or A = 0. R ) ;
case A5: A <> 0. R ; :: thesis: ex c being Element of R st
( c is unital & A * c = B )
A = A * (C * D) by A3, A4, GROUP_1:def 3;
then C * D = 1. R by A5, Th17;
then C divides 1. R ;
then C is unital ;
hence ex c being Element of R st
( c is unital & A * c = B ) by A3; :: thesis: verum
end;
case A6: A = 0. R ; :: thesis: ex c being Element of R st
( c is unital & A * c = B )
1. R divides 1. R ;
then A7: 1. R is unital ;
B = 0. R by A3, A6;
then B = A * (1. R) by A6;
hence ex c being Element of R st
( c is unital & A * c = B ) by A7; :: thesis: verum
end;
end;
end;
hence ex c being Element of R st
( c is unital & A * c = B ) ; :: thesis: verum
end;
for a, b being Element of R st ex c being Element of R st
( c is unital & a * c = b ) holds
a is_associated_to b
proof
let A, B be Element of R; :: thesis: ( ex c being Element of R st
( c is unital & A * c = B ) implies A is_associated_to B )
( ex c being Element of R st
( c is unital & A * c = B ) implies A is_associated_to B )
proof
now :: thesis: ( ex c being Element of R st
( c is unital & A * c = B ) & ex c being Element of R st
( c is unital & A * c = B ) implies A is_associated_to B )
assume ex c being Element of R st
( c is unital & A * c = B ) ; :: thesis: ( ex c being Element of R st
( c is unital & A * c = B ) implies A is_associated_to B )
then consider C being Element of R such that
A8: C is unital and
A9: A * C = B ;
C divides 1. R by A8;
then consider D being Element of R such that
A10: C * D = 1. R ;
A = A * (C * D) by A10
.= B * D by A9, GROUP_1:def 3 ;
then A11: B divides A ;
A divides B by A9;
hence ( ex c being Element of R st
( c is unital & A * c = B ) implies A is_associated_to B ) by A11; :: thesis: verum
end;
hence ( ex c being Element of R st
( c is unital & A * c = B ) implies A is_associated_to B ) ; :: thesis: verum
end;
hence ( ex c being Element of R st
( c is unital & A * c = B ) implies A is_associated_to B ) ; :: thesis: verum
end;
hence for a, b being Element of R holds
( a is_associated_to b iff ex c being Element of R st
( c is unital & a * c = b ) ) by A1; :: thesis: verum