let p be prime odd Nat; :: thesis: for m being positive Nat
for j being Nat st j in Seg m holds
('F' (f_0 (m,p))) . (In (j,F_Real)) in {(In ((p !),INT.Ring))} -Ideal
let m be positive Nat; :: thesis: for j being Nat st j in Seg m holds
('F' (f_0 (m,p))) . (In (j,F_Real)) in {(In ((p !),INT.Ring))} -Ideal
set Gf = 'G' (f_0 (m,p));
set D = Der1 INT.Ring;
let j be Nat; :: thesis: ( j in Seg m implies ('F' (f_0 (m,p))) . (In (j,F_Real)) in {(In ((p !),INT.Ring))} -Ideal )
assume A1: j in Seg m ; :: thesis: ('F' (f_0 (m,p))) . (In (j,F_Real)) in {(In ((p !),INT.Ring))} -Ideal
A2: len (f_0 (m,p)) = len (~ (f_0 (m,p)))
.= (m * p) + p by Th12 ;
then A3: len ('G' (f_0 (m,p))) = (m * p) + p by E_TRANS1:def 8;
then A4: ( 1 <= p & p <= len ('G' (f_0 (m,p))) ) by INT_2:def 4, XREAL_1:38;
set p1 = p -' 1;
A5: len (('G' (f_0 (m,p))) | p) = p by XREAL_1:38, A3, FINSEQ_1:59;
then A6: dom (('G' (f_0 (m,p))) | p) = Seg p by FINSEQ_1:def 3;
A7: dom (('G' (f_0 (m,p))) | p) = dom (p |-> (0. INT.Ring)) by A5, FINSEQ_1:def 3;
A8: eval ((('G' (f_0 (m,p))) | p),(In (j,INT.Ring))) = p |-> (0. INT.Ring)

proof

for k being Nat st k in dom (eval ((('G' (f_0 (m,p))) | p),(In (j,INT.Ring)))) holds
(eval ((('G' (f_0 (m,p))) | p),(In (j,INT.Ring)))) . k = (p |-> (0. INT.Ring)) . k

proof

let k be Nat; :: thesis: ( k in dom (eval ((('G' (f_0 (m,p))) | p),(In (j,INT.Ring)))) implies (eval ((('G' (f_0 (m,p))) | p),(In (j,INT.Ring)))) . k = (p |-> (0. INT.Ring)) . k )
assume A9: k in dom (eval ((('G' (f_0 (m,p))) | p),(In (j,INT.Ring)))) ; :: thesis: (eval ((('G' (f_0 (m,p))) | p),(In (j,INT.Ring)))) . k = (p |-> (0. INT.Ring)) . k
then A10: k in dom (('G' (f_0 (m,p))) | p) by E_TRANS1:def 7;
A11: k in Seg p by A6, A9, E_TRANS1:def 7;
then A12: ( 1 <= k & k <= p ) by FINSEQ_1:1;
then ( 1 <= k & k <= len ('G' (f_0 (m,p))) ) by XREAL_1:38, A3;
then A13: k in dom ('G' (f_0 (m,p))) by FINSEQ_3:25;
k - 1 < k by XREAL_1:44;
then k - 1 < p by A12, XXREAL_0:2;
then A15: k -' 1 < p by A12, XREAL_1:233;
A16: (('G' (f_0 (m,p))) | p) /. k = (('G' (f_0 (m,p))) | p) . k by A10, PARTFUN1:def 6
.= ('G' (f_0 (m,p))) . k by FUNCT_1:49, A11
.= ((Der1 INT.Ring) |^ (k -' 1)) . (f_0 (m,p)) by A13, E_TRANS1:def 8 ;
(eval ((('G' (f_0 (m,p))) | p),(In (j,INT.Ring)))) . k = eval ((~ (((Der1 INT.Ring) |^ (k -' 1)) . (f_0 (m,p)))),(In (j,INT.Ring))) by A16, A10, E_TRANS1:def 7
.= 0. INT.Ring by A1, A15, Th26 ;
hence (eval ((('G' (f_0 (m,p))) | p),(In (j,INT.Ring)))) . k = (p |-> (0. INT.Ring)) . k ; :: thesis: verum

end;

hence eval ((('G' (f_0 (m,p))) | p),(In (j,INT.Ring))) = p |-> (0. INT.Ring) by E_TRANS1:def 7, A7; :: thesis: verum

end;

A17: (Eval (~ (^ (Sum (('G' (f_0 (m,p))) | p))))) . (In (j,F_Real)) = Sum (p |-> (0. INT.Ring)) by A8, E_TRANS1:30
.= 0. INT.Ring by MATRIX_3:11 ;
len (('G' (f_0 (m,p))) /^ p) = (len ('G' (f_0 (m,p)))) - p by A4, RFINSEQ:def 1
.= ((m * p) + p) - p by A2, E_TRANS1:def 8
.= m * p ;
then A18: dom (('G' (f_0 (m,p))) /^ p) = Seg (m * p) by FINSEQ_1:def 3;
for k being Nat st k in dom (eval ((('G' (f_0 (m,p))) /^ p),(In (j,INT.Ring)))) holds
(eval ((('G' (f_0 (m,p))) /^ p),(In (j,INT.Ring)))) . k in {(In ((p !),INT.Ring))} -Ideal

proof

let k be Nat; :: thesis: ( k in dom (eval ((('G' (f_0 (m,p))) /^ p),(In (j,INT.Ring)))) implies (eval ((('G' (f_0 (m,p))) /^ p),(In (j,INT.Ring)))) . k in {(In ((p !),INT.Ring))} -Ideal )
assume A19: k in dom (eval ((('G' (f_0 (m,p))) /^ p),(In (j,INT.Ring)))) ; :: thesis: (eval ((('G' (f_0 (m,p))) /^ p),(In (j,INT.Ring)))) . k in {(In ((p !),INT.Ring))} -Ideal
then A20: k in dom (('G' (f_0 (m,p))) /^ p) by E_TRANS1:def 7;
A21: k in Seg (m * p) by A18, A19, E_TRANS1:def 7;
then A22: ( 1 <= k & k <= m * p ) by FINSEQ_1:1;
then A23: k + p <= (m * p) + p by XREAL_1:6;
1 <= k + p by A22, XREAL_1:38;
then k + p in Seg (len ('G' (f_0 (m,p)))) by A3, A23;
then A24: k + p in dom ('G' (f_0 (m,p))) by FINSEQ_1:def 3;
set kp = k + p;
A25: (k + p) -' 1 = (k + p) - 1 by A22, XREAL_1:38, XREAL_1:233;
1 <= k by FINSEQ_1:1, A21;
then A27: 0 + p <= (k - 1) + p by XREAL_1:6;
A28: (('G' (f_0 (m,p))) /^ p) /. k = (('G' (f_0 (m,p))) /^ p) . k by A20, PARTFUN1:def 6
.= ('G' (f_0 (m,p))) . (p + k) by A4, A20, RFINSEQ:def 1
.= ((Der1 INT.Ring) |^ ((k + p) -' 1)) . (f_0 (m,p)) by A24, E_TRANS1:def 8 ;
eval ((~ (((Der1 INT.Ring) |^ ((k + p) -' 1)) . (f_0 (m,p)))),(In (j,INT.Ring))) in {(In ((p !),INT.Ring))} -Ideal by A1, A25, A27, Th32;
hence (eval ((('G' (f_0 (m,p))) /^ p),(In (j,INT.Ring)))) . k in {(In ((p !),INT.Ring))} -Ideal by A28, E_TRANS1:def 7, A20; :: thesis: verum

end;

then A30: Sum (eval ((('G' (f_0 (m,p))) /^ p),(In (j,INT.Ring)))) in {(In ((p !),INT.Ring))} -Ideal by E_TRANS1:3;
^ (Sum ('G' (f_0 (m,p)))) = ^ (Sum ((('G' (f_0 (m,p))) | p) ^ (('G' (f_0 (m,p))) /^ p)))
.= ^ ((Sum (('G' (f_0 (m,p))) | p)) + (Sum (('G' (f_0 (m,p))) /^ p))) by RLVECT_1:41
.= (^ (Sum (('G' (f_0 (m,p))) | p))) + (^ (Sum (('G' (f_0 (m,p))) /^ p))) by E_TRANS1:27 ;
then ~ (^ (Sum ('G' (f_0 (m,p))))) = (~ (^ (Sum (('G' (f_0 (m,p))) | p)))) + (~ (^ (Sum (('G' (f_0 (m,p))) /^ p)))) by POLYNOM3:def 10;
then Eval (~ (^ (Sum ('G' (f_0 (m,p)))))) = (Eval (~ (^ (Sum (('G' (f_0 (m,p))) | p))))) + (Eval (~ (^ (Sum (('G' (f_0 (m,p))) /^ p))))) by POLYDIFF:55;
then (Eval (~ (^ (Sum ('G' (f_0 (m,p))))))) . (In (j,F_Real)) = (0. INT.Ring) + ((Eval (~ (^ (Sum (('G' (f_0 (m,p))) /^ p))))) . (In (j,F_Real))) by A17, VALUED_1:1
.= (Eval (~ (^ (Sum (('G' (f_0 (m,p))) /^ p))))) . (In (j,F_Real)) ;
hence ('F' (f_0 (m,p))) . (In (j,F_Real)) in {(In ((p !),INT.Ring))} -Ideal by A30, E_TRANS1:30; :: thesis: verum