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	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	supsubc.a2	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
	supsubc.a3	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
	supsubc.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	supsubc.c	⊢ 𝐶 = { 𝑧 ∣ ∃ 𝑣 ∈ 𝐴 𝑧 = ( 𝑣 − 𝐵 ) }
Assertion	supsubc	⊢ ( 𝜑 → ( sup ( 𝐴 , ℝ , < ) − 𝐵 ) = sup ( 𝐶 , ℝ , < ) )

Proof

Step	Hyp	Ref	Expression
1		supsubc.a1	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2		supsubc.a2	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
3		supsubc.a3	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
4		supsubc.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
5		supsubc.c	⊢ 𝐶 = { 𝑧 ∣ ∃ 𝑣 ∈ 𝐴 𝑧 = ( 𝑣 − 𝐵 ) }
6	5	a1i	⊢ ( 𝜑 → 𝐶 = { 𝑧 ∣ ∃ 𝑣 ∈ 𝐴 𝑧 = ( 𝑣 − 𝐵 ) } )
7	1	sselda	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → 𝑣 ∈ ℝ )
8	7	recnd	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → 𝑣 ∈ ℂ )
9	4	recnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
10	9	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
11	8 10	negsubd	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝑣 + - 𝐵 ) = ( 𝑣 − 𝐵 ) )
12	11	eqcomd	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝑣 − 𝐵 ) = ( 𝑣 + - 𝐵 ) )
13	12	eqeq2d	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝑧 = ( 𝑣 − 𝐵 ) ↔ 𝑧 = ( 𝑣 + - 𝐵 ) ) )
14	13	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑣 ∈ 𝐴 𝑧 = ( 𝑣 − 𝐵 ) ↔ ∃ 𝑣 ∈ 𝐴 𝑧 = ( 𝑣 + - 𝐵 ) ) )
15	14	abbidv	⊢ ( 𝜑 → { 𝑧 ∣ ∃ 𝑣 ∈ 𝐴 𝑧 = ( 𝑣 − 𝐵 ) } = { 𝑧 ∣ ∃ 𝑣 ∈ 𝐴 𝑧 = ( 𝑣 + - 𝐵 ) } )
16		eqidd	⊢ ( 𝜑 → { 𝑧 ∣ ∃ 𝑣 ∈ 𝐴 𝑧 = ( 𝑣 + - 𝐵 ) } = { 𝑧 ∣ ∃ 𝑣 ∈ 𝐴 𝑧 = ( 𝑣 + - 𝐵 ) } )
17	6 15 16	3eqtrd	⊢ ( 𝜑 → 𝐶 = { 𝑧 ∣ ∃ 𝑣 ∈ 𝐴 𝑧 = ( 𝑣 + - 𝐵 ) } )
18	17	supeq1d	⊢ ( 𝜑 → sup ( 𝐶 , ℝ , < ) = sup ( { 𝑧 ∣ ∃ 𝑣 ∈ 𝐴 𝑧 = ( 𝑣 + - 𝐵 ) } , ℝ , < ) )
19	4	renegcld	⊢ ( 𝜑 → - 𝐵 ∈ ℝ )
20		eqid	⊢ { 𝑧 ∣ ∃ 𝑣 ∈ 𝐴 𝑧 = ( 𝑣 + - 𝐵 ) } = { 𝑧 ∣ ∃ 𝑣 ∈ 𝐴 𝑧 = ( 𝑣 + - 𝐵 ) }
21	1 2 3 19 20	supaddc	⊢ ( 𝜑 → ( sup ( 𝐴 , ℝ , < ) + - 𝐵 ) = sup ( { 𝑧 ∣ ∃ 𝑣 ∈ 𝐴 𝑧 = ( 𝑣 + - 𝐵 ) } , ℝ , < ) )
22	21	eqcomd	⊢ ( 𝜑 → sup ( { 𝑧 ∣ ∃ 𝑣 ∈ 𝐴 𝑧 = ( 𝑣 + - 𝐵 ) } , ℝ , < ) = ( sup ( 𝐴 , ℝ , < ) + - 𝐵 ) )
23		suprcl	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → sup ( 𝐴 , ℝ , < ) ∈ ℝ )
24	1 2 3 23	syl3anc	⊢ ( 𝜑 → sup ( 𝐴 , ℝ , < ) ∈ ℝ )
25	24	recnd	⊢ ( 𝜑 → sup ( 𝐴 , ℝ , < ) ∈ ℂ )
26	25 9	negsubd	⊢ ( 𝜑 → ( sup ( 𝐴 , ℝ , < ) + - 𝐵 ) = ( sup ( 𝐴 , ℝ , < ) − 𝐵 ) )
27	18 22 26	3eqtrrd	⊢ ( 𝜑 → ( sup ( 𝐴 , ℝ , < ) − 𝐵 ) = sup ( 𝐶 , ℝ , < ) )