Step |
Hyp |
Ref |
Expression |
1 |
|
dvres.k |
⊢ 𝐾 = ( TopOpen ‘ ℂfld ) |
2 |
|
dvres.t |
⊢ 𝑇 = ( 𝐾 ↾t 𝑆 ) |
3 |
|
reldv |
⊢ Rel ( 𝑆 D ( 𝐹 ↾ 𝐵 ) ) |
4 |
|
relres |
⊢ Rel ( ( 𝑆 D 𝐹 ) ↾ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ) |
5 |
|
simpll |
⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → 𝑆 ⊆ ℂ ) |
6 |
|
simplr |
⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → 𝐹 : 𝐴 ⟶ ℂ ) |
7 |
|
inss1 |
⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 |
8 |
|
fssres |
⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) : ( 𝐴 ∩ 𝐵 ) ⟶ ℂ ) |
9 |
6 7 8
|
sylancl |
⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) : ( 𝐴 ∩ 𝐵 ) ⟶ ℂ ) |
10 |
|
resres |
⊢ ( ( 𝐹 ↾ 𝐴 ) ↾ 𝐵 ) = ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) |
11 |
|
ffn |
⊢ ( 𝐹 : 𝐴 ⟶ ℂ → 𝐹 Fn 𝐴 ) |
12 |
|
fnresdm |
⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ 𝐴 ) = 𝐹 ) |
13 |
6 11 12
|
3syl |
⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( 𝐹 ↾ 𝐴 ) = 𝐹 ) |
14 |
13
|
reseq1d |
⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( ( 𝐹 ↾ 𝐴 ) ↾ 𝐵 ) = ( 𝐹 ↾ 𝐵 ) ) |
15 |
10 14
|
syl5eqr |
⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐹 ↾ 𝐵 ) ) |
16 |
15
|
feq1d |
⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) : ( 𝐴 ∩ 𝐵 ) ⟶ ℂ ↔ ( 𝐹 ↾ 𝐵 ) : ( 𝐴 ∩ 𝐵 ) ⟶ ℂ ) ) |
17 |
9 16
|
mpbid |
⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( 𝐹 ↾ 𝐵 ) : ( 𝐴 ∩ 𝐵 ) ⟶ ℂ ) |
18 |
|
simprl |
⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → 𝐴 ⊆ 𝑆 ) |
19 |
7 18
|
sstrid |
⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( 𝐴 ∩ 𝐵 ) ⊆ 𝑆 ) |
20 |
5 17 19
|
dvcl |
⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) ∧ 𝑥 ( 𝑆 D ( 𝐹 ↾ 𝐵 ) ) 𝑦 ) → 𝑦 ∈ ℂ ) |
21 |
20
|
ex |
⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( 𝑥 ( 𝑆 D ( 𝐹 ↾ 𝐵 ) ) 𝑦 → 𝑦 ∈ ℂ ) ) |
22 |
5 6 18
|
dvcl |
⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) ∧ 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝑦 ∈ ℂ ) |
23 |
22
|
ex |
⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( 𝑥 ( 𝑆 D 𝐹 ) 𝑦 → 𝑦 ∈ ℂ ) ) |
24 |
23
|
adantld |
⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ∧ 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝑦 ∈ ℂ ) ) |
25 |
|
eqid |
⊢ ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) = ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) |
26 |
5
|
adantr |
⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) ∧ 𝑦 ∈ ℂ ) → 𝑆 ⊆ ℂ ) |
27 |
6
|
adantr |
⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) ∧ 𝑦 ∈ ℂ ) → 𝐹 : 𝐴 ⟶ ℂ ) |
28 |
18
|
adantr |
⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) ∧ 𝑦 ∈ ℂ ) → 𝐴 ⊆ 𝑆 ) |
29 |
|
simplrr |
⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) ∧ 𝑦 ∈ ℂ ) → 𝐵 ⊆ 𝑆 ) |
30 |
|
simpr |
⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) ∧ 𝑦 ∈ ℂ ) → 𝑦 ∈ ℂ ) |
31 |
1 2 25 26 27 28 29 30
|
dvreslem |
⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) ∧ 𝑦 ∈ ℂ ) → ( 𝑥 ( 𝑆 D ( 𝐹 ↾ 𝐵 ) ) 𝑦 ↔ ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ∧ 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ) ) ) |
32 |
31
|
ex |
⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( 𝑦 ∈ ℂ → ( 𝑥 ( 𝑆 D ( 𝐹 ↾ 𝐵 ) ) 𝑦 ↔ ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ∧ 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ) ) ) ) |
33 |
21 24 32
|
pm5.21ndd |
⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( 𝑥 ( 𝑆 D ( 𝐹 ↾ 𝐵 ) ) 𝑦 ↔ ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ∧ 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ) ) ) |
34 |
|
vex |
⊢ 𝑦 ∈ V |
35 |
34
|
brresi |
⊢ ( 𝑥 ( ( 𝑆 D 𝐹 ) ↾ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ) 𝑦 ↔ ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ∧ 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ) ) |
36 |
33 35
|
bitr4di |
⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( 𝑥 ( 𝑆 D ( 𝐹 ↾ 𝐵 ) ) 𝑦 ↔ 𝑥 ( ( 𝑆 D 𝐹 ) ↾ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ) 𝑦 ) ) |
37 |
3 4 36
|
eqbrrdiv |
⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( 𝑆 D ( 𝐹 ↾ 𝐵 ) ) = ( ( 𝑆 D 𝐹 ) ↾ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ) ) |