This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem itgsubsticclem

Description: lemma for itgsubsticc . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses itgsubsticclem.1 
|- F = ( u e. ( K [,] L ) |-> C )
itgsubsticclem.2 
|- G = ( u e. RR |-> if ( u e. ( K [,] L ) , ( F ` u ) , if ( u < K , ( F ` K ) , ( F ` L ) ) ) )
itgsubsticclem.3 
|- ( ph -> X e. RR )
itgsubsticclem.4 
|- ( ph -> Y e. RR )
itgsubsticclem.5 
|- ( ph -> X <_ Y )
itgsubsticclem.6 
|- ( ph -> ( x e. ( X [,] Y ) |-> A ) e. ( ( X [,] Y ) -cn-> ( K [,] L ) ) )
itgsubsticclem.7 
|- ( ph -> ( x e. ( X (,) Y ) |-> B ) e. ( ( ( X (,) Y ) -cn-> CC ) i^i L^1 ) )
itgsubsticclem.8 
|- ( ph -> F e. ( ( K [,] L ) -cn-> CC ) )
itgsubsticclem.9 
|- ( ph -> K e. RR )
itgsubsticclem.10 
|- ( ph -> L e. RR )
itgsubsticclem.11 
|- ( ph -> K <_ L )
itgsubsticclem.12 
|- ( ph -> ( RR _D ( x e. ( X [,] Y ) |-> A ) ) = ( x e. ( X (,) Y ) |-> B ) )
itgsubsticclem.13 
|- ( u = A -> C = E )
itgsubsticclem.14 
|- ( x = X -> A = K )
itgsubsticclem.15 
|- ( x = Y -> A = L )
Assertion itgsubsticclem 
|- ( ph -> S_ [ K -> L ] C _d u = S_ [ X -> Y ] ( E x. B ) _d x )

Proof

Step Hyp Ref Expression
1 itgsubsticclem.1 
 |-  F = ( u e. ( K [,] L ) |-> C )
2 itgsubsticclem.2 
 |-  G = ( u e. RR |-> if ( u e. ( K [,] L ) , ( F ` u ) , if ( u < K , ( F ` K ) , ( F ` L ) ) ) )
3 itgsubsticclem.3 
 |-  ( ph -> X e. RR )
4 itgsubsticclem.4 
 |-  ( ph -> Y e. RR )
5 itgsubsticclem.5 
 |-  ( ph -> X <_ Y )
6 itgsubsticclem.6 
 |-  ( ph -> ( x e. ( X [,] Y ) |-> A ) e. ( ( X [,] Y ) -cn-> ( K [,] L ) ) )
7 itgsubsticclem.7 
 |-  ( ph -> ( x e. ( X (,) Y ) |-> B ) e. ( ( ( X (,) Y ) -cn-> CC ) i^i L^1 ) )
8 itgsubsticclem.8 
 |-  ( ph -> F e. ( ( K [,] L ) -cn-> CC ) )
9 itgsubsticclem.9 
 |-  ( ph -> K e. RR )
10 itgsubsticclem.10 
 |-  ( ph -> L e. RR )
11 itgsubsticclem.11 
 |-  ( ph -> K <_ L )
12 itgsubsticclem.12 
 |-  ( ph -> ( RR _D ( x e. ( X [,] Y ) |-> A ) ) = ( x e. ( X (,) Y ) |-> B ) )
13 itgsubsticclem.13 
 |-  ( u = A -> C = E )
14 itgsubsticclem.14 
 |-  ( x = X -> A = K )
15 itgsubsticclem.15 
 |-  ( x = Y -> A = L )
16 fveq2 
 |-  ( u = w -> ( G ` u ) = ( G ` w ) )
17 nfcv 
 |-  F/_ w ( G ` u )
18 nfmpt1 
 |-  F/_ u ( u e. RR |-> if ( u e. ( K [,] L ) , ( F ` u ) , if ( u < K , ( F ` K ) , ( F ` L ) ) ) )
19 2 18 nfcxfr 
 |-  F/_ u G
20 nfcv 
 |-  F/_ u w
21 19 20 nffv 
 |-  F/_ u ( G ` w )
22 16 17 21 cbvditg 
 |-  S_ [ K -> L ] ( G ` u ) _d u = S_ [ K -> L ] ( G ` w ) _d w
23 9 10 iccssred 
 |-  ( ph -> ( K [,] L ) C_ RR )
24 23 adantr 
 |-  ( ( ph /\ u e. ( K (,) L ) ) -> ( K [,] L ) C_ RR )
25 ioossicc 
 |-  ( K (,) L ) C_ ( K [,] L )
26 25 sseli 
 |-  ( u e. ( K (,) L ) -> u e. ( K [,] L ) )
27 26 adantl 
 |-  ( ( ph /\ u e. ( K (,) L ) ) -> u e. ( K [,] L ) )
28 24 27 sseldd 
 |-  ( ( ph /\ u e. ( K (,) L ) ) -> u e. RR )
29 27 iftrued 
 |-  ( ( ph /\ u e. ( K (,) L ) ) -> if ( u e. ( K [,] L ) , ( F ` u ) , if ( u < K , ( F ` K ) , ( F ` L ) ) ) = ( F ` u ) )
30 1 a1i 
 |-  ( ph -> F = ( u e. ( K [,] L ) |-> C ) )
31 cncff 
 |-  ( F e. ( ( K [,] L ) -cn-> CC ) -> F : ( K [,] L ) --> CC )
32 8 31 syl 
 |-  ( ph -> F : ( K [,] L ) --> CC )
33 30 32 feq1dd 
 |-  ( ph -> ( u e. ( K [,] L ) |-> C ) : ( K [,] L ) --> CC )
34 33 fvmptelcdm 
 |-  ( ( ph /\ u e. ( K [,] L ) ) -> C e. CC )
35 27 34 syldan 
 |-  ( ( ph /\ u e. ( K (,) L ) ) -> C e. CC )
36 1 fvmpt2 
 |-  ( ( u e. ( K [,] L ) /\ C e. CC ) -> ( F ` u ) = C )
37 27 35 36 syl2anc 
 |-  ( ( ph /\ u e. ( K (,) L ) ) -> ( F ` u ) = C )
38 37 35 eqeltrd 
 |-  ( ( ph /\ u e. ( K (,) L ) ) -> ( F ` u ) e. CC )
39 29 38 eqeltrd 
 |-  ( ( ph /\ u e. ( K (,) L ) ) -> if ( u e. ( K [,] L ) , ( F ` u ) , if ( u < K , ( F ` K ) , ( F ` L ) ) ) e. CC )
40 2 fvmpt2 
 |-  ( ( u e. RR /\ if ( u e. ( K [,] L ) , ( F ` u ) , if ( u < K , ( F ` K ) , ( F ` L ) ) ) e. CC ) -> ( G ` u ) = if ( u e. ( K [,] L ) , ( F ` u ) , if ( u < K , ( F ` K ) , ( F ` L ) ) ) )
41 28 39 40 syl2anc 
 |-  ( ( ph /\ u e. ( K (,) L ) ) -> ( G ` u ) = if ( u e. ( K [,] L ) , ( F ` u ) , if ( u < K , ( F ` K ) , ( F ` L ) ) ) )
42 41 29 37 3eqtrd 
 |-  ( ( ph /\ u e. ( K (,) L ) ) -> ( G ` u ) = C )
43 11 42 ditgeq3d 
 |-  ( ph -> S_ [ K -> L ] ( G ` u ) _d u = S_ [ K -> L ] C _d u )
44 mnfxr 
 |-  -oo e. RR*
45 44 a1i 
 |-  ( ph -> -oo e. RR* )
46 pnfxr 
 |-  +oo e. RR*
47 46 a1i 
 |-  ( ph -> +oo e. RR* )
48 ioomax 
 |-  ( -oo (,) +oo ) = RR
49 48 eqcomi 
 |-  RR = ( -oo (,) +oo )
50 49 a1i 
 |-  ( ph -> RR = ( -oo (,) +oo ) )
51 23 50 sseqtrd 
 |-  ( ph -> ( K [,] L ) C_ ( -oo (,) +oo ) )
52 ax-resscn 
 |-  RR C_ CC
53 50 52 eqsstrrdi 
 |-  ( ph -> ( -oo (,) +oo ) C_ CC )
54 cncfss 
 |-  ( ( ( K [,] L ) C_ ( -oo (,) +oo ) /\ ( -oo (,) +oo ) C_ CC ) -> ( ( X [,] Y ) -cn-> ( K [,] L ) ) C_ ( ( X [,] Y ) -cn-> ( -oo (,) +oo ) ) )
55 51 53 54 syl2anc 
 |-  ( ph -> ( ( X [,] Y ) -cn-> ( K [,] L ) ) C_ ( ( X [,] Y ) -cn-> ( -oo (,) +oo ) ) )
56 55 6 sseldd 
 |-  ( ph -> ( x e. ( X [,] Y ) |-> A ) e. ( ( X [,] Y ) -cn-> ( -oo (,) +oo ) ) )
57 nfmpt1 
 |-  F/_ u ( u e. ( K [,] L ) |-> C )
58 1 57 nfcxfr 
 |-  F/_ u F
59 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
60 eqid 
 |-  U. ( TopOpen ` CCfld ) = U. ( TopOpen ` CCfld )
61 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
62 61 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
63 62 a1i 
 |-  ( ph -> ( TopOpen ` CCfld ) e. Top )
64 23 52 sstrdi 
 |-  ( ph -> ( K [,] L ) C_ CC )
65 ssid 
 |-  CC C_ CC
66 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( K [,] L ) ) = ( ( TopOpen ` CCfld ) |`t ( K [,] L ) )
67 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
68 67 restid 
 |-  ( ( TopOpen ` CCfld ) e. Top -> ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld ) )
69 62 68 ax-mp 
 |-  ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld )
70 69 eqcomi 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
71 61 66 70 cncfcn 
 |-  ( ( ( K [,] L ) C_ CC /\ CC C_ CC ) -> ( ( K [,] L ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( K [,] L ) ) Cn ( TopOpen ` CCfld ) ) )
72 64 65 71 sylancl 
 |-  ( ph -> ( ( K [,] L ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( K [,] L ) ) Cn ( TopOpen ` CCfld ) ) )
73 reex 
 |-  RR e. _V
74 73 a1i 
 |-  ( ph -> RR e. _V )
75 restabs 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ ( K [,] L ) C_ RR /\ RR e. _V ) -> ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( K [,] L ) ) = ( ( TopOpen ` CCfld ) |`t ( K [,] L ) ) )
76 63 23 74 75 syl3anc 
 |-  ( ph -> ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( K [,] L ) ) = ( ( TopOpen ` CCfld ) |`t ( K [,] L ) ) )
77 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
78 77 eqcomi 
 |-  ( ( TopOpen ` CCfld ) |`t RR ) = ( topGen ` ran (,) )
79 78 a1i 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t RR ) = ( topGen ` ran (,) ) )
80 79 oveq1d 
 |-  ( ph -> ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( K [,] L ) ) = ( ( topGen ` ran (,) ) |`t ( K [,] L ) ) )
81 76 80 eqtr3d 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t ( K [,] L ) ) = ( ( topGen ` ran (,) ) |`t ( K [,] L ) ) )
82 81 oveq1d 
 |-  ( ph -> ( ( ( TopOpen ` CCfld ) |`t ( K [,] L ) ) Cn ( TopOpen ` CCfld ) ) = ( ( ( topGen ` ran (,) ) |`t ( K [,] L ) ) Cn ( TopOpen ` CCfld ) ) )
83 72 82 eqtrd 
 |-  ( ph -> ( ( K [,] L ) -cn-> CC ) = ( ( ( topGen ` ran (,) ) |`t ( K [,] L ) ) Cn ( TopOpen ` CCfld ) ) )
84 8 83 eleqtrd 
 |-  ( ph -> F e. ( ( ( topGen ` ran (,) ) |`t ( K [,] L ) ) Cn ( TopOpen ` CCfld ) ) )
85 58 59 60 2 9 10 11 63 84 icccncfext 
 |-  ( ph -> ( G e. ( ( topGen ` ran (,) ) Cn ( ( TopOpen ` CCfld ) |`t ran F ) ) /\ ( G |` ( K [,] L ) ) = F ) )
86 85 simpld 
 |-  ( ph -> G e. ( ( topGen ` ran (,) ) Cn ( ( TopOpen ` CCfld ) |`t ran F ) ) )
87 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
88 eqid 
 |-  U. ( ( TopOpen ` CCfld ) |`t ran F ) = U. ( ( TopOpen ` CCfld ) |`t ran F )
89 87 88 cnf 
 |-  ( G e. ( ( topGen ` ran (,) ) Cn ( ( TopOpen ` CCfld ) |`t ran F ) ) -> G : RR --> U. ( ( TopOpen ` CCfld ) |`t ran F ) )
90 86 89 syl 
 |-  ( ph -> G : RR --> U. ( ( TopOpen ` CCfld ) |`t ran F ) )
91 50 feq2d 
 |-  ( ph -> ( G : RR --> U. ( ( TopOpen ` CCfld ) |`t ran F ) <-> G : ( -oo (,) +oo ) --> U. ( ( TopOpen ` CCfld ) |`t ran F ) ) )
92 90 91 mpbid 
 |-  ( ph -> G : ( -oo (,) +oo ) --> U. ( ( TopOpen ` CCfld ) |`t ran F ) )
93 92 feqmptd 
 |-  ( ph -> G = ( w e. ( -oo (,) +oo ) |-> ( G ` w ) ) )
94 32 frnd 
 |-  ( ph -> ran F C_ CC )
95 cncfss 
 |-  ( ( ran F C_ CC /\ CC C_ CC ) -> ( ( -oo (,) +oo ) -cn-> ran F ) C_ ( ( -oo (,) +oo ) -cn-> CC ) )
96 94 65 95 sylancl 
 |-  ( ph -> ( ( -oo (,) +oo ) -cn-> ran F ) C_ ( ( -oo (,) +oo ) -cn-> CC ) )
97 49 oveq2i 
 |-  ( ( TopOpen ` CCfld ) |`t RR ) = ( ( TopOpen ` CCfld ) |`t ( -oo (,) +oo ) )
98 77 97 eqtri 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t ( -oo (,) +oo ) )
99 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ran F ) = ( ( TopOpen ` CCfld ) |`t ran F )
100 61 98 99 cncfcn 
 |-  ( ( ( -oo (,) +oo ) C_ CC /\ ran F C_ CC ) -> ( ( -oo (,) +oo ) -cn-> ran F ) = ( ( topGen ` ran (,) ) Cn ( ( TopOpen ` CCfld ) |`t ran F ) ) )
101 53 94 100 syl2anc 
 |-  ( ph -> ( ( -oo (,) +oo ) -cn-> ran F ) = ( ( topGen ` ran (,) ) Cn ( ( TopOpen ` CCfld ) |`t ran F ) ) )
102 101 eqcomd 
 |-  ( ph -> ( ( topGen ` ran (,) ) Cn ( ( TopOpen ` CCfld ) |`t ran F ) ) = ( ( -oo (,) +oo ) -cn-> ran F ) )
103 86 102 eleqtrd 
 |-  ( ph -> G e. ( ( -oo (,) +oo ) -cn-> ran F ) )
104 96 103 sseldd 
 |-  ( ph -> G e. ( ( -oo (,) +oo ) -cn-> CC ) )
105 93 104 eqeltrrd 
 |-  ( ph -> ( w e. ( -oo (,) +oo ) |-> ( G ` w ) ) e. ( ( -oo (,) +oo ) -cn-> CC ) )
106 fveq2 
 |-  ( w = A -> ( G ` w ) = ( G ` A ) )
107 3 4 5 45 47 56 7 105 12 106 14 15 itgsubst 
 |-  ( ph -> S_ [ K -> L ] ( G ` w ) _d w = S_ [ X -> Y ] ( ( G ` A ) x. B ) _d x )
108 22 43 107 3eqtr3a 
 |-  ( ph -> S_ [ K -> L ] C _d u = S_ [ X -> Y ] ( ( G ` A ) x. B ) _d x )
109 2 a1i 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> G = ( u e. RR |-> if ( u e. ( K [,] L ) , ( F ` u ) , if ( u < K , ( F ` K ) , ( F ` L ) ) ) ) )
110 simpr 
 |-  ( ( ( ph /\ x e. ( X (,) Y ) ) /\ u = A ) -> u = A )
111 61 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
112 3 4 iccssred 
 |-  ( ph -> ( X [,] Y ) C_ RR )
113 112 52 sstrdi 
 |-  ( ph -> ( X [,] Y ) C_ CC )
114 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ( X [,] Y ) C_ CC ) -> ( ( TopOpen ` CCfld ) |`t ( X [,] Y ) ) e. ( TopOn ` ( X [,] Y ) ) )
115 111 113 114 sylancr 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t ( X [,] Y ) ) e. ( TopOn ` ( X [,] Y ) ) )
116 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ( K [,] L ) C_ CC ) -> ( ( TopOpen ` CCfld ) |`t ( K [,] L ) ) e. ( TopOn ` ( K [,] L ) ) )
117 111 64 116 sylancr 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t ( K [,] L ) ) e. ( TopOn ` ( K [,] L ) ) )
118 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( X [,] Y ) ) = ( ( TopOpen ` CCfld ) |`t ( X [,] Y ) )
119 61 118 66 cncfcn 
 |-  ( ( ( X [,] Y ) C_ CC /\ ( K [,] L ) C_ CC ) -> ( ( X [,] Y ) -cn-> ( K [,] L ) ) = ( ( ( TopOpen ` CCfld ) |`t ( X [,] Y ) ) Cn ( ( TopOpen ` CCfld ) |`t ( K [,] L ) ) ) )
120 113 64 119 syl2anc 
 |-  ( ph -> ( ( X [,] Y ) -cn-> ( K [,] L ) ) = ( ( ( TopOpen ` CCfld ) |`t ( X [,] Y ) ) Cn ( ( TopOpen ` CCfld ) |`t ( K [,] L ) ) ) )
121 6 120 eleqtrd 
 |-  ( ph -> ( x e. ( X [,] Y ) |-> A ) e. ( ( ( TopOpen ` CCfld ) |`t ( X [,] Y ) ) Cn ( ( TopOpen ` CCfld ) |`t ( K [,] L ) ) ) )
122 cnf2 
 |-  ( ( ( ( TopOpen ` CCfld ) |`t ( X [,] Y ) ) e. ( TopOn ` ( X [,] Y ) ) /\ ( ( TopOpen ` CCfld ) |`t ( K [,] L ) ) e. ( TopOn ` ( K [,] L ) ) /\ ( x e. ( X [,] Y ) |-> A ) e. ( ( ( TopOpen ` CCfld ) |`t ( X [,] Y ) ) Cn ( ( TopOpen ` CCfld ) |`t ( K [,] L ) ) ) ) -> ( x e. ( X [,] Y ) |-> A ) : ( X [,] Y ) --> ( K [,] L ) )
123 115 117 121 122 syl3anc 
 |-  ( ph -> ( x e. ( X [,] Y ) |-> A ) : ( X [,] Y ) --> ( K [,] L ) )
124 123 adantr 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> ( x e. ( X [,] Y ) |-> A ) : ( X [,] Y ) --> ( K [,] L ) )
125 eqid 
 |-  ( x e. ( X [,] Y ) |-> A ) = ( x e. ( X [,] Y ) |-> A )
126 125 fmpt 
 |-  ( A. x e. ( X [,] Y ) A e. ( K [,] L ) <-> ( x e. ( X [,] Y ) |-> A ) : ( X [,] Y ) --> ( K [,] L ) )
127 124 126 sylibr 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> A. x e. ( X [,] Y ) A e. ( K [,] L ) )
128 ioossicc 
 |-  ( X (,) Y ) C_ ( X [,] Y )
129 128 sseli 
 |-  ( x e. ( X (,) Y ) -> x e. ( X [,] Y ) )
130 129 adantl 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> x e. ( X [,] Y ) )
131 rsp 
 |-  ( A. x e. ( X [,] Y ) A e. ( K [,] L ) -> ( x e. ( X [,] Y ) -> A e. ( K [,] L ) ) )
132 127 130 131 sylc 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> A e. ( K [,] L ) )
133 132 adantr 
 |-  ( ( ( ph /\ x e. ( X (,) Y ) ) /\ u = A ) -> A e. ( K [,] L ) )
134 110 133 eqeltrd 
 |-  ( ( ( ph /\ x e. ( X (,) Y ) ) /\ u = A ) -> u e. ( K [,] L ) )
135 134 iftrued 
 |-  ( ( ( ph /\ x e. ( X (,) Y ) ) /\ u = A ) -> if ( u e. ( K [,] L ) , ( F ` u ) , if ( u < K , ( F ` K ) , ( F ` L ) ) ) = ( F ` u ) )
136 simpll 
 |-  ( ( ( ph /\ x e. ( X (,) Y ) ) /\ u = A ) -> ph )
137 136 134 34 syl2anc 
 |-  ( ( ( ph /\ x e. ( X (,) Y ) ) /\ u = A ) -> C e. CC )
138 134 137 36 syl2anc 
 |-  ( ( ( ph /\ x e. ( X (,) Y ) ) /\ u = A ) -> ( F ` u ) = C )
139 13 adantl 
 |-  ( ( ( ph /\ x e. ( X (,) Y ) ) /\ u = A ) -> C = E )
140 135 138 139 3eqtrd 
 |-  ( ( ( ph /\ x e. ( X (,) Y ) ) /\ u = A ) -> if ( u e. ( K [,] L ) , ( F ` u ) , if ( u < K , ( F ` K ) , ( F ` L ) ) ) = E )
141 23 adantr 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> ( K [,] L ) C_ RR )
142 141 132 sseldd 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> A e. RR )
143 elex 
 |-  ( A e. ( K [,] L ) -> A e. _V )
144 132 143 syl 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> A e. _V )
145 isset 
 |-  ( A e. _V <-> E. u u = A )
146 144 145 sylib 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> E. u u = A )
147 139 137 eqeltrrd 
 |-  ( ( ( ph /\ x e. ( X (,) Y ) ) /\ u = A ) -> E e. CC )
148 146 147 exlimddv 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> E e. CC )
149 109 140 142 148 fvmptd 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> ( G ` A ) = E )
150 149 oveq1d 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> ( ( G ` A ) x. B ) = ( E x. B ) )
151 5 150 ditgeq3d 
 |-  ( ph -> S_ [ X -> Y ] ( ( G ` A ) x. B ) _d x = S_ [ X -> Y ] ( E x. B ) _d x )
152 108 151 eqtrd 
 |-  ( ph -> S_ [ K -> L ] C _d u = S_ [ X -> Y ] ( E x. B ) _d x )