let R be gcdDomain; :: thesis: for Amp being AmpleSet of R
for r1, r2, s1, s2 being Element of R st r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp holds
(mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1)
let Amp be AmpleSet of R; :: thesis: for r1, r2, s1, s2 being Element of R st r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp holds
(mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1)
let r1, r2, s1, s2 be Element of R; :: thesis: ( 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) )
assume that
A1: r1,r2 are_normalized_wrt Amp and
A2: s1,s2 are_normalized_wrt Amp ; :: thesis: (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1)
gcd (r1,r2,Amp) = 1. R by A1;
then A3: r1,r2 are_co-prime ;
s2 <> 0. R by A2;
then A4: gcd (r1,s2,Amp) <> 0. R by Th33;
r2 in Amp by A1;
then A5: r2 = NF (r2,Amp) by Def9;
gcd (s1,s2,Amp) = 1. R by A2;
then A6: s1,s2 are_co-prime ;
r2 <> 0. R by A1;
then A7: gcd (s1,r2,Amp) <> 0. R by Th33;
s2 in Amp by A2;
then A8: s2 = NF (s2,Amp) by Def9;
now :: thesis: ( ( ( r1 = 0. R or s1 = 0. R ) & (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1) ) or ( r2 = 1. R & s2 = 1. R & (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1) ) or ( s2 <> 0. R & r2 = 1. R & (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1) ) or ( r2 <> 0. R & s2 = 1. R & (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1) ) 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)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1) ) )
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 A9: ( r1 = 0. R or s1 = 0. R ) ; :: thesis: (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1)
then A10: mult1 (r1,r2,s1,s2,Amp) = 0. R by Def18;
now :: thesis: ( ( r1 = 0. R & (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1) ) or ( s1 = 0. R & (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1) ) )
per cases ( r1 = 0. R or s1 = 0. R ) by A9;
case r1 = 0. R ; :: thesis: (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1)
then (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1) = (mult2 (r1,r2,s1,s2,Amp)) * (0. R)
.= 0. R ;
hence (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1) by A10; :: thesis: verum
end;
case s1 = 0. R ; :: thesis: (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1)
then (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1) = (mult2 (r1,r2,s1,s2,Amp)) * (0. R)
.= 0. R ;
hence (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1) by A10; :: thesis: verum
end;
end;
end;
hence (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1) ; :: thesis: verum
end;
case A11: ( r2 = 1. R & s2 = 1. R ) ; :: thesis: (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1)
then ( mult1 (r1,r2,s1,s2,Amp) = r1 * s1 & mult2 (r1,r2,s1,s2,Amp) = 1. R ) by A3, A6, A5, Def18, Def19;
hence (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1) by A11; :: thesis: verum
end;
case A12: ( s2 <> 0. R & r2 = 1. R ) ; :: thesis: (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1)
gcd (r1,s2,Amp) divides r1 by Def12;
then A13: gcd (r1,s2,Amp) divides r1 * s1 by Th7;
then A14: gcd (r1,s2,Amp) divides (r1 * s1) * s2 by Th7;
A15: ((r1 * s1) / (gcd (r1,s2,Amp))) * (r2 * s2) = ((r1 * s1) / (gcd (r1,s2,Amp))) * s2 by A12
.= ((r1 * s1) * s2) / (gcd (r1,s2,Amp)) by A4, A13, A14, Th11 ;
A16: mult2 (r1,r2,s1,s2,Amp) = s2 / (gcd (r1,s2,Amp)) by A3, A6, A5, A8, A12, Def19;
A17: gcd (r1,s2,Amp) divides s2 by Def12;
then A18: gcd (r1,s2,Amp) divides s2 * r1 by Th7;
then A19: gcd (r1,s2,Amp) divides (s2 * r1) * s1 by Th7;
(s2 / (gcd (r1,s2,Amp))) * (r1 * s1) = ((s2 / (gcd (r1,s2,Amp))) * r1) * s1 by GROUP_1:def 3
.= ((s2 * r1) / (gcd (r1,s2,Amp))) * s1 by A4, A17, A18, Th11
.= ((s2 * r1) * s1) / (gcd (r1,s2,Amp)) by A4, A18, A19, Th11
.= ((r1 * s1) * s2) / (gcd (r1,s2,Amp)) by GROUP_1:def 3 ;
hence (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1) by A12, A16, A15, Def18; :: thesis: verum
end;
case A20: ( r2 <> 0. R & s2 = 1. R ) ; :: thesis: (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1)
gcd (s1,r2,Amp) divides s1 by Def12;
then A21: gcd (s1,r2,Amp) divides s1 * r1 by Th7;
then A22: gcd (s1,r2,Amp) divides (s1 * r1) * r2 by Th7;
A23: ((r1 * s1) / (gcd (s1,r2,Amp))) * (r2 * s2) = ((r1 * s1) / (gcd (s1,r2,Amp))) * r2 by A20
.= ((r1 * s1) * r2) / (gcd (s1,r2,Amp)) by A7, A21, A22, Th11 ;
A24: mult2 (r1,r2,s1,s2,Amp) = r2 / (gcd (s1,r2,Amp)) by A3, A6, A5, A8, A20, Def19;
A25: gcd (s1,r2,Amp) divides r2 by Def12;
then A26: gcd (s1,r2,Amp) divides r2 * r1 by Th7;
then A27: gcd (s1,r2,Amp) divides (r2 * r1) * s1 by Th7;
(r2 / (gcd (s1,r2,Amp))) * (r1 * s1) = ((r2 / (gcd (s1,r2,Amp))) * r1) * s1 by GROUP_1:def 3
.= ((r2 * r1) / (gcd (s1,r2,Amp))) * s1 by A7, A25, A26, Th11
.= ((r2 * r1) * s1) / (gcd (s1,r2,Amp)) by A7, A26, A27, Th11
.= ((r1 * s1) * r2) / (gcd (s1,r2,Amp)) by GROUP_1:def 3 ;
hence (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1) by A20, A24, A23, Def18; :: thesis: verum
end;
case A28: ( 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)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1)
A29: ( gcd (s1,r2,Amp) divides r2 & gcd (r1,s2,Amp) divides s2 ) by Def12;
then A30: (gcd (s1,r2,Amp)) * (gcd (r1,s2,Amp)) divides r2 * s2 by Th3;
then A31: (gcd (s1,r2,Amp)) * (gcd (r1,s2,Amp)) divides (r2 * s2) * r1 by Th7;
then A32: (gcd (s1,r2,Amp)) * (gcd (r1,s2,Amp)) divides ((r2 * s2) * r1) * s1 by Th7;
A33: ( gcd (r1,s2,Amp) divides r1 & gcd (s1,r2,Amp) divides s1 ) by Def12;
then A34: (gcd (r1,s2,Amp)) * (gcd (s1,r2,Amp)) divides r1 * s1 by Th3;
then A35: (gcd (r1,s2,Amp)) * (gcd (s1,r2,Amp)) divides (r1 * s1) * r2 by Th7;
then A36: (gcd (r1,s2,Amp)) * (gcd (s1,r2,Amp)) divides ((r1 * s1) * r2) * s2 by Th7;
A37: mult2 (r1,r2,s1,s2,Amp) = (r2 / (gcd (s1,r2,Amp))) * (s2 / (gcd (r1,s2,Amp))) by A3, A6, A5, A8, A28, Def19;
A38: (gcd (r1,s2,Amp)) * (gcd (s1,r2,Amp)) <> 0. R by A4, A7, VECTSP_2:def 1;
A39: ((r2 / (gcd (s1,r2,Amp))) * (s2 / (gcd (r1,s2,Amp)))) * (r1 * s1) = ((r2 * s2) / ((gcd (s1,r2,Amp)) * (gcd (r1,s2,Amp)))) * (r1 * s1) by A4, A7, A29, Th14
.= (((r2 * s2) / ((gcd (s1,r2,Amp)) * (gcd (r1,s2,Amp)))) * r1) * s1 by GROUP_1:def 3
.= (((r2 * s2) * r1) / ((gcd (s1,r2,Amp)) * (gcd (r1,s2,Amp)))) * s1 by A38, A30, A31, Th11
.= (((r2 * s2) * r1) * s1) / ((gcd (s1,r2,Amp)) * (gcd (r1,s2,Amp))) by A38, A31, A32, Th11
.= (r1 * ((r2 * s2) * s1)) / ((gcd (s1,r2,Amp)) * (gcd (r1,s2,Amp))) by GROUP_1:def 3
.= (r1 * ((s1 * r2) * s2)) / ((gcd (s1,r2,Amp)) * (gcd (r1,s2,Amp))) by GROUP_1:def 3
.= ((r1 * (s1 * r2)) * s2) / ((gcd (s1,r2,Amp)) * (gcd (r1,s2,Amp))) by GROUP_1:def 3
.= (((r1 * s1) * r2) * s2) / ((gcd (s1,r2,Amp)) * (gcd (r1,s2,Amp))) by GROUP_1:def 3 ;
((r1 / (gcd (r1,s2,Amp))) * (s1 / (gcd (s1,r2,Amp)))) * (r2 * s2) = ((r1 * s1) / ((gcd (r1,s2,Amp)) * (gcd (s1,r2,Amp)))) * (r2 * s2) by A4, A7, A33, Th14
.= (((r1 * s1) / ((gcd (r1,s2,Amp)) * (gcd (s1,r2,Amp)))) * r2) * s2 by GROUP_1:def 3
.= (((r1 * s1) * r2) / ((gcd (r1,s2,Amp)) * (gcd (s1,r2,Amp)))) * s2 by A34, A35, A38, Th11
.= (((r1 * s1) * r2) * s2) / ((gcd (r1,s2,Amp)) * (gcd (s1,r2,Amp))) by A35, A36, A38, Th11 ;
hence (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1) by A28, A37, A39, Def18; :: thesis: verum
end;
end;
end;
hence (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1) ; :: thesis: verum