let R be non degenerated comRing; for n being Nat
for x, y being Element of R
for D being Derivation of R holds LBZ (D,(n + 1),x,y) = (<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>
let n be Nat; for x, y being Element of R
for D being Derivation of R holds LBZ (D,(n + 1),x,y) = (<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>
let x, y be Element of R; for D being Derivation of R holds LBZ (D,(n + 1),x,y) = (<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>
let D be Derivation of R; LBZ (D,(n + 1),x,y) = (<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>
set p = LBZ (D,(n + 1),x,y);
set q = LBZ0 (D,n,x,y);
set r = (<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>;
set r1 = <*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y));
set r2 = (<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>;
set r3 = (LBZ0 (D,n,x,y)) ^ <*(x * ((D |^ (n + 1)) . y))*>;
<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y)) = Ins ((LBZ0 (D,n,x,y)),0,(((D |^ (n + 1)) . x) * y))
by FINSEQ_5:67;
then A2: len (<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) =
(len (LBZ0 (D,n,x,y))) + 1
by FINSEQ_5:69
.=
n + 1
by Def5
;
A3: len (LBZ (D,(n + 1),x,y)) =
(n + 1) + 1
by Def4
.=
n + 2
;
(<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*> = Ins ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))),(n + 1),(x * ((D |^ (n + 1)) . y)))
by A2, FINSEQ_5:68;
then A4: len ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) =
(n + 1) + 1
by A2, FINSEQ_5:69
.=
len (LBZ (D,(n + 1),x,y))
by A3
;
for k being Nat st 1 <= k & k <= len (LBZ (D,(n + 1),x,y)) holds
(LBZ (D,(n + 1),x,y)) . k = ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) . k
proof
let k be
Nat;
( 1 <= k & k <= len (LBZ (D,(n + 1),x,y)) implies (LBZ (D,(n + 1),x,y)) . k = ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) . k )
assume A5:
( 1
<= k &
k <= len (LBZ (D,(n + 1),x,y)) )
;
(LBZ (D,(n + 1),x,y)) . k = ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) . k
A6:
k in dom (LBZ (D,(n + 1),x,y))
by A5, FINSEQ_3:25;
(n + 1) + 1
> 0 + 1
by XREAL_1:8;
then A7:
(n + 2) -' 1 =
(n + 2) - 1
by XREAL_1:233
.=
n + 1
;
( 1
< k + 1 &
k < (n + 2) + 1 )
by A5, A3, NAT_1:13;
per cases then
( k = 1 or ( 1 < k & k < n + 2 ) or k = n + 2 )
by NAT_1:22;
suppose A9:
k = 1
;
(LBZ (D,(n + 1),x,y)) . k = ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) . k
(n + 1) + 1
> 0 + 1
by XREAL_1:8;
then A10:
(n + 2) -' 1 =
(n + 2) - 1
by XREAL_1:233
.=
n + 1
;
A11:
(LBZ (D,(n + 1),x,y)) . k =
(((n + 1) choose (k -' 1)) * ((D |^ (((n + 1) + 1) -' k)) . x)) * ((D |^ (k -' 1)) . y)
by A6, Def4
.=
(((n + 1) choose 0) * ((D |^ ((n + 2) -' 1)) . x)) * ((D |^ (1 -' 1)) . y)
by A9, XREAL_1:232
.=
(1 * ((D |^ ((n + 2) -' 1)) . x)) * ((D |^ (1 -' 1)) . y)
by NEWTON:19
.=
((D |^ ((n + 2) -' 1)) . x) * ((D |^ (1 -' 1)) . y)
by BINOM:13
.=
((D |^ (n + 1)) . x) * ((D |^ 0) . y)
by A10, XREAL_1:232
.=
((D |^ (n + 1)) . x) * ((id R) . y)
by VECTSP11:18
.=
((D |^ (n + 1)) . x) * y
;
((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) . k =
(Ins ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))),(n + 1),(x * ((D |^ (n + 1)) . y)))) . 1
by A9, A2, FINSEQ_5:68
.=
(<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) . 1
by NAT_1:11, FINSEQ_5:75
.=
(LBZ (D,(n + 1),x,y)) . k
by A11, FINSEQ_1:41
;
hence
(LBZ (D,(n + 1),x,y)) . k = ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) . k
;
verum end; suppose A12:
( 1
< k &
k < n + 2 )
;
(LBZ (D,(n + 1),x,y)) . k = ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) . kA13:
dom (<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) = Seg (n + 1)
by A2, FINSEQ_1:def 3;
1
+ 1
<= k
by A12, INT_1:7;
then A15:
2
- 1
<= k - 1
by XREAL_1:9;
k + 1
<= n + 2
by A12, INT_1:7;
then A17:
(k + 1) - 1
<= (n + 2) - 1
by XREAL_1:9;
then A18:
k in dom (<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y)))
by A13, A12;
reconsider s =
k - 1 as
Nat by A12;
reconsider q1 =
<*(((D |^ (n + 1)) . x) * y)*> as
FinSequence of
R ;
A19:
dom (LBZ0 (D,n,x,y)) =
Seg (len (LBZ0 (D,n,x,y)))
by FINSEQ_1:def 3
.=
Seg n
by Def5
;
k - 1
<= (n + 1) - 1
by A17, XREAL_1:9;
then A21:
s in dom (LBZ0 (D,n,x,y))
by A19, A15;
reconsider t =
s - 1 as
Nat by A15;
A22:
k -' 1
= s
by A12, XREAL_1:233;
A23:
((n + 1) + 1) -' k =
((n + 1) + 1) - k
by A12, XREAL_1:233
.=
(n + 1) - s
.=
(n + 1) -' s
by A12, A17, XREAL_1:9, XREAL_1:233
;
((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) . k =
(q1 ^ (LBZ0 (D,n,x,y))) . (s + 1)
by A18, FINSEQ_1:def 7
.=
(q1 ^ (LBZ0 (D,n,x,y))) . ((len q1) + s)
by FINSEQ_1:39
.=
(LBZ0 (D,n,x,y)) . s
by A21, FINSEQ_1:def 7
.=
(((n choose (s -' 1)) + (n choose s)) * ((D |^ ((n + 1) -' s)) . x)) * ((D |^ s) . y)
by A21, Def5
.=
(((n choose t) + (n choose (t + 1))) * ((D |^ ((n + 1) -' s)) . x)) * ((D |^ s) . y)
by A15, XREAL_1:233
.=
(((n + 1) choose (k -' 1)) * ((D |^ (((n + 1) + 1) -' k)) . x)) * ((D |^ (k -' 1)) . y)
by A23, A22, NEWTON:22
.=
(LBZ (D,(n + 1),x,y)) . k
by A6, Def4
;
hence
(LBZ (D,(n + 1),x,y)) . k = ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) . k
;
verum end; suppose A24:
k = n + 2
;
(LBZ (D,(n + 1),x,y)) . k = ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) . kthen A25:
((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) . k =
(Ins ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))),(n + 1),(x * ((D |^ (n + 1)) . y)))) . ((n + 1) + 1)
by A2, FINSEQ_5:68
.=
x * ((D |^ (n + 1)) . y)
by FINSEQ_5:73, A2
;
(LBZ (D,(n + 1),x,y)) . k =
(((n + 1) choose (n + 1)) * ((D |^ (((n + 1) + 1) -' (n + 2))) . x)) * ((D |^ ((n + 2) -' 1)) . y)
by A7, A24, A6, Def4
.=
(1 * ((D |^ (((n + 1) + 1) -' (n + 2))) . x)) * ((D |^ ((n + 2) -' 1)) . y)
by NEWTON:21
.=
((D |^ ((n + 2) -' (n + 2))) . x) * ((D |^ ((n + 2) -' 1)) . y)
by BINOM:13
.=
((D |^ 0) . x) * ((D |^ (n + 1)) . y)
by A7, XREAL_1:232
.=
((id R) . x) * ((D |^ (n + 1)) . y)
by VECTSP11:18
.=
((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) . k
by A25
;
hence
(LBZ (D,(n + 1),x,y)) . k = ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) . k
;
verum end;
end;
hence
LBZ (D,(n + 1),x,y) = (<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>
by A4; verum