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