:: The correctness of the Generic Algorithms of Brown and Henrici
:: concerning Addition and Multiplication in Fraction Fields
:: by Christoph Schwarzweller
::
:: Received June 16, 1997
:: Copyright (c) 1997-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies BINOP_1, VECTSP_1, XBOOLE_0, ALGSTR_0, SUBSET_1, MESFUNC1,
RELAT_1, LATTICES, ARYTM_3, FUNCSDOM, VECTSP_2, SUPINF_2, CARD_1,
STRUCT_0, RLVECT_1, ARYTM_1, GROUP_1, EQREL_1, TARSKI, SETFAM_1,
MSSUBFAM, INT_2, GCD_1, FUNCT_7, NUMBERS;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, STRUCT_0, ALGSTR_0,
RLVECT_1, GROUP_1, VECTSP_2, VECTSP_1;
constructors BINOP_2, VECTSP_2, MONOID_0;
registrations XBOOLE_0, SUBSET_1, MEMBERED, STRUCT_0, VECTSP_1, MONOID_0,
XREAL_0;
requirements SUBSET, BOOLE;
definitions VECTSP_1, VECTSP_2, XBOOLE_0;
equalities VECTSP_1;
expansions VECTSP_1, XBOOLE_0;
theorems TARSKI, WELLORD2, SUBSET_1, VECTSP_1, VECTSP_2, RLVECT_1, XBOOLE_0,
XCMPLX_1, GROUP_1, STRUCT_0, ALGSTR_0;
schemes SUBSET_1;
begin :: Basics
reserve X,Y for set;
:: Theorems about Integral Domains
registration
cluster commutative right_unital -> left_unital for non empty multLoopStr;
coherence
proof
let R be non empty multLoopStr such that
A1: R is commutative and
A2: R is right_unital;
let x be Element of R;
thus (1.R)*x = x*1.R by A1,GROUP_1:def 12
.= x by A2;
end;
end;
registration
cluster commutative right-distributive -> distributive for non empty
doubleLoopStr;
coherence
proof
let R be non empty doubleLoopStr such that
A1: R is commutative and
A2: R is right-distributive;
let x,y,z be Element of R;
thus x*(y+z) = x*y+x*z by A2;
thus (y+z)*x = x*(y+z) by A1,GROUP_1:def 12
.= x*y+x*z by A2
.= y*x+x*z by A1,GROUP_1:def 12
.= y*x+z*x by A1,GROUP_1:def 12;
end;
cluster commutative left-distributive -> distributive for non empty
doubleLoopStr;
coherence
proof
let R be non empty doubleLoopStr such that
A3: R is commutative and
A4: R is left-distributive;
let x,y,z be Element of R;
thus x*(y+z) = (y+z)*x by A3,GROUP_1:def 12
.= y*x+z*x by A4
.= x*y+z*x by A3,GROUP_1:def 12
.= x*y+x*z by A3,GROUP_1:def 12;
thus thesis by A4;
end;
end;
registration
cluster -> well-unital for Ring;
coherence;
end;
registration
cluster F_Real -> domRing-like;
coherence
proof
set D = F_Real;
hereby
let x,y be Element of F_Real;
A1: 0.D = In(0,REAL) by STRUCT_0:def 6;
assume x*y = 0.D & x <> 0.D;
hence y = 0.D by A1,XCMPLX_1:6;
end;
end;
end;
registration
cluster strict Abelian add-associative right_zeroed right_complementable
associative commutative domRing-like distributive well-unital
non degenerated almost_left_invertible for non empty doubleLoopStr;
existence
proof
take F_Real;
thus thesis;
end;
end;
reserve R for domRing-like commutative Ring;
reserve c for Element of R;
theorem Th1:
for R being domRing-like commutative Ring
for a,b,c being Element of R holds a <> 0.R implies
(a * b = a * c implies b = c) &
(b * a = c * a implies b = c)
proof
let R be domRing-like commutative Ring;
let a,b,c be Element of R;
assume
A1: a <> 0.R;
now
assume a * b = a * c;
then 0.R = (a * b) + (-(a * c)) by RLVECT_1:def 10
.= (a * b) + (a *(-c)) by VECTSP_1:8
.= a * (b + (-c)) by VECTSP_1:def 2
.= a * (b - c) by RLVECT_1:def 11;
then b - c = 0.R by A1,VECTSP_2:def 1;
then c = (b - c) + c by RLVECT_1:4
.= (b + (-c)) + c by RLVECT_1:def 11
.= b + (c + (-c)) by RLVECT_1:def 3
.= b + 0.R by RLVECT_1:def 10
.= b by RLVECT_1:4;
hence b = c;
end;
hence thesis;
end;
:: Definition of Divisibility
definition
let R be non empty multMagma;
let x,y be Element of R;
pred x divides y means
ex z being Element of R st y = x * z;
end;
definition
let R be right_unital non empty multLoopStr;
let x,y be Element of R;
redefine pred x divides y; :: redefines divides (GCD_1, definition)
reflexivity
proof
let A be Element of R;
A * 1.R = A;
hence thesis;
end;
end;
definition
let R be multLoopStr;
let x be Element of R;
attr x is unital means
ex y being Element of R st x * y = 1.R & y * x = 1.R;
end;
:: inserted 2026-08-10
registration
let R be multLoopStr;
cluster unital -> left_invertible for Element of R;
coherence
proof
let x be Element of R;
assume A1: x is unital;
then ex y being Element of R st y * x = 1. R;
hence x is left_invertible by ALGSTR_0:def 27;
end;
end;
:: inserted 2026-08-10
registration
let R be associative well-unital non empty multLoopStr;
cluster unital -> right_mult-cancelable for Element of R;
coherence
proof
let x be Element of R;
assume A1: x is unital;
for y, z being Element of R st y * x = z * x holds y = z
proof
let y, z be Element of R;
assume A2: y * x = z * x;
consider x1 being Element of R such that
A3: x * x1 = 1.R & x1 * x = 1.R by A1;
thus y = y * 1.R
.= y * (x * x1) by A3
.= (y * x) * x1 by GROUP_1:def 3
.= (z * x) * x1 by A2
.= z * (x * x1) by GROUP_1:def 3
.= z * 1.R by A3
.= z;
end;
hence x is right_mult-cancelable by ALGSTR_0:def 21;
end;
end;
registration :: from RING_2
let L be right_unital non empty multLoopStr;
cluster 1. L -> unital;
coherence
proof
1. L = (1. L) * (1. L);
hence 1. L is unital;
end;
end;
:: inserted 2026-08-10
notation
let R be associative well-unital non empty multLoopStr;
let x be Element of R;
synonym x " for / x;
end;
definition
let R be non empty multLoopStr;
let x,y be Element of R;
pred x is_associated_to y means
x divides y & y divides x;
symmetry;
end;
notation
let R be non empty multLoopStr;
let x,y be Element of R;
antonym x is_not_associated_to y for x is_associated_to y;
end;
definition
let R be well-unital non empty multLoopStr;
let x,y be Element of R;
redefine pred x is_associated_to y; :: redefines is_associated_to (GCD_1, definition)
reflexivity
proof
let a be Element of R;
thus a divides a & a divides a;
end;
end;
definition
let R be domRing-like commutative Ring;
let x,y be Element of R;
assume
A1: y divides x;
assume
A2: y <> 0.R;
func x/y -> Element of R means
:Def4:
it * y = x;
existence
proof
ex z being Element of R st x = y * z by A1;
hence thesis;
end;
uniqueness by A2,Th1;
end;
:: Some Lemmata about Divisibility
theorem Th2:
for R being associative non empty multLoopStr
for a,b,c being Element of R holds
a divides b & b divides c implies a divides c
proof
let R be associative non empty multLoopStr;
let A,B,C be Element of R;
now
assume that
A1: A divides B and
A2: B divides C;
consider D being Element of R such that
A3: A * D = B by A1;
consider E being Element of R such that
A4: B * E = C by A2;
A * (D * E) = C by A3,A4,GROUP_1:def 3;
hence thesis;
end;
hence thesis;
end;
theorem Th3:
for R being commutative associative non empty multLoopStr
for a,b,c,d being Element of R st
(b divides a & d divides c) holds (b * d) divides (a * c)
proof
let R be commutative associative non empty multLoopStr;
let a,b,c,d be Element of R;
assume that
A1: b divides a and
A2: d divides c;
consider x being Element of R such that
A3: b * x = a by A1;
consider y being Element of R such that
A4: d * y = c by A2;
(b * d) * (y * x) = ((b * d) * y) * x by GROUP_1:def 3
.= (b * c) * x by A4,GROUP_1:def 3
.= a * c by A3,GROUP_1:def 3;
hence thesis;
end;
theorem Th4:
for R being associative non empty multLoopStr for a,b,c being
Element of R holds a is_associated_to b & b is_associated_to c implies a
is_associated_to c by Th2;
theorem Th5:
for R being associative non empty multLoopStr
for a,b,c being Element of R holds
a divides b implies c * a divides c * b
proof
let R be associative non empty multLoopStr;
let A,B,C be Element of R;
assume A divides B;
then consider D being Element of R such that
A1: A * D = B;
(C * A) * D = C * B by A1,GROUP_1:def 3;
hence thesis;
end;
theorem
for R being non empty multLoopStr
for a,b being Element of R holds
a divides a * b & (R is commutative implies b divides a * b)
proof
let R be non empty multLoopStr;
let a,b be Element of R;
thus a divides a * b;
assume
A1: R is commutative;
take a;
thus thesis by A1,GROUP_1:def 12;
end;
theorem Th7:
for R being associative non empty multLoopStr
for a,b,c being Element of R holds
a divides b implies a divides b * c
proof
let R be associative non empty multLoopStr;
let a,b,c be Element of R;
assume a divides b;
then consider d being Element of R such that
A1: a * d = b;
a * (d * c) = b * c by A1,GROUP_1:def 3;
hence thesis;
end;
theorem Th8:
for a,b being Element of R holds
b divides a & b <> 0.R implies (a/b = 0.R iff a = 0.R)
proof
let a,b be Element of R;
assume that
A1: b divides a and
A2: b <> 0.R;
hereby
assume a/b = 0.R;
then a = 0.R * b by A1,A2,Def4
.= 0.R;
hence a = 0.R;
end;
assume a = 0.R;
then 0.R = (a/b) * b by A1,A2,Def4;
hence thesis by A2,VECTSP_2:def 1;
end;
theorem Th9:
for a being Element of R holds a <> 0.R implies a/a = 1.R
proof
let A be Element of R;
assume
A1: A <> 0.R;
then (A/A) * A = A by Def4
.= 1.R * A;
hence thesis by A1,Th1;
end;
theorem Th10:
for R being non degenerated domRing-like commutative Ring
for a being Element of R holds a/1.R = a
proof
let R be non degenerated domRing-like commutative Ring;
let a be Element of R;
set A = a/1.R;
1.R * a = a;
then
A1: 1.R <> 0.R & 1.R divides a;
A = A * 1.R
.= a by A1,Def4;
hence thesis;
end;
theorem Th11:
for a,b,c being Element of R holds
c <> 0.R implies
(c divides (a * b) & c divides a implies
(a * b) / c = (a / c) * b) &
(c divides (a * b) & c divides b implies
(a * b) / c = a * (b / c))
proof
let A,B,C be Element of R;
assume
A1: C <> 0.R;
A2: now
set A2 = B / C;
set A1 = (A * B) / C;
assume C divides (A * B) & C divides B;
then A1 * C = A * B & A2 * C = B by A1,Def4;
then A1 * C = (A * A2) * C by GROUP_1:def 3;
hence C divides (A * B) & C divides B implies (A * B) / C = A * (B / C) by
A1,Th1;
end;
now
set A2 = A / C;
set A1 = (A * B) / C;
assume C divides (A * B) & C divides A;
then A1 * C = A * B & A2 * C = A by A1,Def4;
then A1 * C = (A2 * B) * C by GROUP_1:def 3;
hence C divides (A * B) & C divides A implies (A * B) / C = (A / C) * B by
A1,Th1;
end;
hence thesis by A2;
end;
theorem Th12:
for a,b,c being Element of R holds
c <> 0.R & c divides a & c divides b & c divides (a + b)
implies (a/c) + (b/c) = (a + b)/c
proof
let a,b,c be Element of R;
assume
A1: c <> 0.R;
set e = b/c;
set d = a/c;
assume that
A2: c divides a & c divides b and
A3: c divides (a + b);
d * c = a & e * c = b by A1,A2,Def4;
then a + b = (d + e) * c by VECTSP_1:def 3;
then (a + b)/c = (d + e) * (c/c) by A1,A3,Th11
.= (d + e) * 1.R by A1,Th9
.= d + e;
hence thesis;
end;
theorem
for a,b,c being Element of R holds
c <> 0.R & c divides a & c divides b implies
(a/c = b/c iff a = b)
proof
let a,b,c be Element of R;
assume
A1: c <> 0.R;
assume that
A2: c divides a and
A3: c divides b;
now
assume (a/c) = (b/c);
consider e being Element of R such that
A4: e = (b/c);
e * c = b by A1,A3,A4,Def4;
hence a/c = b/c implies a = b by A1,A2,A4,Def4;
end;
hence thesis;
end;
theorem Th14:
for a,b,c,d being Element of R holds
b <> 0.R & d <> 0.R & b divides a & d divides c implies
(a/b) * (c/d) = (a * c) / (b * d)
proof
let a,b,c,d be Element of R;
assume that
A1: b <> 0.R & d <> 0.R and
A2: b divides a & d divides c;
A3: (b * d) divides (a * c) by A2,Th3;
set z = (a * c)/(b * d);
set y = c/d;
set x = a/b;
A4: (b * d) <> 0.R by A1,VECTSP_2:def 1;
x * b = a & y * d = c by A1,A2,Def4;
then z * (b * d) = (x * b) * (y * d) by A3,A4,Def4
.= x * (b * (y * d)) by GROUP_1:def 3
.= x * (y * (b * d)) by GROUP_1:def 3
.= (x * y) * (b * d) by GROUP_1:def 3;
hence thesis by A4,Th1;
end;
theorem Th15:
for a,b,c being Element of R holds
a <> 0.R & (a * b) divides (a * c) implies b divides c
proof
let A,B,C be Element of R;
assume that
A1: A <> 0.R and
A2: (A * B) divides (A * C);
consider D being Element of R such that
A3: (A * B) * D = A * C by A2;
A divides (A * C);
then
A4: (A * C)/A = (A/A) * C by A1,Th11;
A divides (A * (B * D));
then
A5: (A * (B * D))/A = (A/A) * (B * D) by A1,Th11;
A6: A * (B * D) = A * C by A3,GROUP_1:def 3;
B * D = 1.R * (B * D)
.= (A/A) * C by A1,A6,A5,A4,Th9
.= 1.R * C by A1,Th9
.= C;
hence thesis;
end;
theorem
for a being Element of R holds a is_associated_to 0.R implies a = 0.R
proof
let A be Element of R;
assume A is_associated_to 0.R;
then 0.R divides A;
then ex D being Element of R st 0.R * D = A;
hence thesis;
end;
theorem Th17:
for a,b being Element of R holds a <> 0.R & a * b = a implies b = 1.R
proof
let A,B be Element of R;
assume that
A1: A <> 0.R and
A2: A * B = A;
set A1 = A/A;
A1 = 1.R & (A * B)/A = (A/A) * B by A1,A2,Th9,Th11;
hence thesis by A2;
end;
theorem Th18:
for a,b being Element of R holds a is_associated_to b iff
ex c st c is unital & a * c = b
proof
A1: for a,b being Element of R holds a is_associated_to b implies
ex c being Element of R st c is unital & a * c = b
proof
let A,B be Element of R;
assume
A2: A is_associated_to 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
per cases;
case
A5: A <> 0.R;
A = A * (C * D) by A3,A4,GROUP_1:def 3;
then C * D = 1.R by A5,Th17;
then C is unital;
hence thesis by A3;
end;
case
A6: A = 0.R;
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 thesis by A7;
end;
end;
hence thesis;
end;
for a,b being Element of R holds (ex c being Element of R st (c is
unital & a * c = b)) implies a is_associated_to b
proof
let A,B be Element of R;
(ex c st (c is unital & A * c = B)) implies A is_associated_to B
proof
now
assume ex c st c is unital & A * c = 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 thesis by A11;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis by A1;
end;
theorem Th19:
for a,b,c being Element of R holds c <> 0.R & c * a
is_associated_to c * b implies a is_associated_to b by Th15;
begin
:: Definition of Ample Set
definition
let R be non empty multLoopStr;
let a be Element of R;
func Class a -> Subset of R means
:Def5:
for b being Element of R holds b in it iff b is_associated_to a;
existence
proof
set M = { b where b is Element of R: b is_associated_to a};
now
let B be object;
now
assume B in M;
then ex B9 being Element of R st B = B9 & B9 is_associated_to a;
hence B in M implies B in the carrier of R;
end;
hence B in M implies B in the carrier of R;
end;
then
A1: M c= the carrier of R by TARSKI:def 3;
now
let A be Element of R;
A in M implies A is_associated_to a
proof
assume A in M;
then ex A9 being Element of R st A = A9 & A9 is_associated_to a;
hence thesis;
end;
hence A in M iff A is_associated_to a;
end;
hence thesis by A1;
end;
uniqueness
proof
defpred P[Element of R] means $1 is_associated_to a;
let X1,X2 be Subset of R such that
A2: for y being Element of R holds y in X1 iff P[y] and
A3: for y being Element of R holds y in X2 iff P[y];
thus X1 = X2 from SUBSET_1:sch 2(A2,A3);
end;
end;
registration
let R be well-unital non empty multLoopStr;
let a be Element of R;
cluster Class a -> non empty;
coherence
proof
a is_associated_to a;
hence thesis by Def5;
end;
end;
theorem Th20:
for R being associative non empty multLoopStr
for a,b being Element of R holds
Class a meets Class b implies Class a = Class b
proof
let R be associative non empty multLoopStr;
let a,b be Element of R;
assume Class a /\ Class b <> {};
then Class a meets Class b;
then consider Z being object such that
A1: Z in Class a and
A2: Z in Class b by XBOOLE_0:3;
reconsider Z as Element of R by A1;
A3: Z is_associated_to b by A2,Def5;
A4: Z is_associated_to a by A1,Def5;
A5: for c being Element of R holds c in Class b implies c in Class a
proof
let c be Element of R;
assume c in Class b;
then c is_associated_to b by Def5;
then Z is_associated_to c by A3,Th4;
then a is_associated_to c by A4,Th4;
hence thesis by Def5;
end;
for c be Element of R holds c in Class a implies c in Class b
proof
let c be Element of R;
assume c in Class a;
then c is_associated_to a by Def5;
then Z is_associated_to c by A4,Th4;
then b is_associated_to c by A3,Th4;
hence thesis by Def5;
end;
hence thesis by A5,SUBSET_1:3;
end;
definition
let R be non empty multLoopStr;
func Classes R -> Subset-Family of R means
:Def6:
for A being Subset of R holds
A in it iff ex a being Element of R st A = Class a;
existence
proof
defpred P[set] means ex a being Element of R st $1 = Class a;
ex F being Subset-Family of R st for A being Subset of R holds A in F
iff P[A] from SUBSET_1:sch 3;
hence thesis;
end;
uniqueness
proof
defpred P[set] means ex a being Element of R st $1 = Class a;
let F1,F2 be Subset-Family of R;
assume
A1: for A being Subset of R holds A in F1 iff P[A];
assume
A2: for A being Subset of R holds A in F2 iff P[A];
thus thesis from SUBSET_1:sch 4(A1,A2);
end;
end;
registration
let R be non empty multLoopStr;
cluster Classes R -> non empty;
coherence
proof
Class 1.R in Classes R by Def6;
hence thesis;
end;
end;
theorem Th21:
for R being well-unital non empty multLoopStr
for X being Subset of R holds
X in Classes R implies X is non empty
proof
let R be well-unital non empty multLoopStr;
let X be Subset of R;
assume X in Classes R;
then ex a being Element of R st X = Class a by Def6;
hence thesis;
end;
definition
let R be associative well-unital non empty multLoopStr;
mode Am of R -> non empty Subset of R means
:Def7:
(for a being Element of R
ex z being Element of it st z is_associated_to a) &
for x,y being Element of it
holds x <> y implies x is_not_associated_to y;
existence
proof
now
let R be associative well-unital non empty multLoopStr;
reconsider M = Classes R as non empty set;
A1: for X st X in M holds X <> {}
proof
let X be set;
assume X in M;
then ex A being Element of R st X = Class A by Def6;
hence thesis;
end;
for X,Y st X in M & Y in M & X <> Y holds X misses Y
proof
let X,Y be set such that
A2: X in M & Y in M and
A3: X <> Y;
assume
A4: X meets Y;
(ex A being Element of R st X = Class A )& ex B being Element of R
st Y = Class B by A2,Def6;
hence contradiction by A3,A4,Th20;
end;
then consider AmpS9 being set such that
A5: for X st X in M ex x being object st AmpS9 /\ X = {x} by A1,WELLORD2:18;
AmpS9 is non empty
proof
Class 1.R in M by Def6;
then ex x being object st AmpS9 /\ Class 1.R = {x} by A5;
hence thesis;
end;
then reconsider AmpS9 as non empty set;
set AmpS = { x where x is Element of AmpS9: ex X being non empty Subset
of R st X in M & AmpS9 /\ X = { x }};
A6: AmpS is non empty Subset of R
proof
AmpS is non empty
proof
A7: Class 1.R in M by Def6;
then consider x being object such that
A8: AmpS9 /\ Class 1.R = {x} by A5;
x in {x} by TARSKI:def 1;
then x in AmpS9 by A8,XBOOLE_0:def 4;
then x in AmpS by A7,A8;
hence thesis;
end;
then reconsider AmpS as non empty set;
now
let A be object;
now
assume A in AmpS;
then consider x being Element of AmpS9 such that
A9: A = x & ex X being non empty Subset of R st X in M &
AmpS9 /\ X = {x};
x in {x} by TARSKI:def 1;
hence A in AmpS implies A in the carrier of R by A9;
end;
hence A in AmpS implies A in the carrier of R;
end;
hence thesis by TARSKI:def 3;
end;
A10: for X being Element of M holds ex z being Element of AmpS st AmpS
/\ X = {z}
proof
let X be Element of M;
consider x being object such that
A11: AmpS9 /\ X = {x} by A5;
X in Classes R;
then
A12: X is non empty Subset of R by Th21;
A13: x in {x} by TARSKI:def 1;
then x in AmpS9 by A11,XBOOLE_0:def 4;
then
A14: x in AmpS by A11,A12;
A15: x in X by A11,A13,XBOOLE_0:def 4;
now
let y be object;
A16: now
assume
A17: y in AmpS /\ X;
then y in AmpS by XBOOLE_0:def 4;
then
A18: ex zz being Element of AmpS9 st y = zz & ex X being non empty
Subset of R st X in M & AmpS9 /\ X = {zz};
y in X by A17,XBOOLE_0:def 4;
hence y in AmpS /\ X implies y in {x} by A11,A18,XBOOLE_0:def 4;
end;
now
assume y in {x};
then y = x by TARSKI:def 1;
hence y in {x} implies y in AmpS /\ X by A15,A14,XBOOLE_0:def 4;
end;
hence y in {x} iff y in AmpS /\ X by A16;
end;
then AmpS /\ X = {x} by TARSKI:2;
hence thesis by A14;
end;
reconsider AmpS as non empty Subset of R by A6;
A19: for x,y being Element of AmpS holds x <> y implies x
is_not_associated_to y
proof
let x,y be Element of AmpS;
assume
A20: x <> y;
x is_associated_to x;
then x in Class x by Def5;
then
A21: x in AmpS /\ Class x by XBOOLE_0:def 4;
Class x in M by Def6;
then consider z being Element of AmpS such that
A22: AmpS /\ Class x = {z} by A10;
assume x is_associated_to y;
then y in Class x by Def5;
then y in AmpS /\ Class x by XBOOLE_0:def 4;
then y = z by A22,TARSKI:def 1;
hence thesis by A20,A21,A22,TARSKI:def 1;
end;
for a being Element of R ex z being Element of AmpS st z
is_associated_to a
proof
let a be Element of R;
reconsider N = Class a as Element of M by Def6;
consider z being Element of AmpS such that
A23: AmpS /\ N = {z} by A10;
z in {z} by TARSKI:def 1;
then z in Class a by A23,XBOOLE_0:def 4;
then z is_associated_to a by Def5;
hence thesis;
end;
hence ex s being non empty Subset of R st (for a being Element of R ex z
being Element of s st z is_associated_to a) & for x,y being Element of s holds
x <> y implies x is_not_associated_to y by A19;
end;
hence thesis;
end;
end;
definition
let R be associative well-unital non empty multLoopStr;
mode AmpleSet of R -> non empty Subset of R means
:Def8:
it is Am of R & 1.R in it;
existence
proof
now
let A be Am of R;
consider x being Element of A such that
A1: x is_associated_to 1.R by Def7;
set A9 = { z where z is Element of A : z <> x } \/ {1.R};
1.R in {1.R} by TARSKI:def 1;
then
A2: 1.R in A9 by XBOOLE_0:def 3;
reconsider A9 as non empty set;
A3: for x being Element of A9 holds x = 1.R or x in A
proof
let y be Element of A9;
per cases by XBOOLE_0:def 3;
suppose
y in {z where z is Element of A: z <> x};
then ex zz being Element of A st y = zz & zz <> x;
hence thesis;
end;
suppose
y in {1.R};
hence thesis by TARSKI:def 1;
end;
end;
now
let x be object;
now
assume
A4: x in A9;
x in the carrier of R
proof
now
per cases by A3,A4;
case
x = 1.R;
hence thesis;
end;
case
x in A;
hence thesis;
end;
end;
hence thesis;
end;
hence x in A9 implies x in the carrier of R;
end;
hence x in A9 implies x in the carrier of R;
end;
then reconsider A9 as non empty Subset of R by TARSKI:def 3;
A5: for z,y being Element of A9 holds z <> y implies z is_not_associated_to y
proof
let z,y be Element of A9;
assume
A6: z <> y;
now
per cases;
case
z = 1.R & y = 1.R;
hence thesis by A6;
end;
case
A7: z = 1.R & y <> 1.R;
assume z is_associated_to y;
not y in {1.R} by A7,TARSKI:def 1;
then y in {zz where zz is Element of A: zz <> x} by XBOOLE_0:def 3;
then ex zz being Element of A st y = zz & zz <> x;
hence thesis by A1,A7,Def7,Th4;
end;
case
A8: z <> 1.R & y = 1.R;
assume z is_associated_to y;
not z in {1.R} by A8,TARSKI:def 1;
then z in {zz where zz is Element of A: zz <> x} by XBOOLE_0:def 3;
then ex zz being Element of A st z = zz & zz <> x;
hence thesis by A1,A8,Def7,Th4;
end;
case
z <> 1.R & y <> 1.R;
then z in A & y in A by A3;
hence thesis by A6,Def7;
end;
end;
hence thesis;
end;
for a being Element of R ex z being Element of A9 st z is_associated_to a
proof
let a be Element of R;
now
per cases;
case
a is_associated_to 1.R;
hence thesis by A2;
end;
case
A9: a is_not_associated_to 1.R;
consider z being Element of A such that
A10: z is_associated_to a by Def7;
z <> x by A1,A9,A10,Th4;
then z in {zz where zz is Element of A : zz <> x};
then z in A9 by XBOOLE_0:def 3;
hence thesis by A10;
end;
end;
hence thesis;
end;
then A9 is Am of R by A5,Def7;
hence thesis by A2;
end;
hence thesis;
end;
end;
theorem Th22:
for R being associative well-unital non empty multLoopStr
for Amp being AmpleSet of R holds
(1.R in Amp) &
(for a being Element of R ex z being Element of Amp st
z is_associated_to a) &
(for x,y being Element of Amp holds x <> y implies
x is_not_associated_to y)
proof
let R be associative well-unital non empty multLoopStr;
let Amp be AmpleSet of R;
Amp is Am of R by Def8;
hence thesis by Def7,Def8;
end;
theorem
for R being associative well-unital non empty multLoopStr
for Amp being AmpleSet of R
for x,y being Element of Amp holds x is_associated_to y
implies x = y by Th22;
theorem Th24:
for Amp being AmpleSet of R holds 0.R is Element of Amp
proof
let Amp be AmpleSet of R;
consider A being Element of Amp such that
A1: A is_associated_to 0.R by Th22;
0.R divides A by A1;
then ex D being Element of R st 0.R * D = A;
hence thesis;
end;
:: Definition of Normalform
definition
let R be associative well-unital non empty multLoopStr;
let Amp be AmpleSet of R;
let x be Element of R;
func NF(x,Amp) -> Element of R means
:Def9:
it in Amp & it is_associated_to x;
existence
proof
now
let Amp be AmpleSet of R;
let x be Element of R;
ex z being Element of Amp st z is_associated_to x by Th22;
hence ex zz being Element of R st zz in Amp & zz is_associated_to x;
end;
hence thesis;
end;
uniqueness by Th4,Th22;
end;
theorem Th25:
for Amp being AmpleSet of R holds NF(0.R,Amp) = 0.R & NF(1.R,Amp) = 1.R
proof
let Amp be AmpleSet of R;
1.R in Amp & 0.R is Element of Amp by Def8,Th24;
hence thesis by Def9;
end;
theorem
for Amp being AmpleSet of R for a being Element of R holds
a in Amp iff a = NF(a,Amp) by Def9;
:: Definition of multiplicative AmpleSet
definition
let R be associative well-unital non empty multLoopStr;
let Amp be AmpleSet of R;
attr Amp is multiplicative means
for x,y being Element of Amp holds x * y in Amp;
end;
theorem Th27:
for Amp being AmpleSet of R holds Amp is multiplicative implies
for x,y being Element of Amp holds y divides x & y <> 0.R implies x/y in Amp
proof
let Amp be AmpleSet of R;
assume
A1: Amp is multiplicative;
let x,y be Element of Amp;
assume that
A2: y divides x and
A3: y <> 0.R;
now
per cases;
case
A4: x <> 0.R;
set d = x/y;
consider d9 being Element of Amp such that
A5: d9 is_associated_to d by Th22;
consider u being Element of R such that
A6: u is unital and
A7: d * u = d9 by A5,Th18;
x = y * d 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 thesis by A11;
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 = d by A7;
hence thesis;
end;
case
A13: x = 0.R;
set d = x/y;
x = y * d by A2,A3,Def4;
then
A14: d = 0.R by A3,A13,VECTSP_2:def 1;
0.R is Element of Amp by Th24;
hence thesis by A14;
end;
end;
hence thesis;
end;
begin
:: Definition of GCD-Domain
definition
let R be non empty multLoopStr;
attr R is gcd-like means
:Def11:
for x,y being Element of R
ex z being Element of R st
z divides x & z divides y &
for zz being Element of R st zz divides x & zz divides y holds
zz divides z;
end;
Lm1: now
let F be Field;
let x,y be Element of F;
now
per cases;
case
A1: x <> 0.F & y <> 0.F;
A2: for zz being Element of F st zz divides x & zz divides y holds zz
divides (1_F)
proof
let zz be Element of F;
assume that
A3: zz divides x and
zz divides y;
now
per cases;
case
zz <> 0.F;
then ex zz9 being Element of F st zz9 * zz = (1_F) by
VECTSP_1:def 9;
hence thesis;
end;
case
A4: zz = 0.F;
assume zz divides x;
then ex d being Element of F st zz * d = x;
hence thesis by A1,A4;
end;
end;
hence thesis by A3;
end;
y = (1_F) * y;
then
A5: (1_F) divides y;
x = (1_F) * x;
then (1_F) divides x;
hence
ex z being Element of F st z divides x & z divides y & for zz being
Element of F st zz divides x & zz divides y holds zz divides z by A5,A2;
end;
case
A6: x = 0.F;
y * 0.F = 0.F;
then
A7: y divides 0.F;
for z being Element of F st z divides 0.F & z divides y holds z
divides y;
hence
ex z being Element of F st z divides x & z divides y & for zz being
Element of F st zz divides x & zz divides y holds zz divides z by A6,A7;
end;
case
A8: y = 0.F;
x * 0.F = 0.F;
then
A9: x divides 0.F;
for z being Element of F st z divides x & z divides 0.F holds z
divides x;
hence
ex z being Element of F st z divides x & z divides y & for zz being
Element of F st zz divides x & zz divides y holds zz divides z by A8,A9;
end;
end;
hence ex z being Element of F st z divides x & z divides y & for zz being
Element of F st zz divides x & zz divides y holds zz divides z;
end;
registration
cluster gcd-like for domRing;
existence
proof
set F = the strict Field;
reconsider F as comRing;
reconsider F as domRing by VECTSP_2:1;
for x,y be Element of F holds ex z being Element of F st z divides x &
z divides y & for zz being Element of F st zz divides x & zz divides y holds zz
divides z by Lm1;
then F is gcd-like;
hence thesis;
end;
end;
registration
cluster gcd-like associative commutative well-unital for
non empty multLoopStr;
existence
proof
set F = the strict Field;
for x,y be Element of F holds ex z being Element of F st z divides x &
z divides y & for zz being Element of F st zz divides x & zz divides y holds zz
divides z by Lm1;
then F is gcd-like;
hence thesis;
end;
end;
registration
cluster gcd-like associative commutative well-unital for non empty
multLoopStr_0;
existence
proof
set F = the strict Field;
for x,y be Element of F holds ex z being Element of F st z divides x &
z divides y & for zz being Element of F st zz divides x & zz divides y holds zz
divides z by Lm1;
then F is gcd-like;
hence thesis;
end;
end;
registration
cluster -> gcd-like for almost_left_invertible add-associative right_zeroed
right_complementable left_unital well-unital left-distributive
right-distributive commutative non empty doubleLoopStr;
coherence
proof
let F be almost_left_invertible add-associative right_zeroed
right_complementable left_unital well-unital left-distributive
right-distributive commutative non empty doubleLoopStr;
let x,y be Element of F;
now
per cases;
case
A1: x <> 0.F & y <> 0.F;
A2: for zz being Element of F st zz divides x & zz divides y holds zz
divides 1_F
proof
let zz be Element of F;
assume that
A3: zz divides x and
zz divides y;
now
per cases;
case
zz <> 0.F;
then ex zz9 being Element of F st zz9 * zz = 1_F by
VECTSP_1:def 9;
hence thesis;
end;
case
A4: zz = 0.F;
assume zz divides x;
then ex d being Element of F st zz * d = x;
hence thesis by A1,A4;
end;
end;
hence thesis by A3;
end;
y = 1_F * y;
then
A5: 1_F divides y;
x = 1_F * x;
then 1_F divides x;
hence ex z being Element of F st z divides x & z divides y & for zz
being Element of F st zz divides x & zz divides y holds zz divides z by A5,A2;
end;
case
A6: x = 0.F;
y * 0.F = 0.F;
then
A7: y divides 0.F;
for z being Element of F st z divides 0.F & z divides y holds z
divides y;
hence ex z being Element of F st z divides x & z divides y & for zz
being Element of F st zz divides x & zz divides y holds zz divides z by A6,A7;
end;
case
A8: y = 0.F;
x * 0.F = 0.F;
then
A9: x divides 0.F;
for z being Element of F st z divides x & z divides 0.F holds z
divides x;
hence ex z being Element of F st z divides x & z divides y & for zz
being Element of F st zz divides x & zz divides y holds zz divides z by A8,A9;
end;
end;
hence thesis;
end;
end;
registration
cluster gcd-like associative commutative well-unital domRing-like unital
distributive non degenerated Abelian add-associative right_zeroed
right_complementable for non empty doubleLoopStr;
existence
proof
take F_Real;
thus thesis;
end;
end;
definition
mode gcdDomain is gcd-like domRing-like non degenerated commutative Ring;
end;
definition
let R be gcd-like associative well-unital non empty multLoopStr;
let Amp be AmpleSet of R;
let x,y be Element of R;
func gcd(x,y,Amp) -> Element of R means
:Def12:
it in Amp & it divides x &
it divides y & for z being Element of R st z divides x & z divides y holds z
divides it;
existence
proof
consider u being Element of R such that
A1: u divides x & u divides y and
A2: for zz being Element of R st zz divides x & zz divides y holds zz
divides u by Def11;
consider z being Element of Amp such that
A3: z is_associated_to u by Th22;
A4: for zz being Element of R st zz divides x & zz divides y holds zz divides z
proof
let zz be Element of R;
assume zz divides x & zz divides y;
then
A5: zz divides u by A2;
u divides z by A3;
hence thesis by A5,Th2;
end;
z divides u by A3;
then z divides x & z divides y by A1,Th2;
hence thesis by A4;
end;
uniqueness
proof
now
let z1 be Element of R such that
A6: z1 in Amp and
A7: z1 divides x & z1 divides y & for z being Element of R st z
divides x & z divides y holds z divides z1;
let z2 be Element of R such that
A8: z2 in Amp and
A9: z2 divides x & z2 divides y & for z being Element of R st z
divides x & z divides y holds z divides z2;
z1 divides z2 & z2 divides z1 by A7,A9;
then z1 is_associated_to z2;
hence z1 = z2 by A6,A8,Th22;
end;
hence thesis;
end;
end;
reserve R for gcdDomain;
:: Lemmata about GCD
theorem Th28:
for Amp being AmpleSet of R for a,b,c being Element of R holds
c divides gcd(a,b,Amp) implies c divides a & c divides b
proof
let Amp be AmpleSet of R;
let A,B,C be Element of R;
assume C divides gcd(A,B,Amp);
then consider D being Element of R such that
A1: C * D = gcd(A,B,Amp);
gcd(A,B,Amp) divides A by Def12;
then consider E being Element of R such that
A2: gcd(A,B,Amp) * E = A;
A3: C * (D * E) = A by A1,A2,GROUP_1:def 3;
gcd(A,B,Amp) divides B by Def12;
then consider E being Element of R such that
A4: gcd(A,B,Amp) * E = B;
C * (D * E) = B by A1,A4,GROUP_1:def 3;
hence thesis by A3;
end;
theorem Th29:
for Amp being AmpleSet of R for a,b being Element of R holds
gcd(a,b,Amp) = gcd(b,a,Amp)
proof
let Amp be AmpleSet of R;
let A,B be Element of R;
set D = gcd(A,B,Amp);
A1: D divides A & for z being Element of R st z divides B & z divides A
holds z divides D by Def12;
D in Amp & D divides B by Def12;
hence thesis by A1,Def12;
end;
theorem Th30:
for Amp being AmpleSet of R for a being Element of R holds
gcd(a,0.R,Amp) = NF(a,Amp) & gcd(0.R,a,Amp) = NF(a,Amp)
proof
let Amp be AmpleSet of R;
let A be Element of R;
A1: NF(A,Amp) in Amp by Def9;
NF(A,Amp) * 0.R = 0.R;
then
A2: NF(A,Amp) divides 0.R;
A3: NF(A,Amp)is_associated_to A by Def9;
A4: for z being Element of R st z divides A & z divides 0.R holds z divides
NF(A,Amp)
by A3,Th2;
NF(A,Amp) divides A by A3;
then gcd(A,0.R,Amp) = NF(A,Amp) by A2,A4,A1,Def12;
hence thesis by Th29;
end;
theorem Th31:
for Amp being AmpleSet of R holds gcd(0.R,0.R,Amp) = 0.R
proof
let Amp be AmpleSet of R;
gcd(0.R,0.R,Amp) = NF(0.R,Amp) by Th30;
hence thesis by Th25;
end;
theorem Th32:
for Amp being AmpleSet of R for a being Element of R holds
gcd(a,1.R,Amp) = 1.R & gcd(1.R,a,Amp) = 1.R
proof
let Amp be AmpleSet of R;
let A be Element of R;
1.R * A = A;
then
A1: 1.R divides A;
1.R in Amp & for z being Element of R st z divides A & z divides 1.R
holds z divides 1.R by Def8;
then gcd(A,1.R,Amp) = 1.R by A1,Def12;
hence thesis by Th29;
end;
theorem Th33:
for Amp being AmpleSet of R for a,b being Element of R holds
gcd(a,b,Amp) = 0.R iff a = 0.R & b = 0.R
proof
let Amp be AmpleSet of R;
let A,B be Element of R;
A1: now
assume
A2: gcd(A,B,Amp) = 0.R;
then 0.R divides B by Def12;
then
A3: ex E being Element of R st 0.R * E = B;
0.R divides A by A2,Def12;
then ex D being Element of R st 0.R * D = A;
hence gcd(A,B,Amp) = 0.R implies A = 0.R & B = 0.R by A3;
end;
A = 0.R & B = 0.R implies gcd(A,B,Amp) = 0.R
proof
assume that
A4: A = 0.R and
A5: B = 0.R;
gcd(A,B,Amp) = NF(A,Amp) by A5,Th30;
hence thesis by A4,Th25;
end;
hence thesis by A1;
end;
theorem Th34:
for Amp being AmpleSet of R for a,b,c being Element of R holds
b is_associated_to c implies
gcd(a,b,Amp) is_associated_to gcd(a,c,Amp) &
gcd(b,a,Amp) is_associated_to gcd(c,a,Amp)
proof
let Amp be AmpleSet of R;
let A,B,C be Element of R;
A1: gcd(A,B,Amp) divides B by Def12;
A2: gcd(A,B,Amp) divides A by Def12;
A3: gcd(A,C,Amp) divides A by Def12;
A4: gcd(A,C,Amp) divides C by Def12;
A5: gcd(A,B,Amp) = gcd(B,A,Amp) by Th29;
assume
A6: B is_associated_to C;
then C divides B;
then gcd(A,C,Amp) divides B by A4,Th2;
then
A7: gcd(A,C,Amp) divides gcd(A,B,Amp) by A3,Def12;
B divides C by A6;
then gcd(A,B,Amp) divides C by A1,Th2;
then gcd(A,B,Amp) divides gcd(A,C,Amp) by A2,Def12;
then gcd(A,B,Amp) is_associated_to gcd(A,C,Amp) by A7;
hence thesis by A5,Th29;
end;
:: Main Theorems
theorem Th35:
for Amp being AmpleSet of R for a,b,c being Element of R holds
gcd(gcd(a,b,Amp),c,Amp) = gcd(a,gcd(b,c,Amp),Amp)
proof
let Amp be AmpleSet of R;
let A,B,C be Element of R;
set D = gcd(gcd(A,B,Amp),C,Amp);
set E = gcd(A,gcd(B,C,Amp),Amp);
A1: D divides C by Def12;
A2: E divides A by Def12;
A3: E divides gcd(B,C,Amp) by Def12;
then
A4: E divides C by Th28;
E divides B by A3,Th28;
then E divides gcd(A,B,Amp) by A2,Def12;
then
A5: E divides D by A4,Def12;
A6: D is Element of Amp & E is Element of Amp by Def12;
A7: D divides gcd(A,B,Amp) by Def12;
then
A8: D divides A by Th28;
D divides B by A7,Th28;
then D divides gcd(B,C,Amp) by A1,Def12;
then D divides E by A8,Def12;
then D is_associated_to E by A5;
hence thesis by A6,Th22;
end;
theorem Th36:
for Amp being AmpleSet of R for a,b,c being Element of R holds
gcd(a * c,b * c,Amp) is_associated_to (c * gcd(a,b,Amp))
proof
let Amp be AmpleSet of R;
let A,B,C be Element of R;
now
per cases;
case
A1: C <> 0.R;
set D = gcd(A,B,Amp);
now
per cases;
case
A2: D <> 0.R;
set E = gcd((A * C),(B * C),Amp);
A3: E divides B * C by Def12;
D divides B by Def12;
then
A4: C * D divides B * C by Th5;
D divides A by Def12;
then C * D divides A * C by Th5;
then C * D divides gcd((A * C),(B * C),Amp) by A4,Def12;
then consider F being Element of R such that
A5: E = (C * D) * F;
A6: E divides A * C by Def12;
(D * F) divides A & (D * F) divides B
proof
consider G being Element of R such that
A7: ((C * D) * F) * G = A * C by A5,A6;
(C * (D * F)) * G = C * A by A7,GROUP_1:def 3;
then
A8: (C * (D * F)) divides C * A;
consider G being Element of R such that
A9: ((C * D) * F) * G = B * C by A5,A3;
(C * (D * F)) * G = C * B by A9,GROUP_1:def 3;
then (C * (D * F)) divides C * B;
hence thesis by A1,A8,Th15;
end;
then
A10: D * F divides D by Def12;
D = D * 1.R;
then F divides 1.R by A2,A10,Th15;
then ex y being Element of R st 1.R = F * y;
then F is unital;
hence thesis by A5,Th18;
end;
case
A11: D = 0.R;
then
A12: C * gcd(A,B,Amp) = 0.R;
A = 0.R & B = 0.R by A11,Th33;
then gcd((A * C),(B * C),Amp) = gcd(0.R,(0.R * C),Amp)
.= gcd(0.R,0.R,Amp)
.= C * gcd(A,B,Amp) by A12,Th31;
hence thesis;
end;
end;
hence thesis;
end;
case
A13: C = 0.R;
then A * C = 0.R & B * C = 0.R;
then gcd((A * C),(B * C),Amp) = 0.R by Th31
.= C * gcd(A,B,Amp) by A13;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th37:
for Amp being AmpleSet of R for a,b,c being Element of R holds
gcd(a,b,Amp) = 1.R implies gcd(a,(b * c),Amp) = gcd(a,c,Amp)
proof
let Amp be AmpleSet of R;
let A,B,C be Element of R;
assume gcd(A,B,Amp) = 1.R;
then
A1: C * (gcd(A,B,Amp)) = C;
gcd((A * C),(B * C),Amp) is_associated_to (C * gcd(A,B,Amp)) by Th36;
then gcd(A,C,Amp) is_associated_to gcd(A,gcd((A * C),(B * C),Amp),Amp) by A1
,Th34;
then
A2: gcd(A,C,Amp) is_associated_to gcd(gcd(A,(A * C),Amp),(B * C),Amp) by Th35;
A3: A * gcd(1.R,C,Amp) = A * 1.R by Th32
.= A;
gcd((A * 1.R),(A * C),Amp) is_associated_to (A * gcd(1.R,C,Amp)) by Th36;
then gcd(A,(A * C),Amp) is_associated_to A by A3;
then
A4: gcd(gcd(A,(A * C),Amp),(B * C),Amp) is_associated_to gcd(A,(B * C),Amp)
by Th34;
gcd(A,(B * C),Amp) is Element of Amp & gcd(A,C,Amp) is Element of Amp
by Def12;
hence thesis by A2,A4,Th4,Th22;
end;
theorem Th38:
for Amp being AmpleSet of R for a,b,c being Element of R holds
c = gcd(a,b,Amp) & c <> 0.R implies gcd((a/c),(b/c),Amp) = 1.R
proof
let Amp be AmpleSet of R;
let A,B,C be Element of R;
assume that
A1: C = gcd(A,B,Amp) and
A2: C <> 0.R;
set A1 = A/C;
C divides A by A1,Def12;
then
A3: A1 * C = A by A2,Def4;
set B1 = B/C;
A4: gcd((A1 * C),(B1 * C),Amp) is_associated_to (C * gcd(A1,B1,Amp)) by Th36;
A5: gcd(A1,B1,Amp) is Element of Amp & 1.R is Element of Amp by Def8,Def12;
C divides B by A1,Def12;
then gcd(A,B,Amp) = gcd((A1 * C),(B1 * C),Amp) by A2,A3,Def4;
then (C * 1.R) is_associated_to (C * gcd(A1,B1,Amp)) by A1,A4;
hence thesis by A2,A5,Th19,Th22;
end;
theorem Th39:
for Amp being AmpleSet of R for a,b,c being Element of R holds
gcd((a + (b * c)),c,Amp) = gcd(a,c,Amp)
proof
let Amp be AmpleSet of R;
let A,B,C be Element of R;
set D = gcd(A,C,Amp);
D divides A by Def12;
then consider E being Element of R such that
A1: D * E = A;
A2: D divides C by Def12;
then consider F being Element of R such that
A3: D * F = C;
A4: for z being Element of R st z divides (A + (B * C)) & z divides C holds
z divides D
proof
let Z be Element of R;
assume that
A5: Z divides (A + (B * C)) and
A6: Z divides C;
consider X being Element of R such that
A7: Z * X = C by A6;
consider Y being Element of R such that
A8: Z * Y = A + (B * C) by A5;
Z * (Y + (-(B * X))) = (Z * Y) + (Z * (-(B * X))) by VECTSP_1:def 2
.= (Z * Y) + (-(Z * (X * B))) by VECTSP_1:8
.= (A + (B * C)) + (-(C * B)) by A7,A8,GROUP_1:def 3
.= A + ((B * C) + (-(C * B))) by RLVECT_1:def 3
.= A + 0.R by RLVECT_1:def 10
.= A by RLVECT_1:4;
then Z divides A;
hence thesis by A6,Def12;
end;
D * (E + (F * B)) = (D * E) + (D * (F * B)) by VECTSP_1:def 2
.= A + (B * C) by A1,A3,GROUP_1:def 3;
then
A9: D divides (A + (B * C));
D is Element of Amp by Def12;
hence thesis by A2,A9,A4,Def12;
end;
begin
:: Brown & Henrici
::$N Brown Theorem
theorem Th40:
for Amp being AmpleSet of R
for r1,r2,s1,s2 being Element of R holds gcd(r1,r2,Amp) = 1.R &
gcd(s1,s2,Amp) = 1.R & r2 <> 0.R implies
gcd(((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp)))),
(r2 * (s2/gcd(r2,s2,Amp))),Amp) = gcd(((r1 * (s2/gcd(r2,s2,Amp))) +
(s1 * (r2/gcd(r2,s2,Amp)))), gcd(r2,s2,Amp),Amp)
proof
let Amp be AmpleSet of R;
let r1,r2,s1,s2 be Element of R;
assume that
A1: gcd(r1,r2,Amp) = 1.R and
A2: gcd(s1,s2,Amp) = 1.R and
A3: r2 <> 0.R;
set d = gcd(r2,s2,Amp);
set r = r2/d;
set s = s2/d;
A4: d <> 0.R by A3,Th33;
then
A5: gcd(r,s,Amp) = 1.R by Th38;
A6: d divides s2 by Def12;
gcd(s,s1,Amp) = 1.R
proof
gcd(s,s1,Amp) divides s by Def12;
then consider e being Element of R such that
A7: gcd(s,s1,Amp) * e = s;
gcd(s,s1,Amp) * (e * d) = s * d by A7,GROUP_1:def 3
.= s2 by A6,A4,Def4;
then
A8: gcd(s,s1,Amp) divides s2;
A9: gcd(s,s1,Amp) is Element of Amp & 1.R is Element of Amp by Def8,Def12;
1.R * gcd(s,s1,Amp) = gcd(s,s1,Amp);
then
A10: 1.R divides gcd(s,s1,Amp);
gcd(s,s1,Amp) divides s1 by Def12;
then gcd(s,s1,Amp) divides gcd(s1,s2,Amp) by A8,Def12;
then gcd(s,s1,Amp) is_associated_to 1.R by A2,A10;
hence thesis by A9,Th22;
end;
then
A11: gcd(s,(s1 * r),Amp) = gcd(s,r,Amp) by Th37;
gcd(((r1 * s) + (s1 * r)),s,Amp) = gcd((s1 * r),s,Amp) by Th39;
then
A12: gcd(((r1 * s) + (s1 * r)),s,Amp) = gcd(s,(s1 * r),Amp) by Th29
.= 1.R by A11,A5,Th29;
A13: d divides (d * r2);
A14: d divides r2 by Def12;
gcd(r,r1,Amp) = 1.R
proof
gcd(r,r1,Amp) divides r by Def12;
then consider e being Element of R such that
A15: gcd(r,r1,Amp) * e = r;
gcd(r,r1,Amp) * (e * d) = r * d by A15,GROUP_1:def 3
.= r2 by A14,A4,Def4;
then
A16: gcd(r,r1,Amp) divides r2;
A17: gcd(r,r1,Amp) is Element of Amp & 1.R is Element of Amp by Def8,Def12;
1.R * gcd(r,r1,Amp) = gcd(r,r1,Amp);
then
A18: 1.R divides gcd(r,r1,Amp);
gcd(r,r1,Amp) divides r1 by Def12;
then gcd(r,r1,Amp) divides gcd(r1,r2,Amp) by A16,Def12;
then gcd(r,r1,Amp) is_associated_to 1.R by A1,A18;
hence thesis by A17,Th22;
end;
then
A19: gcd(r,(r1 * s),Amp) = gcd(r,s,Amp) by Th37;
A20: gcd(((r1 * s) + (s1 * r)),r,Amp) = gcd((r1 * s),r,Amp) by Th39;
gcd(r,s,Amp) = 1.R by A4,Th38;
then
A21: gcd(((r1 * s) + (s1 * r)),(d * r),Amp) = gcd(((r1 * s) + (s1 * r)),d,
Amp) by A20,A19,Th29,Th37;
r2 * s = (1.R * r2) * s
.= ((d/d) * r2) * s by A4,Th9
.= ((d * r2)/d) * s by A4,A13,Th11
.= s * (d * r) by A14,A4,A13,Th11;
hence thesis by A12,A21,Th37;
end;
::$N Henrici Theorem
theorem Th41:
for Amp being AmpleSet of R for r1,r2,s1,s2 being Element of R
holds gcd(r1,r2,Amp) = 1.R & gcd(s1,s2,Amp) = 1.R & r2 <> 0.R & s2 <> 0.R
implies gcd(((r1/gcd(r1,s2,Amp)) * (s1/gcd(s1,r2,Amp))), ((r2/gcd(s1,r2,Amp)) *
(s2/gcd(r1,s2,Amp))),Amp) = 1.R
proof
let Amp be AmpleSet of R;
let r1,r2,s1,s2 be Element of R;
assume that
A1: gcd(r1,r2,Amp) = 1.R and
A2: gcd(s1,s2,Amp) = 1.R and
A3: r2 <> 0.R and
A4: s2 <> 0.R;
set d1 = gcd(r1,s2,Amp);
A5: d1 <> 0.R by A4,Th33;
set d2 = gcd(s1,r2,Amp);
set s19 = s1/d2;
set r29 = r2/d2;
A6: d2 <> 0.R by A3,Th33;
then
A7: gcd(s19,r29,Amp) = 1.R by Th38;
set r19 = r1/d1;
A8: gcd(r19,r29,Amp) divides r29 by Def12;
d2 divides r2 by Def12;
then r29 * d2 = r2 by A6,Def4;
then r29 divides r2;
then
A9: gcd(r19,r29,Amp) divides r2 by A8,Th2;
A10: gcd(r19,r29,Amp) is Element of Amp & 1.R is Element of Amp by Def8,Def12;
d1 divides r1 by Def12;
then r19 * d1 = r1 by A5,Def4;
then
A11: r19 divides r1;
1.R * gcd(r19,r29,Amp) = gcd(r19,r29,Amp);
then
A12: 1.R divides gcd(r19,r29,Amp);
gcd(r19,r29,Amp) divides r19 by Def12;
then gcd(r19,r29,Amp) divides r1 by A11,Th2;
then gcd(r19,r29,Amp) divides gcd(r1,r2,Amp) by A9,Def12;
then gcd(r19,r29,Amp) is_associated_to 1.R by A1,A12;
then gcd(r19,r29,Amp) = 1.R by A10,Th22;
then
A13: gcd(r29,r19,Amp) = 1.R by Th29;
set s29 = s2/d1;
A14: gcd(s19,s29,Amp) divides s29 by Def12;
d1 divides s2 by Def12;
then s29 * d1 = s2 by A5,Def4;
then s29 divides s2;
then
A15: gcd(s19,s29,Amp) divides s2 by A14,Th2;
A16: gcd(s19,s29,Amp) is Element of Amp & 1.R is Element of Amp by Def8,Def12;
d2 divides s1 by Def12;
then s19 * d2 = s1 by A6,Def4;
then
A17: s19 divides s1;
1.R * gcd(s19,s29,Amp) = gcd(s19,s29,Amp);
then
A18: 1.R divides gcd(s19,s29,Amp);
gcd(s19,s29,Amp) divides s19 by Def12;
then gcd(s19,s29,Amp) divides s1 by A17,Th2;
then gcd(s19,s29,Amp) divides gcd(s1,s2,Amp) by A15,Def12;
then gcd(s19,s29,Amp) is_associated_to 1.R by A2,A18;
then
A19: gcd(s19,s29,Amp) = 1.R by A16,Th22;
A20: gcd(s29,r19,Amp) = gcd((r1/d1),(s2/d1),Amp) by Th29
.= 1.R by A5,Th38;
gcd((r19 * s19),r29,Amp) = gcd(r29,(r19 * s19),Amp) by Th29
.= gcd(r29,s19,Amp) by A13,Th37
.= 1.R by A7,Th29;
then gcd((r19 * s19),(r29 * s29),Amp) = gcd((r19 * s19),s29,Amp) by Th37
.= gcd(s29,(r19 * s19),Amp) by Th29
.= gcd(s29,s19,Amp) by A20,Th37
.= 1.R by A19,Th29;
hence thesis;
end;
begin
:: Properties of the Algorithms
definition
let R be gcd-like associative well-unital non empty multLoopStr;
let Amp be AmpleSet of R;
let x,y be Element of R;
pred x,y are_canonical_wrt Amp means
gcd(x,y,Amp) = 1.R;
end;
theorem Th42:
for Amp,Amp9 being AmpleSet of R for x,y being Element of R st
x,y are_canonical_wrt Amp holds x,y are_canonical_wrt Amp9
proof
let Amp,Amp9 be AmpleSet of R;
let x,y be Element of R;
1.R * x = x;
then
A1: 1.R divides x;
1.R * y = y;
then
A2: 1.R divides y;
assume x,y are_canonical_wrt Amp;
then gcd(x,y,Amp) = 1.R;
then
A3: for z being Element of R st z divides x & z divides y holds z divides 1.
R by Def12;
1.R in Amp9 by Def8;
then gcd(x,y,Amp9) = 1.R by A3,A1,A2,Def12;
hence thesis;
end;
definition
let R be gcd-like associative well-unital non empty multLoopStr;
let x,y be Element of R;
pred x,y are_co-prime means
ex Amp being AmpleSet of R st gcd(x,y, Amp) = 1.R;
end;
definition
let R be gcdDomain;
let x,y be Element of R;
redefine pred x,y are_co-prime; :: redefines are_co-prime (GCD_1, definition)
symmetry
proof
let x,y be Element of R;
given Amp being AmpleSet of R such that
A1: gcd(x,y,Amp) = 1.R;
gcd(y,x,Amp) = 1.R by A1,Th29;
hence thesis;
end;
end;
theorem Th43:
for Amp being AmpleSet of R for x,y being Element of R holds
x,y are_co-prime implies gcd(x,y,Amp) = 1.R
proof
let Amp be AmpleSet of R;
let x,y be Element of R;
assume x,y are_co-prime;
then consider Amp9 being AmpleSet of R such that
A1: gcd(x,y,Amp9) = 1.R;
x,y are_canonical_wrt Amp9 by A1;
then x,y are_canonical_wrt Amp by Th42;
hence thesis;
end;
definition
let R be gcd-like associative well-unital non empty multLoopStr_0;
let Amp be AmpleSet of R;
let x,y be Element of R;
pred x,y are_normalized_wrt Amp means
gcd(x,y,Amp) = 1.R & y in Amp & y <> 0.R;
end;
:: Addition
definition
let R be gcdDomain;
let Amp be AmpleSet of R;
let r1,r2,s1,s2 be Element of R;
assume that
A1: r1,r2 are_co-prime and
A2: s1,s2 are_co-prime and
A3: r2 = NF(r2,Amp) and
A4: s2 = NF(s2,Amp);
func add1(r1,r2,s1,s2,Amp) -> Element of R equals
:Def16:
s1 if r1 = 0.R, r1 if s1 = 0.R,
(r1 * s2) + (r2 * s1) if gcd(r2,s2,Amp) = 1.R,
0.R if (r1 * (s2/gcd(r2,s2,Amp))) +
(s1 * (r2/gcd(r2,s2,Amp))) = 0.R
otherwise ((r1 * (s2/gcd(r2,s2,Amp))) +
(s1 * (r2/gcd(r2,s2,Amp)))) /
gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))),
gcd(r2,s2,Amp),Amp);
coherence;
consistency
proof
A5: gcd(s1,s2,Amp) = 1.R by A2,Th43;
A6: s1 = 0.R & gcd(r2,s2,Amp) = 1.R implies for z being Element of R
holds z = r1 iff z = (r1 * s2) + (r2 * s1)
proof
assume that
A7: s1 = 0.R and
gcd(r2,s2,Amp) = 1.R;
A8: s2 = 1.R by A4,A5,A7,Th30;
let z be Element of R;
(r1 * s2) + (r2 * s1) = (r1 * s2) + 0.R by A7
.= r1 * 1.R by A8,RLVECT_1:4
.= r1;
hence thesis;
end;
A9: s1 = 0.R & (r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))) =
0.R implies for z being Element of R holds z = r1 iff z = 0.R
proof
A10: 1.R <> 0.R;
assume that
A11: s1 = 0.R and
A12: (r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))) = 0.R;
let z be Element of R;
A13: s2 = 1.R by A4,A5,A11,Th30;
then
A14: gcd(r2,s2,Amp) = 1.R by Th32;
0.R = (r1*(s2/gcd(r2,s2,Amp)))+0.R by A11,A12
.= r1*(1.R/gcd(r2,s2,Amp)) by A13,RLVECT_1:4
.= r1*1.R by A14,A10,Th9
.= r1;
hence thesis;
end;
A15: gcd(r1,r2,Amp) = 1.R by A1,Th43;
A16: r1 = 0.R & gcd(r2,s2,Amp) = 1.R implies for z being Element of R holds
z = s1 iff z = (r1 * s2) + (r2 * s1)
proof
assume that
A17: r1 = 0.R and
gcd(r2,s2,Amp) = 1.R;
A18: r2 = 1.R by A3,A15,A17,Th30;
let z be Element of R;
(r1 * s2) + (r2 * s1) = 0.R + (r2 * s1) by A17
.= 1.R * s1 by A18,RLVECT_1:4
.= s1;
hence thesis;
end;
A19: r1 = 0.R & (r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))) =
0.R implies for z being Element of R holds z = s1 iff z = 0.R
proof
A20: 1.R <> 0.R;
assume that
A21: r1 = 0.R and
A22: (r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))) = 0.R;
let z be Element of R;
A23: r2 = 1.R by A3,A15,A21,Th30;
then
A24: gcd(r2,s2,Amp) = 1.R by Th32;
0.R = 0.R+(s1*(r2/gcd(r2,s2,Amp))) by A21,A22
.= s1*(1.R/gcd(r2,s2,Amp)) by A23,RLVECT_1:4
.= s1*1.R by A24,A20,Th9
.= s1;
hence thesis;
end;
gcd(r2,s2,Amp) = 1.R & (r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,
s2,Amp))) = 0.R implies for z being Element of R holds z = (r1 * s2) + (r2 * s1
) iff z = 0.R
proof
assume
A25: gcd(r2,s2,Amp) = 1.R & (r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/
gcd(r2,s2,Amp) )) = 0.R;
let z be Element of R;
0.R = (r1 * s2) + (s1 * (r2/1.R)) by A25,Th10
.= (r1 * s2) + (s1 * r2) by Th10;
hence thesis;
end;
hence thesis by A16,A19,A6,A9;
end;
end;
definition
let R be gcdDomain;
let Amp be AmpleSet of R;
let r1,r2,s1,s2 be Element of R;
assume that
A1: r1,r2 are_co-prime and
A2: s1,s2 are_co-prime and
A3: r2 = NF(r2,Amp) and
A4: s2 = NF(s2,Amp);
func add2(r1,r2,s1,s2,Amp) -> Element of R equals
:Def17:
s2 if r1 = 0.R,
r2 if s1 = 0.R,
r2 * s2 if gcd(r2,s2,Amp) = 1.R,
1.R if (r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))) = 0.R
otherwise (r2 * (s2/gcd(r2,s2,Amp))) /
gcd((r1 * (s2/gcd(r2,s2,Amp))) +
(s1 * (r2/gcd(r2,s2,Amp))), gcd(r2,s2,Amp),Amp);
coherence;
consistency
proof
A5: gcd(r2,s2,Amp) = 1.R & (r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,
s2,Amp))) = 0.R implies for z being Element of R holds z = r2 * s2 iff z = 1.R
proof
assume that
A6: gcd(r2,s2,Amp) = 1.R and
A7: (r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))) = 0.R;
A8: 0.R = (r1 * s2) + (s1 * (r2/1.R)) by A6,A7,Th10
.= (r1 * s2) + (s1 * r2) by Th10;
then
A9: r1 * s2 = -(s1 * r2) by RLVECT_1:6;
A10: s1 * r2 = -(r1 * s2) by A8,RLVECT_1:6;
gcd(s2,s1,Amp) = 1.R by A2,Th43;
then gcd(s2,s1*r2,Amp) = gcd(s2,r2,Amp) by Th37
.= 1.R by A6,Th29;
then 1.R = gcd(1.R*s2,-(r1*s2),Amp) by A10
.= gcd(1.R*s2,(-r1)*s2,Amp) by VECTSP_1:8;
then
A11: 1.R is_associated_to s2 * gcd(1.R,(-r1),Amp) by Th36;
let z be Element of R;
A12: 1.R in Amp by Th22;
gcd(r2,r1,Amp) = 1.R by A1,Th43;
then gcd(r2,r1*s2,Amp) = 1.R by A6,Th37;
then 1.R = gcd(1.R*r2,-(s1*r2),Amp) by A9
.= gcd(1.R*r2,(-s1)*r2,Amp) by VECTSP_1:8;
then
A13: 1.R is_associated_to r2 * gcd(1.R,(-s1),Amp) by Th36;
s2 * gcd(1.R,(-r1),Amp) = s2 * 1.R by Th32
.= s2;
then
A14: s2 = 1.R by A4,A12,A11,Def9;
r2 * gcd(1.R,(-s1),Amp) = r2 * 1.R by Th32
.= r2;
then r2 = 1.R by A3,A13,A12,Def9;
hence thesis by A14;
end;
A15: gcd(r1,r2,Amp) = 1.R by A1,Th43;
A16: r1 = 0.R & gcd(r2,s2,Amp) = 1.R implies for z being Element of R
holds z = s2 iff z = r2 * s2
proof
assume that
A17: r1 = 0.R and
gcd(r2,s2,Amp) = 1.R;
let z be Element of R;
r2 = 1.R by A3,A15,A17,Th30;
hence thesis;
end;
A18: gcd(s1,s2,Amp) = 1.R by A2,Th43;
A19: s1 = 0.R & gcd(r2,s2,Amp) = 1.R implies for z being Element of R
holds z = r2 iff z = r2 * s2
proof
assume that
A20: s1 = 0.R and
gcd(r2,s2,Amp) = 1.R;
let z be Element of R;
s2 = 1.R by A4,A18,A20,Th30;
hence thesis;
end;
A21: s1 = 0.R & (r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))) =
0.R implies for z being Element of R holds z = r2 iff z = 1.R
proof
A22: 1.R <> 0.R;
assume that
A23: s1 = 0.R and
A24: (r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))) = 0.R;
let z be Element of R;
A25: s2 = 1.R by A4,A18,A23,Th30;
then
A26: gcd(r2,s2,Amp) = 1.R by Th32;
0.R = (r1*(s2/gcd(r2,s2,Amp)))+0.R by A23,A24
.= r1*(1.R/gcd(r2,s2,Amp)) by A25,RLVECT_1:4
.= r1*1.R by A26,A22,Th9
.= r1;
hence thesis by A3,A15,Th30;
end;
A27: r1 = 0.R & (r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))) =
0.R implies for z being Element of R holds z = s2 iff z = 1.R
proof
A28: 1.R <> 0.R;
assume that
A29: r1 = 0.R and
A30: (r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))) = 0.R;
let z be Element of R;
A31: r2 = 1.R by A3,A15,A29,Th30;
then
A32: gcd(r2,s2,Amp) = 1.R by Th32;
0.R = 0.R+(s1*(r2/gcd(r2,s2,Amp))) by A29,A30
.= s1*(1.R/gcd(r2,s2,Amp)) by A31,RLVECT_1:4
.= s1*1.R by A32,A28,Th9
.= s1;
hence thesis by A4,A18,Th30;
end;
r1 = 0.R & s1 = 0.R implies for z being Element of R holds z = s2 iff
z = r2
proof
assume that
A33: r1 = 0.R and
A34: s1 = 0.R;
let z be Element of R;
r2 = 1.R by A3,A15,A33,Th30;
hence thesis by A4,A18,A34,Th30;
end;
hence thesis by A16,A27,A19,A21,A5;
end;
end;
theorem
for Amp being AmpleSet of R for r1,r2,s1,s2 being Element of R holds
Amp is multiplicative &
r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp implies
add1(r1,r2,s1,s2,Amp),add2(r1,r2,s1,s2,Amp) are_normalized_wrt Amp
proof
let Amp be AmpleSet of R;
let r1,r2,s1,s2 be Element of R;
assume that
A1: Amp is multiplicative and
A2: r1,r2 are_normalized_wrt Amp and
A3: s1,s2 are_normalized_wrt Amp;
A4: r2 <> 0.R by A2;
r2 in Amp by A2;
then
A5: r2 = NF(r2,Amp) by Def9;
s2 in Amp by A3;
then
A6: s2 = NF(s2,Amp) by Def9;
A7: gcd(r1,r2,Amp) = 1.R by A2;
then
A8: r1,r2 are_co-prime;
A9: gcd(s1,s2,Amp) = 1.R by A3;
then
A10: s1,s2 are_co-prime;
A11: s2 <> 0.R by A3;
now
per cases;
case
A12: r1 = 0.R;
then add2(r1,r2,s1,s2,Amp) = s2 by A5,A6,A8,A10,Def17;
hence thesis by A3,A5,A6,A8,A10,A12,Def16;
end;
case
A13: s1 = 0.R;
then add2(r1,r2,s1,s2,Amp) = r2 by A5,A6,A8,A10,Def17;
hence thesis by A2,A5,A6,A8,A10,A13,Def16;
end;
case
A14: gcd(r2,s2,Amp) = 1.R;
then
A15: add2(r1,r2,s1,s2,Amp) = r2 * s2 by A5,A6,A8,A10,Def17;
add1(r1,r2,s1,s2,Amp) = (r1 * s2) + (r2 * s1) by A5,A6,A8,A10,A14,Def16;
then
A16: gcd(add1(r1,r2,s1,s2,Amp),add2(r1,r2,s1,s2,Amp),Amp) = gcd(((r1 * (
s2/1.R)) + (s1 * r2)), (r2 * s2),Amp) by A15,Th10
.= gcd((r1 * (s2/1.R)) + (s1 * (r2/1.R)), (r2 * s2),Amp) by Th10
.= gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))), (r2
* (s2/gcd(r2,s2,Amp))),Amp) by A14,Th10
.= gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))), gcd(
r2,s2,Amp),Amp) by A4,A7,A9,Th40
.= 1.R by A14,Th32;
reconsider r2,s2 as Element of Amp by A2,A3;
r2 * s2 in Amp & r2 * s2 <> 0.R by A1,A4,A11,VECTSP_2:def 1;
hence thesis by A15,A16;
end;
case
A17: (r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))) = 0.R;
A18: 1.R in Amp & 1.R <> 0.R by Th22;
A19: add2(r1,r2,s1,s2,Amp) = 1.R by A5,A6,A8,A10,A17,Def17;
then gcd(add1(r1,r2,s1,s2,Amp),add2(r1,r2,s1,s2,Amp),Amp) = 1.R by Th32;
hence thesis by A19,A18;
end;
case
r1 <> 0.R & s1 <> 0.R & gcd(r2,s2,Amp) <> 1.R & (r1 * (s2/gcd(
r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))) <> 0.R;
then
A20: add1(r1,r2,s1,s2,Amp) = ((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd
(r2,s2,Amp )))) / gcd(((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))))
, gcd(r2,s2,Amp),Amp) & add2(r1,r2,s1,s2,Amp) = (r2 * (s2/gcd(r2,s2,Amp))) /
gcd(((r1 * ( s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp)))), gcd(r2,s2,Amp),
Amp) by A5,A6,A8,A10,Def16,Def17;
gcd(r2,s2,Amp) <> 0.R by A4,Th33;
then
A21: gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))), gcd(r2
,s2,Amp),Amp) <> 0.R by Th33;
gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))), (r2 *
(s2/gcd(r2,s2,Amp))),Amp) = gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,
s2,Amp))), gcd(r2,s2,Amp),Amp) by A4,A7,A9,Th40;
then
A22: gcd( ((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp)))) /
gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))), gcd(r2,s2,Amp),Amp
), ((r2 * (s2/gcd(r2,s2,Amp)))) / gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/
gcd(r2,s2,Amp))), gcd(r2,s2,Amp),Amp), Amp) = 1.R by A21,Th38;
reconsider r2,s2 as Element of Amp by A2,A3;
A23: gcd(r2,s2,Amp) divides s2 by Def12;
reconsider z2 = gcd(((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,
Amp)))), gcd(r2,s2,Amp),Amp) as Element of Amp by Def12;
A24: gcd(r2,s2,Amp) <> 0.R by A4,Th33;
then
A25: z2 <> 0.R by Th33;
gcd(r2,s2,Amp) in Amp by Def12;
then reconsider z3 = s2/gcd(r2,s2,Amp) as Element of Amp by A1,A23,A24
,Th27;
r2 * z3 in Amp by A1;
then reconsider z1 = r2 * (s2/gcd(r2,s2,Amp)) as Element of Amp;
A26: r2 * s2 <> 0.R by A4,A11,VECTSP_2:def 1;
A27: gcd(r2,s2,Amp) divides r2 * s2 by A23,Th7;
then z1 = (r2 * s2)/gcd(r2,s2,Amp) by A23,A24,Th11;
then
A28: z1 <> 0.R by A24,A26,A27,Th8;
z2 divides gcd(r2,s2,Amp) & gcd(r2,s2,Amp) divides r2 by Def12;
then
A29: z2 divides r2 by Th2;
then z2 divides z1 by Th7;
then
A30: z1 / z2 <> 0.R by A25,A28,Th8;
z1 / z2 in Amp by A1,A29,A25,Th7,Th27;
hence thesis by A20,A22,A30;
end;
end;
hence thesis;
end;
theorem
for Amp being AmpleSet of R for r1,r2,s1,s2 being Element of R holds
r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp implies
add1(r1,r2,s1,s2,Amp) * (r2 * s2) =
add2(r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2))
proof
let Amp be AmpleSet of R;
let r1,r2,s1,s2 be Element of R;
assume that
A1: r1,r2 are_normalized_wrt Amp and
A2: s1,s2 are_normalized_wrt Amp;
gcd(r1,r2,Amp) = 1.R by A1;
then
A3: r1,r2 are_co-prime;
s2 in Amp by A2;
then
A4: s2 = NF(s2,Amp) by Def9;
gcd(s1,s2,Amp) = 1.R by A2;
then
A5: s1,s2 are_co-prime;
r2 in Amp by A1;
then
A6: r2 = NF(r2,Amp) by Def9;
A7: r2 <> 0.R by A1;
now
per cases;
case
A8: r1 = 0.R;
then
A9: add1(r1,r2,s1,s2,Amp) = s1 by A3,A5,A6,A4,Def16;
add2(r1,r2,s1,s2,Amp) = s2 by A3,A5,A6,A4,A8,Def17;
then
add2(r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2)) = s2 * (0.R + (s1 *
r2)) by A8
.= s2 * (s1 * r2) by RLVECT_1:4
.= add1(r1,r2,s1,s2,Amp) * (r2 * s2) by A9,GROUP_1:def 3;
hence thesis;
end;
case
A10: s1 = 0.R;
then
A11: add1(r1,r2,s1,s2,Amp) = r1 by A3,A5,A6,A4,Def16;
add2(r1,r2,s1,s2,Amp) = r2 by A3,A5,A6,A4,A10,Def17;
then
add2(r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2)) = r2 * ((r1 * s2) +
0.R) by A10
.= r2 * (r1 * s2) by RLVECT_1:4
.= add1(r1,r2,s1,s2,Amp) * (r2 * s2) by A11,GROUP_1:def 3;
hence thesis;
end;
case
A12: gcd(r2,s2,Amp) = 1.R;
then add2(r1,r2,s1,s2,Amp) = r2 * s2 by A3,A5,A6,A4,Def17;
hence thesis by A3,A5,A6,A4,A12,Def16;
end;
case
A13: (r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))) = 0.R;
A14: (r1 * s2) + (s1 * r2) = 0.R
proof
A15: gcd(r2,s2,Amp) divides r2 by Def12;
then
A16: gcd(r2,s2,Amp) divides s1 * r2 by Th7;
A17: gcd(r2,s2,Amp) divides s2 by Def12;
then consider f being Element of R such that
A18: gcd(r2,s2,Amp) * f = s2;
A19: gcd(r2,s2,Amp) <> 0.R by A7,Th33;
consider e being Element of R such that
A20: gcd(r2,s2,Amp) * e = r2 by A15;
gcd(r2,s2,Amp) * ((e * s1)+(f * r1)) = (gcd(r2,s2,Amp) * (e * s1)
)+(gcd(r2,s2,Amp) * (f * r1)) by VECTSP_1:def 2
.= ((gcd(r2,s2,Amp) * e) * s1)+(gcd(r2,s2,Amp) * (f * r1)) by
GROUP_1:def 3
.= (r1 * s2)+(s1 * r2) by A20,A18,GROUP_1:def 3;
then
A21: gcd(r2,s2,Amp) divides (r1 * s2) + (s1 * r2);
A22: gcd(r2,s2,Amp) divides r1 * s2 by A17,Th7;
then 0.R = (r1 * s2)/gcd(r2,s2,Amp) + (s1 * (r2/gcd(r2,s2,Amp))) by A13
,A19,A17,Th11
.= (r1 * s2)/gcd(r2,s2,Amp) + (s1 * r2)/gcd(r2,s2,Amp) by A19,A15,A16
,Th11;
then
A23: 0.R = ((r1 * s2) + (s1 * r2)) / gcd(r2,s2,Amp) by A19,A22,A16,A21,Th12;
0.R = 0.R * gcd(r2,s2,Amp)
.= ((r1 * s2) + (s1 * r2)) by A19,A21,A23,Def4;
hence thesis;
end;
add1(r1,r2,s1,s2,Amp) = 0.R by A3,A5,A6,A4,A13,Def16;
then add1(r1,r2,s1,s2,Amp) * (r2 * s2) = 0.R
.= add2(r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2)) by A14;
hence thesis;
end;
case
A24: r1 <> 0.R & s1 <> 0.R & gcd(r2,s2,Amp) <> 1.R & (r1 * (s2/gcd(
r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))) <> 0.R;
A25: gcd(r2,s2,Amp) divides s2 by Def12;
then
A26: gcd(r2,s2,Amp) divides r1 * s2 by Th7;
then
A27: gcd(r2,s2,Amp) divides ((r1 * s2) * r2) by Th7;
then
A28: gcd(r2,s2,Amp) divides (((r1 * s2) * r2) * s2) by Th7;
A29: add1(r1,r2,s1,s2,Amp) = ((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd
(r2,s2,Amp)))) / gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))),
gcd(r2,s2,Amp),Amp) by A3,A5,A6,A4,A24,Def16;
A30: gcd(r2,s2,Amp) divides r2 by Def12;
then
A31: gcd(r2,s2,Amp) divides s1 * r2 by Th7;
gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))), gcd(r2
,s2,Amp),Amp) divides gcd(r2,s2,Amp) by Def12;
then
gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))), gcd(r2
,s2,Amp),Amp) divides r2 by A30,Th2;
then
A32: gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))), gcd(r2
,s2,Amp),Amp) divides (r2 * (s2/gcd(r2,s2,Amp))) by Th7;
then
A33: gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))), gcd(r2
,s2,Amp),Amp) divides (r2 * (s2/gcd(r2,s2,Amp))) * ((r1 * s2)+(s1 * r2)) by Th7
;
A34: gcd(r2,s2,Amp) divides ((s1 * r2) * r2) by A30,Th7;
then
A35: gcd(r2,s2,Amp) divides (((s1 * r2) * r2) * s2) by Th7;
A36: gcd(r2,s2,Amp) divides (r2 * s2) by A30,Th7;
then
A37: gcd(r2,s2,Amp) divides ((r2 * s2) * r1) by Th7;
then
A38: gcd(r2,s2,Amp) divides (((r2 * s2) * r1) * s2) by Th7;
A39: gcd(r2,s2,Amp) divides ((r2 * s2) * s1) by A36,Th7;
then
A40: gcd(r2,s2,Amp) divides (((r2 * s2) * s1) * r2) by Th7;
A41: add2(r1,r2,s1,s2,Amp) = (r2 * (s2/gcd(r2,s2,Amp))) / gcd((r1 * (s2/
gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))), gcd(r2,s2,Amp),Amp) by A3,A5,A6
,A4,A24,Def17;
A42: gcd(r2,s2,Amp) <> 0.R by A7,Th33;
then
A43: gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))), gcd(r2
,s2,Amp),Amp) <> 0.R by Th33;
A44: (r2 * (s2/gcd(r2,s2,Amp))) * ((r1 * s2) + (s1 * r2)) = ((r2 * (s2/
gcd(r2,s2,Amp))) * (r1 * s2)) + ((r2 * (s2/gcd(r2,s2,Amp))) * (s1 * r2)) by
VECTSP_1:def 2
.= (((r2 * (s2/gcd(r2,s2,Amp))) * r1) * s2) + ((r2 * (s2/gcd(r2,s2,
Amp))) * (s1 * r2)) by GROUP_1:def 3
.= (((r2 * (s2/gcd(r2,s2,Amp))) * r1) * s2) + (((r2 * (s2/gcd(r2,s2,
Amp))) * s1) * r2) by GROUP_1:def 3
.= ((((r2 * s2)/gcd(r2,s2,Amp)) * r1) * s2) + (((r2 * (s2/gcd(r2,s2,
Amp))) * s1) * r2) by A42,A25,A36,Th11
.= ((((r2 * s2)/gcd(r2,s2,Amp)) * r1) * s2) + ((((r2 * s2)/gcd(r2,s2
,Amp)) * s1) * r2) by A42,A25,A36,Th11
.= ((((r2 * s2) * r1)/gcd(r2,s2,Amp)) * s2) + ((((r2 * s2)/gcd(r2,s2
,Amp)) * s1) * r2) by A42,A36,A37,Th11
.= ((((r2 * s2) * r1)/gcd(r2,s2,Amp)) * s2) + ((((r2 * s2) * s1)/gcd
(r2,s2,Amp)) * r2) by A42,A36,A39,Th11
.= ((((r2 * s2) * r1) * s2)/gcd(r2,s2,Amp)) + ((((r2 * s2) * s1)/gcd
(r2,s2,Amp)) * r2) by A42,A37,A38,Th11
.= (((r1 * (s2 * r2)) * s2)/gcd(r2,s2,Amp)) + ((((r2 * s2) * s1) *
r2)/gcd(r2,s2,Amp)) by A42,A39,A40,Th11
.= ((((r1 * s2) * r2) * s2)/gcd(r2,s2,Amp)) + ((((r2 * s2) * s1) *
r2)/gcd(r2,s2,Amp)) by GROUP_1:def 3
.= ((((r1 * s2) * r2) * s2)/gcd(r2,s2,Amp)) + ((s1 * ((r2 * s2) * r2
))/gcd(r2,s2,Amp)) by GROUP_1:def 3
.= ((((r1 * s2) * r2) * s2)/gcd(r2,s2,Amp)) + ((s1 * ((r2 * r2) * s2
))/gcd(r2,s2,Amp)) by GROUP_1:def 3
.= ((((r1 * s2) * r2) * s2)/gcd(r2,s2,Amp)) + (((s1 * (r2 * r2)) *
s2)/gcd(r2,s2,Amp)) by GROUP_1:def 3
.= ((((r1 * s2) * r2) * s2)/gcd(r2,s2,Amp)) + ((((s1 * r2) * r2) *
s2)/gcd(r2,s2,Amp)) by GROUP_1:def 3;
A45: ((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp)))) * (r2 *
s2) = ((r1 * (s2/gcd(r2,s2,Amp))) * (r2 * s2)) + ((s1 * (r2/gcd(r2,s2,Amp))) *
(r2 * s2)) by VECTSP_1:def 7
.= (((r1 * s2)/gcd(r2,s2,Amp)) * (r2 * s2)) + ((s1 * (r2/gcd(r2,s2,
Amp))) * (r2 * s2)) by A42,A25,A26,Th11
.= (((r1 * s2)/gcd(r2,s2,Amp)) * (r2 * s2)) + (((s1 * r2)/gcd(r2,s2,
Amp)) * (r2 * s2)) by A42,A30,A31,Th11
.= ((((r1 * s2)/gcd(r2,s2,Amp)) * r2) * s2) + (((s1 * r2)/gcd(r2,s2,
Amp)) * (r2 * s2)) by GROUP_1:def 3
.= ((((r1 * s2)/gcd(r2,s2,Amp)) * r2) * s2) + ((((s1 * r2)/gcd(r2,s2
,Amp)) * r2) * s2) by GROUP_1:def 3
.= ((((r1 * s2) * r2)/gcd(r2,s2,Amp)) * s2) + ((((s1 * r2)/gcd(r2,s2
,Amp)) * r2) * s2) by A42,A26,A27,Th11
.= ((((r1 * s2) * r2)/gcd(r2,s2,Amp)) * s2) + ((((s1 * r2) * r2)/gcd
(r2,s2,Amp)) * s2) by A42,A31,A34,Th11
.= ((((r1 * s2) * r2) * s2)/gcd(r2,s2,Amp)) + ((((s1 * r2) * r2)/gcd
(r2,s2,Amp)) * s2) by A42,A27,A28,Th11
.= ((((r1 * s2) * r2) * s2)/gcd(r2,s2,Amp)) + ((((s1 * r2) * r2) *
s2)/gcd(r2,s2,Amp)) by A42,A34,A35,Th11;
A46: gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))), gcd(r2
,s2,Amp),Amp) divides ((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))))
by Def12;
then
gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))), gcd(r2
,s2,Amp),Amp) divides ((r1*(s2/gcd(r2,s2,Amp)))+(s1 * (r2/gcd(r2,s2,Amp)))) * (
r2*s2) by Th7;
then add1(r1,r2,s1,s2,Amp) * (r2 * s2) = (((r1 * (s2/gcd(r2,s2,Amp)))+(
s1 * (r2/gcd(r2,s2,Amp)))) * (r2 * s2)) / gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1
* (r2/gcd(r2,s2,Amp))), gcd(r2,s2,Amp),Amp) by A29,A43,A46,Th11
.= add2(r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2)) by A41,A45,A44,A43
,A32,A33,Th11;
hence thesis;
end;
end;
hence thesis;
end;
:: Multiplication
definition
let R be gcdDomain;
let Amp be AmpleSet of R;
let r1,r2,s1,s2 be Element of R;
func mult1(r1,r2,s1,s2,Amp) -> Element of R equals
:Def18:
0.R if r1 = 0.R or s1 = 0.R,
r1 * s1 if r2 = 1.R & s2 = 1.R,
(r1 * s1)/gcd(r1,s2,Amp) if s2 <> 0.R & r2 = 1.R,
(r1 * s1)/gcd(s1,r2,Amp) if r2 <> 0.R & s2 = 1.R
otherwise (r1/gcd(r1,s2,Amp)) * (s1/gcd(s1,r2,Amp));
coherence;
consistency
proof
A1: (r1 = 0.R or s1 = 0.R) & r2 <> 0.R & s2 = 1.R implies for z being
Element of R holds z = 0.R iff z = (r1 * s1)/gcd(s1,r2,Amp)
proof
set d = (r1 * s1)/gcd(s1,r2,Amp);
assume that
A2: r1 = 0.R or s1 = 0.R and
A3: r2 <> 0.R and
s2 = 1.R;
A4: gcd(s1,r2,Amp) <> 0.R by A3,Th33;
let z be Element of R;
A5: r1 * s1 = 0.R
proof
now
per cases by A2;
case
r1 = 0.R;
hence thesis;
end;
case
s1 = 0.R;
hence thesis;
end;
end;
hence thesis;
end;
gcd(s1,r2,Amp) divides s1 by Def12;
then gcd(s1,r2,Amp) divides r1 * s1 by Th7;
then d * gcd(s1,r2,Amp) = 0.R by A5,A4,Def4;
hence thesis by A4,VECTSP_2:def 1;
end;
A6: (r1 = 0.R or s1 = 0.R) & s2 <> 0.R & r2 = 1.R implies for z being
Element of R holds z = 0.R iff z = (r1 * s1)/gcd(r1,s2,Amp)
proof
set d = (r1 * s1)/gcd(r1,s2,Amp);
assume that
A7: r1 = 0.R or s1 = 0.R and
A8: s2 <> 0.R and
r2 = 1.R;
A9: gcd(r1,s2,Amp) <> 0.R by A8,Th33;
let z be Element of R;
A10: r1 * s1 = 0.R
proof
now
per cases by A7;
case
r1 = 0.R;
hence thesis;
end;
case
s1 = 0.R;
hence thesis;
end;
end;
hence thesis;
end;
gcd(r1,s2,Amp) divides r1 by Def12;
then gcd(r1,s2,Amp) divides r1 * s1 by Th7;
then d * gcd(r1,s2,Amp) = 0.R by A10,A9,Def4;
hence thesis by A9,VECTSP_2:def 1;
end;
A11: r2 = 1.R & s2 = 1.R & r2 <> 0.R & s2 = 1.R implies for z being
Element of R holds z = r1 * s1 iff z = (r1 * s1)/gcd(s1,r2,Amp)
proof
assume that
A12: r2 = 1.R and
s2 = 1.R and
r2 <> 0.R and
s2 = 1.R;
gcd(s1,r2,Amp) = 1.R by A12,Th32;
hence thesis by Th10;
end;
r2 = 1.R & s2 = 1.R & s2 <> 0.R & r2 = 1.R implies for z being
Element of R holds z = r1 * s1 iff z = (r1 * s1)/gcd(r1,s2,Amp)
proof
assume that
r2 = 1.R and
A13: s2 = 1.R and
s2 <> 0.R and
r2 = 1.R;
gcd(r1,s2,Amp) = 1.R by A13,Th32;
hence thesis by Th10;
end;
hence thesis by A6,A1,A11;
end;
end;
definition
let R be gcdDomain;
let Amp be AmpleSet of R;
let r1,r2,s1,s2 be Element of R;
assume that
A1: r1,r2 are_co-prime and
A2: s1,s2 are_co-prime and
A3: r2 = NF(r2,Amp) and
A4: s2 = NF(s2,Amp);
func mult2(r1,r2,s1,s2,Amp) -> Element of R equals
:Def19:
1.R if r1 = 0.R or s1 = 0.R,
1.R if r2 = 1.R & s2 = 1.R,
s2/gcd(r1,s2,Amp) if s2 <> 0.R & r2 = 1.R,
r2/gcd(s1,r2,Amp) if r2 <> 0.R & s2 = 1.R
otherwise (r2/gcd(s1,r2,Amp)) * (s2/gcd(r1,s2,Amp));
coherence;
consistency
proof
A5: gcd(s1,s2,Amp) = 1.R by A2,Th43;
A6: (r1 = 0.R or s1 = 0.R) & s2 <> 0.R & r2 = 1.R implies for z being
Element of R holds z = 1.R iff z = s2/gcd(r1,s2,Amp)
proof
assume that
A7: r1 = 0.R or s1 = 0.R and
A8: s2 <> 0.R and
r2 = 1.R;
now
per cases by A7;
case
r1 = 0.R;
then gcd(r1,s2,Amp) = s2 by A4,Th30;
hence thesis by A8,Th9;
end;
case
A9: s1 = 0.R;
A10: 1.R <> 0.R;
A11: 1.R = s2 by A4,A5,A9,Th30;
then gcd(r1,s2,Amp) = 1.R by Th32;
hence thesis by A11,A10,Th9;
end;
end;
hence thesis;
end;
A12: gcd(r1,r2,Amp) = 1.R by A1,Th43;
A13: (r1 = 0.R or s1 = 0.R) & r2 <> 0.R & s2 = 1.R implies for z being
Element of R holds z = 1.R iff z = r2/gcd(s1,r2,Amp)
proof
assume that
A14: r1 = 0.R or s1 = 0.R and
A15: r2 <> 0.R and
s2 = 1.R;
now
per cases by A14;
case
s1 = 0.R;
then gcd(s1,r2,Amp) = r2 by A3,Th30;
hence thesis by A15,Th9;
end;
case
A16: r1 = 0.R;
A17: 1.R <> 0.R;
A18: 1.R = r2 by A3,A12,A16,Th30;
then gcd(s1,r2,Amp) = 1.R by Th32;
hence thesis by A18,A17,Th9;
end;
end;
hence thesis;
end;
A19: r2 = 1.R & s2 = 1.R & r2 <> 0.R & s2 = 1.R implies for z being
Element of R holds z = 1.R iff z = r2/gcd(s1,r2,Amp)
proof
assume that
A20: r2 = 1.R and
s2 = 1.R and
A21: r2 <> 0.R and
s2 = 1.R;
gcd(s1,r2,Amp) = 1.R by A20,Th32;
hence thesis by A20,A21,Th9;
end;
r2 = 1.R & s2 = 1.R & s2 <> 0.R & r2 = 1.R implies for z being
Element of R holds z = 1.R iff z = s2/gcd(r1,s2,Amp)
proof
assume that
r2 = 1.R and
A22: s2 = 1.R and
A23: s2 <> 0.R and
r2 = 1.R;
gcd(r1,s2,Amp) = 1.R by A22,Th32;
hence thesis by A22,A23,Th9;
end;
hence thesis by A6,A13,A19;
end;
end;
theorem
for Amp being AmpleSet of R for r1,r2,s1,s2 being Element of R holds
Amp is multiplicative &
r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp implies
mult1(r1,r2,s1,s2,Amp),mult2(r1,r2,s1,s2,Amp) are_normalized_wrt Amp
proof
let Amp be AmpleSet of R;
let r1,r2,s1,s2 be Element of R;
assume that
A1: Amp is multiplicative and
A2: r1,r2 are_normalized_wrt Amp and
A3: s1,s2 are_normalized_wrt Amp;
A4: gcd(r1,r2,Amp) = 1.R by A2;
then
A5: r1,r2 are_co-prime;
s2 in Amp by A3;
then
A6: s2 = NF(s2,Amp) by Def9;
r2 in Amp by A2;
then
A7: r2 = NF(r2,Amp) by Def9;
A8: r2 <> 0.R by A2;
then
A9: gcd(s1,r2,Amp) <> 0.R by Th33;
A10: gcd(s1,s2,Amp) = 1.R by A3;
then
A11: s1,s2 are_co-prime;
A12: s2 <> 0.R by A3;
then
A13: gcd(r1,s2,Amp) <> 0.R by Th33;
now
per cases;
case
A14: r1 = 0.R or s1 = 0.R;
A15: 1.R in Amp & 1.R <> 0.R by Th22;
A16: mult2(r1,r2,s1,s2,Amp) = 1.R by A5,A11,A7,A6,A14,Def19;
then
gcd(mult1(r1,r2,s1,s2,Amp),mult2(r1,r2,s1,s2,Amp),Amp) = 1.R by Th32;
hence thesis by A16,A15;
end;
case
A17: r2 = 1.R & s2 = 1.R;
A18: 1.R in Amp & 1.R <> 0.R by Th22;
A19: mult2(r1,r2,s1,s2,Amp) = 1.R by A5,A11,A7,A17,Def19;
then
gcd(mult1(r1,r2,s1,s2,Amp),mult2(r1,r2,s1,s2,Amp),Amp) = 1.R by Th32;
hence thesis by A19,A18;
end;
case
A20: s2 <> 0.R & r2 = 1.R;
then
A21: gcd(s1,r2,Amp) = 1.R by Th32;
then r2/gcd(s1,r2,Amp) = 1.R by A20,Th9;
then
A22: s2/gcd(r1,s2,Amp) = (s2/gcd(r1,s2,Amp)) * (r2/gcd(s1,r2,Amp));
A23: gcd(r1,s2,Amp) divides r1 by Def12;
then gcd(r1,s2,Amp) divides (r1 * s1) by Th7;
then
A24: (r1 * s1)/gcd(r1,s2,Amp) = (r1/gcd(r1,s2,Amp)) * s1 by A13,A23,Th11
.= (r1/gcd(r1,s2,Amp)) * (s1/gcd(s1,r2,Amp)) by A21,Th10;
A25: mult2(r1,r2,s1,s2,Amp) = s2/gcd(r1,s2,Amp) by A5,A11,A7,A6,A20,Def19;
reconsider zz = gcd(r1,s2,Amp) as Element of Amp by Def12;
A26: gcd(r1,s2,Amp) divides s2 & gcd(r1,s2,Amp) <> 0.R by A12,Def12,Th33;
then
A27: s2/gcd(r1,s2,Amp) <> 0.R by A12,Th8;
mult1(r1,r2,s1,s2,Amp) = (r1 * s1)/gcd(r1,s2,Amp) by A20,Def18;
then
A28: gcd(mult1(r1,r2,s1,s2,Amp),mult2(r1,r2,s1,s2,Amp),Amp) = 1.R by A4,A10,A8
,A12,A25,A24,A22,Th41;
reconsider s2 as Element of Amp by A3;
s2/zz in Amp by A1,A26,Th27;
hence thesis by A25,A28,A27;
end;
case
A29: r2 <> 0.R & s2 = 1.R;
then
A30: gcd(r1,s2,Amp) = 1.R by Th32;
then s2/gcd(r1,s2,Amp) = 1.R by A29,Th9;
then
A31: r2/gcd(s1,r2,Amp) = (r2/gcd(s1,r2,Amp)) * (s2/gcd(r1,s2,Amp));
A32: gcd(s1,r2,Amp) divides s1 by Def12;
then gcd(s1,r2,Amp) divides (r1 * s1) by Th7;
then
A33: (r1 * s1)/gcd(s1,r2,Amp) = r1 * (s1/gcd(s1,r2,Amp)) by A9,A32,Th11
.= (r1/gcd(r1,s2,Amp)) * (s1/gcd(s1,r2,Amp)) by A30,Th10;
A34: mult2(r1,r2,s1,s2,Amp) = r2/gcd(s1,r2,Amp) by A5,A11,A7,A6,A29,Def19;
reconsider zz = gcd(s1,r2,Amp) as Element of Amp by Def12;
A35: gcd(s1,r2,Amp) divides r2 & gcd(s1,r2,Amp) <> 0.R by A8,Def12,Th33;
then
A36: r2/gcd(s1,r2,Amp) <> 0.R by A8,Th8;
mult1(r1,r2,s1,s2,Amp) = (r1 * s1)/gcd(s1,r2,Amp) by A29,Def18;
then
A37: gcd(mult1(r1,r2,s1,s2,Amp),mult2(r1,r2,s1,s2,Amp),Amp) = 1.R by A4,A10,A8
,A12,A34,A33,A31,Th41;
reconsider r2 as Element of Amp by A2;
r2/zz in Amp by A1,A35,Th27;
hence thesis by A34,A37,A36;
end;
case
A38: not(r1 = 0.R or s1 = 0.R) & not(r2 = 1.R & s2 = 1.R) & not(s2
<> 0.R & r2 = 1.R) & not(r2 <> 0.R & s2 = 1.R);
reconsider z2 = gcd(s1,r2,Amp) as Element of Amp by Def12;
reconsider z1 = gcd(r1,s2,Amp) as Element of Amp by Def12;
A39: gcd(r1,s2,Amp) divides s2 & gcd(r1,s2,Amp) <> 0.R by A12,Def12,Th33;
then
A40: s2/gcd(r1,s2,Amp) <> 0.R by A12,Th8;
A41: mult2(r1,r2,s1,s2,Amp) = (r2/gcd(s1,r2,Amp)) * (s2/gcd(r1,s2,Amp))
by A5,A11,A7,A6,A38,Def19;
mult1(r1,r2,s1,s2,Amp) = (r1/gcd(r1,s2,Amp)) * (s1/gcd(s1,r2, Amp))
by A38,Def18;
then
A42: gcd(mult1(r1,r2,s1,s2,Amp),mult2(r1,r2,s1,s2,Amp),Amp) = 1.R by A4,A10,A8
,A12,A41,Th41;
A43: gcd(s1,r2,Amp) divides r2 & gcd(s1,r2,Amp) <> 0.R by A8,Def12,Th33;
then
A44: r2/gcd(s1,r2,Amp) <> 0.R by A8,Th8;
reconsider s2 as Element of Amp by A3;
reconsider u = s2/z1 as Element of Amp by A1,A39,Th27;
reconsider r2 as Element of Amp by A2;
reconsider v = r2/z2 as Element of Amp by A1,A43,Th27;
A45: v * u <> 0.R by A40,A44,VECTSP_2:def 1;
v * u in Amp by A1;
hence thesis by A41,A42,A45;
end;
end;
hence thesis;
end;
theorem
for Amp being AmpleSet of R for r1,r2,s1,s2 being Element of R holds
r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp implies
mult1(r1,r2,s1,s2,Amp) * (r2 * s2) = mult2(r1,r2,s1,s2,Amp) * (r1 * s1)
proof
let Amp be AmpleSet of R;
let r1,r2,s1,s2 be Element of R;
assume that
A1: r1,r2 are_normalized_wrt Amp and
A2: s1,s2 are_normalized_wrt Amp;
gcd(r1,r2,Amp) = 1.R by A1;
then
A3: r1,r2 are_co-prime;
s2 <> 0.R by A2;
then
A4: gcd(r1,s2,Amp) <> 0.R by Th33;
r2 in Amp by A1;
then
A5: r2 = NF(r2,Amp) by Def9;
gcd(s1,s2,Amp) = 1.R by A2;
then
A6: s1,s2 are_co-prime;
r2 <> 0.R by A1;
then
A7: gcd(s1,r2,Amp) <> 0.R by Th33;
s2 in Amp by A2;
then
A8: s2 = NF(s2,Amp) by Def9;
now
per cases;
case
A9: r1 = 0.R or s1 = 0.R;
then
A10: mult1(r1,r2,s1,s2,Amp) = 0.R by Def18;
now
per cases by A9;
case
r1 = 0.R;
then mult2(r1,r2,s1,s2,Amp) * (r1 * s1) = mult2(r1,r2,s1,s2,Amp) *
0.R
.= 0.R;
hence thesis by A10;
end;
case
s1 = 0.R;
then mult2(r1,r2,s1,s2,Amp) * (r1 * s1) = mult2(r1,r2,s1,s2,Amp) *
0.R
.= 0.R;
hence thesis by A10;
end;
end;
hence thesis;
end;
case
A11: r2 = 1.R & s2 = 1.R;
then mult1(r1,r2,s1,s2,Amp) = r1 * s1 & mult2(r1,r2,s1,s2,Amp) = 1.R by
A3,A6,A5,Def18,Def19;
hence thesis by A11;
end;
case
A12: s2 <> 0.R & r2 = 1.R;
gcd(r1,s2,Amp) divides r1 by Def12;
then
A13: gcd(r1,s2,Amp) divides (r1 * s1) by Th7;
then
A14: gcd(r1,s2,Amp) divides (r1 * s1) * s2 by Th7;
A15: ((r1 * s1)/gcd(r1,s2,Amp)) * (r2 * s2) = ((r1 * s1)/gcd(r1,s2,Amp))
* s2 by A12
.= ((r1 * s1) * s2)/gcd(r1,s2,Amp) by A4,A13,A14,Th11;
A16: mult2(r1,r2,s1,s2,Amp) = s2/gcd(r1,s2,Amp) by A3,A6,A5,A8,A12,Def19;
A17: gcd(r1,s2,Amp) divides s2 by Def12;
then
A18: gcd(r1,s2,Amp) divides s2 * r1 by Th7;
then
A19: gcd(r1,s2,Amp) divides (s2 * r1) * s1 by Th7;
(s2/gcd(r1,s2,Amp)) * (r1 * s1) = ((s2/gcd(r1,s2,Amp)) * r1) * s1
by GROUP_1:def 3
.= ((s2 * r1)/gcd(r1,s2,Amp)) * s1 by A4,A17,A18,Th11
.= ((s2 * r1) * s1)/gcd(r1,s2,Amp) by A4,A18,A19,Th11
.= ((r1 * s1) * s2)/gcd(r1,s2,Amp) by GROUP_1:def 3;
hence thesis by A12,A16,A15,Def18;
end;
case
A20: r2 <> 0.R & s2 = 1.R;
gcd(s1,r2,Amp) divides s1 by Def12;
then
A21: gcd(s1,r2,Amp) divides (s1 * r1) by Th7;
then
A22: gcd(s1,r2,Amp) divides (s1 * r1) * r2 by Th7;
A23: ((r1 * s1)/gcd(s1,r2,Amp)) * (r2 * s2) = ((r1 * s1)/gcd(s1,r2,Amp))
* r2 by A20
.= ((r1 * s1) * r2)/gcd(s1,r2,Amp) by A7,A21,A22,Th11;
A24: mult2(r1,r2,s1,s2,Amp) = r2/gcd(s1,r2,Amp) by A3,A6,A5,A8,A20,Def19;
A25: gcd(s1,r2,Amp) divides r2 by Def12;
then
A26: gcd(s1,r2,Amp) divides r2 * r1 by Th7;
then
A27: gcd(s1,r2,Amp) divides (r2 * r1) * s1 by Th7;
(r2/gcd(s1,r2,Amp)) * (r1 * s1) = ((r2/gcd(s1,r2,Amp)) * r1) * s1
by GROUP_1:def 3
.= ((r2 * r1)/gcd(s1,r2,Amp)) * s1 by A7,A25,A26,Th11
.= ((r2 * r1) * s1)/gcd(s1,r2,Amp) by A7,A26,A27,Th11
.= ((r1 * s1) * r2)/gcd(s1,r2,Amp) by GROUP_1:def 3;
hence thesis by A20,A24,A23,Def18;
end;
case
A28: not(r1 = 0.R or s1 = 0.R) & not(r2 = 1.R & s2 = 1.R) & not(s2
<> 0.R & r2 = 1.R) & not(r2 <> 0.R & s2 = 1.R);
A29: gcd(s1,r2,Amp) divides r2 & gcd(r1,s2,Amp) divides s2 by Def12;
then
A30: (gcd(s1,r2,Amp) * gcd(r1,s2,Amp)) divides r2 * s2 by Th3;
then
A31: (gcd(s1,r2,Amp) * gcd(r1,s2,Amp)) divides (r2 * s2) * r1 by Th7;
then
A32: (gcd(s1,r2,Amp) * gcd(r1,s2,Amp)) divides ((r2 * s2) * r1) * s1 by Th7;
A33: gcd(r1,s2,Amp) divides r1 & gcd(s1,r2,Amp) divides s1 by Def12;
then
A34: (gcd(r1,s2,Amp) *gcd(s1,r2,Amp)) divides r1 * s1 by Th3;
then
A35: (gcd(r1,s2,Amp) * gcd(s1,r2,Amp)) divides (r1 * s1) * r2 by Th7;
then
A36: (gcd(r1,s2,Amp) * gcd(s1,r2,Amp)) divides ((r1 * s1) * r2) * s2 by Th7;
A37: mult2(r1,r2,s1,s2,Amp) = (r2/gcd(s1,r2,Amp)) * (s2/gcd(r1,s2,Amp))
by A3,A6,A5,A8,A28,Def19;
A38: (gcd(r1,s2,Amp) * gcd(s1,r2,Amp)) <> 0.R by A4,A7,VECTSP_2:def 1;
A39: ((r2/gcd(s1,r2,Amp)) * (s2/gcd(r1,s2,Amp))) * (r1 * s1) = ((r2 * s2
)/(gcd(s1,r2,Amp) * gcd(r1,s2,Amp))) * (r1 * s1) by A4,A7,A29,Th14
.= (((r2 * s2)/(gcd(s1,r2,Amp) * gcd(r1,s2,Amp))) * r1) * s1 by
GROUP_1:def 3
.= (((r2 * s2) * r1)/(gcd(s1,r2,Amp) * gcd(r1,s2,Amp))) * s1 by A38,A30
,A31,Th11
.= (((r2 * s2) * r1) * s1)/(gcd(s1,r2,Amp) * gcd(r1,s2,Amp)) by A38,A31
,A32,Th11
.= (r1 * ((r2 * s2) * s1))/(gcd(s1,r2,Amp) * gcd(r1,s2,Amp)) by
GROUP_1:def 3
.= (r1 * ((s1 * r2) * s2))/(gcd(s1,r2,Amp) * gcd(r1,s2,Amp)) by
GROUP_1:def 3
.= ((r1 * (s1 * r2)) * s2)/(gcd(s1,r2,Amp) * gcd(r1,s2,Amp)) by
GROUP_1:def 3
.= (((r1 * s1) * r2) * s2)/(gcd(s1,r2,Amp) * gcd(r1,s2,Amp)) by
GROUP_1:def 3;
((r1/gcd(r1,s2,Amp)) * (s1/gcd(s1,r2,Amp))) * (r2 * s2) = ((r1 * s1
)/(gcd(r1,s2,Amp) * gcd(s1,r2,Amp))) * (r2 * s2) by A4,A7,A33,Th14
.= (((r1 * s1)/(gcd(r1,s2,Amp) * gcd(s1,r2,Amp))) * r2) * s2 by
GROUP_1:def 3
.= (((r1 * s1) * r2)/(gcd(r1,s2,Amp) * gcd(s1,r2,Amp))) * s2 by A34,A35
,A38,Th11
.= (((r1 * s1) * r2) * s2)/(gcd(r1,s2,Amp) * gcd(s1,r2,Amp)) by A35,A36
,A38,Th11;
hence thesis by A28,A37,A39,Def18;
end;
end;
hence thesis;
end;
theorem
for F be add-associative right_zeroed right_complementable Abelian
distributive non empty doubleLoopStr,
x,y being Element of F holds
(-x)*y = -x*y & x*(-y) = -x*y by VECTSP_1:8,9;
theorem
for F being almost_left_invertible commutative Ring
for a, b being Element of F st
a <> 0.F & b <> 0.F holds a"*b" = (b*a)"
proof
let F be almost_left_invertible commutative Ring;
let a,b be Element of F such that
A1: a <> 0.F and
A2: b <> 0.F;
A3: b*a * (a"*b") = b*a*a"*b" by GROUP_1:def 3
.= b*(a*a")*b" by GROUP_1:def 3
.= b*1_F*b" by A1,VECTSP_1:def 10
.= b*b"
.= 1_F by A2,VECTSP_1:def 10;
b*a <> 0.F by A1,A2,VECTSP_1:12;
hence thesis by A3,VECTSP_1:def 10;
end;
definition
let R be commutative non empty multLoopStr;
let x be Element of R;
redefine attr x is unital means :: redefines unital (GCD_1, definition)
x divides 1.R;
compatibility
proof
thus x is unital iff x divides 1.R
proof
hereby
assume x is unital;
hence x divides 1.R;
end;
assume x divides 1.R;
then ex y being Element of R st 1.R = x*y;
hence thesis;
end;
end;
end;