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 fvmptelrn
 |-  ( ( 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 61 tgioo2
 |-  ( 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 )