Metamath Proof Explorer

Theorem itgsubstlem

Description: Lemma for itgsubst . (Contributed by Mario Carneiro, 12-Sep-2014)

Ref Expression
Hypotheses itgsubst.x 
|- ( ph -> X e. RR )
itgsubst.y 
|- ( ph -> Y e. RR )
itgsubst.le 
|- ( ph -> X <_ Y )
itgsubst.z 
|- ( ph -> Z e. RR* )
itgsubst.w 
|- ( ph -> W e. RR* )
itgsubst.a 
|- ( ph -> ( x e. ( X [,] Y ) |-> A ) e. ( ( X [,] Y ) -cn-> ( Z (,) W ) ) )
itgsubst.b 
|- ( ph -> ( x e. ( X (,) Y ) |-> B ) e. ( ( ( X (,) Y ) -cn-> CC ) i^i L^1 ) )
itgsubst.c 
|- ( ph -> ( u e. ( Z (,) W ) |-> C ) e. ( ( Z (,) W ) -cn-> CC ) )
itgsubst.da 
|- ( ph -> ( RR _D ( x e. ( X [,] Y ) |-> A ) ) = ( x e. ( X (,) Y ) |-> B ) )
itgsubst.e 
|- ( u = A -> C = E )
itgsubst.k 
|- ( x = X -> A = K )
itgsubst.l 
|- ( x = Y -> A = L )
itgsubst.m 
|- ( ph -> M e. ( Z (,) W ) )
itgsubst.n 
|- ( ph -> N e. ( Z (,) W ) )
itgsubst.cl2 
|- ( ( ph /\ x e. ( X [,] Y ) ) -> A e. ( M (,) N ) )
Assertion itgsubstlem 
|- ( ph -> S_ [ K -> L ] C _d u = S_ [ X -> Y ] ( E x. B ) _d x )

Proof

Step Hyp Ref Expression
1 itgsubst.x 
 |-  ( ph -> X e. RR )
2 itgsubst.y 
 |-  ( ph -> Y e. RR )
3 itgsubst.le 
 |-  ( ph -> X <_ Y )
4 itgsubst.z 
 |-  ( ph -> Z e. RR* )
5 itgsubst.w 
 |-  ( ph -> W e. RR* )
6 itgsubst.a 
 |-  ( ph -> ( x e. ( X [,] Y ) |-> A ) e. ( ( X [,] Y ) -cn-> ( Z (,) W ) ) )
7 itgsubst.b 
 |-  ( ph -> ( x e. ( X (,) Y ) |-> B ) e. ( ( ( X (,) Y ) -cn-> CC ) i^i L^1 ) )
8 itgsubst.c 
 |-  ( ph -> ( u e. ( Z (,) W ) |-> C ) e. ( ( Z (,) W ) -cn-> CC ) )
9 itgsubst.da 
 |-  ( ph -> ( RR _D ( x e. ( X [,] Y ) |-> A ) ) = ( x e. ( X (,) Y ) |-> B ) )
10 itgsubst.e 
 |-  ( u = A -> C = E )
11 itgsubst.k 
 |-  ( x = X -> A = K )
12 itgsubst.l 
 |-  ( x = Y -> A = L )
13 itgsubst.m 
 |-  ( ph -> M e. ( Z (,) W ) )
14 itgsubst.n 
 |-  ( ph -> N e. ( Z (,) W ) )
15 itgsubst.cl2 
 |-  ( ( ph /\ x e. ( X [,] Y ) ) -> A e. ( M (,) N ) )
16 3 ditgpos 
 |-  ( ph -> S_ [ X -> Y ] ( E x. B ) _d x = S. ( X (,) Y ) ( E x. B ) _d x )
17 ax-resscn 
 |-  RR C_ CC
18 17 a1i 
 |-  ( ph -> RR C_ CC )
19 iccssre 
 |-  ( ( X e. RR /\ Y e. RR ) -> ( X [,] Y ) C_ RR )
20 1 2 19 syl2anc 
 |-  ( ph -> ( X [,] Y ) C_ RR )
21 eqidd 
 |-  ( ph -> ( x e. ( X [,] Y ) |-> A ) = ( x e. ( X [,] Y ) |-> A ) )
22 eqidd 
 |-  ( ph -> ( v e. ( M (,) N ) |-> S. ( M (,) v ) C _d u ) = ( v e. ( M (,) N ) |-> S. ( M (,) v ) C _d u ) )
23 oveq2 
 |-  ( v = A -> ( M (,) v ) = ( M (,) A ) )
24 itgeq1 
 |-  ( ( M (,) v ) = ( M (,) A ) -> S. ( M (,) v ) C _d u = S. ( M (,) A ) C _d u )
25 23 24 syl 
 |-  ( v = A -> S. ( M (,) v ) C _d u = S. ( M (,) A ) C _d u )
26 15 21 22 25 fmptco 
 |-  ( ph -> ( ( v e. ( M (,) N ) |-> S. ( M (,) v ) C _d u ) o. ( x e. ( X [,] Y ) |-> A ) ) = ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) )
27 15 fmpttd 
 |-  ( ph -> ( x e. ( X [,] Y ) |-> A ) : ( X [,] Y ) --> ( M (,) N ) )
28 ioossicc 
 |-  ( M (,) N ) C_ ( M [,] N )
29 eliooord 
 |-  ( M e. ( Z (,) W ) -> ( Z < M /\ M < W ) )
30 13 29 syl 
 |-  ( ph -> ( Z < M /\ M < W ) )
31 30 simpld 
 |-  ( ph -> Z < M )
32 eliooord 
 |-  ( N e. ( Z (,) W ) -> ( Z < N /\ N < W ) )
33 14 32 syl 
 |-  ( ph -> ( Z < N /\ N < W ) )
34 33 simprd 
 |-  ( ph -> N < W )
35 iccssioo 
 |-  ( ( ( Z e. RR* /\ W e. RR* ) /\ ( Z < M /\ N < W ) ) -> ( M [,] N ) C_ ( Z (,) W ) )
36 4 5 31 34 35 syl22anc 
 |-  ( ph -> ( M [,] N ) C_ ( Z (,) W ) )
37 28 36 sstrid 
 |-  ( ph -> ( M (,) N ) C_ ( Z (,) W ) )
38 ioossre 
 |-  ( Z (,) W ) C_ RR
39 38 a1i 
 |-  ( ph -> ( Z (,) W ) C_ RR )
40 39 17 sstrdi 
 |-  ( ph -> ( Z (,) W ) C_ CC )
41 37 40 sstrd 
 |-  ( ph -> ( M (,) N ) C_ CC )
42 cncfcdm 
 |-  ( ( ( M (,) N ) C_ CC /\ ( x e. ( X [,] Y ) |-> A ) e. ( ( X [,] Y ) -cn-> ( Z (,) W ) ) ) -> ( ( x e. ( X [,] Y ) |-> A ) e. ( ( X [,] Y ) -cn-> ( M (,) N ) ) <-> ( x e. ( X [,] Y ) |-> A ) : ( X [,] Y ) --> ( M (,) N ) ) )
43 41 6 42 syl2anc 
 |-  ( ph -> ( ( x e. ( X [,] Y ) |-> A ) e. ( ( X [,] Y ) -cn-> ( M (,) N ) ) <-> ( x e. ( X [,] Y ) |-> A ) : ( X [,] Y ) --> ( M (,) N ) ) )
44 27 43 mpbird 
 |-  ( ph -> ( x e. ( X [,] Y ) |-> A ) e. ( ( X [,] Y ) -cn-> ( M (,) N ) ) )
45 28 sseli 
 |-  ( v e. ( M (,) N ) -> v e. ( M [,] N ) )
46 38 14 sselid 
 |-  ( ph -> N e. RR )
47 46 rexrd 
 |-  ( ph -> N e. RR* )
48 47 adantr 
 |-  ( ( ph /\ v e. ( M [,] N ) ) -> N e. RR* )
49 38 13 sselid 
 |-  ( ph -> M e. RR )
50 elicc2 
 |-  ( ( M e. RR /\ N e. RR ) -> ( v e. ( M [,] N ) <-> ( v e. RR /\ M <_ v /\ v <_ N ) ) )
51 49 46 50 syl2anc 
 |-  ( ph -> ( v e. ( M [,] N ) <-> ( v e. RR /\ M <_ v /\ v <_ N ) ) )
52 51 biimpa 
 |-  ( ( ph /\ v e. ( M [,] N ) ) -> ( v e. RR /\ M <_ v /\ v <_ N ) )
53 52 simp3d 
 |-  ( ( ph /\ v e. ( M [,] N ) ) -> v <_ N )
54 iooss2 
 |-  ( ( N e. RR* /\ v <_ N ) -> ( M (,) v ) C_ ( M (,) N ) )
55 48 53 54 syl2anc 
 |-  ( ( ph /\ v e. ( M [,] N ) ) -> ( M (,) v ) C_ ( M (,) N ) )
56 55 sselda 
 |-  ( ( ( ph /\ v e. ( M [,] N ) ) /\ u e. ( M (,) v ) ) -> u e. ( M (,) N ) )
57 37 sselda 
 |-  ( ( ph /\ u e. ( M (,) N ) ) -> u e. ( Z (,) W ) )
58 cncff 
 |-  ( ( u e. ( Z (,) W ) |-> C ) e. ( ( Z (,) W ) -cn-> CC ) -> ( u e. ( Z (,) W ) |-> C ) : ( Z (,) W ) --> CC )
59 8 58 syl 
 |-  ( ph -> ( u e. ( Z (,) W ) |-> C ) : ( Z (,) W ) --> CC )
60 59 fvmptelcdm 
 |-  ( ( ph /\ u e. ( Z (,) W ) ) -> C e. CC )
61 57 60 syldan 
 |-  ( ( ph /\ u e. ( M (,) N ) ) -> C e. CC )
62 61 adantlr 
 |-  ( ( ( ph /\ v e. ( M [,] N ) ) /\ u e. ( M (,) N ) ) -> C e. CC )
63 56 62 syldan 
 |-  ( ( ( ph /\ v e. ( M [,] N ) ) /\ u e. ( M (,) v ) ) -> C e. CC )
64 ioombl 
 |-  ( M (,) v ) e. dom vol
65 64 a1i 
 |-  ( ( ph /\ v e. ( M [,] N ) ) -> ( M (,) v ) e. dom vol )
66 28 a1i 
 |-  ( ph -> ( M (,) N ) C_ ( M [,] N ) )
67 ioombl 
 |-  ( M (,) N ) e. dom vol
68 67 a1i 
 |-  ( ph -> ( M (,) N ) e. dom vol )
69 36 sselda 
 |-  ( ( ph /\ u e. ( M [,] N ) ) -> u e. ( Z (,) W ) )
70 69 60 syldan 
 |-  ( ( ph /\ u e. ( M [,] N ) ) -> C e. CC )
71 36 resmptd 
 |-  ( ph -> ( ( u e. ( Z (,) W ) |-> C ) |` ( M [,] N ) ) = ( u e. ( M [,] N ) |-> C ) )
72 rescncf 
 |-  ( ( M [,] N ) C_ ( Z (,) W ) -> ( ( u e. ( Z (,) W ) |-> C ) e. ( ( Z (,) W ) -cn-> CC ) -> ( ( u e. ( Z (,) W ) |-> C ) |` ( M [,] N ) ) e. ( ( M [,] N ) -cn-> CC ) ) )
73 36 8 72 sylc 
 |-  ( ph -> ( ( u e. ( Z (,) W ) |-> C ) |` ( M [,] N ) ) e. ( ( M [,] N ) -cn-> CC ) )
74 71 73 eqeltrrd 
 |-  ( ph -> ( u e. ( M [,] N ) |-> C ) e. ( ( M [,] N ) -cn-> CC ) )
75 cniccibl 
 |-  ( ( M e. RR /\ N e. RR /\ ( u e. ( M [,] N ) |-> C ) e. ( ( M [,] N ) -cn-> CC ) ) -> ( u e. ( M [,] N ) |-> C ) e. L^1 )
76 49 46 74 75 syl3anc 
 |-  ( ph -> ( u e. ( M [,] N ) |-> C ) e. L^1 )
77 66 68 70 76 iblss 
 |-  ( ph -> ( u e. ( M (,) N ) |-> C ) e. L^1 )
78 77 adantr 
 |-  ( ( ph /\ v e. ( M [,] N ) ) -> ( u e. ( M (,) N ) |-> C ) e. L^1 )
79 55 65 62 78 iblss 
 |-  ( ( ph /\ v e. ( M [,] N ) ) -> ( u e. ( M (,) v ) |-> C ) e. L^1 )
80 63 79 itgcl 
 |-  ( ( ph /\ v e. ( M [,] N ) ) -> S. ( M (,) v ) C _d u e. CC )
81 45 80 sylan2 
 |-  ( ( ph /\ v e. ( M (,) N ) ) -> S. ( M (,) v ) C _d u e. CC )
82 81 fmpttd 
 |-  ( ph -> ( v e. ( M (,) N ) |-> S. ( M (,) v ) C _d u ) : ( M (,) N ) --> CC )
83 37 38 sstrdi 
 |-  ( ph -> ( M (,) N ) C_ RR )
84 fveq2 
 |-  ( t = u -> ( ( u e. ( M (,) N ) |-> C ) ` t ) = ( ( u e. ( M (,) N ) |-> C ) ` u ) )
85 nffvmpt1 
 |-  F/_ u ( ( u e. ( M (,) N ) |-> C ) ` t )
86 nfcv 
 |-  F/_ t ( ( u e. ( M (,) N ) |-> C ) ` u )
87 84 85 86 cbvitg 
 |-  S. ( M (,) v ) ( ( u e. ( M (,) N ) |-> C ) ` t ) _d t = S. ( M (,) v ) ( ( u e. ( M (,) N ) |-> C ) ` u ) _d u
88 eqid 
 |-  ( u e. ( M (,) N ) |-> C ) = ( u e. ( M (,) N ) |-> C )
89 88 fvmpt2 
 |-  ( ( u e. ( M (,) N ) /\ C e. CC ) -> ( ( u e. ( M (,) N ) |-> C ) ` u ) = C )
90 56 63 89 syl2anc 
 |-  ( ( ( ph /\ v e. ( M [,] N ) ) /\ u e. ( M (,) v ) ) -> ( ( u e. ( M (,) N ) |-> C ) ` u ) = C )
91 90 itgeq2dv 
 |-  ( ( ph /\ v e. ( M [,] N ) ) -> S. ( M (,) v ) ( ( u e. ( M (,) N ) |-> C ) ` u ) _d u = S. ( M (,) v ) C _d u )
92 87 91 eqtrid 
 |-  ( ( ph /\ v e. ( M [,] N ) ) -> S. ( M (,) v ) ( ( u e. ( M (,) N ) |-> C ) ` t ) _d t = S. ( M (,) v ) C _d u )
93 92 mpteq2dva 
 |-  ( ph -> ( v e. ( M [,] N ) |-> S. ( M (,) v ) ( ( u e. ( M (,) N ) |-> C ) ` t ) _d t ) = ( v e. ( M [,] N ) |-> S. ( M (,) v ) C _d u ) )
94 93 oveq2d 
 |-  ( ph -> ( RR _D ( v e. ( M [,] N ) |-> S. ( M (,) v ) ( ( u e. ( M (,) N ) |-> C ) ` t ) _d t ) ) = ( RR _D ( v e. ( M [,] N ) |-> S. ( M (,) v ) C _d u ) ) )
95 eqid 
 |-  ( v e. ( M [,] N ) |-> S. ( M (,) v ) ( ( u e. ( M (,) N ) |-> C ) ` t ) _d t ) = ( v e. ( M [,] N ) |-> S. ( M (,) v ) ( ( u e. ( M (,) N ) |-> C ) ` t ) _d t )
96 1 rexrd 
 |-  ( ph -> X e. RR* )
97 2 rexrd 
 |-  ( ph -> Y e. RR* )
98 lbicc2 
 |-  ( ( X e. RR* /\ Y e. RR* /\ X <_ Y ) -> X e. ( X [,] Y ) )
99 96 97 3 98 syl3anc 
 |-  ( ph -> X e. ( X [,] Y ) )
100 n0i 
 |-  ( X e. ( X [,] Y ) -> -. ( X [,] Y ) = (/) )
101 99 100 syl 
 |-  ( ph -> -. ( X [,] Y ) = (/) )
102 feq3 
 |-  ( ( M (,) N ) = (/) -> ( ( x e. ( X [,] Y ) |-> A ) : ( X [,] Y ) --> ( M (,) N ) <-> ( x e. ( X [,] Y ) |-> A ) : ( X [,] Y ) --> (/) ) )
103 27 102 syl5ibcom 
 |-  ( ph -> ( ( M (,) N ) = (/) -> ( x e. ( X [,] Y ) |-> A ) : ( X [,] Y ) --> (/) ) )
104 f00 
 |-  ( ( x e. ( X [,] Y ) |-> A ) : ( X [,] Y ) --> (/) <-> ( ( x e. ( X [,] Y ) |-> A ) = (/) /\ ( X [,] Y ) = (/) ) )
105 104 simprbi 
 |-  ( ( x e. ( X [,] Y ) |-> A ) : ( X [,] Y ) --> (/) -> ( X [,] Y ) = (/) )
106 103 105 syl6 
 |-  ( ph -> ( ( M (,) N ) = (/) -> ( X [,] Y ) = (/) ) )
107 101 106 mtod 
 |-  ( ph -> -. ( M (,) N ) = (/) )
108 49 rexrd 
 |-  ( ph -> M e. RR* )
109 ioo0 
 |-  ( ( M e. RR* /\ N e. RR* ) -> ( ( M (,) N ) = (/) <-> N <_ M ) )
110 108 47 109 syl2anc 
 |-  ( ph -> ( ( M (,) N ) = (/) <-> N <_ M ) )
111 107 110 mtbid 
 |-  ( ph -> -. N <_ M )
112 46 49 letrid 
 |-  ( ph -> ( N <_ M \/ M <_ N ) )
113 112 ord 
 |-  ( ph -> ( -. N <_ M -> M <_ N ) )
114 111 113 mpd 
 |-  ( ph -> M <_ N )
115 resmpt 
 |-  ( ( M (,) N ) C_ ( M [,] N ) -> ( ( u e. ( M [,] N ) |-> C ) |` ( M (,) N ) ) = ( u e. ( M (,) N ) |-> C ) )
116 28 115 ax-mp 
 |-  ( ( u e. ( M [,] N ) |-> C ) |` ( M (,) N ) ) = ( u e. ( M (,) N ) |-> C )
117 rescncf 
 |-  ( ( M (,) N ) C_ ( M [,] N ) -> ( ( u e. ( M [,] N ) |-> C ) e. ( ( M [,] N ) -cn-> CC ) -> ( ( u e. ( M [,] N ) |-> C ) |` ( M (,) N ) ) e. ( ( M (,) N ) -cn-> CC ) ) )
118 28 74 117 mpsyl 
 |-  ( ph -> ( ( u e. ( M [,] N ) |-> C ) |` ( M (,) N ) ) e. ( ( M (,) N ) -cn-> CC ) )
119 116 118 eqeltrrid 
 |-  ( ph -> ( u e. ( M (,) N ) |-> C ) e. ( ( M (,) N ) -cn-> CC ) )
120 95 49 46 114 119 77 ftc1cn 
 |-  ( ph -> ( RR _D ( v e. ( M [,] N ) |-> S. ( M (,) v ) ( ( u e. ( M (,) N ) |-> C ) ` t ) _d t ) ) = ( u e. ( M (,) N ) |-> C ) )
121 36 38 sstrdi 
 |-  ( ph -> ( M [,] N ) C_ RR )
122 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
123 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
124 iccntr 
 |-  ( ( M e. RR /\ N e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( M [,] N ) ) = ( M (,) N ) )
125 49 46 124 syl2anc 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( M [,] N ) ) = ( M (,) N ) )
126 18 121 80 122 123 125 dvmptntr 
 |-  ( ph -> ( RR _D ( v e. ( M [,] N ) |-> S. ( M (,) v ) C _d u ) ) = ( RR _D ( v e. ( M (,) N ) |-> S. ( M (,) v ) C _d u ) ) )
127 94 120 126 3eqtr3rd 
 |-  ( ph -> ( RR _D ( v e. ( M (,) N ) |-> S. ( M (,) v ) C _d u ) ) = ( u e. ( M (,) N ) |-> C ) )
128 127 dmeqd 
 |-  ( ph -> dom ( RR _D ( v e. ( M (,) N ) |-> S. ( M (,) v ) C _d u ) ) = dom ( u e. ( M (,) N ) |-> C ) )
129 88 61 dmmptd 
 |-  ( ph -> dom ( u e. ( M (,) N ) |-> C ) = ( M (,) N ) )
130 128 129 eqtrd 
 |-  ( ph -> dom ( RR _D ( v e. ( M (,) N ) |-> S. ( M (,) v ) C _d u ) ) = ( M (,) N ) )
131 dvcn 
 |-  ( ( ( RR C_ CC /\ ( v e. ( M (,) N ) |-> S. ( M (,) v ) C _d u ) : ( M (,) N ) --> CC /\ ( M (,) N ) C_ RR ) /\ dom ( RR _D ( v e. ( M (,) N ) |-> S. ( M (,) v ) C _d u ) ) = ( M (,) N ) ) -> ( v e. ( M (,) N ) |-> S. ( M (,) v ) C _d u ) e. ( ( M (,) N ) -cn-> CC ) )
132 18 82 83 130 131 syl31anc 
 |-  ( ph -> ( v e. ( M (,) N ) |-> S. ( M (,) v ) C _d u ) e. ( ( M (,) N ) -cn-> CC ) )
133 44 132 cncfco 
 |-  ( ph -> ( ( v e. ( M (,) N ) |-> S. ( M (,) v ) C _d u ) o. ( x e. ( X [,] Y ) |-> A ) ) e. ( ( X [,] Y ) -cn-> CC ) )
134 26 133 eqeltrrd 
 |-  ( ph -> ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) e. ( ( X [,] Y ) -cn-> CC ) )
135 cncff 
 |-  ( ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) e. ( ( X [,] Y ) -cn-> CC ) -> ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) : ( X [,] Y ) --> CC )
136 134 135 syl 
 |-  ( ph -> ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) : ( X [,] Y ) --> CC )
137 136 fvmptelcdm 
 |-  ( ( ph /\ x e. ( X [,] Y ) ) -> S. ( M (,) A ) C _d u e. CC )
138 iccntr 
 |-  ( ( X e. RR /\ Y e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( X [,] Y ) ) = ( X (,) Y ) )
139 1 2 138 syl2anc 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( X [,] Y ) ) = ( X (,) Y ) )
140 18 20 137 122 123 139 dvmptntr 
 |-  ( ph -> ( RR _D ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) ) = ( RR _D ( x e. ( X (,) Y ) |-> S. ( M (,) A ) C _d u ) ) )
141 reelprrecn 
 |-  RR e. { RR , CC }
142 141 a1i 
 |-  ( ph -> RR e. { RR , CC } )
143 ioossicc 
 |-  ( X (,) Y ) C_ ( X [,] Y )
144 143 sseli 
 |-  ( x e. ( X (,) Y ) -> x e. ( X [,] Y ) )
145 144 15 sylan2 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> A e. ( M (,) N ) )
146 elin 
 |-  ( ( x e. ( X (,) Y ) |-> B ) e. ( ( ( X (,) Y ) -cn-> CC ) i^i L^1 ) <-> ( ( x e. ( X (,) Y ) |-> B ) e. ( ( X (,) Y ) -cn-> CC ) /\ ( x e. ( X (,) Y ) |-> B ) e. L^1 ) )
147 7 146 sylib 
 |-  ( ph -> ( ( x e. ( X (,) Y ) |-> B ) e. ( ( X (,) Y ) -cn-> CC ) /\ ( x e. ( X (,) Y ) |-> B ) e. L^1 ) )
148 147 simpld 
 |-  ( ph -> ( x e. ( X (,) Y ) |-> B ) e. ( ( X (,) Y ) -cn-> CC ) )
149 cncff 
 |-  ( ( x e. ( X (,) Y ) |-> B ) e. ( ( X (,) Y ) -cn-> CC ) -> ( x e. ( X (,) Y ) |-> B ) : ( X (,) Y ) --> CC )
150 148 149 syl 
 |-  ( ph -> ( x e. ( X (,) Y ) |-> B ) : ( X (,) Y ) --> CC )
151 150 fvmptelcdm 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> B e. CC )
152 61 fmpttd 
 |-  ( ph -> ( u e. ( M (,) N ) |-> C ) : ( M (,) N ) --> CC )
153 nfcv 
 |-  F/_ v C
154 nfcsb1v 
 |-  F/_ u [_ v / u ]_ C
155 csbeq1a 
 |-  ( u = v -> C = [_ v / u ]_ C )
156 153 154 155 cbvmpt 
 |-  ( u e. ( M (,) N ) |-> C ) = ( v e. ( M (,) N ) |-> [_ v / u ]_ C )
157 156 fmpt 
 |-  ( A. v e. ( M (,) N ) [_ v / u ]_ C e. CC <-> ( u e. ( M (,) N ) |-> C ) : ( M (,) N ) --> CC )
158 152 157 sylibr 
 |-  ( ph -> A. v e. ( M (,) N ) [_ v / u ]_ C e. CC )
159 158 r19.21bi 
 |-  ( ( ph /\ v e. ( M (,) N ) ) -> [_ v / u ]_ C e. CC )
160 38 17 sstri 
 |-  ( Z (,) W ) C_ CC
161 cncff 
 |-  ( ( x e. ( X [,] Y ) |-> A ) e. ( ( X [,] Y ) -cn-> ( Z (,) W ) ) -> ( x e. ( X [,] Y ) |-> A ) : ( X [,] Y ) --> ( Z (,) W ) )
162 6 161 syl 
 |-  ( ph -> ( x e. ( X [,] Y ) |-> A ) : ( X [,] Y ) --> ( Z (,) W ) )
163 162 fvmptelcdm 
 |-  ( ( ph /\ x e. ( X [,] Y ) ) -> A e. ( Z (,) W ) )
164 160 163 sselid 
 |-  ( ( ph /\ x e. ( X [,] Y ) ) -> A e. CC )
165 18 20 164 122 123 139 dvmptntr 
 |-  ( ph -> ( RR _D ( x e. ( X [,] Y ) |-> A ) ) = ( RR _D ( x e. ( X (,) Y ) |-> A ) ) )
166 165 9 eqtr3d 
 |-  ( ph -> ( RR _D ( x e. ( X (,) Y ) |-> A ) ) = ( x e. ( X (,) Y ) |-> B ) )
167 127 156 eqtrdi 
 |-  ( ph -> ( RR _D ( v e. ( M (,) N ) |-> S. ( M (,) v ) C _d u ) ) = ( v e. ( M (,) N ) |-> [_ v / u ]_ C ) )
168 csbeq1 
 |-  ( v = A -> [_ v / u ]_ C = [_ A / u ]_ C )
169 142 142 145 151 81 159 166 167 25 168 dvmptco 
 |-  ( ph -> ( RR _D ( x e. ( X (,) Y ) |-> S. ( M (,) A ) C _d u ) ) = ( x e. ( X (,) Y ) |-> ( [_ A / u ]_ C x. B ) ) )
170 nfcvd 
 |-  ( A e. ( M (,) N ) -> F/_ u E )
171 170 10 csbiegf 
 |-  ( A e. ( M (,) N ) -> [_ A / u ]_ C = E )
172 145 171 syl 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> [_ A / u ]_ C = E )
173 172 oveq1d 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> ( [_ A / u ]_ C x. B ) = ( E x. B ) )
174 173 mpteq2dva 
 |-  ( ph -> ( x e. ( X (,) Y ) |-> ( [_ A / u ]_ C x. B ) ) = ( x e. ( X (,) Y ) |-> ( E x. B ) ) )
175 140 169 174 3eqtrd 
 |-  ( ph -> ( RR _D ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) ) = ( x e. ( X (,) Y ) |-> ( E x. B ) ) )
176 resmpt 
 |-  ( ( X (,) Y ) C_ ( X [,] Y ) -> ( ( x e. ( X [,] Y ) |-> E ) |` ( X (,) Y ) ) = ( x e. ( X (,) Y ) |-> E ) )
177 143 176 ax-mp 
 |-  ( ( x e. ( X [,] Y ) |-> E ) |` ( X (,) Y ) ) = ( x e. ( X (,) Y ) |-> E )
178 eqidd 
 |-  ( ph -> ( u e. ( Z (,) W ) |-> C ) = ( u e. ( Z (,) W ) |-> C ) )
179 163 21 178 10 fmptco 
 |-  ( ph -> ( ( u e. ( Z (,) W ) |-> C ) o. ( x e. ( X [,] Y ) |-> A ) ) = ( x e. ( X [,] Y ) |-> E ) )
180 6 8 cncfco 
 |-  ( ph -> ( ( u e. ( Z (,) W ) |-> C ) o. ( x e. ( X [,] Y ) |-> A ) ) e. ( ( X [,] Y ) -cn-> CC ) )
181 179 180 eqeltrrd 
 |-  ( ph -> ( x e. ( X [,] Y ) |-> E ) e. ( ( X [,] Y ) -cn-> CC ) )
182 rescncf 
 |-  ( ( X (,) Y ) C_ ( X [,] Y ) -> ( ( x e. ( X [,] Y ) |-> E ) e. ( ( X [,] Y ) -cn-> CC ) -> ( ( x e. ( X [,] Y ) |-> E ) |` ( X (,) Y ) ) e. ( ( X (,) Y ) -cn-> CC ) ) )
183 143 181 182 mpsyl 
 |-  ( ph -> ( ( x e. ( X [,] Y ) |-> E ) |` ( X (,) Y ) ) e. ( ( X (,) Y ) -cn-> CC ) )
184 177 183 eqeltrrid 
 |-  ( ph -> ( x e. ( X (,) Y ) |-> E ) e. ( ( X (,) Y ) -cn-> CC ) )
185 184 148 mulcncf 
 |-  ( ph -> ( x e. ( X (,) Y ) |-> ( E x. B ) ) e. ( ( X (,) Y ) -cn-> CC ) )
186 175 185 eqeltrd 
 |-  ( ph -> ( RR _D ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) ) e. ( ( X (,) Y ) -cn-> CC ) )
187 ioombl 
 |-  ( X (,) Y ) e. dom vol
188 187 a1i 
 |-  ( ph -> ( X (,) Y ) e. dom vol )
189 fco 
 |-  ( ( ( u e. ( Z (,) W ) |-> C ) : ( Z (,) W ) --> CC /\ ( x e. ( X [,] Y ) |-> A ) : ( X [,] Y ) --> ( Z (,) W ) ) -> ( ( u e. ( Z (,) W ) |-> C ) o. ( x e. ( X [,] Y ) |-> A ) ) : ( X [,] Y ) --> CC )
190 59 162 189 syl2anc 
 |-  ( ph -> ( ( u e. ( Z (,) W ) |-> C ) o. ( x e. ( X [,] Y ) |-> A ) ) : ( X [,] Y ) --> CC )
191 179 feq1d 
 |-  ( ph -> ( ( ( u e. ( Z (,) W ) |-> C ) o. ( x e. ( X [,] Y ) |-> A ) ) : ( X [,] Y ) --> CC <-> ( x e. ( X [,] Y ) |-> E ) : ( X [,] Y ) --> CC ) )
192 190 191 mpbid 
 |-  ( ph -> ( x e. ( X [,] Y ) |-> E ) : ( X [,] Y ) --> CC )
193 192 fvmptelcdm 
 |-  ( ( ph /\ x e. ( X [,] Y ) ) -> E e. CC )
194 144 193 sylan2 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> E e. CC )
195 eqidd 
 |-  ( ph -> ( x e. ( X (,) Y ) |-> E ) = ( x e. ( X (,) Y ) |-> E ) )
196 eqidd 
 |-  ( ph -> ( x e. ( X (,) Y ) |-> B ) = ( x e. ( X (,) Y ) |-> B ) )
197 188 194 151 195 196 offval2 
 |-  ( ph -> ( ( x e. ( X (,) Y ) |-> E ) oF x. ( x e. ( X (,) Y ) |-> B ) ) = ( x e. ( X (,) Y ) |-> ( E x. B ) ) )
198 175 197 eqtr4d 
 |-  ( ph -> ( RR _D ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) ) = ( ( x e. ( X (,) Y ) |-> E ) oF x. ( x e. ( X (,) Y ) |-> B ) ) )
199 143 a1i 
 |-  ( ph -> ( X (,) Y ) C_ ( X [,] Y ) )
200 cniccibl 
 |-  ( ( X e. RR /\ Y e. RR /\ ( x e. ( X [,] Y ) |-> E ) e. ( ( X [,] Y ) -cn-> CC ) ) -> ( x e. ( X [,] Y ) |-> E ) e. L^1 )
201 1 2 181 200 syl3anc 
 |-  ( ph -> ( x e. ( X [,] Y ) |-> E ) e. L^1 )
202 199 188 193 201 iblss 
 |-  ( ph -> ( x e. ( X (,) Y ) |-> E ) e. L^1 )
203 iblmbf 
 |-  ( ( x e. ( X (,) Y ) |-> E ) e. L^1 -> ( x e. ( X (,) Y ) |-> E ) e. MblFn )
204 202 203 syl 
 |-  ( ph -> ( x e. ( X (,) Y ) |-> E ) e. MblFn )
205 147 simprd 
 |-  ( ph -> ( x e. ( X (,) Y ) |-> B ) e. L^1 )
206 cniccbdd 
 |-  ( ( X e. RR /\ Y e. RR /\ ( x e. ( X [,] Y ) |-> E ) e. ( ( X [,] Y ) -cn-> CC ) ) -> E. y e. RR A. z e. ( X [,] Y ) ( abs ` ( ( x e. ( X [,] Y ) |-> E ) ` z ) ) <_ y )
207 1 2 181 206 syl3anc 
 |-  ( ph -> E. y e. RR A. z e. ( X [,] Y ) ( abs ` ( ( x e. ( X [,] Y ) |-> E ) ` z ) ) <_ y )
208 ssralv 
 |-  ( ( X (,) Y ) C_ ( X [,] Y ) -> ( A. z e. ( X [,] Y ) ( abs ` ( ( x e. ( X [,] Y ) |-> E ) ` z ) ) <_ y -> A. z e. ( X (,) Y ) ( abs ` ( ( x e. ( X [,] Y ) |-> E ) ` z ) ) <_ y ) )
209 143 208 ax-mp 
 |-  ( A. z e. ( X [,] Y ) ( abs ` ( ( x e. ( X [,] Y ) |-> E ) ` z ) ) <_ y -> A. z e. ( X (,) Y ) ( abs ` ( ( x e. ( X [,] Y ) |-> E ) ` z ) ) <_ y )
210 eqid 
 |-  ( x e. ( X (,) Y ) |-> E ) = ( x e. ( X (,) Y ) |-> E )
211 210 194 dmmptd 
 |-  ( ph -> dom ( x e. ( X (,) Y ) |-> E ) = ( X (,) Y ) )
212 211 raleqdv 
 |-  ( ph -> ( A. z e. dom ( x e. ( X (,) Y ) |-> E ) ( abs ` ( ( x e. ( X (,) Y ) |-> E ) ` z ) ) <_ y <-> A. z e. ( X (,) Y ) ( abs ` ( ( x e. ( X (,) Y ) |-> E ) ` z ) ) <_ y ) )
213 177 fveq1i 
 |-  ( ( ( x e. ( X [,] Y ) |-> E ) |` ( X (,) Y ) ) ` z ) = ( ( x e. ( X (,) Y ) |-> E ) ` z )
214 fvres 
 |-  ( z e. ( X (,) Y ) -> ( ( ( x e. ( X [,] Y ) |-> E ) |` ( X (,) Y ) ) ` z ) = ( ( x e. ( X [,] Y ) |-> E ) ` z ) )
215 213 214 eqtr3id 
 |-  ( z e. ( X (,) Y ) -> ( ( x e. ( X (,) Y ) |-> E ) ` z ) = ( ( x e. ( X [,] Y ) |-> E ) ` z ) )
216 215 fveq2d 
 |-  ( z e. ( X (,) Y ) -> ( abs ` ( ( x e. ( X (,) Y ) |-> E ) ` z ) ) = ( abs ` ( ( x e. ( X [,] Y ) |-> E ) ` z ) ) )
217 216 breq1d 
 |-  ( z e. ( X (,) Y ) -> ( ( abs ` ( ( x e. ( X (,) Y ) |-> E ) ` z ) ) <_ y <-> ( abs ` ( ( x e. ( X [,] Y ) |-> E ) ` z ) ) <_ y ) )
218 217 ralbiia 
 |-  ( A. z e. ( X (,) Y ) ( abs ` ( ( x e. ( X (,) Y ) |-> E ) ` z ) ) <_ y <-> A. z e. ( X (,) Y ) ( abs ` ( ( x e. ( X [,] Y ) |-> E ) ` z ) ) <_ y )
219 212 218 bitr2di 
 |-  ( ph -> ( A. z e. ( X (,) Y ) ( abs ` ( ( x e. ( X [,] Y ) |-> E ) ` z ) ) <_ y <-> A. z e. dom ( x e. ( X (,) Y ) |-> E ) ( abs ` ( ( x e. ( X (,) Y ) |-> E ) ` z ) ) <_ y ) )
220 209 219 imbitrid 
 |-  ( ph -> ( A. z e. ( X [,] Y ) ( abs ` ( ( x e. ( X [,] Y ) |-> E ) ` z ) ) <_ y -> A. z e. dom ( x e. ( X (,) Y ) |-> E ) ( abs ` ( ( x e. ( X (,) Y ) |-> E ) ` z ) ) <_ y ) )
221 220 reximdv 
 |-  ( ph -> ( E. y e. RR A. z e. ( X [,] Y ) ( abs ` ( ( x e. ( X [,] Y ) |-> E ) ` z ) ) <_ y -> E. y e. RR A. z e. dom ( x e. ( X (,) Y ) |-> E ) ( abs ` ( ( x e. ( X (,) Y ) |-> E ) ` z ) ) <_ y ) )
222 207 221 mpd 
 |-  ( ph -> E. y e. RR A. z e. dom ( x e. ( X (,) Y ) |-> E ) ( abs ` ( ( x e. ( X (,) Y ) |-> E ) ` z ) ) <_ y )
223 bddmulibl 
 |-  ( ( ( x e. ( X (,) Y ) |-> E ) e. MblFn /\ ( x e. ( X (,) Y ) |-> B ) e. L^1 /\ E. y e. RR A. z e. dom ( x e. ( X (,) Y ) |-> E ) ( abs ` ( ( x e. ( X (,) Y ) |-> E ) ` z ) ) <_ y ) -> ( ( x e. ( X (,) Y ) |-> E ) oF x. ( x e. ( X (,) Y ) |-> B ) ) e. L^1 )
224 204 205 222 223 syl3anc 
 |-  ( ph -> ( ( x e. ( X (,) Y ) |-> E ) oF x. ( x e. ( X (,) Y ) |-> B ) ) e. L^1 )
225 198 224 eqeltrd 
 |-  ( ph -> ( RR _D ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) ) e. L^1 )
226 1 2 3 186 225 134 ftc2 
 |-  ( ph -> S. ( X (,) Y ) ( ( RR _D ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) ) ` t ) _d t = ( ( ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) ` Y ) - ( ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) ` X ) ) )
227 fveq2 
 |-  ( t = x -> ( ( RR _D ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) ) ` t ) = ( ( RR _D ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) ) ` x ) )
228 nfcv 
 |-  F/_ x RR
229 nfcv 
 |-  F/_ x _D
230 nfmpt1 
 |-  F/_ x ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u )
231 228 229 230 nfov 
 |-  F/_ x ( RR _D ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) )
232 nfcv 
 |-  F/_ x t
233 231 232 nffv 
 |-  F/_ x ( ( RR _D ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) ) ` t )
234 nfcv 
 |-  F/_ t ( ( RR _D ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) ) ` x )
235 227 233 234 cbvitg 
 |-  S. ( X (,) Y ) ( ( RR _D ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) ) ` t ) _d t = S. ( X (,) Y ) ( ( RR _D ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) ) ` x ) _d x
236 175 fveq1d 
 |-  ( ph -> ( ( RR _D ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) ) ` x ) = ( ( x e. ( X (,) Y ) |-> ( E x. B ) ) ` x ) )
237 ovex 
 |-  ( E x. B ) e. _V
238 eqid 
 |-  ( x e. ( X (,) Y ) |-> ( E x. B ) ) = ( x e. ( X (,) Y ) |-> ( E x. B ) )
239 238 fvmpt2 
 |-  ( ( x e. ( X (,) Y ) /\ ( E x. B ) e. _V ) -> ( ( x e. ( X (,) Y ) |-> ( E x. B ) ) ` x ) = ( E x. B ) )
240 237 239 mpan2 
 |-  ( x e. ( X (,) Y ) -> ( ( x e. ( X (,) Y ) |-> ( E x. B ) ) ` x ) = ( E x. B ) )
241 236 240 sylan9eq 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> ( ( RR _D ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) ) ` x ) = ( E x. B ) )
242 241 itgeq2dv 
 |-  ( ph -> S. ( X (,) Y ) ( ( RR _D ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) ) ` x ) _d x = S. ( X (,) Y ) ( E x. B ) _d x )
243 235 242 eqtrid 
 |-  ( ph -> S. ( X (,) Y ) ( ( RR _D ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) ) ` t ) _d t = S. ( X (,) Y ) ( E x. B ) _d x )
244 28 15 sselid 
 |-  ( ( ph /\ x e. ( X [,] Y ) ) -> A e. ( M [,] N ) )
245 elicc2 
 |-  ( ( M e. RR /\ N e. RR ) -> ( A e. ( M [,] N ) <-> ( A e. RR /\ M <_ A /\ A <_ N ) ) )
246 49 46 245 syl2anc 
 |-  ( ph -> ( A e. ( M [,] N ) <-> ( A e. RR /\ M <_ A /\ A <_ N ) ) )
247 246 adantr 
 |-  ( ( ph /\ x e. ( X [,] Y ) ) -> ( A e. ( M [,] N ) <-> ( A e. RR /\ M <_ A /\ A <_ N ) ) )
248 244 247 mpbid 
 |-  ( ( ph /\ x e. ( X [,] Y ) ) -> ( A e. RR /\ M <_ A /\ A <_ N ) )
249 248 simp2d 
 |-  ( ( ph /\ x e. ( X [,] Y ) ) -> M <_ A )
250 249 ditgpos 
 |-  ( ( ph /\ x e. ( X [,] Y ) ) -> S_ [ M -> A ] C _d u = S. ( M (,) A ) C _d u )
251 250 mpteq2dva 
 |-  ( ph -> ( x e. ( X [,] Y ) |-> S_ [ M -> A ] C _d u ) = ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) )
252 251 fveq1d 
 |-  ( ph -> ( ( x e. ( X [,] Y ) |-> S_ [ M -> A ] C _d u ) ` Y ) = ( ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) ` Y ) )
253 ubicc2 
 |-  ( ( X e. RR* /\ Y e. RR* /\ X <_ Y ) -> Y e. ( X [,] Y ) )
254 96 97 3 253 syl3anc 
 |-  ( ph -> Y e. ( X [,] Y ) )
255 ditgeq2 
 |-  ( A = L -> S_ [ M -> A ] C _d u = S_ [ M -> L ] C _d u )
256 12 255 syl 
 |-  ( x = Y -> S_ [ M -> A ] C _d u = S_ [ M -> L ] C _d u )
257 eqid 
 |-  ( x e. ( X [,] Y ) |-> S_ [ M -> A ] C _d u ) = ( x e. ( X [,] Y ) |-> S_ [ M -> A ] C _d u )
258 ditgex 
 |-  S_ [ M -> L ] C _d u e. _V
259 256 257 258 fvmpt 
 |-  ( Y e. ( X [,] Y ) -> ( ( x e. ( X [,] Y ) |-> S_ [ M -> A ] C _d u ) ` Y ) = S_ [ M -> L ] C _d u )
260 254 259 syl 
 |-  ( ph -> ( ( x e. ( X [,] Y ) |-> S_ [ M -> A ] C _d u ) ` Y ) = S_ [ M -> L ] C _d u )
261 252 260 eqtr3d 
 |-  ( ph -> ( ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) ` Y ) = S_ [ M -> L ] C _d u )
262 251 fveq1d 
 |-  ( ph -> ( ( x e. ( X [,] Y ) |-> S_ [ M -> A ] C _d u ) ` X ) = ( ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) ` X ) )
263 ditgeq2 
 |-  ( A = K -> S_ [ M -> A ] C _d u = S_ [ M -> K ] C _d u )
264 11 263 syl 
 |-  ( x = X -> S_ [ M -> A ] C _d u = S_ [ M -> K ] C _d u )
265 ditgex 
 |-  S_ [ M -> K ] C _d u e. _V
266 264 257 265 fvmpt 
 |-  ( X e. ( X [,] Y ) -> ( ( x e. ( X [,] Y ) |-> S_ [ M -> A ] C _d u ) ` X ) = S_ [ M -> K ] C _d u )
267 99 266 syl 
 |-  ( ph -> ( ( x e. ( X [,] Y ) |-> S_ [ M -> A ] C _d u ) ` X ) = S_ [ M -> K ] C _d u )
268 262 267 eqtr3d 
 |-  ( ph -> ( ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) ` X ) = S_ [ M -> K ] C _d u )
269 261 268 oveq12d 
 |-  ( ph -> ( ( ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) ` Y ) - ( ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) ` X ) ) = ( S_ [ M -> L ] C _d u - S_ [ M -> K ] C _d u ) )
270 lbicc2 
 |-  ( ( M e. RR* /\ N e. RR* /\ M <_ N ) -> M e. ( M [,] N ) )
271 108 47 114 270 syl3anc 
 |-  ( ph -> M e. ( M [,] N ) )
272 11 eleq1d 
 |-  ( x = X -> ( A e. ( M [,] N ) <-> K e. ( M [,] N ) ) )
273 244 ralrimiva 
 |-  ( ph -> A. x e. ( X [,] Y ) A e. ( M [,] N ) )
274 272 273 99 rspcdva 
 |-  ( ph -> K e. ( M [,] N ) )
275 12 eleq1d 
 |-  ( x = Y -> ( A e. ( M [,] N ) <-> L e. ( M [,] N ) ) )
276 275 273 254 rspcdva 
 |-  ( ph -> L e. ( M [,] N ) )
277 49 46 271 274 276 61 77 ditgsplit 
 |-  ( ph -> S_ [ M -> L ] C _d u = ( S_ [ M -> K ] C _d u + S_ [ K -> L ] C _d u ) )
278 277 oveq1d 
 |-  ( ph -> ( S_ [ M -> L ] C _d u - S_ [ M -> K ] C _d u ) = ( ( S_ [ M -> K ] C _d u + S_ [ K -> L ] C _d u ) - S_ [ M -> K ] C _d u ) )
279 49 46 271 274 61 77 ditgcl 
 |-  ( ph -> S_ [ M -> K ] C _d u e. CC )
280 49 46 274 276 61 77 ditgcl 
 |-  ( ph -> S_ [ K -> L ] C _d u e. CC )
281 279 280 pncan2d 
 |-  ( ph -> ( ( S_ [ M -> K ] C _d u + S_ [ K -> L ] C _d u ) - S_ [ M -> K ] C _d u ) = S_ [ K -> L ] C _d u )
282 269 278 281 3eqtrd 
 |-  ( ph -> ( ( ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) ` Y ) - ( ( x e. ( X [,] Y ) |-> S. ( M (,) A ) C _d u ) ` X ) ) = S_ [ K -> L ] C _d u )
283 226 243 282 3eqtr3d 
 |-  ( ph -> S. ( X (,) Y ) ( E x. B ) _d x = S_ [ K -> L ] C _d u )
284 16 283 eqtr2d 
 |-  ( ph -> S_ [ K -> L ] C _d u = S_ [ X -> Y ] ( E x. B ) _d x )