let L be Field; :: thesis: for p, q being Polynomial of L st len p <> 0 & len q > 1 holds
len (Subst p,q) = ((((len p) * (len q)) - (len p)) - (len q)) + 2
let p, q be Polynomial of L; :: thesis: ( len p <> 0 & len q > 1 implies len (Subst p,q) = ((((len p) * (len q)) - (len p)) - (len q)) + 2 )
assume that
A1: len p <> 0 and
A2: len q > 1 ; :: thesis: len (Subst p,q) = ((((len p) * (len q)) - (len p)) - (len q)) + 2
consider F being FinSequence of the carrier of (Polynom-Ring L) such that
A3: Subst p,q = Sum F and
A4: len F = len p and
A5: for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * (q `^ (n -' 1)) by Def5;
reconsider k = ((((len p) * (len q)) - (len p)) - (len q)) + 1 as Element of NAT by A1, A2, Th1, INT_1:16;
len F > 0 by A1, A4;
then A6: 0 + 1 <= len F by NAT_1:13;
then A7: 1 in dom F by FINSEQ_3:27;
defpred S1[ Nat] means for F1 being Polynomial of L st F1 = Sum (F | $1) holds
len F1 <= len (q `^ ($1 -' 1));
A8: S1[1]
proof
let F1 be Polynomial of L; :: thesis: ( F1 = Sum (F | 1) implies len F1 <= len (q `^ (1 -' 1)) )
assume A9: F1 = Sum (F | 1) ; :: thesis: len F1 <= len (q `^ (1 -' 1))
not F is empty by A1, A4, CARD_1:47;
then F | 1 = <*(F /. 1)*> by FINSEQ_5:23;
then Sum (F | 1) = F /. 1 by RLVECT_1:61
.= F . 1 by A7, PARTFUN1:def 8
.= (p . (1 -' 1)) * (q `^ (1 -' 1)) by A5, A7
.= (p . 0 ) * (q `^ (1 -' 1)) by XREAL_1:234
.= (p . 0 ) * (q `^ 0 ) by XREAL_1:234
.= (p . 0 ) * (1_. L) by Th16
.= <%(p . 0 )%> by Th30 ;
then len F1 <= 1 by A9, ALGSEQ_1:def 6;
then len F1 <= len (1_. L) by POLYNOM4:7;
then len F1 <= len (q `^ 0 ) by Th16;
hence len F1 <= len (q `^ (1 -' 1)) by XREAL_1:234; :: thesis: verum
end;
A10: for n being non empty Nat st S1[n] holds
S1[n + 1]
proof
let n be non empty Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A11: for F1 being Polynomial of L st F1 = Sum (F | n) holds
len F1 <= len (q `^ (n -' 1)) ; :: thesis: S1[n + 1]
let F1 be Polynomial of L; :: thesis: ( F1 = Sum (F | (n + 1)) implies len F1 <= len (q `^ ((n + 1) -' 1)) )
assume A12: F1 = Sum (F | (n + 1)) ; :: thesis: len F1 <= len (q `^ ((n + 1) -' 1))
reconsider F2 = Sum (F | n) as Polynomial of L by POLYNOM3:def 12;
n >= 0 + 1 by NAT_1:13;
then A13: n - 1 >= 0 by XREAL_1:21;
len q >= 0 + 1 by A2;
then A14: (len q) - 1 >= 0 by XREAL_1:21;
A15: len (q `^ (n -' 1)) = (((n -' 1) * (len q)) - (n -' 1)) + 1 by A2, Th24
.= (((n - 1) * (len q)) - (n -' 1)) + 1 by A13, XREAL_0:def 2
.= (((n * (len q)) - (1 * (len q))) - (n - 1)) + 1 by A13, XREAL_0:def 2
.= ((((n * (len q)) - (len q)) - n) + 1) + 1 ;
reconsider nn = n as Element of NAT by ORDINAL1:def 13;
(n * (len q)) + ((len q) -' 1) >= n * (len q) by NAT_1:11;
then (n * (len q)) - ((len q) -' 1) <= n * (len q) by XREAL_1:22;
then (n * (len q)) - ((len q) - 1) <= n * (len q) by A14, XREAL_0:def 2;
then (((n * (len q)) - (len q)) + 1) - n <= (n * (len q)) - n by XREAL_1:11;
then ((((n * (len q)) - (len q)) - n) + 1) + 1 <= ((n * (len q)) - n) + 1 by XREAL_1:8;
then A16: len (q `^ (n -' 1)) <= len (q `^ nn) by A2, A15, Th24;
per cases ( n + 1 <= len F or n + 1 > len F ) ;
suppose A17: n + 1 <= len F ; :: thesis: len F1 <= len (q `^ ((n + 1) -' 1))
n + 1 >= 1 by NAT_1:11;
then A18: n + 1 in dom F by A17, FINSEQ_3:27;
F | (n + 1) = (F | n) ^ <*(F /. (nn + 1))*> by A17, JORDAN8:2;
then A19: F1 = (Sum (F | n)) + (F /. (n + 1)) by A12, FVSUM_1:87;
reconsider maxFq = max (len F2),(len ((p . nn) * (q `^ nn))) as Element of NAT by FINSEQ_2:1;
A20: ( maxFq >= len F2 & maxFq >= len ((p . nn) * (q `^ nn)) ) by XXREAL_0:25;
F /. (n + 1) = F . (n + 1) by A18, PARTFUN1:def 8
.= (p . ((n + 1) -' 1)) * (q `^ ((n + 1) -' 1)) by A5, A18
.= (p . nn) * (q `^ ((n + 1) -' 1)) by NAT_D:34
.= (p . nn) * (q `^ nn) by NAT_D:34 ;
then F1 = F2 + ((p . nn) * (q `^ nn)) by A19, POLYNOM3:def 12;
then A21: len F1 <= maxFq by A20, POLYNOM4:9;
len F2 <= len (q `^ (n -' 1)) by A11;
then A22: len F2 <= len (q `^ nn) by A16, XXREAL_0:2;
len ((p . nn) * (q `^ nn)) <= len (q `^ nn)
proof
per cases ( p . n <> 0. L or p . n = 0. L ) ;
suppose p . n <> 0. L ; :: thesis: len ((p . nn) * (q `^ nn)) <= len (q `^ nn)
hence len ((p . nn) * (q `^ nn)) <= len (q `^ nn) by Th26; :: thesis: verum
end;
suppose p . n = 0. L ; :: thesis: len ((p . nn) * (q `^ nn)) <= len (q `^ nn)
hence len ((p . nn) * (q `^ nn)) <= len (q `^ nn) by Th25; :: thesis: verum
end;
end;
end;
then maxFq <= len (q `^ nn) by A22, XXREAL_0:28;
then len F1 <= len (q `^ nn) by A21, XXREAL_0:2;
hence len F1 <= len (q `^ ((n + 1) -' 1)) by NAT_D:34; :: thesis: verum
end;
suppose A23: n + 1 > len F ; :: thesis: len F1 <= len (q `^ ((n + 1) -' 1))
then n >= len F by NAT_1:13;
then ( F | n = F & F | (n + 1) = F ) by A23, FINSEQ_1:79;
then len F1 <= len (q `^ (n -' 1)) by A11, A12;
then len F1 <= len (q `^ nn) by A16, XXREAL_0:2;
hence len F1 <= len (q `^ ((n + 1) -' 1)) by NAT_D:34; :: thesis: verum
end;
end;
end;
A24: for n being non empty Nat holds S1[n] from NAT_1:sch 10(A8, A10);
 len p > 0 by A1;
then len p >= 0 + 1 by NAT_1:13;
then A25: (len p) - 1 >= 0 by XREAL_1:21;
F | (len F) = F by FINSEQ_1:79;
then A26: len (Subst p,q) <= len (q `^ ((len F) -' 1)) by A1, A3, A4, A24;
A27: len (q `^ ((len F) -' 1)) = ((((len p) -' 1) * (len q)) - ((len p) -' 1)) + 1 by A2, A4, Th24
.= ((((len p) -' 1) * (len q)) - ((len p) - 1)) + 1 by A25, XREAL_0:def 2
.= ((((len p) - 1) * (len q)) - ((len p) - 1)) + 1 by A25, XREAL_0:def 2
.= ((((len p) * (len q)) - (len p)) - (len q)) + (1 + 1) ;
len (Subst p,q) >= ((((len p) * (len q)) - (len p)) - (len q)) + (1 + 1)
proof
assume A28: len (Subst p,q) < ((((len p) * (len q)) - (len p)) - (len q)) + (1 + 1) ; :: thesis: contradiction
then len (Subst p,q) < k + 1 ;
then len (Subst p,q) <= k by NAT_1:13;
then A29: (Subst p,q) . k = 0. L by ALGSEQ_1:22;
set lF1 = (len F) -' 1;
set F1 = F | ((len F) -' 1);
reconsider sF1 = Sum (F | ((len F) -' 1)) as Polynomial of L by POLYNOM3:def 12;
A30: len F = ((len F) -' 1) + 1 by A6, XREAL_1:237;
then A31: F = (F | ((len F) -' 1)) ^ <*(F /. (len F))*> by FINSEQ_5:24;
then A32: Sum F = (Sum (F | ((len F) -' 1))) + (F /. (len F)) by FVSUM_1:87;
A33: len F = (len (F | ((len F) -' 1))) + 1 by A31, FINSEQ_2:19;
now
per cases ( len (F | ((len F) -' 1)) <> {} or len (F | ((len F) -' 1)) = {} ) ;
suppose A34: len (F | ((len F) -' 1)) <> {} ; :: thesis: contradiction
then len (F | ((len F) -' 1)) > 0 ;
then 0 + 1 <= len (F | ((len F) -' 1)) by NAT_1:13;
then A35: 1 in dom (F | ((len F) -' 1)) by FINSEQ_3:27;
defpred S2[ Nat] means for F2 being Polynomial of L st F2 = Sum ((F | ((len F) -' 1)) | $1) holds
len F2 <= ((($1 * (len q)) - (len q)) - $1) + 2;
A36: S2[1]
proof
let F2 be Polynomial of L; :: thesis: ( F2 = Sum ((F | ((len F) -' 1)) | 1) implies len F2 <= (((1 * (len q)) - (len q)) - 1) + 2 )
assume A37: F2 = Sum ((F | ((len F) -' 1)) | 1) ; :: thesis: len F2 <= (((1 * (len q)) - (len q)) - 1) + 2
not F | ((len F) -' 1) is empty by A34, CARD_1:47;
then (F | ((len F) -' 1)) | 1 = <*((F | ((len F) -' 1)) /. 1)*> by FINSEQ_5:23;
then Sum ((F | ((len F) -' 1)) | 1) = (F | ((len F) -' 1)) /. 1 by RLVECT_1:61
.= (F | ((len F) -' 1)) . 1 by A35, PARTFUN1:def 8
.= F . 1 by A31, A35, FINSEQ_1:def 7
.= (p . (1 -' 1)) * (q `^ (1 -' 1)) by A5, A7
.= (p . 0 ) * (q `^ (1 -' 1)) by XREAL_1:234
.= (p . 0 ) * (q `^ 0 ) by XREAL_1:234
.= (p . 0 ) * (1_. L) by Th16
.= <%(p . 0 )%> by Th30 ;
hence len F2 <= (((1 * (len q)) - (len q)) - 1) + 2 by A37, ALGSEQ_1:def 6; :: thesis: verum
end;
A38: for n being non empty Nat st S2[n] holds
S2[n + 1]
proof
let n be non empty Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A39: for F2 being Polynomial of L st F2 = Sum ((F | ((len F) -' 1)) | n) holds
len F2 <= (((n * (len q)) - (len q)) - n) + 2 ; :: thesis: S2[n + 1]
let F2 be Polynomial of L; :: thesis: ( F2 = Sum ((F | ((len F) -' 1)) | (n + 1)) implies len F2 <= ((((n + 1) * (len q)) - (len q)) - (n + 1)) + 2 )
assume A40: F2 = Sum ((F | ((len F) -' 1)) | (n + 1)) ; :: thesis: len F2 <= ((((n + 1) * (len q)) - (len q)) - (n + 1)) + 2
reconsider F3 = Sum ((F | ((len F) -' 1)) | n) as Polynomial of L by POLYNOM3:def 12;
A41: len F3 <= (((n * (len q)) - (len q)) - n) + 2 by A39;
A42: ((((n * (len q)) - (len q)) - n) + 2) + 0 <= ((((n * (len q)) - (len q)) - n) + 2) + 1 by XREAL_1:8;
len q >= 0 + (1 + 1) by A2, NAT_1:13;
then (len q) - 2 >= 0 by XREAL_1:21;
then (((n * (len q)) - n) + 1) + 0 <= (((n * (len q)) - n) + 1) + ((len q) - 2) by XREAL_1:9;
then (((n * (len q)) - n) + 1) - ((len q) - 2) <= ((n * (len q)) - n) + 1 by XREAL_1:22;
then (((n * (len q)) - (len q)) - n) + 2 <= ((n * (len q)) - n) + 1 by A42, XXREAL_0:2;
then A43: len F3 <= ((n * (len q)) - n) + 1 by A41, XXREAL_0:2;
now
per cases ( n + 1 <= len (F | ((len F) -' 1)) or n + 1 > len (F | ((len F) -' 1)) ) ;
suppose A44: n + 1 <= len (F | ((len F) -' 1)) ; :: thesis: len F2 <= ((((n + 1) * (len q)) - (len q)) - (n + 1)) + 2
A45: n + 1 >= 1 by NAT_1:11;
then A46: n + 1 in dom (F | ((len F) -' 1)) by A44, FINSEQ_3:27;
len (F | ((len F) -' 1)) <= len F by A33, NAT_1:11;
then n + 1 <= len F by A44, XXREAL_0:2;
then A47: n + 1 in dom F by A45, FINSEQ_3:27;
reconsider nn = n as Element of NAT by ORDINAL1:def 13;
A48: (F | ((len F) -' 1)) /. (n + 1) = (F | ((len F) -' 1)) . (n + 1) by A46, PARTFUN1:def 8
.= F . (n + 1) by A31, A46, FINSEQ_1:def 7
.= (p . ((n + 1) -' 1)) * (q `^ ((n + 1) -' 1)) by A5, A47
.= (p . nn) * (q `^ ((n + 1) -' 1)) by NAT_D:34
.= (p . nn) * (q `^ nn) by NAT_D:34 ;
reconsider maxFq = max (len F3),(len ((p . nn) * (q `^ nn))) as Element of NAT by FINSEQ_2:1;
A49: ( maxFq >= len F3 & maxFq >= len ((p . nn) * (q `^ nn)) ) by XXREAL_0:25;
(F | ((len F) -' 1)) | (nn + 1) = ((F | ((len F) -' 1)) | nn) ^ <*((F | ((len F) -' 1)) /. (nn + 1))*> by A44, JORDAN8:2;
then F2 = (Sum ((F | ((len F) -' 1)) | n)) + ((F | ((len F) -' 1)) /. (n + 1)) by A40, FVSUM_1:87
.= F3 + ((p . nn) * (q `^ nn)) by A48, POLYNOM3:def 12 ;
then A50: len F2 <= maxFq by A49, POLYNOM4:9;
len ((p . nn) * (q `^ nn)) <= ((n * (len q)) - n) + 1
proof
per cases ( p . n <> 0. L or p . n = 0. L ) ;
suppose p . n <> 0. L ; :: thesis: len ((p . nn) * (q `^ nn)) <= ((n * (len q)) - n) + 1
then len ((p . nn) * (q `^ nn)) = len (q `^ nn) by Th26;
hence len ((p . nn) * (q `^ nn)) <= ((n * (len q)) - n) + 1 by A2, Th24; :: thesis: verum
end;
suppose A51: p . n = 0. L ; :: thesis: len ((p . nn) * (q `^ nn)) <= ((n * (len q)) - n) + 1
len q >= 0 + 1 by A2;
then (len q) - 1 >= 0 by XREAL_1:21;
then A52: n * ((len q) - 1) >= 0 ;
n * (len q) <= (n * (len q)) + 1 by NAT_1:11;
then (n * (len q)) - n <= ((n * (len q)) + 1) - n by XREAL_1:11;
hence len ((p . nn) * (q `^ nn)) <= ((n * (len q)) - n) + 1 by A51, A52, Th25; :: thesis: verum
end;
end;
end;
then maxFq <= ((n * (len q)) - n) + 1 by A43, XXREAL_0:28;
hence len F2 <= ((((n + 1) * (len q)) - (len q)) - (n + 1)) + 2 by A50, XXREAL_0:2; :: thesis: verum
end;
suppose A53: n + 1 > len (F | ((len F) -' 1)) ; :: thesis: len F2 <= ((((n + 1) * (len q)) - (len q)) - (n + 1)) + 2
then n >= len (F | ((len F) -' 1)) by NAT_1:13;
then ( (F | ((len F) -' 1)) | n = F | ((len F) -' 1) & (F | ((len F) -' 1)) | (n + 1) = F | ((len F) -' 1) ) by A53, FINSEQ_1:79;
then A54: len F2 <= (((n * (len q)) - (len q)) - n) + 2 by A39, A40;
- (len q) <= - 1 by A2, XREAL_1:26;
then ((n * (len q)) - n) + (- (len q)) <= ((n * (len q)) - n) + (- 1) by XREAL_1:8;
then (((n * (len q)) - (len q)) - n) + 2 <= ((((n + 1) * (len q)) - (len q)) - (n + 1)) + 2 by XREAL_1:8;
hence len F2 <= ((((n + 1) * (len q)) - (len q)) - (n + 1)) + 2 by A54, XXREAL_0:2; :: thesis: verum
end;
end;
end;
hence len F2 <= ((((n + 1) * (len q)) - (len q)) - (n + 1)) + 2 ; :: thesis: verum
end;
A55: for n being non empty Nat holds S2[n] from NAT_1:sch 10(A36, A38);
 (F | ((len F) -' 1)) | (len (F | ((len F) -' 1))) = F | ((len F) -' 1) by FINSEQ_1:79;
then A56: len sF1 <= ((((len (F | ((len F) -' 1))) * (len q)) - (len q)) - (len (F | ((len F) -' 1)))) + 2 by A34, A55;
0 + (len q) >= 1 + 1 by A2, NAT_1:13;
then 2 - (len q) <= 0 by XREAL_1:22;
then (2 - (len q)) + k <= 0 + k by XREAL_1:8;
then A57: sF1 . k = 0. L by A4, A33, A56, ALGSEQ_1:22, XXREAL_0:2;
A58: len F in dom F by A6, FINSEQ_3:27;
then F /. (len F) = F . (len F) by PARTFUN1:def 8
.= (p . ((len F) -' 1)) * (q `^ ((len F) -' 1)) by A5, A58 ;
then Subst p,q = sF1 + ((p . ((len F) -' 1)) * (q `^ ((len F) -' 1))) by A3, A32, POLYNOM3:def 12;
then A59: (Subst p,q) . k = (sF1 . k) + (((p . ((len F) -' 1)) * (q `^ ((len F) -' 1))) . k) by NORMSP_1:def 5
.= ((p . ((len F) -' 1)) * (q `^ ((len F) -' 1))) . k by A57, RLVECT_1:def 7
.= (p . ((len F) -' 1)) * ((q `^ ((len F) -' 1)) . k) by Def3 ;
A60: p . ((len F) -' 1) <> 0. L by A4, A30, ALGSEQ_1:25;
len (q `^ ((len F) -' 1)) = k + 1 by A27;
then (q `^ ((len F) -' 1)) . k <> 0. L by ALGSEQ_1:25;
hence contradiction by A29, A59, A60, VECTSP_1:44; :: thesis: verum
end;
suppose A61: len (F | ((len F) -' 1)) = {} ; :: thesis: contradiction
then A62: F | ((len F) -' 1) = <*> the carrier of (Polynom-Ring L) by FINSEQ_1:32;
A63: len F = 0 + 1 by A31, A61, FINSEQ_2:19;
A64: F /. 1 = F . 1 by A7, PARTFUN1:def 8
.= (p . (1 -' 1)) * (q `^ (1 -' 1)) by A5, A7
.= (p . 0 ) * (q `^ (1 -' 1)) by XREAL_1:234
.= (p . 0 ) * (q `^ 0 ) by XREAL_1:234
.= (p . 0 ) * (1_. L) by Th16
.= <%(p . 0 )%> by Th30 ;
A65: 0. (Polynom-Ring L) = 0_. L by POLYNOM3:def 12;
A66: Sum F = (0. (Polynom-Ring L)) + (F /. 1) by A32, A62, A63, RLVECT_1:60
.= (0_. L) + <%(p . 0 )%> by A64, A65, POLYNOM3:def 12
.= <%(p . 0 )%> by POLYNOM3:29 ;
p . 0 <> 0. L by A4, A63, ALGSEQ_1:25;
hence contradiction by A3, A4, A28, A63, A66, Th34; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
hence len (Subst p,q) = ((((len p) * (len q)) - (len p)) - (len q)) + 2 by A26, A27, XXREAL_0:1; :: thesis: verum