let n, k be Nat; :: thesis: for p being INT -valued Polynomial of n,F_Real
for x, y being n -element XFinSequence of NAT st k <> 0 & ( for i being Nat st i in n holds
k divides (x . i) - (y . i) ) holds
k divides (eval (p,(@ x))) - (eval (p,(@ y)))
let p be INT -valued Polynomial of n,F_Real; :: thesis: for x, y being n -element XFinSequence of NAT st k <> 0 & ( for i being Nat st i in n holds
k divides (x . i) - (y . i) ) holds
k divides (eval (p,(@ x))) - (eval (p,(@ y)))
let x, y be n -element XFinSequence of NAT ; :: thesis: ( k <> 0 & ( for i being Nat st i in n holds
k divides (x . i) - (y . i) ) implies k divides (eval (p,(@ x))) - (eval (p,(@ y))) )
assume that
A1: k <> 0 and
A2: for i being Nat st i in n holds
k divides (x . i) - (y . i) ; :: thesis: k divides (eval (p,(@ x))) - (eval (p,(@ y)))
reconsider FR = F_Real as Field ;
reconsider pF = p as Polynomial of n,FR ;
reconsider xF = @ x, yF = @ y as Function of n, the carrier of FR ;
set sgmF = SgmX ((BagOrder n),(Support pF));
set sgm = SgmX ((BagOrder n),(Support p));
consider X being FinSequence of the carrier of FR such that
A3: ( len X = len (SgmX ((BagOrder n),(Support pF))) & eval (pF,xF) = Sum X ) and
A4: for i being Element of NAT st 1 <= i & i <= len X holds
X /. i = ((pF * (SgmX ((BagOrder n),(Support pF)))) /. i) * (eval (((SgmX ((BagOrder n),(Support pF))) /. i),xF)) by POLYNOM2:def 4;
consider Y being FinSequence of the carrier of FR such that
A5: ( len Y = len (SgmX ((BagOrder n),(Support pF))) & eval (pF,yF) = Sum Y ) and
A6: for i being Element of NAT st 1 <= i & i <= len Y holds
Y /. i = ((pF * (SgmX ((BagOrder n),(Support pF)))) /. i) * (eval (((SgmX ((BagOrder n),(Support pF))) /. i),yF)) by POLYNOM2:def 4;
reconsider Yr = Y, Xr = X as FinSequence of REAL ;
defpred S1[ Nat] means ( $1 <= len X implies ( (Sum (Xr | $1)) - (Sum (Yr | $1)) is Integer & ( for d being Integer st d = (Sum (Xr | $1)) - (Sum (Yr | $1)) holds
k divides d ) ) );
A7: S1[ 0 ] by INT_2:12;
A8: for i being Nat st S1[i] holds
S1[i + 1]
proof
A9: len (p * (SgmX ((BagOrder n),(Support p)))) = len (SgmX ((BagOrder n),(Support p))) by CARD_1:def 7;
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A10: S1[i] ; :: thesis: S1[i + 1]
set i1 = i + 1;
set O = (pF * (SgmX ((BagOrder n),(Support pF)))) /. (i + 1);
set O1 = eval (((SgmX ((BagOrder n),(Support pF))) /. (i + 1)),xF);
set O2 = eval (((SgmX ((BagOrder n),(Support pF))) /. (i + 1)),yF);
( @ x is INT -valued & @ y is INT -valued ) by HILB10_2:def 1;
then reconsider o1 = eval (((SgmX ((BagOrder n),(Support pF))) /. (i + 1)),xF), o2 = eval (((SgmX ((BagOrder n),(Support pF))) /. (i + 1)),yF) as Integer ;
assume A11: i + 1 <= len X ; :: thesis: ( (Sum (Xr | (i + 1))) - (Sum (Yr | (i + 1))) is Integer & ( for d being Integer st d = (Sum (Xr | (i + 1))) - (Sum (Yr | (i + 1))) holds
k divides d ) )
then reconsider S = (Sum (Xr | i)) - (Sum (Yr | i)) as Integer by A10, NAT_1:13;
A12: i + 1 in dom X by A11, NAT_1:11, FINSEQ_3:25;
then A13: ( X | (i + 1) = (X | i) ^ <*(X . (i + 1))*> & X . (i + 1) = X /. (i + 1) & Xr . (i + 1) = Xr /. (i + 1) ) by FINSEQ_5:10, PARTFUN1:def 6;
A14: Sum (X | i) = Sum (Xr | i) by MATRPROB:36;
dom (pF * (SgmX ((BagOrder n),(Support pF)))) = dom X by A3, A9, FINSEQ_3:29;
then (pF * (SgmX ((BagOrder n),(Support pF)))) . (i + 1) = (pF * (SgmX ((BagOrder n),(Support pF)))) /. (i + 1) by A12, PARTFUN1:def 6;
then reconsider o = (pF * (SgmX ((BagOrder n),(Support pF)))) /. (i + 1) as Integer ;
A15: Sum (Xr | (i + 1)) = Sum (X | (i + 1)) by MATRPROB:36
.= (Sum (X | i)) + (Sum <*(X /. (i + 1))*>) by A13, RLVECT_1:41
.= addreal . ((Sum (X | i)),(X /. (i + 1))) by RLVECT_1:44
.= (Sum (Xr | i)) + (Xr /. (i + 1)) by A14, BINOP_2:def 9 ;
i + 1 in dom Y by A11, NAT_1:11, FINSEQ_3:25, A3, A5;
then A16: ( Y | (i + 1) = (Y | i) ^ <*(Y . (i + 1))*> & Y . (i + 1) = Y /. (i + 1) & Yr . (i + 1) = Yr /. (i + 1) ) by FINSEQ_5:10, PARTFUN1:def 6;
A17: Sum (Y | i) = Sum (Yr | i) by MATRPROB:36;
A18: Sum (Yr | (i + 1)) = Sum (Y | (i + 1)) by MATRPROB:36
.= (Sum (Y | i)) + (Sum <*(Y /. (i + 1))*>) by A16, RLVECT_1:41
.= addreal . ((Sum (Y | i)),(Y /. (i + 1))) by RLVECT_1:44
.= (Sum (Yr | i)) + (Yr /. (i + 1)) by A17, BINOP_2:def 9 ;
A19: Yr /. (i + 1) = ((pF * (SgmX ((BagOrder n),(Support pF)))) /. (i + 1)) * (eval (((SgmX ((BagOrder n),(Support pF))) /. (i + 1)),yF)) by A3, A5, A6, A11, NAT_1:11;
reconsider OO1 = ((pF * (SgmX ((BagOrder n),(Support pF)))) /. (i + 1)) * (eval (((SgmX ((BagOrder n),(Support pF))) /. (i + 1)),xF)), OO2 = ((pF * (SgmX ((BagOrder n),(Support pF)))) /. (i + 1)) * (eval (((SgmX ((BagOrder n),(Support pF))) /. (i + 1)),yF)), PS = (p * (SgmX ((BagOrder n),(Support p)))) /. (i + 1) as Element of F_Real ;
A20: (Xr /. (i + 1)) - (Yr /. (i + 1)) = OO1 - OO2 by A4, A11, NAT_1:11, A19
.= PS * ((eval (((SgmX ((BagOrder n),(Support pF))) /. (i + 1)),(@ x))) - (eval (((SgmX ((BagOrder n),(Support pF))) /. (i + 1)),(@ y)))) by VECTSP_1:11
.= o * (o1 - o2) ;
k divides o1 - o2
proof
set b = (SgmX ((BagOrder n),(Support pF))) /. (i + 1);
set SG = SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1))));
consider H1 being FinSequence of FR such that
A21: ( len H1 = len (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1))))) & eval (((SgmX ((BagOrder n),(Support pF))) /. (i + 1)),xF) = Product H1 ) and
A22: for i being Element of NAT st 1 <= i & i <= len H1 holds
H1 /. i = (power FR) . (((xF * (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1)))))) /. i),((((SgmX ((BagOrder n),(Support pF))) /. (i + 1)) * (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1)))))) /. i)) by POLYNOM2:def 2;
consider H2 being FinSequence of FR such that
A23: ( len H2 = len (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1))))) & eval (((SgmX ((BagOrder n),(Support pF))) /. (i + 1)),yF) = Product H2 ) and
A24: for i being Element of NAT st 1 <= i & i <= len H2 holds
H2 /. i = (power FR) . (((yF * (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1)))))) /. i),((((SgmX ((BagOrder n),(Support pF))) /. (i + 1)) * (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1)))))) /. i)) by POLYNOM2:def 2;
defpred S2[ Nat] means ( $1 <= len (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1))))) implies ( Product (H1 | $1) is integer & Product (H2 | $1) is integer & ( for i1, i2 being Integer st i1 = Product (H1 | $1) & i2 = Product (H2 | $1) holds
k divides i1 - i2 ) ) );
reconsider ZERO = 0 as Nat ;
A25: S2[ 0 ]
proof
assume 0 <= len (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1))))) ; :: thesis: ( Product (H1 | 0) is integer & Product (H2 | 0) is integer & ( for i1, i2 being Integer st i1 = Product (H1 | 0) & i2 = Product (H2 | 0) holds
k divides i1 - i2 ) )
H2 | ZERO = <*> the carrier of F_Real ;
then Product (H2 | ZERO) = 1_ F_Real by GROUP_4:8
.= 1 ;
hence ( Product (H1 | 0) is integer & Product (H2 | 0) is integer & ( for i1, i2 being Integer st i1 = Product (H1 | 0) & i2 = Product (H2 | 0) holds
k divides i1 - i2 ) ) by INT_2:12; :: thesis: verum
end;
A26: for i being Nat st S2[i] holds
S2[i + 1]
proof
let i be Nat; :: thesis: ( S2[i] implies S2[i + 1] )
assume A27: S2[i] ; :: thesis: S2[i + 1]
set i1 = i + 1;
set B = (((SgmX ((BagOrder n),(Support pF))) /. (i + 1)) * (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1)))))) /. (i + 1);
assume A28: i + 1 <= len (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1))))) ; :: thesis: ( Product (H1 | (i + 1)) is integer & Product (H2 | (i + 1)) is integer & ( for i1, i2 being Integer st i1 = Product (H1 | (i + 1)) & i2 = Product (H2 | (i + 1)) holds
k divides i1 - i2 ) )
then reconsider p1 = Product (H1 | i), p2 = Product (H2 | i) as Integer by A27, NAT_1:13;
A29: i + 1 in dom (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1))))) by NAT_1:11, A28, FINSEQ_3:25;
A30: ( len x = n & x = xF & y = yF ) by CARD_1:def 7, HILB10_2:def 1;
( rng (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1))))) c= n & n = dom xF & n = dom yF ) by PARTFUN1:def 2, RELAT_1:def 19;
then ( i + 1 in dom (xF * (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1)))))) & i + 1 in dom (yF * (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1)))))) ) by A29, RELAT_1:27;
then A31: ( (xF * (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1)))))) /. (i + 1) = (xF * (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1)))))) . (i + 1) & (xF * (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1)))))) . (i + 1) = xF . ((SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1))))) . (i + 1)) & (yF * (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1)))))) /. (i + 1) = (yF * (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1)))))) . (i + 1) & (yF * (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1)))))) . (i + 1) = yF . ((SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1))))) . (i + 1)) & (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1))))) . (i + 1) in dom xF ) by PARTFUN1:def 6, FUNCT_1:11, FUNCT_1:12;
then A32: (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1))))) . (i + 1) in dom x by HILB10_2:def 1;
set sg = (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1))))) . (i + 1);
reconsider xS = (xF * (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1)))))) /. (i + 1), yS = (yF * (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1)))))) /. (i + 1) as Integer by A31, A30;
reconsider xfSG = (xF * (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1)))))) /. (i + 1), yfSG = (yF * (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1)))))) /. (i + 1) as Element of F_Real ;
H1 /. (i + 1) = (power FR) . (((xF * (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1)))))) /. (i + 1)),((((SgmX ((BagOrder n),(Support pF))) /. (i + 1)) * (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1)))))) /. (i + 1))) by NAT_1:11, A22, A28, A21;
then A33: H1 /. (i + 1) = xS |^ ((((SgmX ((BagOrder n),(Support pF))) /. (i + 1)) * (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1)))))) /. (i + 1)) by NIVEN:7;
H2 /. (i + 1) = (power FR) . (((yF * (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1)))))) /. (i + 1)),((((SgmX ((BagOrder n),(Support pF))) /. (i + 1)) * (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1)))))) /. (i + 1))) by NAT_1:11, A28, A23, A24;
then A34: H2 /. (i + 1) = yS |^ ((((SgmX ((BagOrder n),(Support pF))) /. (i + 1)) * (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1)))))) /. (i + 1)) by NIVEN:7;
i + 1 in dom H1 by A28, NAT_1:11, FINSEQ_3:25, A21;
then ( H1 | (i + 1) = (H1 | i) ^ <*(H1 . (i + 1))*> & H1 . (i + 1) = H1 /. (i + 1) ) by FINSEQ_5:10, PARTFUN1:def 6;
then A35: Product (H1 | (i + 1)) = (Product (H1 | i)) * (H1 /. (i + 1)) by GROUP_4:6
.= p1 * (xS |^ ((((SgmX ((BagOrder n),(Support pF))) /. (i + 1)) * (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1)))))) /. (i + 1))) by A33, BINOP_2:def 11 ;
i + 1 in dom H2 by A28, NAT_1:11, FINSEQ_3:25, A23;
then ( H2 | (i + 1) = (H2 | i) ^ <*(H2 . (i + 1))*> & H2 . (i + 1) = H2 /. (i + 1) ) by FINSEQ_5:10, PARTFUN1:def 6;
then A36: Product (H2 | (i + 1)) = (Product (H2 | i)) * (H2 /. (i + 1)) by GROUP_4:6
.= p2 * (yS |^ ((((SgmX ((BagOrder n),(Support pF))) /. (i + 1)) * (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1)))))) /. (i + 1))) by A34, BINOP_2:def 11 ;
k divides (x . ((SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1))))) . (i + 1))) - (y . ((SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1))))) . (i + 1))) by A2, A31, A32;
then A37: xS |^ ((((SgmX ((BagOrder n),(Support pF))) /. (i + 1)) * (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1)))))) /. (i + 1)),yS |^ ((((SgmX ((BagOrder n),(Support pF))) /. (i + 1)) * (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1)))))) /. (i + 1)) are_congruent_mod k by A1, GR_CY_3:34, INT_1:def 4, A31, A30;
k divides p1 - p2 by NAT_1:13, A28, A27;
then p1,p2 are_congruent_mod k by INT_1:def 4;
hence ( Product (H1 | (i + 1)) is integer & Product (H2 | (i + 1)) is integer & ( for i1, i2 being Integer st i1 = Product (H1 | (i + 1)) & i2 = Product (H2 | (i + 1)) holds
k divides i1 - i2 ) ) by A35, A36, INT_1:def 4, A37, INT_1:18; :: thesis: verum
end;
for i being Nat holds S2[i] from NAT_1:sch 2(A25, A26);
 then S2[ len (SgmX ((RelIncl n),(support ((SgmX ((BagOrder n),(Support pF))) /. (i + 1)))))] ;
hence k divides o1 - o2 by A23, A21; :: thesis: verum
end;
then k divides o * (o1 - o2) by INT_2:2;
then A38: k divides - (o * (o1 - o2)) by INT_2:10;
k divides S by A10, A11, NAT_1:13;
then k divides S - (- (o * (o1 - o2))) by A38, INT_5:1;
hence ( (Sum (Xr | (i + 1))) - (Sum (Yr | (i + 1))) is Integer & ( for d being Integer st d = (Sum (Xr | (i + 1))) - (Sum (Yr | (i + 1))) holds
k divides d ) ) by A18, A15, A20; :: thesis: verum
end;
A39: for i being Nat holds S1[i] from NAT_1:sch 2(A7, A8);
 ( Sum (Xr | (len X)) = eval (pF,xF) & Sum (Yr | (len X)) = eval (pF,yF) ) by A5, A3, MATRPROB:36;
hence k divides (eval (p,(@ x))) - (eval (p,(@ y))) by A39; :: thesis: verum