let R be gcdDomain; :: thesis: for Amp being AmpleSet of R
for r1, r2, s1, s2 being Element of R st Amp is multiplicative & r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp holds
mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp
let Amp be AmpleSet of R; :: thesis: for r1, r2, s1, s2 being Element of R st Amp is multiplicative & r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp holds
mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp
let r1, r2, s1, s2 be Element of R; :: thesis: ( 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 )
assume that
A1: Amp is multiplicative and
A2: r1,r2 are_normalized_wrt Amp and
A3: s1,s2 are_normalized_wrt Amp ; :: thesis: mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) 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 :: thesis: ( ( ( r1 = 0. R or s1 = 0. R ) & mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp ) or ( r2 = 1. R & s2 = 1. R & mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp ) or ( s2 <> 0. R & r2 = 1. R & mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp ) or ( r2 <> 0. R & s2 = 1. R & mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp ) or ( not r1 = 0. R & not s1 = 0. R & ( not r2 = 1. R or not s2 = 1. R ) & ( not s2 <> 0. R or not r2 = 1. R ) & ( not r2 <> 0. R or not s2 = 1. R ) & mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp ) )
per cases ( r1 = 0. R or s1 = 0. R or ( r2 = 1. R & s2 = 1. R ) or ( s2 <> 0. R & r2 = 1. R ) or ( r2 <> 0. R & s2 = 1. R ) or ( not r1 = 0. R & not s1 = 0. R & ( not r2 = 1. R or not s2 = 1. R ) & ( not s2 <> 0. R or not r2 = 1. R ) & ( not r2 <> 0. R or not s2 = 1. R ) ) ) ;
case A14: ( r1 = 0. R or s1 = 0. R ) ; :: thesis: mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp
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 mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp by A16, A15; :: thesis: verum
end;
case A17: ( r2 = 1. R & s2 = 1. R ) ; :: thesis: mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp
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 mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp by A19, A18; :: thesis: verum
end;
case A20: ( s2 <> 0. R & r2 = 1. R ) ; :: thesis: mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp
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 = s2 as Element of Amp by A3;
s2 / zz in Amp by A1, A26, Th27;
hence mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp by A25, A28, A27; :: thesis: verum
end;
case A29: ( r2 <> 0. R & s2 = 1. R ) ; :: thesis: mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp
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 = r2 as Element of Amp by A2;
r2 / zz in Amp by A1, A35, Th27;
hence mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp by A34, A37, A36; :: thesis: verum
end;
case A38: ( not r1 = 0. R & not s1 = 0. R & ( not r2 = 1. R or not s2 = 1. R ) & ( not s2 <> 0. R or not r2 = 1. R ) & ( not r2 <> 0. R or not s2 = 1. R ) ) ; :: thesis: mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp
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 = s2 as Element of Amp by A3;
reconsider u = s2 / z1 as Element of Amp by A1, A39, Th27;
reconsider r2 = 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 mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp by A41, A42, A45; :: thesis: verum
end;
end;
end;
hence mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp ; :: thesis: verum