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 ffvelcdm โŠข ( ( ๐‘Œ : ๐‘† โŸถ โ„‚ โˆง 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 ffvelcdm โŠข ( ( ๐‘Œ : ๐‘† โŸถ โ„‚ โˆง ๐‘ฆ โˆˆ ๐‘† ) โ†’ ( ๐‘Œ โ€˜ ๐‘ฆ ) โˆˆ โ„‚ )
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 } ) โ†” โˆƒ ๐‘ โˆˆ โ„‚ ๐‘Œ = ( ๐‘† ร— { ๐‘ } ) ) )