Metamath Proof Explorer


Theorem supsubc

Description: The supremum function distributes over subtraction in a sense similar to that in supaddc . (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses supsubc.a1
|- ( ph -> A C_ RR )
supsubc.a2
|- ( ph -> A =/= (/) )
supsubc.a3
|- ( ph -> E. x e. RR A. y e. A y <_ x )
supsubc.b
|- ( ph -> B e. RR )
supsubc.c
|- C = { z | E. v e. A z = ( v - B ) }
Assertion supsubc
|- ( ph -> ( sup ( A , RR , < ) - B ) = sup ( C , RR , < ) )

Proof

Step Hyp Ref Expression
1 supsubc.a1
 |-  ( ph -> A C_ RR )
2 supsubc.a2
 |-  ( ph -> A =/= (/) )
3 supsubc.a3
 |-  ( ph -> E. x e. RR A. y e. A y <_ x )
4 supsubc.b
 |-  ( ph -> B e. RR )
5 supsubc.c
 |-  C = { z | E. v e. A z = ( v - B ) }
6 5 a1i
 |-  ( ph -> C = { z | E. v e. A z = ( v - B ) } )
7 1 sselda
 |-  ( ( ph /\ v e. A ) -> v e. RR )
8 7 recnd
 |-  ( ( ph /\ v e. A ) -> v e. CC )
9 4 recnd
 |-  ( ph -> B e. CC )
10 9 adantr
 |-  ( ( ph /\ v e. A ) -> B e. CC )
11 8 10 negsubd
 |-  ( ( ph /\ v e. A ) -> ( v + -u B ) = ( v - B ) )
12 11 eqcomd
 |-  ( ( ph /\ v e. A ) -> ( v - B ) = ( v + -u B ) )
13 12 eqeq2d
 |-  ( ( ph /\ v e. A ) -> ( z = ( v - B ) <-> z = ( v + -u B ) ) )
14 13 rexbidva
 |-  ( ph -> ( E. v e. A z = ( v - B ) <-> E. v e. A z = ( v + -u B ) ) )
15 14 abbidv
 |-  ( ph -> { z | E. v e. A z = ( v - B ) } = { z | E. v e. A z = ( v + -u B ) } )
16 eqidd
 |-  ( ph -> { z | E. v e. A z = ( v + -u B ) } = { z | E. v e. A z = ( v + -u B ) } )
17 6 15 16 3eqtrd
 |-  ( ph -> C = { z | E. v e. A z = ( v + -u B ) } )
18 17 supeq1d
 |-  ( ph -> sup ( C , RR , < ) = sup ( { z | E. v e. A z = ( v + -u B ) } , RR , < ) )
19 4 renegcld
 |-  ( ph -> -u B e. RR )
20 eqid
 |-  { z | E. v e. A z = ( v + -u B ) } = { z | E. v e. A z = ( v + -u B ) }
21 1 2 3 19 20 supaddc
 |-  ( ph -> ( sup ( A , RR , < ) + -u B ) = sup ( { z | E. v e. A z = ( v + -u B ) } , RR , < ) )
22 21 eqcomd
 |-  ( ph -> sup ( { z | E. v e. A z = ( v + -u B ) } , RR , < ) = ( sup ( A , RR , < ) + -u B ) )
23 suprcl
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR , < ) e. RR )
24 1 2 3 23 syl3anc
 |-  ( ph -> sup ( A , RR , < ) e. RR )
25 24 recnd
 |-  ( ph -> sup ( A , RR , < ) e. CC )
26 25 9 negsubd
 |-  ( ph -> ( sup ( A , RR , < ) + -u B ) = ( sup ( A , RR , < ) - B ) )
27 18 22 26 3eqtrrd
 |-  ( ph -> ( sup ( A , RR , < ) - B ) = sup ( C , RR , < ) )