defpred S1[ Nat] means for S, E, F being RealNormSpace
for u being PartFunc of S,E
for v being PartFunc of S,F
for w being PartFunc of S,[:E,F:]
for Z being Subset of S st w = <:u,v:> & u is_differentiable_on $1 + 1,Z & v is_differentiable_on $1 + 1,Z holds
( w is_differentiable_on $1 + 1,Z & ex T being Lipschitzian LinearOperator of [:(diff_SP (($1 + 1),S,E)),(diff_SP (($1 + 1),S,F)):],(diff_SP (($1 + 1),S,[:E,F:])) st diff (w,($1 + 1),Z) = T * <:(diff (u,($1 + 1),Z)),(diff (v,($1 + 1),Z)):> );
A1:
S1[ 0 ]
proof
let S,
E,
F be
RealNormSpace;
for u being PartFunc of S,E
for v being PartFunc of S,F
for w being PartFunc of S,[:E,F:]
for Z being Subset of S st w = <:u,v:> & u is_differentiable_on 0 + 1,Z & v is_differentiable_on 0 + 1,Z holds
( w is_differentiable_on 0 + 1,Z & ex T being Lipschitzian LinearOperator of [:(diff_SP ((0 + 1),S,E)),(diff_SP ((0 + 1),S,F)):],(diff_SP ((0 + 1),S,[:E,F:])) st diff (w,(0 + 1),Z) = T * <:(diff (u,(0 + 1),Z)),(diff (v,(0 + 1),Z)):> )let u be
PartFunc of
S,
E;
for v being PartFunc of S,F
for w being PartFunc of S,[:E,F:]
for Z being Subset of S st w = <:u,v:> & u is_differentiable_on 0 + 1,Z & v is_differentiable_on 0 + 1,Z holds
( w is_differentiable_on 0 + 1,Z & ex T being Lipschitzian LinearOperator of [:(diff_SP ((0 + 1),S,E)),(diff_SP ((0 + 1),S,F)):],(diff_SP ((0 + 1),S,[:E,F:])) st diff (w,(0 + 1),Z) = T * <:(diff (u,(0 + 1),Z)),(diff (v,(0 + 1),Z)):> )let v be
PartFunc of
S,
F;
for w being PartFunc of S,[:E,F:]
for Z being Subset of S st w = <:u,v:> & u is_differentiable_on 0 + 1,Z & v is_differentiable_on 0 + 1,Z holds
( w is_differentiable_on 0 + 1,Z & ex T being Lipschitzian LinearOperator of [:(diff_SP ((0 + 1),S,E)),(diff_SP ((0 + 1),S,F)):],(diff_SP ((0 + 1),S,[:E,F:])) st diff (w,(0 + 1),Z) = T * <:(diff (u,(0 + 1),Z)),(diff (v,(0 + 1),Z)):> )let w be
PartFunc of
S,
[:E,F:];
for Z being Subset of S st w = <:u,v:> & u is_differentiable_on 0 + 1,Z & v is_differentiable_on 0 + 1,Z holds
( w is_differentiable_on 0 + 1,Z & ex T being Lipschitzian LinearOperator of [:(diff_SP ((0 + 1),S,E)),(diff_SP ((0 + 1),S,F)):],(diff_SP ((0 + 1),S,[:E,F:])) st diff (w,(0 + 1),Z) = T * <:(diff (u,(0 + 1),Z)),(diff (v,(0 + 1),Z)):> )let Z be
Subset of
S;
( w = <:u,v:> & u is_differentiable_on 0 + 1,Z & v is_differentiable_on 0 + 1,Z implies ( w is_differentiable_on 0 + 1,Z & ex T being Lipschitzian LinearOperator of [:(diff_SP ((0 + 1),S,E)),(diff_SP ((0 + 1),S,F)):],(diff_SP ((0 + 1),S,[:E,F:])) st diff (w,(0 + 1),Z) = T * <:(diff (u,(0 + 1),Z)),(diff (v,(0 + 1),Z)):> ) )
assume A2:
(
w = <:u,v:> &
u is_differentiable_on 0 + 1,
Z &
v is_differentiable_on 0 + 1,
Z )
;
( w is_differentiable_on 0 + 1,Z & ex T being Lipschitzian LinearOperator of [:(diff_SP ((0 + 1),S,E)),(diff_SP ((0 + 1),S,F)):],(diff_SP ((0 + 1),S,[:E,F:])) st diff (w,(0 + 1),Z) = T * <:(diff (u,(0 + 1),Z)),(diff (v,(0 + 1),Z)):> )
then
(
Z c= dom u &
u | Z is_differentiable_on Z &
Z c= dom v &
v | Z is_differentiable_on Z )
by NDIFF_6:15;
then A3:
(
u is_differentiable_on Z &
v is_differentiable_on Z )
;
then A4:
(
diff (
w,
0,
Z)
is_differentiable_on Z & ex
T being
Lipschitzian LinearOperator of
[:(diff_SP (1,S,E)),(diff_SP (1,S,F)):],
(diff_SP (1,S,[:E,F:])) st
(
T = CTP (
S,
(diff_SP (0,S,E)),
(diff_SP (0,S,F))) &
diff (
w,1,
Z)
= T * <:(diff (u,1,Z)),(diff (v,1,Z)):> ) )
by A2, Th58;
A5:
diff (
w,
0,
Z)
= w | Z
by NDIFF_6:11;
A6:
diff_SP (
0,
S,
[:E,F:])
= [:E,F:]
by NDIFF_6:7;
then
w is_differentiable_on Z
by A4, A5, Th3;
hence
w is_differentiable_on 0 + 1,
Z
by A2, A3, A5, A6, Th58, NDIFF_6:15;
ex T being Lipschitzian LinearOperator of [:(diff_SP ((0 + 1),S,E)),(diff_SP ((0 + 1),S,F)):],(diff_SP ((0 + 1),S,[:E,F:])) st diff (w,(0 + 1),Z) = T * <:(diff (u,(0 + 1),Z)),(diff (v,(0 + 1),Z)):>
thus
ex
T being
Lipschitzian LinearOperator of
[:(diff_SP ((0 + 1),S,E)),(diff_SP ((0 + 1),S,F)):],
(diff_SP ((0 + 1),S,[:E,F:])) st
diff (
w,
(0 + 1),
Z)
= T * <:(diff (u,(0 + 1),Z)),(diff (v,(0 + 1),Z)):>
by A4;
verum
end;
A7:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume A8:
S1[
i]
;
S1[i + 1]
let S,
E,
F be
RealNormSpace;
for u being PartFunc of S,E
for v being PartFunc of S,F
for w being PartFunc of S,[:E,F:]
for Z being Subset of S st w = <:u,v:> & u is_differentiable_on (i + 1) + 1,Z & v is_differentiable_on (i + 1) + 1,Z holds
( w is_differentiable_on (i + 1) + 1,Z & ex T being Lipschitzian LinearOperator of [:(diff_SP (((i + 1) + 1),S,E)),(diff_SP (((i + 1) + 1),S,F)):],(diff_SP (((i + 1) + 1),S,[:E,F:])) st diff (w,((i + 1) + 1),Z) = T * <:(diff (u,((i + 1) + 1),Z)),(diff (v,((i + 1) + 1),Z)):> )let u be
PartFunc of
S,
E;
for v being PartFunc of S,F
for w being PartFunc of S,[:E,F:]
for Z being Subset of S st w = <:u,v:> & u is_differentiable_on (i + 1) + 1,Z & v is_differentiable_on (i + 1) + 1,Z holds
( w is_differentiable_on (i + 1) + 1,Z & ex T being Lipschitzian LinearOperator of [:(diff_SP (((i + 1) + 1),S,E)),(diff_SP (((i + 1) + 1),S,F)):],(diff_SP (((i + 1) + 1),S,[:E,F:])) st diff (w,((i + 1) + 1),Z) = T * <:(diff (u,((i + 1) + 1),Z)),(diff (v,((i + 1) + 1),Z)):> )let v be
PartFunc of
S,
F;
for w being PartFunc of S,[:E,F:]
for Z being Subset of S st w = <:u,v:> & u is_differentiable_on (i + 1) + 1,Z & v is_differentiable_on (i + 1) + 1,Z holds
( w is_differentiable_on (i + 1) + 1,Z & ex T being Lipschitzian LinearOperator of [:(diff_SP (((i + 1) + 1),S,E)),(diff_SP (((i + 1) + 1),S,F)):],(diff_SP (((i + 1) + 1),S,[:E,F:])) st diff (w,((i + 1) + 1),Z) = T * <:(diff (u,((i + 1) + 1),Z)),(diff (v,((i + 1) + 1),Z)):> )let w be
PartFunc of
S,
[:E,F:];
for Z being Subset of S st w = <:u,v:> & u is_differentiable_on (i + 1) + 1,Z & v is_differentiable_on (i + 1) + 1,Z holds
( w is_differentiable_on (i + 1) + 1,Z & ex T being Lipschitzian LinearOperator of [:(diff_SP (((i + 1) + 1),S,E)),(diff_SP (((i + 1) + 1),S,F)):],(diff_SP (((i + 1) + 1),S,[:E,F:])) st diff (w,((i + 1) + 1),Z) = T * <:(diff (u,((i + 1) + 1),Z)),(diff (v,((i + 1) + 1),Z)):> )let Z be
Subset of
S;
( w = <:u,v:> & u is_differentiable_on (i + 1) + 1,Z & v is_differentiable_on (i + 1) + 1,Z implies ( w is_differentiable_on (i + 1) + 1,Z & ex T being Lipschitzian LinearOperator of [:(diff_SP (((i + 1) + 1),S,E)),(diff_SP (((i + 1) + 1),S,F)):],(diff_SP (((i + 1) + 1),S,[:E,F:])) st diff (w,((i + 1) + 1),Z) = T * <:(diff (u,((i + 1) + 1),Z)),(diff (v,((i + 1) + 1),Z)):> ) )
assume A9:
(
w = <:u,v:> &
u is_differentiable_on (i + 1) + 1,
Z &
v is_differentiable_on (i + 1) + 1,
Z )
;
( w is_differentiable_on (i + 1) + 1,Z & ex T being Lipschitzian LinearOperator of [:(diff_SP (((i + 1) + 1),S,E)),(diff_SP (((i + 1) + 1),S,F)):],(diff_SP (((i + 1) + 1),S,[:E,F:])) st diff (w,((i + 1) + 1),Z) = T * <:(diff (u,((i + 1) + 1),Z)),(diff (v,((i + 1) + 1),Z)):> )
(i + 1) + 0 <= (i + 1) + 1
by XREAL_1:7;
then A10:
(
u is_differentiable_on i + 1,
Z &
v is_differentiable_on i + 1,
Z )
by A9, NDIFF_6:17;
then A11:
(
w is_differentiable_on i + 1,
Z & ex
T0 being
Lipschitzian LinearOperator of
[:(diff_SP ((i + 1),S,E)),(diff_SP ((i + 1),S,F)):],
(diff_SP ((i + 1),S,[:E,F:])) st
diff (
w,
(i + 1),
Z)
= T0 * <:(diff (u,(i + 1),Z)),(diff (v,(i + 1),Z)):> )
by A8, A9;
consider T0 being
Lipschitzian LinearOperator of
[:(diff_SP ((i + 1),S,E)),(diff_SP ((i + 1),S,F)):],
(diff_SP ((i + 1),S,[:E,F:])) such that A12:
diff (
w,
(i + 1),
Z)
= T0 * <:(diff (u,(i + 1),Z)),(diff (v,(i + 1),Z)):>
by A8, A9, A10;
A13:
(
diff (
u,
i,
Z)
is_differentiable_on Z &
diff (
v,
i,
Z)
is_differentiable_on Z )
by A10, NDIFF_6:14;
set E1 =
diff_SP (
(i + 1),
S,
E);
set F1 =
diff_SP (
(i + 1),
S,
F);
set u1 =
diff (
u,
(i + 1),
Z);
set v1 =
diff (
v,
(i + 1),
Z);
set w1 =
<:(diff (u,(i + 1),Z)),(diff (v,(i + 1),Z)):>;
diff (
u,
(i + 1),
Z)
= (diff (u,i,Z)) `| Z
by NDIFF_6:13;
then A14:
dom (diff (u,(i + 1),Z)) = Z
by A13, NDIFF_1:def 9;
diff (
v,
(i + 1),
Z)
= (diff (v,i,Z)) `| Z
by NDIFF_6:13;
then A15:
dom (diff (v,(i + 1),Z)) = Z
by A13, NDIFF_1:def 9;
A16:
dom <:(diff (u,(i + 1),Z)),(diff (v,(i + 1),Z)):> =
(dom (diff (u,(i + 1),Z))) /\ (dom (diff (v,(i + 1),Z)))
by FUNCT_3:def 7
.=
Z
by A14, A15
;
A17:
[:(rng (diff (u,(i + 1),Z))),(rng (diff (v,(i + 1),Z))):] c= [#] [:(diff_SP ((i + 1),S,E)),(diff_SP ((i + 1),S,F)):]
by ZFMISC_1:96;
rng <:(diff (u,(i + 1),Z)),(diff (v,(i + 1),Z)):> c= [:(rng (diff (u,(i + 1),Z))),(rng (diff (v,(i + 1),Z))):]
by FUNCT_3:51;
then
rng <:(diff (u,(i + 1),Z)),(diff (v,(i + 1),Z)):> c= [#] [:(diff_SP ((i + 1),S,E)),(diff_SP ((i + 1),S,F)):]
by A17, XBOOLE_1:1;
then reconsider w1 =
<:(diff (u,(i + 1),Z)),(diff (v,(i + 1),Z)):> as
PartFunc of
S,
[:(diff_SP ((i + 1),S,E)),(diff_SP ((i + 1),S,F)):] by A16, RELSET_1:4;
A18:
diff (
u,
(i + 1),
Z)
is_differentiable_on Z
by A9, NDIFF_6:14;
A19:
diff (
v,
(i + 1),
Z)
is_differentiable_on Z
by A9, NDIFF_6:14;
consider T1 being
Lipschitzian LinearOperator of
[:(diff_SP (1,S,(diff_SP ((i + 1),S,E)))),(diff_SP (1,S,(diff_SP ((i + 1),S,F)))):],
(diff_SP (1,S,[:(diff_SP ((i + 1),S,E)),(diff_SP ((i + 1),S,F)):])) such that A20:
(
T1 = CTP (
S,
(diff_SP (0,S,(diff_SP ((i + 1),S,E)))),
(diff_SP (0,S,(diff_SP ((i + 1),S,F))))) &
diff (
w1,1,
Z)
= T1 * <:(diff ((diff (u,(i + 1),Z)),1,Z)),(diff ((diff (v,(i + 1),Z)),1,Z)):> )
by A18, A19, Th58;
A21:
diff (
(diff (u,(i + 1),Z)),1,
Z) =
((diff (u,(i + 1),Z)) | Z) `| Z
by NDIFF_6:11
.=
(diff (u,(i + 1),Z)) `| Z
by A9, Th4, NDIFF_6:14
.=
diff (
u,
((i + 1) + 1),
Z)
by NDIFF_6:13
;
A22:
diff (
(diff (v,(i + 1),Z)),1,
Z) =
((diff (v,(i + 1),Z)) | Z) `| Z
by NDIFF_6:11
.=
(diff (v,(i + 1),Z)) `| Z
by NDIFF_6:14, A9, Th4
.=
diff (
v,
((i + 1) + 1),
Z)
by NDIFF_6:13
;
A23:
diff_SP (
0,
S,
[:(diff_SP ((i + 1),S,E)),(diff_SP ((i + 1),S,F)):])
= [:(diff_SP ((i + 1),S,E)),(diff_SP ((i + 1),S,F)):]
by NDIFF_6:7;
A24:
diff (
w1,
0,
Z)
= w1 | Z
by NDIFF_6:11;
then A25:
w1 | Z is_differentiable_on Z
by A18, A19, A23, Th58;
w1 is_differentiable_on Z
by Th3, A25;
then A26:
w1 is_differentiable_on 1,
Z
by A18, A19, A23, A24, Th58, NDIFF_6:15;
(
T0 * w1 is_differentiable_on 1,
Z &
diff (
(T0 * w1),1,
Z)
= (LTRN (1,T0,S)) * (diff (w1,1,Z)) )
by A26, Th25;
then A27:
(
Z c= dom (diff (w,(i + 1),Z)) &
(diff (w,(i + 1),Z)) | Z is_differentiable_on Z )
by A12, NDIFF_6:15;
then A28:
diff (
w,
(i + 1),
Z)
is_differentiable_on Z
;
for
k being
Nat st
k <= ((i + 1) + 1) - 1 holds
diff (
w,
k,
Z)
is_differentiable_on Z
hence
w is_differentiable_on (i + 1) + 1,
Z
by A11, NDIFF_6:14;
ex T being Lipschitzian LinearOperator of [:(diff_SP (((i + 1) + 1),S,E)),(diff_SP (((i + 1) + 1),S,F)):],(diff_SP (((i + 1) + 1),S,[:E,F:])) st diff (w,((i + 1) + 1),Z) = T * <:(diff (u,((i + 1) + 1),Z)),(diff (v,((i + 1) + 1),Z)):>
set L3 =
LTRN (1,
T0,
S);
A30:
(diff_SP (S,(diff_SP ((i + 1),S,E)))) . 1 =
R_NormSpace_of_BoundedLinearOperators (
S,
(diff_SP ((i + 1),S,E)))
by NDIFF_6:7
.=
diff_SP (
((i + 1) + 1),
S,
E)
by NDIFF_6:10
;
A31:
(diff_SP (S,(diff_SP ((i + 1),S,F)))) . 1 =
R_NormSpace_of_BoundedLinearOperators (
S,
(diff_SP ((i + 1),S,F)))
by NDIFF_6:7
.=
diff_SP (
((i + 1) + 1),
S,
F)
by NDIFF_6:10
;
A32:
diff_SP (1,
S,
(diff_SP ((i + 1),S,[:E,F:]))) =
R_NormSpace_of_BoundedLinearOperators (
S,
(diff_SP ((i + 1),S,[:E,F:])))
by NDIFF_6:7
.=
diff_SP (
((i + 1) + 1),
S,
[:E,F:])
by NDIFF_6:10
;
reconsider T3 =
(LTRN (1,T0,S)) * T1 as
Lipschitzian LinearOperator of
[:(diff_SP (((i + 1) + 1),S,E)),(diff_SP (((i + 1) + 1),S,F)):],
(diff_SP (((i + 1) + 1),S,[:E,F:])) by A30, A31, A32, LOPBAN_2:2;
take
T3
;
diff (w,((i + 1) + 1),Z) = T3 * <:(diff (u,((i + 1) + 1),Z)),(diff (v,((i + 1) + 1),Z)):>
thus diff (
w,
((i + 1) + 1),
Z) =
(diff (w,(i + 1),Z)) `| Z
by NDIFF_6:13
.=
((diff (w,(i + 1),Z)) | Z) `| Z
by A28, Th4
.=
diff (
(diff (w,(i + 1),Z)),1,
Z)
by NDIFF_6:11
.=
(LTRN (1,T0,S)) * (diff (w1,1,Z))
by A12, A26, Th25
.=
T3 * <:(diff (u,((i + 1) + 1),Z)),(diff (v,((i + 1) + 1),Z)):>
by A20, A21, A22, RELAT_1:36
;
verum
end;
for i being Nat holds S1[i]
from NAT_1:sch 2(A1, A7);
hence
for i being Nat
for S, E, F being RealNormSpace
for u being PartFunc of S,E
for v being PartFunc of S,F
for w being PartFunc of S,[:E,F:]
for Z being Subset of S st w = <:u,v:> & u is_differentiable_on i + 1,Z & v is_differentiable_on i + 1,Z holds
( w is_differentiable_on i + 1,Z & ex T being Lipschitzian LinearOperator of [:(diff_SP ((i + 1),S,E)),(diff_SP ((i + 1),S,F)):],(diff_SP ((i + 1),S,[:E,F:])) st diff (w,(i + 1),Z) = T * <:(diff (u,(i + 1),Z)),(diff (v,(i + 1),Z)):> )
; verum