Metamath Proof Explorer

Theorem dvconstbi

Description: The derivative of a function on S is zero iff it is a constant function. Roughly a biconditional S analogue of dvconst and dveq0 . Corresponds to integration formula " S. 0 _d x = C " in section 4.1 of LarsonHostetlerEdwards p. 278. (Contributed by Steve Rodriguez, 11-Nov-2015)

Ref Expression
Hypotheses dvconstbi.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
dvconstbi.y ⊢ ( 𝜑 → 𝑌 : 𝑆 ⟶ ℂ )
dvconstbi.dy ⊢ ( 𝜑 → dom ( 𝑆 D 𝑌 ) = 𝑆 )
Assertion dvconstbi ( 𝜑 → ( ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ↔ ∃ 𝑐 ∈ ℂ 𝑌 = ( 𝑆 × { 𝑐 } ) ) )

Proof

Step Hyp Ref Expression
1 dvconstbi.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2 dvconstbi.y ⊢ ( 𝜑 → 𝑌 : 𝑆 ⟶ ℂ )
3 dvconstbi.dy ⊢ ( 𝜑 → dom ( 𝑆 D 𝑌 ) = 𝑆 )
4 elpri ⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 = ℝ ∨ 𝑆 = ℂ ) )
5 1 4 syl ⊢ ( 𝜑 → ( 𝑆 = ℝ ∨ 𝑆 = ℂ ) )
6 0re ⊢ 0 ∈ ℝ
7 eleq2 ⊢ ( 𝑆 = ℝ → ( 0 ∈ 𝑆 ↔ 0 ∈ ℝ ) )
8 6 7 mpbiri ⊢ ( 𝑆 = ℝ → 0 ∈ 𝑆 )
9 0cn ⊢ 0 ∈ ℂ
10 eleq2 ⊢ ( 𝑆 = ℂ → ( 0 ∈ 𝑆 ↔ 0 ∈ ℂ ) )
11 9 10 mpbiri ⊢ ( 𝑆 = ℂ → 0 ∈ 𝑆 )
12 8 11 jaoi ⊢ ( ( 𝑆 = ℝ ∨ 𝑆 = ℂ ) → 0 ∈ 𝑆 )
13 5 12 syl ⊢ ( 𝜑 → 0 ∈ 𝑆 )
14 ffvelrn ⊢ ( ( 𝑌 : 𝑆 ⟶ ℂ ∧ 0 ∈ 𝑆 ) → ( 𝑌 ‘ 0 ) ∈ ℂ )
15 2 13 14 syl2anc ⊢ ( 𝜑 → ( 𝑌 ‘ 0 ) ∈ ℂ )
16 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ) → ( 𝑌 ‘ 0 ) ∈ ℂ )
17 2 ffnd ⊢ ( 𝜑 → 𝑌 Fn 𝑆 )
18 17 adantr ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ) → 𝑌 Fn 𝑆 )
19 fvex ⊢ ( 𝑌 ‘ 0 ) ∈ V
20 fnconstg ⊢ ( ( 𝑌 ‘ 0 ) ∈ V → ( 𝑆 × { ( 𝑌 ‘ 0 ) } ) Fn 𝑆 )
21 19 20 mp1i ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ) → ( 𝑆 × { ( 𝑌 ‘ 0 ) } ) Fn 𝑆 )
22 19 fvconst2 ⊢ ( 𝑦 ∈ 𝑆 → ( ( 𝑆 × { ( 𝑌 ‘ 0 ) } ) ‘ 𝑦 ) = ( 𝑌 ‘ 0 ) )
23 22 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ) ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑆 × { ( 𝑌 ‘ 0 ) } ) ‘ 𝑦 ) = ( 𝑌 ‘ 0 ) )
24 eqid ⊢ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) = ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) )
25 1 24 sblpnf ⊢ ( ( 𝜑 ∧ 0 ∈ 𝑆 ) → ( 0 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) +∞ ) = 𝑆 )
26 13 25 mpdan ⊢ ( 𝜑 → ( 0 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) +∞ ) = 𝑆 )
27 26 eleq2d ⊢ ( 𝜑 → ( 𝑦 ∈ ( 0 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) +∞ ) ↔ 𝑦 ∈ 𝑆 ) )
28 27 biimpar ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ ( 0 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) +∞ ) )
29 13 26 eleqtrrd ⊢ ( 𝜑 → 0 ∈ ( 0 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) +∞ ) )
30 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ) → 𝑆 ∈ { ℝ , ℂ } )
31 ssidd ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ) → 𝑆 ⊆ 𝑆 )
32 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ) → 𝑌 : 𝑆 ⟶ ℂ )
33 13 adantr ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ) → 0 ∈ 𝑆 )
34 pnfxr ⊢ +∞ ∈ ℝ*
35 34 a1i ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ) → +∞ ∈ ℝ* )
36 eqid ⊢ ( 0 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) +∞ ) = ( 0 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) +∞ )
37 26 adantr ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ) → ( 0 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) +∞ ) = 𝑆 )
38 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ) → dom ( 𝑆 D 𝑌 ) = 𝑆 )
39 37 38 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ) → ( 0 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) +∞ ) = dom ( 𝑆 D 𝑌 ) )
40 eqimss ⊢ ( ( 0 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) +∞ ) = dom ( 𝑆 D 𝑌 ) → ( 0 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) +∞ ) ⊆ dom ( 𝑆 D 𝑌 ) )
41 39 40 syl ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ) → ( 0 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) +∞ ) ⊆ dom ( 𝑆 D 𝑌 ) )
42 6 a1i ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ) → 0 ∈ ℝ )
43 26 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) +∞ ) ↔ 𝑥 ∈ 𝑆 ) )
44 43 biimpa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) +∞ ) ) → 𝑥 ∈ 𝑆 )
45 44 3adant2 ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ∧ 𝑥 ∈ ( 0 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) +∞ ) ) → 𝑥 ∈ 𝑆 )
46 fveq1 ⊢ ( ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) → ( ( 𝑆 D 𝑌 ) ‘ 𝑥 ) = ( ( 𝑆 × { 0 } ) ‘ 𝑥 ) )
47 c0ex ⊢ 0 ∈ V
48 47 fvconst2 ⊢ ( 𝑥 ∈ 𝑆 → ( ( 𝑆 × { 0 } ) ‘ 𝑥 ) = 0 )
49 46 48 sylan9eq ⊢ ( ( ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑆 D 𝑌 ) ‘ 𝑥 ) = 0 )
50 49 9 eqeltrdi ⊢ ( ( ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑆 D 𝑌 ) ‘ 𝑥 ) ∈ ℂ )
51 50 abscld ⊢ ( ( ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ∧ 𝑥 ∈ 𝑆 ) → ( abs ‘ ( ( 𝑆 D 𝑌 ) ‘ 𝑥 ) ) ∈ ℝ )
52 49 abs00bd ⊢ ( ( ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ∧ 𝑥 ∈ 𝑆 ) → ( abs ‘ ( ( 𝑆 D 𝑌 ) ‘ 𝑥 ) ) = 0 )
53 eqle ⊢ ( ( ( abs ‘ ( ( 𝑆 D 𝑌 ) ‘ 𝑥 ) ) ∈ ℝ ∧ ( abs ‘ ( ( 𝑆 D 𝑌 ) ‘ 𝑥 ) ) = 0 ) → ( abs ‘ ( ( 𝑆 D 𝑌 ) ‘ 𝑥 ) ) ≤ 0 )
54 51 52 53 syl2anc ⊢ ( ( ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ∧ 𝑥 ∈ 𝑆 ) → ( abs ‘ ( ( 𝑆 D 𝑌 ) ‘ 𝑥 ) ) ≤ 0 )
55 54 3adant1 ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ∧ 𝑥 ∈ 𝑆 ) → ( abs ‘ ( ( 𝑆 D 𝑌 ) ‘ 𝑥 ) ) ≤ 0 )
56 45 55 syld3an3 ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ∧ 𝑥 ∈ ( 0 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) +∞ ) ) → ( abs ‘ ( ( 𝑆 D 𝑌 ) ‘ 𝑥 ) ) ≤ 0 )
57 56 3expa ⊢ ( ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ) ∧ 𝑥 ∈ ( 0 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) +∞ ) ) → ( abs ‘ ( ( 𝑆 D 𝑌 ) ‘ 𝑥 ) ) ≤ 0 )
58 30 24 31 32 33 35 36 41 42 57 dvlip2 ⊢ ( ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ) ∧ ( 0 ∈ ( 0 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) +∞ ) ∧ 𝑦 ∈ ( 0 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) +∞ ) ) ) → ( abs ‘ ( ( 𝑌 ‘ 0 ) − ( 𝑌 ‘ 𝑦 ) ) ) ≤ ( 0 · ( abs ‘ ( 0 − 𝑦 ) ) ) )
59 29 58 sylanr1 ⊢ ( ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ) ∧ ( 𝜑 ∧ 𝑦 ∈ ( 0 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) +∞ ) ) ) → ( abs ‘ ( ( 𝑌 ‘ 0 ) − ( 𝑌 ‘ 𝑦 ) ) ) ≤ ( 0 · ( abs ‘ ( 0 − 𝑦 ) ) ) )
60 59 3impdi ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ∧ 𝑦 ∈ ( 0 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) +∞ ) ) → ( abs ‘ ( ( 𝑌 ‘ 0 ) − ( 𝑌 ‘ 𝑦 ) ) ) ≤ ( 0 · ( abs ‘ ( 0 − 𝑦 ) ) ) )
61 28 60 syl3an3 ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ∧ ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ) → ( abs ‘ ( ( 𝑌 ‘ 0 ) − ( 𝑌 ‘ 𝑦 ) ) ) ≤ ( 0 · ( abs ‘ ( 0 − 𝑦 ) ) ) )
62 61 3expa ⊢ ( ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ) ∧ ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ) → ( abs ‘ ( ( 𝑌 ‘ 0 ) − ( 𝑌 ‘ 𝑦 ) ) ) ≤ ( 0 · ( abs ‘ ( 0 − 𝑦 ) ) ) )
63 62 3impdi ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ∧ 𝑦 ∈ 𝑆 ) → ( abs ‘ ( ( 𝑌 ‘ 0 ) − ( 𝑌 ‘ 𝑦 ) ) ) ≤ ( 0 · ( abs ‘ ( 0 − 𝑦 ) ) ) )
64 recnprss ⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
65 1 64 syl ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
66 65 sseld ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑆 → 𝑦 ∈ ℂ ) )
67 subcl ⊢ ( ( 0 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 0 − 𝑦 ) ∈ ℂ )
68 67 abscld ⊢ ( ( 0 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( abs ‘ ( 0 − 𝑦 ) ) ∈ ℝ )
69 9 68 mpan ⊢ ( 𝑦 ∈ ℂ → ( abs ‘ ( 0 − 𝑦 ) ) ∈ ℝ )
70 66 69 syl6 ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑆 → ( abs ‘ ( 0 − 𝑦 ) ) ∈ ℝ ) )
71 70 imp ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( abs ‘ ( 0 − 𝑦 ) ) ∈ ℝ )
72 71 recnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( abs ‘ ( 0 − 𝑦 ) ) ∈ ℂ )
73 72 mul02d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( 0 · ( abs ‘ ( 0 − 𝑦 ) ) ) = 0 )
74 73 3adant2 ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ∧ 𝑦 ∈ 𝑆 ) → ( 0 · ( abs ‘ ( 0 − 𝑦 ) ) ) = 0 )
75 63 74 breqtrd ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ∧ 𝑦 ∈ 𝑆 ) → ( abs ‘ ( ( 𝑌 ‘ 0 ) − ( 𝑌 ‘ 𝑦 ) ) ) ≤ 0 )
76 ffvelrn ⊢ ( ( 𝑌 : 𝑆 ⟶ ℂ ∧ 𝑦 ∈ 𝑆 ) → ( 𝑌 ‘ 𝑦 ) ∈ ℂ )
77 14 76 anim12dan ⊢ ( ( 𝑌 : 𝑆 ⟶ ℂ ∧ ( 0 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( ( 𝑌 ‘ 0 ) ∈ ℂ ∧ ( 𝑌 ‘ 𝑦 ) ∈ ℂ ) )
78 2 77 sylan ⊢ ( ( 𝜑 ∧ ( 0 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( ( 𝑌 ‘ 0 ) ∈ ℂ ∧ ( 𝑌 ‘ 𝑦 ) ∈ ℂ ) )
79 78 3impb ⊢ ( ( 𝜑 ∧ 0 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑌 ‘ 0 ) ∈ ℂ ∧ ( 𝑌 ‘ 𝑦 ) ∈ ℂ ) )
80 13 79 syl3an2 ⊢ ( ( 𝜑 ∧ 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑌 ‘ 0 ) ∈ ℂ ∧ ( 𝑌 ‘ 𝑦 ) ∈ ℂ ) )
81 80 3anidm12 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑌 ‘ 0 ) ∈ ℂ ∧ ( 𝑌 ‘ 𝑦 ) ∈ ℂ ) )
82 subcl ⊢ ( ( ( 𝑌 ‘ 0 ) ∈ ℂ ∧ ( 𝑌 ‘ 𝑦 ) ∈ ℂ ) → ( ( 𝑌 ‘ 0 ) − ( 𝑌 ‘ 𝑦 ) ) ∈ ℂ )
83 81 82 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑌 ‘ 0 ) − ( 𝑌 ‘ 𝑦 ) ) ∈ ℂ )
84 83 absge0d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 0 ≤ ( abs ‘ ( ( 𝑌 ‘ 0 ) − ( 𝑌 ‘ 𝑦 ) ) ) )
85 84 3adant2 ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ∧ 𝑦 ∈ 𝑆 ) → 0 ≤ ( abs ‘ ( ( 𝑌 ‘ 0 ) − ( 𝑌 ‘ 𝑦 ) ) ) )
86 83 abscld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( abs ‘ ( ( 𝑌 ‘ 0 ) − ( 𝑌 ‘ 𝑦 ) ) ) ∈ ℝ )
87 letri3 ⊢ ( ( ( abs ‘ ( ( 𝑌 ‘ 0 ) − ( 𝑌 ‘ 𝑦 ) ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( abs ‘ ( ( 𝑌 ‘ 0 ) − ( 𝑌 ‘ 𝑦 ) ) ) = 0 ↔ ( ( abs ‘ ( ( 𝑌 ‘ 0 ) − ( 𝑌 ‘ 𝑦 ) ) ) ≤ 0 ∧ 0 ≤ ( abs ‘ ( ( 𝑌 ‘ 0 ) − ( 𝑌 ‘ 𝑦 ) ) ) ) ) )
88 86 6 87 sylancl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( abs ‘ ( ( 𝑌 ‘ 0 ) − ( 𝑌 ‘ 𝑦 ) ) ) = 0 ↔ ( ( abs ‘ ( ( 𝑌 ‘ 0 ) − ( 𝑌 ‘ 𝑦 ) ) ) ≤ 0 ∧ 0 ≤ ( abs ‘ ( ( 𝑌 ‘ 0 ) − ( 𝑌 ‘ 𝑦 ) ) ) ) ) )
89 88 3adant2 ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ∧ 𝑦 ∈ 𝑆 ) → ( ( abs ‘ ( ( 𝑌 ‘ 0 ) − ( 𝑌 ‘ 𝑦 ) ) ) = 0 ↔ ( ( abs ‘ ( ( 𝑌 ‘ 0 ) − ( 𝑌 ‘ 𝑦 ) ) ) ≤ 0 ∧ 0 ≤ ( abs ‘ ( ( 𝑌 ‘ 0 ) − ( 𝑌 ‘ 𝑦 ) ) ) ) ) )
90 75 85 89 mpbir2and ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ∧ 𝑦 ∈ 𝑆 ) → ( abs ‘ ( ( 𝑌 ‘ 0 ) − ( 𝑌 ‘ 𝑦 ) ) ) = 0 )
91 83 abs00ad ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( abs ‘ ( ( 𝑌 ‘ 0 ) − ( 𝑌 ‘ 𝑦 ) ) ) = 0 ↔ ( ( 𝑌 ‘ 0 ) − ( 𝑌 ‘ 𝑦 ) ) = 0 ) )
92 91 3adant2 ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ∧ 𝑦 ∈ 𝑆 ) → ( ( abs ‘ ( ( 𝑌 ‘ 0 ) − ( 𝑌 ‘ 𝑦 ) ) ) = 0 ↔ ( ( 𝑌 ‘ 0 ) − ( 𝑌 ‘ 𝑦 ) ) = 0 ) )
93 90 92 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑌 ‘ 0 ) − ( 𝑌 ‘ 𝑦 ) ) = 0 )
94 subeq0 ⊢ ( ( ( 𝑌 ‘ 0 ) ∈ ℂ ∧ ( 𝑌 ‘ 𝑦 ) ∈ ℂ ) → ( ( ( 𝑌 ‘ 0 ) − ( 𝑌 ‘ 𝑦 ) ) = 0 ↔ ( 𝑌 ‘ 0 ) = ( 𝑌 ‘ 𝑦 ) ) )
95 81 94 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( ( 𝑌 ‘ 0 ) − ( 𝑌 ‘ 𝑦 ) ) = 0 ↔ ( 𝑌 ‘ 0 ) = ( 𝑌 ‘ 𝑦 ) ) )
96 95 3adant2 ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ∧ 𝑦 ∈ 𝑆 ) → ( ( ( 𝑌 ‘ 0 ) − ( 𝑌 ‘ 𝑦 ) ) = 0 ↔ ( 𝑌 ‘ 0 ) = ( 𝑌 ‘ 𝑦 ) ) )
97 93 96 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝑌 ‘ 0 ) = ( 𝑌 ‘ 𝑦 ) )
98 97 3expa ⊢ ( ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝑌 ‘ 0 ) = ( 𝑌 ‘ 𝑦 ) )
99 23 98 eqtr2d ⊢ ( ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝑌 ‘ 𝑦 ) = ( ( 𝑆 × { ( 𝑌 ‘ 0 ) } ) ‘ 𝑦 ) )
100 18 21 99 eqfnfvd ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ) → 𝑌 = ( 𝑆 × { ( 𝑌 ‘ 0 ) } ) )
101 sneq ⊢ ( 𝑥 = ( 𝑌 ‘ 0 ) → { 𝑥 } = { ( 𝑌 ‘ 0 ) } )
102 101 xpeq2d ⊢ ( 𝑥 = ( 𝑌 ‘ 0 ) → ( 𝑆 × { 𝑥 } ) = ( 𝑆 × { ( 𝑌 ‘ 0 ) } ) )
103 102 rspceeqv ⊢ ( ( ( 𝑌 ‘ 0 ) ∈ ℂ ∧ 𝑌 = ( 𝑆 × { ( 𝑌 ‘ 0 ) } ) ) → ∃ 𝑥 ∈ ℂ 𝑌 = ( 𝑆 × { 𝑥 } ) )
104 16 100 103 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ) → ∃ 𝑥 ∈ ℂ 𝑌 = ( 𝑆 × { 𝑥 } ) )
105 104 ex ⊢ ( 𝜑 → ( ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) → ∃ 𝑥 ∈ ℂ 𝑌 = ( 𝑆 × { 𝑥 } ) ) )
106 oveq2 ⊢ ( 𝑌 = ( 𝑆 × { 𝑥 } ) → ( 𝑆 D 𝑌 ) = ( 𝑆 D ( 𝑆 × { 𝑥 } ) ) )
107 106 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑌 = ( 𝑆 × { 𝑥 } ) ) → ( 𝑆 D 𝑌 ) = ( 𝑆 D ( 𝑆 × { 𝑥 } ) ) )
108 dvsconst ⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑥 ∈ ℂ ) → ( 𝑆 D ( 𝑆 × { 𝑥 } ) ) = ( 𝑆 × { 0 } ) )
109 1 108 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝑆 D ( 𝑆 × { 𝑥 } ) ) = ( 𝑆 × { 0 } ) )
110 109 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑌 = ( 𝑆 × { 𝑥 } ) ) → ( 𝑆 D ( 𝑆 × { 𝑥 } ) ) = ( 𝑆 × { 0 } ) )
111 107 110 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑌 = ( 𝑆 × { 𝑥 } ) ) → ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) )
112 111 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℂ 𝑌 = ( 𝑆 × { 𝑥 } ) → ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ) )
113 105 112 impbid ⊢ ( 𝜑 → ( ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ↔ ∃ 𝑥 ∈ ℂ 𝑌 = ( 𝑆 × { 𝑥 } ) ) )
114 sneq ⊢ ( 𝑐 = 𝑥 → { 𝑐 } = { 𝑥 } )
115 114 xpeq2d ⊢ ( 𝑐 = 𝑥 → ( 𝑆 × { 𝑐 } ) = ( 𝑆 × { 𝑥 } ) )
116 115 eqeq2d ⊢ ( 𝑐 = 𝑥 → ( 𝑌 = ( 𝑆 × { 𝑐 } ) ↔ 𝑌 = ( 𝑆 × { 𝑥 } ) ) )
117 116 cbvrexvw ⊢ ( ∃ 𝑐 ∈ ℂ 𝑌 = ( 𝑆 × { 𝑐 } ) ↔ ∃ 𝑥 ∈ ℂ 𝑌 = ( 𝑆 × { 𝑥 } ) )
118 113 117 bitr4di ⊢ ( 𝜑 → ( ( 𝑆 D 𝑌 ) = ( 𝑆 × { 0 } ) ↔ ∃ 𝑐 ∈ ℂ 𝑌 = ( 𝑆 × { 𝑐 } ) ) )