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 ) |