let I be commutative domRing-like Ring; :: thesis: for F, F' being non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for f being Function of I,F
for f' being Function of I,F' st I has_Field_of_Quotients_Pair F,f & I has_Field_of_Quotients_Pair F',f' holds
F is_ringisomorph_to F'
let F, F' be non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; :: thesis: for f being Function of I,F
for f' being Function of I,F' st I has_Field_of_Quotients_Pair F,f & I has_Field_of_Quotients_Pair F',f' holds
F is_ringisomorph_to F'
let f be Function of I,F; :: thesis: for f' being Function of I,F' st I has_Field_of_Quotients_Pair F,f & I has_Field_of_Quotients_Pair F',f' holds
F is_ringisomorph_to F'
let f' be Function of I,F'; :: thesis: ( I has_Field_of_Quotients_Pair F,f & I has_Field_of_Quotients_Pair F',f' implies F is_ringisomorph_to F' )
assume that
A1: I has_Field_of_Quotients_Pair F,f and
A2: I has_Field_of_Quotients_Pair F',f' ; :: thesis: F is_ringisomorph_to F'
A3: (id F') * f' = f' by FUNCT_2:23;
A4: f is RingMonomorphism by A1, Def29;
then consider h2 being Function of F',F such that
A5: ( h2 is RingHomomorphism & h2 * f' = f ) and
for h' being Function of F',F st h' is RingHomomorphism & h' * f' = f holds
h' = h2 by A2, Def29;
consider h3 being Function of F,F such that
h3 is RingHomomorphism and
h3 * f = f and
A6: for h' being Function of F,F st h' is RingHomomorphism & h' * f = f holds
h' = h3 by A1, A4, Def29;
A7: (id F) * f = f by FUNCT_2:23;
A8: f' is RingMonomorphism by A2, Def29;
then consider h1 being Function of F,F' such that
A9: h1 is RingHomomorphism and
A10: h1 * f = f' and
for h' being Function of F,F' st h' is RingHomomorphism & h' * f = f' holds
h' = h1 by A1, Def29;
( (h2 * h1) * f = f & h2 * h1 is RingHomomorphism ) by A9, A10, A5, Th57, RELAT_1:55;
then A11: h2 * h1 = h3 by A6
.= id the carrier of F by A7, A6 ;
consider h3 being Function of F',F' such that
h3 is RingHomomorphism and
h3 * f' = f' and
A12: for h' being Function of F',F' st h' is RingHomomorphism & h' * f' = f' holds
h' = h3 by A2, A8, Def29;
( (h1 * h2) * f' = f' & h1 * h2 is RingHomomorphism ) by A9, A10, A5, Th57, RELAT_1:55;
then h1 * h2 = h3 by A12
.= id the carrier of F' by A3, A12 ;
then rng h1 = the carrier of F' by FUNCT_2:24;
then A13: h1 is RingEpimorphism by A9, Def22;
h1 is one-to-one by A11, FUNCT_2:37;
then h1 is RingMonomorphism by A9, Def23;
hence F is_ringisomorph_to F' by A13, Def26; :: thesis: verum