Copyright (c) 1997 Association of Mizar Users
environ
vocabulary BINOP_1, VECTSP_1, LATTICES, ALGSTR_2, VECTSP_2, FUNCSDOM,
RLVECT_1, FUNCT_1, ARYTM_3, ARYTM_1, GROUP_1, EQREL_1, BOOLE, SETFAM_1,
COHSP_1, INT_2, RELAT_1, GCD_1;
notation TARSKI, XBOOLE_0, SUBSET_1, REAL_1, STRUCT_0, RLVECT_1, VECTSP_2,
VECTSP_1, FUNCSDOM, BINOP_1;
constructors FUNCSDOM, ALGSTR_2, VECTSP_2, REAL_1, MEMBERED;
clusters STRUCT_0, VECTSP_1, VECTSP_2, SUBSET_1, ALGSTR_1, XBOOLE_0, MEMBERED;
requirements SUBSET, BOOLE;
definitions VECTSP_1, VECTSP_2, XBOOLE_0;
theorems TARSKI, WELLORD2, SUBSET_1, VECTSP_1, VECTSP_2, RLVECT_1, XBOOLE_0,
XCMPLX_1;
schemes SETFAM_1, GROUP_2, SUBSET_1;
begin :: Basics
reserve X,Y for set;
:: Theorems about Integral Domains
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
cluster commutative right_unital -> left_unital (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,VECTSP_1:def 17
.= x by A2,VECTSP_1:def 13;
end;
end;
definition
cluster commutative right-distributive -> distributive
(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,VECTSP_1:def 11;
thus (y+z)*x = x*(y+z) by A1,VECTSP_1:def 17
.= x*y+x*z by A2,VECTSP_1:def 11
.= y*x+x*z by A1,VECTSP_1:def 17
.= y*x+z*x by A1,VECTSP_1:def 17;
end;
cluster commutative left-distributive ->
distributive (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,VECTSP_1:def 17
.= y*x+z*x by A4,VECTSP_1:def 12
.= x*y+z*x by A3,VECTSP_1:def 17
.= x*y+x*z by A3,VECTSP_1:def 17;
thus (y+z)*x = y*x+z*x by A4,VECTSP_1:def 12;
end;
end;
definition
cluster -> well-unital Ring;
coherence;
end;
definition
cluster F_Real -> domRing-like;
coherence
proof
set D = F_Real;
hereby
let x,y be Element of F_Real;
assume that
A1: x*y = 0.D & x <> 0.D;
reconsider x' = x, y' = y as Real by VECTSP_1:def 15;
A2:x*y = multreal.(x',y') by VECTSP_1:def 10,def 15
.= x'*y' by VECTSP_1:def 14;
0.D = 0 by RLVECT_1:def 2,VECTSP_1:def 15;
hence y = 0.D by A1,A2,XCMPLX_1:6;
end;
end;
end;
definition
cluster strict Abelian add-associative right_zeroed right_complementable
associative commutative domRing-like distributive
well-unital non degenerated Field-like (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:40
.= a * (b + (-c)) by VECTSP_1:def 11
.= a * (b - c) by RLVECT_1:def 11;
then b - c = 0.R by A1,VECTSP_2:def 5;
then c = (b - c) + c by RLVECT_1:10
.= (b + (-c)) + c by RLVECT_1:def 11
.= b + (c + (-c)) by RLVECT_1:def 6
.= b + 0.R by RLVECT_1:def 10
.= b by RLVECT_1:10;
hence b = c;
end;
hence thesis;
end;
:: Definition of Divisibility
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let R be non empty HGrStr;
let x,y be Element of R;
pred x divides y means :Def1:
ex z being Element of R st y = x * z;
end;
definition
let R be well-unital (non empty multLoopStr);
let x,y be Element of R;
redefine pred x divides y;
reflexivity
proof let A be Element of R;
A * 1_ R = A by VECTSP_2:def 2;
hence thesis by Def1;
end;
end;
definition
let R be non empty multLoopStr;
let x be Element of R;
attr x is unital means :Def2:
x divides 1_ R;
end;
definition
let R be non empty multLoopStr;
let x,y be Element of R;
pred x is_associated_to y means :Def3:
x divides y & y divides x;
symmetry;
antonym x is_not_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;
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,Def1;
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 A1: A divides B & B divides C;
then consider D being Element of R such that
A2: A * D = B by Def1;
consider E being Element of R such that
A3: B * E = C by A1,Def1;
A * (D * E) = C by A2,A3,VECTSP_1:def 16;
hence (A divides B & B divides C) implies A divides C by Def1;
end;
hence thesis;
end;
theorem
Th3:for R being commutative associative (non empty multLoopStr)
for a,b,c,d being Element of R holds
(b divides a & d divides c) implies (b * d) divides (a * c)
proof
let R be commutative associative (non empty multLoopStr);
let a,b,c,d be Element of R;
assume A1: (b divides a) & (d divides c);
then consider x being Element of R such that
A2: b * x = a by Def1;
consider y being Element of R such that
A3: d * y = c by A1,Def1;
(b * d) * (y * x) = ((b * d) * y) * x by VECTSP_1:def 16
.= (b * c) * x by A3,VECTSP_1:def 16
.= a * c by A2,VECTSP_1:def 16;
hence thesis by Def1;
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
proof
let R be associative (non empty multLoopStr);
let A,B,C be Element of R;
now
assume A1: A is_associated_to B & B is_associated_to C;
then A2: A divides B & B divides A by Def3;
B divides C & C divides B by A1,Def3;
then A divides C & C divides A by A2,Th2;
hence (A is_associated_to B & B is_associated_to C)
implies A is_associated_to C by Def3;
end;
hence thesis;
end;
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 by Def1;
(C * A) * D = C * B by A1,VECTSP_1:def 16;
hence thesis by Def1;
end;
theorem
Th6: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
proof
take b;
thus thesis;
end;
assume
A1:R is commutative;
take a;
thus thesis by A1,VECTSP_1:def 17;
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 by Def1;
a * (d * c) = b * c by A1,VECTSP_1:def 16;
hence thesis by Def1;
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 A1: b divides a & b <> 0.R;
hereby assume a/b = 0.R;
then a = 0.R * b by A1,Def4
.= 0.R by VECTSP_1:39;
hence a = 0.R;
end;
assume a = 0.R;
then 0.R = (a/b) * b by A1,Def4;
hence a/b = 0.R by A1,VECTSP_2:def 5;
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 by VECTSP_2:def 2;
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;
A1: 1_ R <> 0.R by VECTSP_1:def 21;
1_ R * a = a by VECTSP_2:def 2;
then A2: 1_ R divides a by Def1;
A = A * 1_ R by VECTSP_2:def 2
.= a by A1,A2,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
assume A3: C divides (A * B) & C divides A;
set A1 = (A * B) / C;
A4: A1 * C = A * B by A1,A3,Def4;
set A2 = A / C;
A2 * C = A by A1,A3,Def4;
then A1 * C = (A2 * B) * C by A4,VECTSP_1:def 16;
hence (C divides (A * B) & C divides A) implies
(A * B) / C = (A / C) * B by A1,Th1;
end;
now
assume A5: (C divides (A * B)) & C divides B;
set A1 = (A * B) / C;
A6: A1 * C = A * B by A1,A5,Def4;
set A2 = B / C;
A2 * C = B by A1,A5,Def4;
then A1 * C = (A * A2) * C by A6,VECTSP_1:def 16;
hence C divides (A * B) & C divides B implies
(A * B) / C = A * (B / C) 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;
assume A2: c divides a & c divides b & c divides (a + b);
set d = a/c;
set e = b/c;
A3: d * c = a by A1,A2,Def4;
e * c = b by A1,A2,Def4;
then a + b = (d + e) * c by A3,VECTSP_1:def 12;
then (a + b)/c = (d + e) * (c/c) by A1,A2,Th11
.= (d + e) * 1_ R by A1,Th9
.= d + e by VECTSP_1:def 13;
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 A2: c divides a & c divides b;
now assume (a/c) = (b/c);
consider e being Element of R such that
A3: e = (b/c);
e * c = b by A1,A2,A3,Def4;
hence a/c = b/c implies a = b by A1,A2,A3,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 A1: b <> 0.R & d <> 0.R & b divides a & d divides c;
set x = a/b;
set y = c/d;
set z = (a * c)/(b * d);
A2: x * b = a by A1,Def4;
A3: y * d = c by A1,Def4;
A4: (b * d) divides (a * c) by A1,Th3;
A5: (b * d) <> 0.R by A1,VECTSP_2:def 5;
then z * (b * d) = (x * b) * (y * d) by A2,A3,A4,Def4
.= x * (b * (y * d)) by VECTSP_1:def 16
.= x * (y * (b * d)) by VECTSP_1:def 16
.= (x * y) * (b * d) by VECTSP_1:def 16;
hence thesis by A5,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 A1: (A <> 0.R) & (A * B) divides (A * C);
then consider D being Element of R such that
A2: (A * B) * D = A * C by Def1;
A3: A * (B * D) = A * C by A2,VECTSP_1:def 16;
A4: (A * (B * D))/A = (A/A) * (B * D)
proof
A divides (A * (B * D)) by Th6;
hence thesis by A1,Th11;
end;
A5: (A * C)/A = (A/A) * C
proof
A divides (A * C) by Th6;
hence thesis by A1,Th11;
end;
B * D = 1_ R * (B * D) by VECTSP_1:def 19
.= (A/A) * C by A1,A3,A4,A5,Th9
.= 1_ R * C by A1,Th9
.= C by VECTSP_1:def 19;
hence thesis by Def1;
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 by Def3;
then consider D being Element of R such that
A1: 0.R * D = A by Def1;
thus thesis by A1,VECTSP_1:39;
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 A1: A <> 0.R & A * B = A;
set A1 = A/A;
A2: A1 = 1_ R by A1,Th9;
(A * B)/A = (A/A) * B by A1,Th11;
hence thesis by A1,A2,VECTSP_1:def 19;
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 A is_associated_to B;
then A2: A divides B & B divides A by Def3;
then consider C being Element of R such that
A3: B = A * C by Def1;
consider D being Element of R such that
A4: A = B * D by A2,Def1;
now per cases;
case A5: A <> 0.R;
A = A * (C * D) by A3,A4,VECTSP_1:def 16;
then C * D = 1_ R by A5,Th17;
then C divides 1_ R by Def1;
then C is unital by Def2;
hence ex c being Element of R st
c is unital & B = A * c by A3;
case A6: A = 0.R;
then B = 0.R by A3,VECTSP_1:39;
then A7: B = A * 1_ R by A6,VECTSP_1:def 13;
1_ R is unital
proof
thus 1_ R divides 1_ R;
end;
hence ex c being Element of R st
c is unital & B = A * c by A7;
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 & A * C = B;
C divides 1_ R by A8,Def2;
then consider D being Element of R such that
A9: C * D = 1_ R by Def1;
A = A * (C * D) by A9,VECTSP_1:def 13
.= B * D by A8,VECTSP_1:def 16;
then A10: B divides A by Def1;
A divides B by A8,Def1;
hence thesis by A10,Def3;
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
proof
let A,B,C be Element of R;
assume A1: C <> 0.R & (C * A) is_associated_to (C * B);
then (C * A) divides (C * B) by Def3;
then A2: A divides B by A1,Th15;
C * B divides C * A by A1,Def3;
then B divides A by A1,Th15;
hence thesis by A2,Def3;
end;
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 set;
now assume B in M;
then ex B' being Element of R st
B = B' & B' 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 A' being Element of R st
A = A' & A' 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;
for X1,X2 being Subset of R st
(for y being Element of R holds y in X1 iff P[y]) &
(for y being Element of R holds y in X2 iff P[y]) holds
X1 = X2 from Subset_Eq;
hence thesis;
end;
end;
definition
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 by XBOOLE_0:def 7;
then consider Z being set such that
A1: Z in Class a & Z in Class b by XBOOLE_0:3;
reconsider Z as Element of R by A1;
A2: Z is_associated_to a by A1,Def5;
A3: Z is_associated_to b by A1,Def5;
A4: 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 A2,Th4;
then b is_associated_to c by A3,Th4;
hence thesis by Def5;
end;
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 A2,Th4;
hence thesis by Def5;
end;
hence thesis by A4,SUBSET_1:8;
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 SubFamEx;
hence thesis;
end;
uniqueness
proof
let F1,F2 be Subset-Family of R;
defpred P[set] means ex a being Element of R st $1 = Class a;
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 SubFamComp(A1,A2);
end;
end;
definition 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 consider A being Element of R such that
A2: X = Class A by Def6;
thus thesis by A2;
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 A3: X in M & Y in M & X <> Y;
assume A4: X meets Y;
consider A being Element of R such that
A5: X = Class A by A3,Def6;
consider B being Element of R such that
A6: Y = Class B by A3,Def6;
thus contradiction by A3,A4,A5,A6,Th20;
end;
then consider AmpS' being set such that A7:
for X st X in M ex x being set
st AmpS' /\ X = {x} by A1,WELLORD2:27;
AmpS' is non empty
proof
Class 1_ R in M by Def6;
then consider x being set such that
A8: AmpS' /\ Class 1_ R = {x} by A7;
thus thesis by A8;
end;
then reconsider AmpS' as non empty set;
set AmpS = { x where x is Element of AmpS':
ex X being non empty Subset of R
st X in M & AmpS' /\ X = { x }};
A9: 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 set such that
A10: AmpS' /\ X = {x} by A7;
X in Classes R;
then A11: X is non empty Subset of R by Th21;
A12: x in {x} by TARSKI:def 1;
then A13: x in AmpS' by A10,XBOOLE_0:def 3;
A14: x in X by A10,A12,XBOOLE_0:def 3;
A15: x in AmpS by A10,A11,A13;
AmpS /\ X = {x}
proof
now let y be set;
A16: now
assume y in {x};
then y = x by TARSKI:def 1;
hence y in {x} implies y in AmpS /\ X by A14,A15,XBOOLE_0:def 3;
end;
now
assume A17: y in AmpS /\ X;
then A18: y in X by XBOOLE_0:def 3;
y in AmpS by A17,XBOOLE_0:def 3;
then consider zz being Element of AmpS' such that
A19: y = zz &
(ex X being non empty Subset of R
st X in M & AmpS' /\ X = {zz});
thus y in AmpS /\ X implies y in {x} by A10,A18,A19,XBOOLE_0:def 3;
end;
hence y in {x} iff y in AmpS /\ X by A16;
end;
hence thesis by TARSKI:2;
end;
hence thesis by A15;
end;
AmpS is non empty Subset of R
proof
AmpS is non empty
proof
A20: Class 1_ R in M by Def6;
then consider x being set such that
A21: AmpS' /\ Class 1_ R = {x} by A7;
x in {x} by TARSKI:def 1;
then x in AmpS' by A21,XBOOLE_0:def 3;
then x in AmpS by A20,A21;
hence thesis;
end;
then reconsider AmpS as non empty set;
now let A be set;
now
assume A in AmpS;
then consider x being Element of AmpS' such that
A22: A = x &
(ex X being non empty Subset of R
st X in M & AmpS' /\ X = {x});
consider X being non empty Subset of R such that
A23: X in M & AmpS' /\ X = {x} by A22;
x in {x} by TARSKI:def 1;
then x in X by A23,XBOOLE_0:def 3;
hence (A in AmpS) implies (A in the carrier of R) by A22;
end;
hence (A in AmpS) implies (A in the carrier of R);
end;
hence thesis by TARSKI:def 3;
end;
then reconsider AmpS as non empty Subset of R;
A24: 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
A25: AmpS /\ N = {z} by A9;
z in {z} by TARSKI:def 1;
then z in Class a by A25,XBOOLE_0:def 3;
then z is_associated_to a by Def5;
hence thesis;
end;
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 A26: x <> y;
assume A27: x is_associated_to y;
x is_associated_to x;
then A28: x in Class x by Def5;
A29: y in Class x by A27,Def5;
A30: x in AmpS /\ Class x by A28,XBOOLE_0:def 3;
A31: y in AmpS /\ Class x by A29,XBOOLE_0:def 3;
Class x in M by Def6;
then consider z being Element of AmpS such that
A32: AmpS /\ Class x = {z} by A9;
y = z by A31,A32,TARSKI:def 1;
hence thesis by A26,A30,A32,TARSKI:def 1;
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 A24;
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 A' = { z where z is Element of A : z <> x } \/ {1_ R};
A2: 1_ R in A'
proof
1_ R in {1_ R} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 2;
end;
reconsider A' as non empty set;
A3: for x being Element of A' holds x = 1_ R or x in A
proof
let y be Element of A';
now per cases by XBOOLE_0:def 2;
case 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;
case y in {1_ R};
hence thesis by TARSKI:def 1;
end;
hence thesis;
end;
A' is non empty Subset of R
proof
now let x be set;
now
assume A4: x in A';
x in the carrier of R
proof
now per cases by A3,A4;
case x = 1_ R;
hence thesis;
case x in A;
hence thesis;
end;
hence thesis;
end;
hence x in A' implies x in the carrier of R;
end;
hence x in A' implies x in the carrier of R;
end;
hence thesis by TARSKI:def 3;
end;
then reconsider A' as non empty Subset of R;
A5: for a being Element of R ex z being Element of A'
st z is_associated_to a
proof
let a be Element of R;
now per cases;
case a is_associated_to 1_ R;
hence ex z being Element of A' st z is_associated_to a
by A2;
case A6: a is_not_associated_to 1_ R;
consider z being Element of A such that
A7: z is_associated_to a by Def7;
z <> x by A1,A6,A7,Th4;
then z in {zz where zz is Element of A : zz <> x};
then z in A' by XBOOLE_0:def 2;
hence ex z being Element of A' st z is_associated_to a
by A7;
end;
hence thesis;
end;
for z,y being Element of A' holds
z <> y implies z is_not_associated_to y
proof
let z,y be Element of A';
assume A8: z <> y;
now per cases;
case z = 1_ R & y = 1_ R;
hence thesis by A8;
case A9: z = 1_ R & y <> 1_ R;
then not( y in {1_ R} ) by TARSKI:def 1;
then y in {zz where zz is Element of A: zz <> x}
by XBOOLE_0:def 2;
then A10: ex zz being Element of A st y = zz & zz <> x;
assume z is_associated_to y;
then x is_associated_to y by A1,A9,Th4;
hence thesis by A10,Def7;
case A11: z <> 1_ R & y = 1_ R;
then not( z in {1_ R} ) by TARSKI:def 1;
then z in {zz where zz is Element of A: zz <> x}
by XBOOLE_0:def 2;
then A12: ex zz being Element of A st z = zz & zz <> x;
assume z is_associated_to y;
then z is_associated_to x by A1,A11,Th4;
hence thesis by A12,Def7;
case A13: z <> 1_ R & y <> 1_ R;
then A14: z in A by A3;
y in A by A3,A13;
hence thesis by A8,A14,Def7;
end;
hence thesis;
end;
then A' 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,Def3;
then consider D being Element of R such that
A2: 0.R * D = A by Def1;
thus thesis by A2,VECTSP_1:39;
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;
consider z being Element of Amp such that
A1: z is_associated_to x by Th22;
thus ex zz being Element of R st
zz in Amp & zz is_associated_to x by A1;
end;
hence thesis;
end;
uniqueness
proof
let z1,z2 be Element of R; assume
A2: z1 in Amp & z1 is_associated_to x &
z2 in Amp & z2 is_associated_to x;
then z1 is_associated_to z2 by Th4;
hence thesis by A2,Th22;
end;
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;
A1: 1_ R in Amp by Def8;
0.R is Element of Amp by Th24;
hence thesis by A1,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 :Def10:
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 A2: y divides x & y <> 0.R;
now per cases;
case A3: x <> 0.R;
set d = x/y;
A4: x = y * d by A2,Def4;
consider d' being Element of Amp such that
A5: d' is_associated_to d by Th22;
consider u being Element of R such that
A6: u is unital & d * u = d' by A5,Th18;
A7: u * x = y * d' by A4,A6,VECTSP_1:def 16;
A8: y * d' in Amp by A1,Def10;
A9: x is_associated_to u * x
proof
x divides x;
then A10: x divides u * x by Th7;
u divides 1_ R by A6,Def2;
then consider e being Element of R such that
A11: u * e = 1_ R by Def1;
(u * x) * e = (e * u) * x by VECTSP_1:def 16
.= x by A11,VECTSP_1:def 19;
then u * x divides x by Def1;
hence thesis by A10,Def3;
end;
1_ R * x = x by VECTSP_1:def 19
.= u * x by A7,A8,A9,Th22;
then u = 1_ R by A3,Th1;
then d' = d by A6,VECTSP_1:def 13;
hence thesis;
case A12: x = 0.R;
set d = x/y;
x = y * d by A2,Def4;
then A13: d = 0.R by A2,A12,VECTSP_2:def 5;
0.R is Element of Amp by Th24;
hence thesis by A13;
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;
x = (1_ F) * x by VECTSP_2:1;
then A2: (1_ F) divides x by Def1;
y = (1_ F) * y by VECTSP_2:1;
then A3: (1_ F) divides y by Def1;
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 A4: zz divides x & zz divides y;
now per cases;
case zz <> 0.F;
then consider zz' being Element of F such that
A5: zz * zz' = (1_ F) by VECTSP_1:def 20;
thus zz divides (1_ F) by A5,Def1;
case A6: zz = 0.F;
assume zz divides x;
then consider d being Element of F such that
A7: zz * d = x by Def1;
thus zz divides (1_ F) by A1,A6,A7,VECTSP_1:39;
end;
hence thesis by A4;
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)) by A2,A3;
case A8: x = 0.F;
y * 0.F = 0.F by VECTSP_1:39;
then A9: y divides 0.F by Def1;
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 A8,A9;
case A10: y = 0.F;
x * 0.F = 0.F by VECTSP_1:39;
then A11: x divides 0.F by Def1;
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 A10,A11;
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;
definition
cluster gcd-like domRing;
existence
proof
consider F being strict Field;
reconsider F as comRing;
reconsider F as domRing by VECTSP_2:13;
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 by Def11;
hence thesis;
end;
end;
definition
cluster gcd-like associative commutative well-unital (non empty multLoopStr);
existence
proof
consider F being 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 by Def11;
hence thesis;
end;
end;
definition
cluster gcd-like associative commutative well-unital
(non empty multLoopStr_0);
existence
proof
consider F being 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 by Def11;
hence thesis;
end;
end;
definition
cluster -> gcd-like
(Field-like add-associative right_zeroed right_complementable
left_unital right_unital left-distributive right-distributive
commutative (non empty doubleLoopStr));
coherence
proof
let F be Field-like add-associative right_zeroed right_complementable
left_unital right_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;
x = 1_ F * x by VECTSP_1:def 19;
then A2: 1_ F divides x by Def1;
y = 1_ F * y by VECTSP_1:def 19;
then A3: 1_ F divides y by Def1;
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 A4: zz divides x & zz divides y;
now per cases;
case zz <> 0.F;
then consider zz' being Element of F such that
A5: zz * zz' = 1_ F by VECTSP_1:def 20;
thus zz divides 1_ F by A5,Def1;
case A6: zz = 0.F;
assume zz divides x;
then consider d being Element of F such that
A7: zz * d = x by Def1;
thus zz divides 1_ F by A1,A6,A7,VECTSP_1:39;
end;
hence thesis by A4;
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)) by A2,A3;
case A8: x = 0.F;
y * 0.F = 0.F by VECTSP_1:36;
then A9: y divides 0.F by Def1;
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 A8,A9;
case A10: y = 0.F;
x * 0.F = 0.F by VECTSP_1:36;
then A11: x divides 0.F by Def1;
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 A10,A11;
end;
hence thesis;
end;
end;
definition
cluster gcd-like associative commutative well-unital domRing-like
well-unital distributive non degenerated
Abelian add-associative right_zeroed right_complementable
(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 &
(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
A2: z is_associated_to u by Th22;
A3: z divides u by A2,Def3;
then A4: z divides x by A1,Th2;
A5: z divides y by A1,A3,Th2;
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 A6: zz divides u by A1;
u divides z by A2,Def3;
hence thesis by A6,Th2;
end;
hence thesis by A4,A5;
end;
uniqueness
proof
now
let z1 be Element of R such that
A7: z1 in Amp &
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 &
z2 divides x &
z2 divides y &
(for z being Element of R
st (z divides x & z divides y)
holds (z divides z2));
z1 is_associated_to z2
proof
A9: z1 divides z2 by A7,A8;
z2 divides z1 by A7,A8;
hence thesis by A9,Def3;
end;
hence z1 = z2 by A7,A8,Th22;
end;
hence thesis;
end;
end;
reserve R for gcdDomain;
:: Lemmata about GCD
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
canceled;
theorem
Th29: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) by Def1;
gcd(A,B,Amp) divides A by Def12;
then consider E being Element of R such that
A2: gcd(A,B,Amp) * E = A by Def1;
A3: C * (D * E) = A by A1,A2,VECTSP_1:def 16;
gcd(A,B,Amp) divides B by Def12;
then consider E being Element of R such that
A4: gcd(A,B,Amp) * E = B by Def1;
C * (D * E) = B by A1,A4,VECTSP_1:def 16;
hence thesis by A3,Def1;
end;
theorem
Th30: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 in Amp by Def12;
A2: D divides B & D divides A by Def12;
for z being Element of R
st (z divides B & z divides A)
holds (z divides D) by Def12;
hence gcd(A,B,Amp) = gcd(B,A,Amp) by A1,A2,Def12;
end;
theorem
Th31: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)is_associated_to A by Def9;
then A2: NF(A,Amp) divides A by Def3;
NF(A,Amp) * 0.R = 0.R by VECTSP_1:36;
then A3: NF(A,Amp) divides 0.R by Def1;
A4: for z being Element of R
st (z divides A & z divides 0.R)
holds (z divides NF(A,Amp))
proof
let z be Element of R;
assume A5: z divides A & z divides 0.R;
A divides NF(A,Amp) by A1,Def3;
hence thesis by A5,Th2;
end;
NF(A,Amp) in Amp by Def9;
then gcd(A,0.R,Amp) = NF(A,Amp) by A2,A3,A4,Def12;
hence thesis by Th30;
end;
theorem
Th32: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 Th31;
hence thesis by Th25;
end;
theorem
Th33: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;
A1: 1_ R in Amp by Def8;
1_ R * A = A by VECTSP_1:def 19;
then A2: 1_ R divides A by Def1;
for z being Element of R
st (z divides A & z divides 1_ R)
holds (z divides 1_ R);
then gcd(A,1_ R,Amp) = 1_ R by A1,A2,Def12;
hence thesis by Th30;
end;
theorem
Th34: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: (A = 0.R & B = 0.R) implies (gcd(A,B,Amp) = 0.R)
proof
assume A2: A = 0.R & B = 0.R;
then gcd(A,B,Amp) = NF(A,Amp) by Th31;
hence thesis by A2,Th25;
end;
now assume gcd(A,B,Amp) = 0.R;
then A3: 0.R divides A & 0.R divides B by Def12;
then consider D being Element of R such that
A4: 0.R * D = A by Def1;
consider E being Element of R such that
A5: 0.R * E = B by A3,Def1;
thus (gcd(A,B,Amp) = 0.R) implies (A = 0.R & B = 0.R) by A4,A5,VECTSP_1:39;
end;
hence thesis by A1;
end;
theorem
Th35: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;
assume A1: B is_associated_to C;
then A2: B divides C by Def3;
gcd(A,B,Amp) divides B by Def12;
then A3: gcd(A,B,Amp) divides C by A2,Th2;
gcd(A,B,Amp) divides A by Def12;
then A4: gcd(A,B,Amp) divides gcd(A,C,Amp) by A3,Def12;
A5: gcd(A,B,Amp) = gcd(B,A,Amp) by Th30;
A6: C divides B by A1,Def3;
gcd(A,C,Amp) divides C by Def12;
then A7: gcd(A,C,Amp) divides B by A6,Th2;
gcd(A,C,Amp) divides A by Def12;
then gcd(A,C,Amp) divides gcd(A,B,Amp) by A7,Def12;
then gcd(A,B,Amp) is_associated_to gcd(A,C,Amp) by A4,Def3;
hence thesis by A5,Th30;
end;
:: Main Theorems
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem
Th36: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);
D divides gcd(A,B,Amp) & D divides C by Def12;
then D divides A & D divides B & D divides C by Th29;
then D divides A & D divides gcd(B,C,Amp) by Def12;
then A1: D divides E by Def12;
E divides gcd(B,C,Amp) & E divides A by Def12;
then E divides B & E divides C & E divides A by Th29;
then E divides C & E divides gcd(A,B,Amp) by Def12;
then E divides D by Def12;
then A2: D is_associated_to E by A1,Def3;
A3: D is Element of Amp by Def12;
E is Element of Amp by Def12;
hence thesis by A2,A3,Th22;
end;
theorem
Th37: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);
D divides A & D divides B by Def12;
then C * D divides A * C & C * D divides B * C by Th5;
then C * D divides gcd((A * C),(B * C),Amp) by Def12;
then consider F being Element of R such that
A3: E = (C * D) * F by Def1;
A4: E divides A * C by Def12;
A5: E divides B * C by Def12;
(D * F) divides A & (D * F) divides B
proof
consider G being Element of R such that
A6: ((C * D) * F) * G = A * C by A3,A4,Def1;
(C * (D * F)) * G = C * A by A6,VECTSP_1:def 16;
then A7: (C * (D * F)) divides C * A by Def1;
consider G being Element of R such that
A8: ((C * D) * F) * G = B * C by A3,A5,Def1;
(C * (D * F)) * G = C * B by A8,VECTSP_1:def 16;
then (C * (D * F)) divides C * B by Def1;
hence thesis by A1,A7,Th15;
end;
then A9: D * F divides D by Def12;
F divides 1_ R
proof
D = D * 1_ R by VECTSP_1:def 13;
hence thesis by A2,A9,Th15;
end;
then F is unital by Def2;
hence gcd((A * C),(B * C),Amp) is_associated_to (C * gcd(A,B,Amp)) by A3,Th18
;
case A10: D = 0.R;
then A11: A = 0.R & B = 0.R by Th34;
A12: C * gcd(A,B,Amp) = 0.R by A10,VECTSP_1:39;
gcd((A * C),(B * C),Amp)
= gcd(0.R,(0.R * C),Amp) by A11,VECTSP_1:39
.= gcd(0.R,0.R,Amp) by VECTSP_1:39
.= C * gcd(A,B,Amp) by A12,Th32;
hence gcd((A * C),(B * C),Amp) is_associated_to (C * gcd(A,B,Amp));
end;
hence gcd((A * C),(B * C),Amp) is_associated_to (C * gcd(A,B,Amp));
case A13: C = 0.R;
then A14: A * C = 0.R by VECTSP_1:39;
B * C = 0.R by A13,VECTSP_1:39;
then gcd((A * C),(B * C),Amp)
= 0.R by A14,Th32
.= C * gcd(A,B,Amp) by A13,VECTSP_1:39;
hence gcd((A * C),(B * C),Amp) is_associated_to (C * gcd(A,B,Amp));
end;
hence thesis;
end;
theorem
Th38: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 A1: gcd(A,B,Amp) = 1_ R;
A2: gcd((A * C),(B * C),Amp) is_associated_to (C * gcd(A,B,Amp))
by Th37;
C * (gcd(A,B,Amp)) = C by A1,VECTSP_1:def 13;
then gcd(A,C,Amp) is_associated_to gcd(A,gcd((A * C),(B * C),Amp),Amp)
by A2,Th35;
then A3: gcd(A,C,Amp) is_associated_to gcd(gcd(A,(A * C),Amp),(B * C),Amp)
by Th36;
gcd(A,(A * C),Amp) is_associated_to A
proof
A4: gcd((A * 1_ R),(A * C),Amp) is_associated_to (A * gcd(1_ R,C,Amp))
by Th37;
A * gcd(1_ R,C,Amp) = A * 1_ R by Th33
.= A by VECTSP_1:def 13;
hence thesis by A4,VECTSP_1:def 13;
end;
then gcd(gcd(A,(A * C),Amp),(B * C),Amp) is_associated_to gcd(A,(B * C),Amp)
by Th35;
then A5: gcd(A,(B * C),Amp) is_associated_to gcd(A,C,Amp) by A3,Th4;
A6: gcd(A,(B * C),Amp) is Element of Amp by Def12;
gcd(A,C,Amp) is Element of Amp by Def12;
hence thesis by A5,A6,Th22;
end;
theorem
Th39: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 A1: ((C = gcd(A,B,Amp)) & (C <> 0.R));
set A1 = A/C;
set B1 = B/C;
C divides A by A1,Def12;
then A2: A1 * C = A by A1,Def4;
C divides B by A1,Def12;
then A3: gcd(A,B,Amp) = gcd((A1 * C),(B1 * C),Amp) by A1,A2,Def4;
gcd((A1 * C),(B1 * C),Amp) is_associated_to (C * gcd(A1,B1,Amp))
by Th37;
then (C * 1_ R) is_associated_to (C * gcd(A1,B1,Amp)) by A1,A3,VECTSP_1:def 13
;
then A4: gcd(A1,B1,Amp) is_associated_to 1_ R by A1,Th19;
A5: gcd(A1,B1,Amp) is Element of Amp by Def12;
1_ R is Element of Amp by Def8;
hence thesis by A4,A5,Th22;
end;
theorem
Th40: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);
A1: D divides A & D divides C by Def12;
A2: D is Element of Amp by Def12;
consider E being Element of R such that
A3: D * E = A by A1,Def1;
consider F being Element of R such that
A4: D * F = C by A1,Def1;
A5: D divides (A + (B * C))
proof
D * (E + (F * B)) = (D * E) + (D * (F * B)) by VECTSP_1:def 11
.= A + (B * C) by A3,A4,VECTSP_1:def 16;
hence thesis by Def1;
end;
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 A6: Z divides (A + (B * C)) & (Z divides C);
then consider X being Element of R such that
A7: Z * X = C by Def1;
consider Y being Element of R such that
A8: Z * Y = A + (B * C) by A6,Def1;
Z * (Y + (-(B * X))) = (Z * Y) + (Z * (-(B * X))) by VECTSP_1:def 11
.= (Z * Y) + (-(Z * (X * B))) by VECTSP_1:40
.= (A + (B * C)) + (-(C * B)) by A7,A8,VECTSP_1:def
16
.= A + ((B * C) + (-(C * B))) by RLVECT_1:def 6
.= A + 0.R by RLVECT_1:def 10
.= A by RLVECT_1:10;
then Z divides A by Def1;
hence thesis by A6,Def12;
end;
hence thesis by A1,A2,A5,Def12;
end;
begin
:: Brown & Henrici
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
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 * (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 A1: gcd(r1,r2,Amp) = 1_ R & gcd(s1,s2,Amp) = 1_ R &
r2 <> 0.R & s2 <> 0.R;
set d = gcd(r2,s2,Amp);
A2: d divides s2 by Def12;
A3: d divides r2 by Def12;
A4: d <> 0.R by A1,Th34;
set r = r2/d;
set s = s2/d;
A5: gcd(((r1 * s) + (s1 * r)),s,Amp) = gcd((s1 * r),s,Amp) by Th40;
gcd(s,s1,Amp) = 1_ R
proof
A6: gcd(s,s1,Amp) divides s1 by Def12;
gcd(s,s1,Amp) divides s by Def12;
then consider e being Element of R such that
A7: gcd(s,s1,Amp) * e = s by Def1;
gcd(s,s1,Amp) * (e * d)
= s * d by A7,VECTSP_1:def 16
.= s2 by A2,A4,Def4;
then gcd(s,s1,Amp) divides s2 by Def1;
then A8: gcd(s,s1,Amp) divides gcd(s1,s2,Amp) by A6,Def12;
1_ R * gcd(s,s1,Amp) = gcd(s,s1,Amp) by VECTSP_1:def 19;
then 1_ R divides gcd(s,s1,Amp) by Def1;
then A9: gcd(s,s1,Amp) is_associated_to 1_ R by A1,A8,Def3;
A10: gcd(s,s1,Amp) is Element of Amp by Def12;
1_ R is Element of Amp by Def8;
hence thesis by A9,A10,Th22;
end;
then A11: gcd(s,(s1 * r),Amp) = gcd(s,r,Amp) by Th38;
A12: gcd(r,s,Amp) = 1_ R by A4,Th39;
A13: gcd(((r1 * s) + (s1 * r)),s,Amp)
= gcd(s,(s1 * r),Amp) by A5,Th30
.= 1_ R by A11,A12,Th30;
A14: r2 * s = s * (d * r)
proof
A15: d divides (d * r2) by Th6;
r2 * s = (1_ R * r2) * s by VECTSP_1:def 19
.= ((d/d) * r2) * s by A4,Th9
.= ((d * r2)/d) * s by A4,A15,Th11
.= s * (d * r) by A3,A4,A15,Th11;
hence thesis;
end;
A16: gcd(((r1 * s) + (s1 * r)),r,Amp) = gcd((r1 * s),r,Amp) by Th40;
gcd(r,r1,Amp) = 1_ R
proof
A17: gcd(r,r1,Amp) divides r1 by Def12;
gcd(r,r1,Amp) divides r by Def12;
then consider e being Element of R such that
A18: gcd(r,r1,Amp) * e = r by Def1;
gcd(r,r1,Amp) * (e * d)
= r * d by A18,VECTSP_1:def 16
.= r2 by A3,A4,Def4;
then gcd(r,r1,Amp) divides r2 by Def1;
then A19: gcd(r,r1,Amp) divides gcd(r1,r2,Amp) by A17,Def12;
1_ R * gcd(r,r1,Amp) = gcd(r,r1,Amp) by VECTSP_1:def 19;
then 1_ R divides gcd(r,r1,Amp) by Def1;
then A20: gcd(r,r1,Amp) is_associated_to 1_ R by A1,A19,Def3;
A21: gcd(r,r1,Amp) is Element of Amp by Def12;
1_ R is Element of Amp by Def8;
hence thesis by A20,A21,Th22;
end;
then A22: gcd(r,(r1 * s),Amp) = gcd(r,s,Amp) by Th38;
gcd(r,s,Amp) = 1_ R by A4,Th39;
then gcd(((r1 * s) + (s1 * r)),r,Amp)
= 1_ R by A16,A22,Th30;
then gcd(((r1 * s) + (s1 * r)),(d * r),Amp)
= gcd(((r1 * s) + (s1 * r)),d,Amp) by Th38;
hence thesis by A13,A14,Th38;
end;
theorem
Th42: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 A1: gcd(r1,r2,Amp) = 1_ R & gcd(s1,s2,Amp) = 1_ R &
r2 <> 0.R & s2 <> 0.R;
set d1 = gcd(r1,s2,Amp);
set d2 = gcd(s1,r2,Amp);
A2: d1 <> 0.R by A1,Th34;
A3: d2 <> 0.R by A1,Th34;
set r1' = r1/d1;
set s1' = s1/d2;
set r2' = r2/d2;
set s2' = s2/d1;
d1 divides r1 by Def12;
then r1' * d1 = r1 by A2,Def4;
then A4: r1' divides r1 by Def1;
d2 divides r2 by Def12;
then r2' * d2 = r2 by A3,Def4;
then A5: r2' divides r2 by Def1;
A6: gcd(r1',r2',Amp) divides r1' by Def12;
A7: gcd(r1',r2',Amp) divides r2' by Def12;
A8: gcd(r1',r2',Amp) divides r1 by A4,A6,Th2;
gcd(r1',r2',Amp) divides r2 by A5,A7,Th2;
then A9: gcd(r1',r2',Amp) divides gcd(r1,r2,Amp) by A8,Def12;
1_ R * gcd(r1',r2',Amp) = gcd(r1',r2',Amp) by VECTSP_1:def 19;
then 1_ R divides gcd(r1',r2',Amp) by Def1;
then A10: gcd(r1',r2',Amp) is_associated_to 1_ R by A1,A9,Def3;
A11: gcd(r1',r2',Amp) is Element of Amp by Def12;
1_ R is Element of Amp by Def8;
then gcd(r1',r2',Amp) = 1_ R by A10,A11,Th22;
then A12: gcd(r2',r1',Amp) = 1_ R by Th30;
d1 divides s2 by Def12;
then s2' * d1 = s2 by A2,Def4;
then A13: s2' divides s2 by Def1;
d2 divides s1 by Def12;
then s1' * d2 = s1 by A3,Def4;
then A14: s1' divides s1 by Def1;
A15: gcd(s1',s2',Amp) divides s1' by Def12;
A16: gcd(s1',s2',Amp) divides s2' by Def12;
A17: gcd(s1',s2',Amp) divides s1 by A14,A15,Th2;
gcd(s1',s2',Amp) divides s2 by A13,A16,Th2;
then A18: gcd(s1',s2',Amp) divides gcd(s1,s2,Amp) by A17,Def12;
1_ R * gcd(s1',s2',Amp) = gcd(s1',s2',Amp) by VECTSP_1:def 19;
then 1_ R divides gcd(s1',s2',Amp) by Def1;
then A19: gcd(s1',s2',Amp) is_associated_to 1_ R by A1,A18,Def3;
A20: gcd(s1',s2',Amp) is Element of Amp by Def12;
1_ R is Element of Amp by Def8;
then A21: gcd(s1',s2',Amp) = 1_ R by A19,A20,Th22;
A22: gcd(s2',r1',Amp) = gcd((r1/d1),(s2/d1),Amp) by Th30
.= 1_ R by A2,Th39;
A23: gcd(s1',r2',Amp) = 1_ R by A3,Th39;
gcd((r1' * s1'),r2',Amp) = gcd(r2',(r1' * s1'),Amp) by Th30
.= gcd(r2',s1',Amp) by A12,Th38
.= 1_ R by A23,Th30;
then gcd((r1' * s1'),(r2' * s2'),Amp)
= gcd((r1' * s1'),s2',Amp) by Th38
.= gcd(s2',(r1' * s1'),Amp) by Th30
.= gcd(s2',s1',Amp) by A22,Th38
.= 1_ R by A21,Th30;
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 :Def13:
gcd(x,y,Amp) = 1_ R;
end;
theorem
Th43:for Amp,Amp' being AmpleSet of R
for x,y being Element of R holds
x,y are_canonical_wrt Amp iff x,y are_canonical_wrt Amp'
proof
let Amp,Amp' be AmpleSet of R;
let x,y be Element of R;
A1: now assume x,y are_canonical_wrt Amp;
then gcd(x,y,Amp) = 1_ R by Def13;
then A2: for z being Element of R
st (z divides x & z divides y)
holds (z divides 1_ R) by Def12;
A3: 1_ R * x = x by VECTSP_1:def 19;
A4: 1_ R * y = y by VECTSP_1:def 19;
A5: 1_ R divides x by A3,Def1;
A6: 1_ R divides y by A4,Def1;
1_ R in Amp' by Def8;
then gcd(x,y,Amp') = 1_ R by A2,A5,A6,Def12;
hence x,y are_canonical_wrt Amp' by Def13;
end;
now assume x,y are_canonical_wrt Amp';
then gcd(x,y,Amp') = 1_ R by Def13;
then A7: for z being Element of R
st (z divides x & z divides y)
holds (z divides 1_ R) by Def12;
A8: 1_ R * x = x by VECTSP_1:def 19;
A9: 1_ R * y = y by VECTSP_1:def 19;
A10: 1_ R divides x by A8,Def1;
A11: 1_ R divides y by A9,Def1;
1_ R in Amp by Def8;
then gcd(x,y,Amp) = 1_ R by A7,A10,A11,Def12;
hence x,y are_canonical_wrt Amp by Def13;
end;
hence thesis by A1;
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 :Def14:
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;
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,Th30;
hence thesis by Def14;
end;
end;
theorem
Th44: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 Amp' being AmpleSet of R such that
A1: gcd(x,y,Amp') = 1_ R by Def14;
x,y are_canonical_wrt Amp' by A1,Def13;
then x,y are_canonical_wrt Amp by Th43;
hence thesis by Def13;
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 :Def15:
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 A1: r1,r2 are_co-prime & s1,s2 are_co-prime &
r2 = NF(r2,Amp) & 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
A2: gcd(r1,r2,Amp) = 1_ R & gcd(s1,s2,Amp) = 1_ R by A1,Th44;
A3: 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 A4: r1 = 0.R & gcd(r2,s2,Amp) = 1_ R;
let z be Element of R;
A5: r2 = 1_ R by A1,A2,A4,Th31;
(r1 * s2) + (r2 * s1) = 0.R + (r2 * s1) by A4,VECTSP_1:39
.= 1_ R * s1 by A5,RLVECT_1:10
.= s1 by VECTSP_1:def 19;
hence thesis;
end;
A6: 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
assume A7: r1 = 0.R & (r1 * (s2/gcd(r2,s2,Amp))) +
(s1 * (r2/gcd(r2,s2,Amp))) = 0.R;
let z be Element of R;
A8: r2 = 1_ R by A1,A2,A7,Th31;
then A9: gcd(r2,s2,Amp) = 1_ R by Th33;
A10: 1_ R <> 0.R by VECTSP_1:def 21;
0.R = 0.R+(s1*(r2/gcd(r2,s2,Amp))) by A7,VECTSP_1:39
.= s1*(1_ R/gcd(r2,s2,Amp)) by A8,RLVECT_1:10
.= s1*1_ R by A9,A10,Th9
.= s1 by VECTSP_1:def 13;
hence thesis;
end;
A11: 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 A12: s1 = 0.R & gcd(r2,s2,Amp) = 1_ R;
let z be Element of R;
A13: s2 = 1_ R by A1,A2,A12,Th31;
(r1 * s2) + (r2 * s1) = (r1 * s2) + 0.R by A12,VECTSP_1:39
.= r1 * 1_ R by A13,RLVECT_1:10
.= r1 by VECTSP_1:def 13;
hence thesis;
end;
A14: 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
assume A15: s1 = 0.R & (r1 * (s2/gcd(r2,s2,Amp))) +
(s1 * (r2/gcd(r2,s2,Amp))) = 0.R;
let z be Element of R;
A16: s2 = 1_ R by A1,A2,A15,Th31;
then A17: gcd(r2,s2,Amp) = 1_ R by Th33;
A18: 1_ R <> 0.R by VECTSP_1:def 21;
0.R = (r1*(s2/gcd(r2,s2,Amp)))+0.R by A15,VECTSP_1:39
.= r1*(1_ R/gcd(r2,s2,Amp)) by A16,RLVECT_1:10
.= r1*1_ R by A17,A18,Th9
.= r1 by VECTSP_1:def 13;
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 A19: 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 A19,Th10
.= (r1 * s2) + (s1 * r2) by Th10;
hence thesis;
end;
hence thesis by A3,A6,A11,A14;
end;
end;
definition
let R be gcdDomain;
let Amp be AmpleSet of R;
let r1,r2,s1,s2 be Element of R;
assume A1: r1,r2 are_co-prime & s1,s2 are_co-prime &
r2 = NF(r2,Amp) & 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
A2: gcd(r1,r2,Amp) = 1_ R & gcd(s1,s2,Amp) = 1_ R by A1,Th44;
A3: r1 = 0.R & s1 = 0.R implies
for z being Element of R
holds z = s2 iff z = r2
proof
assume A4: r1 = 0.R & s1 = 0.R;
let z be Element of R;
r2 = 1_ R by A1,A2,A4,Th31;
hence thesis by A1,A2,A4,Th31;
end;
A5: 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 A6: r1 = 0.R & gcd(r2,s2,Amp) = 1_ R;
let z be Element of R;
r2 = 1_ R by A1,A2,A6,Th31;
hence thesis by VECTSP_1:def 19;
end;
A7: 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
assume A8: r1 = 0.R & (r1 * (s2/gcd(r2,s2,Amp))) +
(s1 * (r2/gcd(r2,s2,Amp))) = 0.R;
let z be Element of R;
A9: r2 = 1_ R by A1,A2,A8,Th31;
then A10: gcd(r2,s2,Amp) = 1_ R by Th33;
A11: 1_ R <> 0.R by VECTSP_1:def 21;
0.R
= 0.R+(s1*(r2/gcd(r2,s2,Amp))) by A8,VECTSP_1:39
.= s1*(1_ R/gcd(r2,s2,Amp)) by A9,RLVECT_1:10
.= s1*1_ R by A10,A11,Th9
.= s1 by VECTSP_1:def 13;
hence thesis by A1,A2,Th31;
end;
A12: 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 A13: s1 = 0.R & gcd(r2,s2,Amp) = 1_ R;
let z be Element of R;
s2 = 1_ R by A1,A2,A13,Th31;
hence thesis by VECTSP_1:def 13;
end;
A14: 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
assume A15: s1 = 0.R & (r1 * (s2/gcd(r2,s2,Amp))) +
(s1 * (r2/gcd(r2,s2,Amp))) = 0.R;
let z be Element of R;
A16: s2 = 1_ R by A1,A2,A15,Th31;
then A17: gcd(r2,s2,Amp) = 1_ R by Th33;
A18: 1_ R <> 0.R by VECTSP_1:def 21;
0.R
= (r1*(s2/gcd(r2,s2,Amp)))+0.R by A15,VECTSP_1:39
.= r1*(1_ R/gcd(r2,s2,Amp)) by A16,RLVECT_1:10
.= r1*1_ R by A17,A18,Th9
.= r1 by VECTSP_1:def 13;
hence thesis by A1,A2,Th31;
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 = r2 * s2 iff z = 1_ R
proof
assume A19: 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;
A20: 0.R
= (r1 * s2) + (s1 * (r2/1_ R)) by A19,Th10
.= (r1 * s2) + (s1 * r2) by Th10;
then A21: r1 * s2 = -(s1 * r2) by RLVECT_1:19;
A22: s1 * r2 = -(r1 * s2) by A20,RLVECT_1:19;
gcd(r2,r1,Amp) = 1_ R by A1,Th44;
then gcd(r2,r1*s2,Amp) = 1_ R by A19,Th38;
then A23: 1_ R = gcd(1_ R*r2,-(s1*r2),Amp) by A21,VECTSP_1:def 19
.= gcd(1_ R*r2,(-s1)*r2,Amp) by VECTSP_1:40;
A24: r2 * gcd(1_ R,(-s1),Amp) = r2 * 1_ R by Th33
.= r2 by VECTSP_1:def 13;
A25: 1_ R is_associated_to r2 * gcd(1_ R,(-s1),Amp) by A23,Th37;
A26: 1_ R in Amp by Th22;
then A27: r2 = 1_ R by A1,A24,A25,Def9;
gcd(s2,s1,Amp) = 1_ R by A1,Th44;
then gcd(s2,s1*r2,Amp) = gcd(s2,r2,Amp) by Th38
.= 1_ R by A19,Th30;
then A28: 1_ R = gcd(1_ R*s2,-(r1*s2),Amp) by A22,VECTSP_1:def 19
.= gcd(1_ R*s2,(-r1)*s2,Amp) by VECTSP_1:40;
A29: s2 * gcd(1_ R,(-r1),Amp) = s2 * 1_ R by Th33
.= s2 by VECTSP_1:def 13;
1_ R is_associated_to s2 * gcd(1_ R,(-r1),Amp) by A28,Th37;
then s2 = 1_ R by A1,A26,A29,Def9;
hence thesis by A27,VECTSP_1:def 13;
end;
hence thesis by A3,A5,A7,A12,A14;
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 A1: Amp is multiplicative &
r1,r2 are_normalized_wrt Amp &
s1,s2 are_normalized_wrt Amp;
then A2: r2 in Amp & s2 in Amp &
r2 <> 0.R & s2 <> 0.R by Def15;
then A3: r2 = NF(r2,Amp) & s2 = NF(s2,Amp) &
r2 <> 0.R & s2 <> 0.R by Def9;
A4: gcd(r1,r2,Amp) = 1_ R & gcd(s1,s2,Amp) = 1_ R
by A1,Def15;
then A5: r1,r2 are_co-prime & s1,s2 are_co-prime by Def14;
now per cases;
case A6: r1 = 0.R;
then add2(r1,r2,s1,s2,Amp) = s2 by A3,A5,Def17;
hence thesis by A1,A3,A5,A6,Def16;
case A7: s1 = 0.R;
then add2(r1,r2,s1,s2,Amp) = r2 by A3,A5,Def17;
hence thesis by A1,A3,A5,A7,Def16;
case A8: gcd(r2,s2,Amp) = 1_ R;
then A9: add1(r1,r2,s1,s2,Amp) = (r1 * s2) + (r2 * s1) by A3,A5,Def16;
A10: add2(r1,r2,s1,s2,Amp) = r2 * s2 by A3,A5,A8,Def17;
then A11: 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 A9,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 A8,Th10
.= gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))),
gcd(r2,s2,Amp),Amp) by A2,A4,Th41
.= 1_ R by A8,Th33;
reconsider r2,s2 as Element of Amp by A1,Def15;
A12: r2 * s2 in Amp by A1,Def10;
r2 * s2 <> 0.R by A2,VECTSP_2:def 5;
hence thesis by A10,A11,A12,Def15;
case (r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))) = 0.R;
then A13: add2(r1,r2,s1,s2,Amp) = 1_ R by A3,A5,Def17;
then A14: gcd(add1(r1,r2,s1,s2,Amp),add2(r1,r2,s1,s2,Amp),Amp)
= 1_ R by Th33;
A15: 1_ R in Amp by Th22;
1_ R <> 0.R by VECTSP_1:def 21;
hence thesis by A13,A14,A15,Def15;
case A16: 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 A17: 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,Def16;
A18: 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,A16,Def17;
A19: 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 A2,A4,Th41;
gcd(r2,s2,Amp) <> 0.R by A2,Th34;
then gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))),
gcd(r2,s2,Amp),Amp)
<> 0.R by Th34;
then A20: 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 A19,Th39;
reconsider r2,s2 as Element of Amp by A1,Def15;
A21: gcd(r2,s2,Amp) divides s2 by Def12;
A22: gcd(r2,s2,Amp) <> 0.R by A2,Th34;
gcd(r2,s2,Amp) in Amp by Def12;
then reconsider z3 = s2/gcd(r2,s2,Amp) as Element of Amp by A1,A21,A22,Th27;
r2 * z3 in Amp by A1,Def10;
then reconsider z1 = r2 * (s2/gcd(r2,s2,Amp)) as Element of Amp;
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;
A23: z2 divides z1
proof
A24: z2 divides gcd(r2,s2,Amp) by Def12;
gcd(r2,s2,Amp) divides r2 by Def12;
then z2 divides r2 by A24,Th2;
hence thesis by Th7;
end;
A25: z2 <> 0.R by A22,Th34;
then A26: z1 / z2 in Amp by A1,A23,Th27;
z1 / z2 <> 0.R
proof
A27: r2 * s2 <> 0.R by A2,VECTSP_2:def 5;
A28: gcd(r2,s2,Amp) divides r2 * s2 by A21,Th7;
then z1 = (r2 * s2)/gcd(r2,s2,Amp) by A21,A22,Th11;
then z1 <> 0.R by A22,A27,A28,Th8;
hence thesis by A23,A25,Th8;
end;
hence thesis by A17,A18,A20,A26,Def15;
end;
hence thesis;
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) * (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 A1: Amp is multiplicative &
r1,r2 are_normalized_wrt Amp &
s1,s2 are_normalized_wrt Amp;
then gcd(r1,r2,Amp) = 1_ R & gcd(s1,s2,Amp) = 1_ R &
s2 in Amp & r2 in Amp by Def15;
then A2: r1,r2 are_co-prime & s1,s2 are_co-prime &
r2 <> 0.R & s2 <> 0.R &
r2 = NF(r2,Amp) & s2 = NF(s2,Amp) by A1,Def9,Def14,Def15;
now per cases;
case A3: r1 = 0.R;
then A4: add1(r1,r2,s1,s2,Amp) = s1 by A2,Def16;
add2(r1,r2,s1,s2,Amp) = s2 by A2,A3,Def17;
then add2(r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2))
= s2 * (0.R + (s1 * r2)) by A3,VECTSP_1:39
.= s2 * (s1 * r2) by RLVECT_1:10
.= add1(r1,r2,s1,s2,Amp) * (r2 * s2) by A4,VECTSP_1:def 16;
hence thesis;
case A5: s1 = 0.R;
then A6: add1(r1,r2,s1,s2,Amp) = r1 by A2,Def16;
add2(r1,r2,s1,s2,Amp) = r2 by A2,A5,Def17;
then add2(r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2))
= r2 * ((r1 * s2) + 0.R) by A5,VECTSP_1:39
.= r2 * (r1 * s2) by RLVECT_1:10
.= add1(r1,r2,s1,s2,Amp) * (r2 * s2) by A6,VECTSP_1:def 16;
hence thesis;
case A7: gcd(r2,s2,Amp) = 1_ R;
then add2(r1,r2,s1,s2,Amp) = r2 * s2 by A2,Def17;
hence thesis by A2,A7,Def16;
case A8: (r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))) = 0.R;
then A9: add1(r1,r2,s1,s2,Amp) = 0.R by A2,Def16;
A10: (r1 * s2) + (s1 * r2) = 0.R
proof
A11: gcd(r2,s2,Amp) <> 0.R by A2,Th34;
A12: gcd(r2,s2,Amp) divides s2 by Def12;
A13: gcd(r2,s2,Amp) divides r2 by Def12;
A14: gcd(r2,s2,Amp) divides r1 * s2 by A12,Th7;
A15: gcd(r2,s2,Amp) divides s1 * r2 by A13,Th7;
A16: 0.R
= (r1 * s2)/gcd(r2,s2,Amp) + (s1 * (r2/gcd(r2,s2,Amp)))
by A8,A11,A12,A14,Th11
.= (r1 * s2)/gcd(r2,s2,Amp) + (s1 * r2)/gcd(r2,s2,Amp)
by A11,A13,A15,Th11;
consider e being Element of R such that
A17: gcd(r2,s2,Amp) * e = r2 by A13,Def1;
consider f being Element of R such that
A18: gcd(r2,s2,Amp) * f = s2 by A12,Def1;
gcd(r2,s2,Amp) * ((e * s1)+(f * r1))
= (gcd(r2,s2,Amp) * (e * s1))+(gcd(r2,s2,Amp) * (f * r1))
by VECTSP_1:def 11
.= ((gcd(r2,s2,Amp) * e) * s1)+(gcd(r2,s2,Amp) * (f * r1))
by VECTSP_1:def 16
.= (r1 * s2)+(s1 * r2) by A17,A18,VECTSP_1:def 16;
then A19: gcd(r2,s2,Amp) divides (r1 * s2) + (s1 * r2) by Def1;
then A20: 0.R
= ((r1 * s2) + (s1 * r2)) / gcd(r2,s2,Amp) by A11,A14,A15,A16,Th12
;
0.R = 0.R * gcd(r2,s2,Amp) by VECTSP_1:39
.= ((r1 * s2) + (s1 * r2)) by A11,A19,A20,Def4;
hence thesis;
end;
add1(r1,r2,s1,s2,Amp) * (r2 * s2)
= 0.R by A9,VECTSP_1:39
.= add2(r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2)) by A10,VECTSP_1:39;
hence thesis;
case A21: 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 A22: 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 A2,Def16;
A23: 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 A2,A21,Def17;
A24: gcd(r2,s2,Amp) <> 0.R by A2,Th34;
A25: gcd(r2,s2,Amp) divides s2 by Def12;
A26: gcd(r2,s2,Amp) divides r2 by Def12;
A27: gcd(r2,s2,Amp) divides r1 * s2 by A25,Th7;
A28: gcd(r2,s2,Amp) divides s1 * r2 by A26,Th7;
A29: gcd(r2,s2,Amp) divides ((r1 * s2) * r2) by A27,Th7;
A30: gcd(r2,s2,Amp) divides ((s1 * r2) * r2) by A26,Th7;
A31: gcd(r2,s2,Amp) divides (((r1 * s2) * r2) * s2) by A29,Th7;
A32: gcd(r2,s2,Amp) divides (((s1 * r2) * r2) * s2) by A30,Th7;
A33: ((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 18
.= (((r1 * s2)/gcd(r2,s2,Amp)) * (r2 * s2)) +
((s1 * (r2/gcd(r2,s2,Amp))) * (r2 * s2)) by A24,A25,A27,Th11
.= (((r1 * s2)/gcd(r2,s2,Amp)) * (r2 * s2)) +
(((s1 * r2)/gcd(r2,s2,Amp)) * (r2 * s2)) by A24,A26,A28,Th11
.= ((((r1 * s2)/gcd(r2,s2,Amp)) * r2) * s2) +
(((s1 * r2)/gcd(r2,s2,Amp)) * (r2 * s2)) by VECTSP_1:def 16
.= ((((r1 * s2)/gcd(r2,s2,Amp)) * r2) * s2) +
((((s1 * r2)/gcd(r2,s2,Amp)) * r2) * s2) by VECTSP_1:def 16
.= ((((r1 * s2) * r2)/gcd(r2,s2,Amp)) * s2) +
((((s1 * r2)/gcd(r2,s2,Amp)) * r2) * s2) by A24,A27,A29,Th11
.= ((((r1 * s2) * r2)/gcd(r2,s2,Amp)) * s2) +
((((s1 * r2) * r2)/gcd(r2,s2,Amp)) * s2) by A24,A28,A30,Th11
.= ((((r1 * s2) * r2) * s2)/gcd(r2,s2,Amp)) +
((((s1 * r2) * r2)/gcd(r2,s2,Amp)) * s2) by A24,A29,A31,Th11
.= ((((r1 * s2) * r2) * s2)/gcd(r2,s2,Amp)) +
((((s1 * r2) * r2) * s2)/gcd(r2,s2,Amp)) by A24,A30,A32,Th11;
A34: gcd(r2,s2,Amp) divides (r2 * s2) by A26,Th7;
then A35: gcd(r2,s2,Amp) divides ((r2 * s2) * r1) by Th7;
A36: gcd(r2,s2,Amp) divides ((r2 * s2) * s1) by A34,Th7;
A37: gcd(r2,s2,Amp) divides (((r2 * s2) * r1) * s2) by A35,Th7;
A38: gcd(r2,s2,Amp) divides (((r2 * s2) * s1) * r2) by A36,Th7;
A39: (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 11
.= (((r2 * (s2/gcd(r2,s2,Amp))) * r1) * s2) +
((r2 * (s2/gcd(r2,s2,Amp))) * (s1 * r2)) by VECTSP_1:def 16
.= (((r2 * (s2/gcd(r2,s2,Amp))) * r1) * s2) +
(((r2 * (s2/gcd(r2,s2,Amp))) * s1) * r2) by VECTSP_1:def 16
.= ((((r2 * s2)/gcd(r2,s2,Amp)) * r1) * s2) +
(((r2 * (s2/gcd(r2,s2,Amp))) * s1) * r2) by A24,A25,A34,Th11
.= ((((r2 * s2)/gcd(r2,s2,Amp)) * r1) * s2) +
((((r2 * s2)/gcd(r2,s2,Amp)) * s1) * r2) by A24,A25,A34,Th11
.= ((((r2 * s2) * r1)/gcd(r2,s2,Amp)) * s2) +
((((r2 * s2)/gcd(r2,s2,Amp)) * s1) * r2) by A24,A34,A35,Th11
.= ((((r2 * s2) * r1)/gcd(r2,s2,Amp)) * s2) +
((((r2 * s2) * s1)/gcd(r2,s2,Amp)) * r2) by A24,A34,A36,Th11
.= ((((r2 * s2) * r1) * s2)/gcd(r2,s2,Amp)) +
((((r2 * s2) * s1)/gcd(r2,s2,Amp)) * r2) by A24,A35,A37,Th11
.= (((r1 * (s2 * r2)) * s2)/gcd(r2,s2,Amp)) +
((((r2 * s2) * s1) * r2)/gcd(r2,s2,Amp)) by A24,A36,A38,Th11
.= ((((r1 * s2) * r2) * s2)/gcd(r2,s2,Amp)) +
((((r2 * s2) * s1) * r2)/gcd(r2,s2,Amp)) by VECTSP_1:def 16
.= ((((r1 * s2) * r2) * s2)/gcd(r2,s2,Amp)) +
((s1 * ((r2 * s2) * r2))/gcd(r2,s2,Amp)) by VECTSP_1:def 16
.= ((((r1 * s2) * r2) * s2)/gcd(r2,s2,Amp)) +
((s1 * ((r2 * r2) * s2))/gcd(r2,s2,Amp)) by VECTSP_1:def 16
.= ((((r1 * s2) * r2) * s2)/gcd(r2,s2,Amp)) +
(((s1 * (r2 * r2)) * s2)/gcd(r2,s2,Amp)) by VECTSP_1:def 16
.= ((((r1 * s2) * r2) * s2)/gcd(r2,s2,Amp)) +
((((s1 * r2) * r2) * s2)/gcd(r2,s2,Amp)) by VECTSP_1:def 16;
A40: gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))),
gcd(r2,s2,Amp),Amp)
<> 0.R by A24,Th34;
A41: 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 A42: 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;
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 A26,Th2;
then A43: 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 A44: 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;
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 A22,A40,A41,A42,Th11
.= add2(r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2)) by A23,A33,A39,A40,
A43,A44,Th11;
hence thesis;
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 = 1_ R & s2 = 1_ R) implies
for z being Element of R
holds z = 0.R iff z = r1 * s1
proof
assume A2: (r1 = 0.R or s1 = 0.R) &
(r2 = 1_ R & s2 = 1_ R);
now per cases by A2;
case r1 = 0.R;
hence thesis by VECTSP_1:39;
case s1 = 0.R;
hence thesis by VECTSP_1:39;
end;
hence thesis;
end;
A3: ((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
assume A4: (r1 = 0.R or s1 = 0.R) &
s2 <> 0.R & r2 = 1_ R;
let z be Element of R;
A5: r1 * s1 = 0.R
proof
now per cases by A4;
case r1 = 0.R;
hence thesis by VECTSP_1:39;
case s1 = 0.R;
hence thesis by VECTSP_1:39;
end;
hence thesis;
end;
gcd(r1,s2,Amp) divides r1 by Def12;
then A6: gcd(r1,s2,Amp) divides r1 * s1 by Th7;
A7: gcd(r1,s2,Amp) <> 0.R by A4,Th34;
set d = (r1 * s1)/gcd(r1,s2,Amp);
d * gcd(r1,s2,Amp) = 0.R by A5,A6,A7,Def4;
hence thesis by A7,VECTSP_2:def 5;
end;
A8: ((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
assume A9: (r1 = 0.R or s1 = 0.R) &
r2 <> 0.R & s2 = 1_ R;
let z be Element of R;
A10: r1 * s1 = 0.R
proof
now per cases by A9;
case r1 = 0.R;
hence thesis by VECTSP_1:39;
case s1 = 0.R;
hence thesis by VECTSP_1:39;
end;
hence thesis;
end;
gcd(s1,r2,Amp) divides s1 by Def12;
then A11: gcd(s1,r2,Amp) divides r1 * s1 by Th7;
A12: gcd(s1,r2,Amp) <> 0.R by A9,Th34;
set d = (r1 * s1)/gcd(s1,r2,Amp);
d * gcd(s1,r2,Amp) = 0.R by A10,A11,A12,Def4;
hence thesis by A12,VECTSP_2:def 5;
end;
A13: ((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 r2 = 1_ R & s2 = 1_ R &
s2 <> 0.R & r2 = 1_ R;
then gcd(r1,s2,Amp) = 1_ R by Th33;
hence thesis by Th10;
end;
A14: ((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 r2 = 1_ R & s2 = 1_ R &
r2 <> 0.R & s2 = 1_ R;
then gcd(s1,r2,Amp) = 1_ R by Th33;
hence thesis by Th10;
end;
((s2 <> 0.R & r2 = 1_ R) & (r2 <> 0.R & s2 = 1_ R))
implies for z being Element of R
holds z = (r1 * s1)/gcd(r1,s2,Amp) iff
z = (r1 * s1)/gcd(s1,r2,Amp)
proof
assume A15: s2 <> 0.R & r2 = 1_ R &
r2 <> 0.R & s2 = 1_ R;
then gcd(s1,r2,Amp) = 1_ R by Th33;
hence thesis by A15,Th33;
end;
hence thesis by A1,A3,A8,A13,A14;
end;
end;
definition
let R be gcdDomain;
let Amp be AmpleSet of R;
let r1,r2,s1,s2 be Element of R;
assume A1: r1,r2 are_co-prime & s1,s2 are_co-prime &
r2 = NF(r2,Amp) & 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
A2: gcd(r1,r2,Amp) = 1_ R & gcd(s1,s2,Amp) = 1_ R by A1,Th44;
A3: (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 A4: (r1 = 0.R or s1 = 0.R) &
s2 <> 0.R & r2 = 1_ R;
now per cases by A4;
case r1 = 0.R;
then gcd(r1,s2,Amp) = s2 by A1,Th31;
hence thesis by A4,Th9;
case s1 = 0.R;
then A5: 1_ R = s2 by A1,A2,Th31;
then A6: gcd(r1,s2,Amp) = 1_ R by Th33;
1_ R <> 0.R by VECTSP_1:def 21;
hence thesis by A5,A6,Th9;
end;
hence thesis;
end;
A7: (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 A8: (r1 = 0.R or s1 = 0.R) &
r2 <> 0.R & s2 = 1_ R;
now per cases by A8;
case s1 = 0.R;
then gcd(s1,r2,Amp) = r2 by A1,Th31;
hence thesis by A8,Th9;
case r1 = 0.R;
then A9: 1_ R = r2 by A1,A2,Th31;
then A10: gcd(s1,r2,Amp) = 1_ R by Th33;
1_ R <> 0.R by VECTSP_1:def 21;
hence thesis by A9,A10,Th9;
end;
hence thesis;
end;
A11: (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 A12: r2 = 1_ R & s2 = 1_ R &
s2 <> 0.R & r2 = 1_ R;
then gcd(r1,s2,Amp) = 1_ R by Th33;
hence thesis by A12,Th9;
end;
A13: (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 A14: r2 = 1_ R & s2 = 1_ R &
r2 <> 0.R & s2 = 1_ R;
then gcd(s1,r2,Amp) = 1_ R by Th33;
hence thesis by A14,Th9;
end;
(s2 <> 0.R & r2 = 1_ R) & (r2 <> 0.R & s2 = 1_ R)
implies for z being Element of R
holds z = s2/gcd(r1,s2,Amp) iff z = r2/gcd(s1,r2,Amp)
proof
assume A15: s2 <> 0.R & r2 = 1_ R &
r2 <> 0.R & s2 = 1_ R;
then gcd(r1,s2,Amp) = 1_ R by Th33;
hence thesis by A15,Th33;
end;
hence thesis by A3,A7,A11,A13;
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 A1: Amp is multiplicative &
r1,r2 are_normalized_wrt Amp &
s1,s2 are_normalized_wrt Amp;
then A2: gcd(r1,r2,Amp) = 1_ R & gcd(s1,s2,Amp) = 1_ R &
s2 in Amp & r2 in Amp by Def15;
then A3: r1,r2 are_co-prime & s1,s2 are_co-prime &
r2 <> 0.R & s2 <> 0.R &
r2 = NF(r2,Amp) & s2 = NF(s2,Amp) by A1,Def9,Def14,Def15;
then A4: gcd(r1,s2,Amp) <> 0.R & gcd(s1,r2,Amp) <> 0.R by Th34;
now per cases;
case r1 = 0.R or s1 = 0.R;
then A5: mult2(r1,r2,s1,s2,Amp) = 1_ R by A3,Def19;
then A6: gcd(mult1(r1,r2,s1,s2,Amp),mult2(r1,r2,s1,s2,Amp),Amp)
= 1_ R by Th33;
A7: 1_ R in Amp by Th22;
1_ R <> 0.R by VECTSP_1:def 21;
hence thesis by A5,A6,A7,Def15;
case r2 = 1_ R & s2 = 1_ R;
then A8: mult2(r1,r2,s1,s2,Amp) = 1_ R by A3,Def19;
then A9: gcd(mult1(r1,r2,s1,s2,Amp),mult2(r1,r2,s1,s2,Amp),Amp)
= 1_ R by Th33;
A10: 1_ R in Amp by Th22;
1_ R <> 0.R by VECTSP_1:def 21;
hence thesis by A8,A9,A10,Def15;
case A11: s2 <> 0.R & r2 = 1_ R;
then A12: mult1(r1,r2,s1,s2,Amp) = (r1 * s1)/gcd(r1,s2,Amp) by Def18;
A13: mult2(r1,r2,s1,s2,Amp) = s2/gcd(r1,s2,Amp) by A3,A11,Def19;
A14: gcd(s1,r2,Amp) = 1_ R by A11,Th33;
A15: r2/gcd(s1,r2,Amp) = 1_ R
proof
1_ R <> 0.R by VECTSP_1:def 21;
hence thesis by A11,A14,Th9;
end;
A16: gcd(r1,s2,Amp) divides r1 by Def12;
then gcd(r1,s2,Amp) divides (r1 * s1) by Th7;
then A17: (r1 * s1)/gcd(r1,s2,Amp)
= (r1/gcd(r1,s2,Amp)) * s1 by A4,A16,Th11
.= (r1/gcd(r1,s2,Amp)) * (s1/gcd(s1,r2,Amp)) by A14,Th10;
s2/gcd(r1,s2,Amp)
= (s2/gcd(r1,s2,Amp)) * (r2/gcd(s1,r2,Amp)) by A15,VECTSP_1:def 13;
then A18: gcd(mult1(r1,r2,s1,s2,Amp),mult2(r1,r2,s1,s2,Amp),Amp)
= 1_ R by A2,A3,A12,A13,A17,Th42;
A19: gcd(r1,s2,Amp) divides s2 by Def12;
A20: gcd(r1,s2,Amp) <> 0.R by A3,Th34;
then A21: s2/gcd(r1,s2,Amp) <> 0.R by A3,A19,Th8;
reconsider zz = gcd(r1,s2,Amp) as Element of Amp by Def12;
reconsider s2 as Element of Amp by A1,Def15;
s2/zz in Amp by A1,A19,A20,Th27;
hence thesis by A13,A18,A21,Def15;
case A22: r2 <> 0.R & s2 = 1_ R;
then A23: mult1(r1,r2,s1,s2,Amp) = (r1 * s1)/gcd(s1,r2,Amp) by Def18;
A24: mult2(r1,r2,s1,s2,Amp) = r2/gcd(s1,r2,Amp) by A3,A22,Def19;
A25: gcd(r1,s2,Amp) = 1_ R by A22,Th33;
A26: s2/gcd(r1,s2,Amp) = 1_ R
proof
1_ R <> 0.R by VECTSP_1:def 21;
hence thesis by A22,A25,Th9;
end;
A27: gcd(s1,r2,Amp) divides s1 by Def12;
then gcd(s1,r2,Amp) divides (r1 * s1) by Th7;
then A28: (r1 * s1)/gcd(s1,r2,Amp)
= r1 * (s1/gcd(s1,r2,Amp)) by A4,A27,Th11
.= (r1/gcd(r1,s2,Amp)) * (s1/gcd(s1,r2,Amp)) by A25,Th10;
r2/gcd(s1,r2,Amp)
= (r2/gcd(s1,r2,Amp)) * (s2/gcd(r1,s2,Amp)) by A26,VECTSP_1:def 13;
then A29: gcd(mult1(r1,r2,s1,s2,Amp),mult2(r1,r2,s1,s2,Amp),Amp)
= 1_ R by A2,A3,A23,A24,A28,Th42;
A30: gcd(s1,r2,Amp) divides r2 by Def12;
A31: gcd(s1,r2,Amp) <> 0.R by A3,Th34;
then A32: r2/gcd(s1,r2,Amp) <> 0.R by A3,A30,Th8;
reconsider zz = gcd(s1,r2,Amp) as Element of Amp by Def12;
reconsider r2 as Element of Amp by A1,Def15;
r2/zz in Amp by A1,A30,A31,Th27;
hence thesis by A24,A29,A32,Def15;
case A33: 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);
then A34: mult1(r1,r2,s1,s2,Amp) = (r1/gcd(r1,s2,Amp)) * (s1/gcd(s1,r2,Amp))
by Def18;
A35: mult2(r1,r2,s1,s2,Amp) = (r2/gcd(s1,r2,Amp)) * (s2/gcd(r1,s2,Amp))
by A3,A33,Def19;
then A36: gcd(mult1(r1,r2,s1,s2,Amp),mult2(r1,r2,s1,s2,Amp),Amp)
= 1_ R by A2,A3,A34,Th42;
A37: gcd(r1,s2,Amp) divides s2 by Def12;
A38: gcd(r1,s2,Amp) <> 0.R by A3,Th34;
then A39: s2/gcd(r1,s2,Amp) <> 0.R by A3,A37,Th8;
reconsider z1 = gcd(r1,s2,Amp) as Element of Amp by Def12;
reconsider s2 as Element of Amp by A1,Def15;
A40: gcd(s1,r2,Amp) divides r2 by Def12;
A41: gcd(s1,r2,Amp) <> 0.R by A3,Th34;
then A42: r2/gcd(s1,r2,Amp) <> 0.R by A3,A40,Th8;
reconsider z2 = gcd(s1,r2,Amp) as Element of Amp by Def12;
reconsider r2 as Element of Amp by A1,Def15;
reconsider u = s2/z1 as Element of Amp by A1,A37,A38,Th27;
reconsider v = r2/z2 as Element of Amp by A1,A40,A41,Th27;
A43: v * u in Amp by A1,Def10;
v * u <> 0.R by A39,A42,VECTSP_2:def 5;
hence thesis by A35,A36,A43,Def15;
end;
hence thesis;
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) * (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 A1: Amp is multiplicative &
r1,r2 are_normalized_wrt Amp &
s1,s2 are_normalized_wrt Amp;
then gcd(r1,r2,Amp) = 1_ R & gcd(s1,s2,Amp) = 1_ R &
s2 in Amp & r2 in Amp by Def15;
then A2: r1,r2 are_co-prime & s1,s2 are_co-prime &
r2 <> 0.R & s2 <> 0.R &
r2 = NF(r2,Amp) & s2 = NF(s2,Amp) by A1,Def9,Def14,Def15;
then A3: gcd(r1,s2,Amp) <> 0.R & gcd(s1,r2,Amp) <> 0.R by Th34;
now per cases;
case A4: r1 = 0.R or s1 = 0.R;
then A5: mult1(r1,r2,s1,s2,Amp) = 0.R by Def18;
now per cases by A4;
case r1 = 0.R;
then mult2(r1,r2,s1,s2,Amp) * (r1 * s1)
= mult2(r1,r2,s1,s2,Amp) * 0.R by VECTSP_1:39
.= 0.R by VECTSP_1:39;
hence thesis by A5,VECTSP_1:39;
case s1 = 0.R;
then mult2(r1,r2,s1,s2,Amp) * (r1 * s1)
= mult2(r1,r2,s1,s2,Amp) * 0.R by VECTSP_1:39
.= 0.R by VECTSP_1:39;
hence thesis by A5,VECTSP_1:39;
end;
hence thesis;
case A6: r2 = 1_ R & s2 = 1_ R;
then A7: mult1(r1,r2,s1,s2,Amp) = r1 * s1 by Def18;
mult2(r1,r2,s1,s2,Amp) = 1_ R by A2,A6,Def19;
hence thesis by A6,A7,VECTSP_1:def 13;
case A8: s2 <> 0.R & r2 = 1_ R;
then A9: mult2(r1,r2,s1,s2,Amp) = s2/gcd(r1,s2,Amp) by A2,Def19;
gcd(r1,s2,Amp) divides r1 by Def12;
then A10: gcd(r1,s2,Amp) divides (r1 * s1) by Th7;
then A11: gcd(r1,s2,Amp) divides (r1 * s1) * s2 by Th7;
A12: ((r1 * s1)/gcd(r1,s2,Amp)) * (r2 * s2)
= ((r1 * s1)/gcd(r1,s2,Amp)) * s2 by A8,VECTSP_1:def 19
.= ((r1 * s1) * s2)/gcd(r1,s2,Amp) by A3,A10,A11,Th11;
A13: gcd(r1,s2,Amp) divides s2 by Def12;
then A14: gcd(r1,s2,Amp) divides s2 * r1 by Th7;
then A15: 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 VECTSP_1:def 16
.= ((s2 * r1)/gcd(r1,s2,Amp)) * s1 by A3,A13,A14,Th11
.= ((s2 * r1) * s1)/gcd(r1,s2,Amp) by A3,A14,A15,Th11
.= ((r1 * s1) * s2)/gcd(r1,s2,Amp) by VECTSP_1:def 16;
hence thesis by A8,A9,A12,Def18;
case A16: r2 <> 0.R & s2 = 1_ R;
then A17: mult2(r1,r2,s1,s2,Amp) = r2/gcd(s1,r2,Amp) by A2,Def19;
gcd(s1,r2,Amp) divides s1 by Def12;
then A18: gcd(s1,r2,Amp) divides (s1 * r1) by Th7;
then A19: gcd(s1,r2,Amp) divides (s1 * r1) * r2 by Th7;
A20: ((r1 * s1)/gcd(s1,r2,Amp)) * (r2 * s2)
= ((r1 * s1)/gcd(s1,r2,Amp)) * r2 by A16,VECTSP_1:def 13
.= ((r1 * s1) * r2)/gcd(s1,r2,Amp) by A3,A18,A19,Th11;
A21: gcd(s1,r2,Amp) divides r2 by Def12;
then A22: gcd(s1,r2,Amp) divides r2 * r1 by Th7;
then A23: 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 VECTSP_1:def 16
.= ((r2 * r1)/gcd(s1,r2,Amp)) * s1 by A3,A21,A22,Th11
.= ((r2 * r1) * s1)/gcd(s1,r2,Amp) by A3,A22,A23,Th11
.= ((r1 * s1) * r2)/gcd(s1,r2,Amp) by VECTSP_1:def 16;
hence thesis by A16,A17,A20,Def18;
case A24: 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);
then A25: mult2(r1,r2,s1,s2,Amp) =
(r2/gcd(s1,r2,Amp)) * (s2/gcd(r1,s2,Amp)) by A2,Def19;
A26: gcd(r1,s2,Amp) divides r1 by Def12;
A27: gcd(s1,r2,Amp) divides s1 by Def12;
then A28: (gcd(r1,s2,Amp) *gcd(s1,r2,Amp)) divides r1 * s1
by A26,Th3;
then A29: (gcd(r1,s2,Amp) * gcd(s1,r2,Amp)) divides (r1 * s1) * r2
by Th7;
then A30: (gcd(r1,s2,Amp) * gcd(s1,r2,Amp)) divides ((r1 * s1) * r2) * s2
by Th7;
A31: (gcd(r1,s2,Amp) * gcd(s1,r2,Amp)) <> 0.R by A3,VECTSP_2:def 5;
A32: ((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 A3,A26,A27,Th14
.= (((r1 * s1)/(gcd(r1,s2,Amp) * gcd(s1,r2,Amp))) * r2) * s2
by VECTSP_1:def 16
.= (((r1 * s1) * r2)/(gcd(r1,s2,Amp) * gcd(s1,r2,Amp))) * s2
by A28,A29,A31,Th11
.= (((r1 * s1) * r2) * s2)/(gcd(r1,s2,Amp) * gcd(s1,r2,Amp))
by A29,A30,A31,Th11;
A33: gcd(s1,r2,Amp) divides r2 by Def12;
A34: gcd(r1,s2,Amp) divides s2 by Def12;
then A35: (gcd(s1,r2,Amp) * gcd(r1,s2,Amp)) divides r2 * s2
by A33,Th3;
then A36: (gcd(s1,r2,Amp) * gcd(r1,s2,Amp)) divides (r2 * s2) * r1
by Th7;
then A37: (gcd(s1,r2,Amp) * gcd(r1,s2,Amp)) divides ((r2 * s2) * r1) * s1
by Th7;
((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 A3,A33,A34,Th14
.= (((r2 * s2)/(gcd(s1,r2,Amp) * gcd(r1,s2,Amp))) * r1) * s1
by VECTSP_1:def 16
.= (((r2 * s2) * r1)/(gcd(s1,r2,Amp) * gcd(r1,s2,Amp))) * s1
by A31,A35,A36,Th11
.= (((r2 * s2) * r1) * s1)/(gcd(s1,r2,Amp) * gcd(r1,s2,Amp))
by A31,A36,A37,Th11
.= (r1 * ((r2 * s2) * s1))/(gcd(s1,r2,Amp) * gcd(r1,s2,Amp))
by VECTSP_1:def 16
.= (r1 * ((s1 * r2) * s2))/(gcd(s1,r2,Amp) * gcd(r1,s2,Amp))
by VECTSP_1:def 16
.= ((r1 * (s1 * r2)) * s2)/(gcd(s1,r2,Amp) * gcd(r1,s2,Amp))
by VECTSP_1:def 16
.= (((r1 * s1) * r2) * s2)/(gcd(s1,r2,Amp) * gcd(r1,s2,Amp))
by VECTSP_1:def 16;
hence thesis by A24,A25,A32,Def18;
end;
hence thesis;
end;
canceled 2;
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:40,41;
canceled;
theorem
for F being Field-like 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 Field-like commutative Ring;
let a,b be Element of F such that
A1: a <> 0.F and
A2: b <> 0.F;
A3: b*a <> 0.F by A1,A2,VECTSP_1:44;
b*a * (a"*b") = b*a*a"*b" by VECTSP_1:def 16
.= b*(a*a")*b" by VECTSP_1:def 16
.= b*1_ F*b" by A1,VECTSP_1:def 22
.= b*b" by VECTSP_1:def 13
.= 1_ F by A2,VECTSP_1:def 22;
hence thesis by A3,VECTSP_1:def 22;
end;