Theorem shft2rab

Description: If B is a shift of A by C , then A is a shift of B by -u C . (Contributed by Mario Carneiro, 22-Mar-2014) (Revised by Mario Carneiro, 6-Apr-2015)

	Ref	Expression
Hypotheses	ovolshft.1	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	ovolshft.2	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	ovolshft.3	⊢ ( 𝜑 → 𝐵 = { 𝑥 ∈ ℝ ∣ ( 𝑥 − 𝐶 ) ∈ 𝐴 } )
Assertion	shft2rab	⊢ ( 𝜑 → 𝐴 = { 𝑦 ∈ ℝ ∣ ( 𝑦 − - 𝐶 ) ∈ 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		ovolshft.1	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2		ovolshft.2	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
3		ovolshft.3	⊢ ( 𝜑 → 𝐵 = { 𝑥 ∈ ℝ ∣ ( 𝑥 − 𝐶 ) ∈ 𝐴 } )
4	1	sseld	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ℝ ) )
5	4	pm4.71rd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↔ ( 𝑦 ∈ ℝ ∧ 𝑦 ∈ 𝐴 ) ) )
6		recn	⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
7	2	recnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
8		subneg	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝑦 − - 𝐶 ) = ( 𝑦 + 𝐶 ) )
9	6 7 8	syl2anr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑦 − - 𝐶 ) = ( 𝑦 + 𝐶 ) )
10	3	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝐵 = { 𝑥 ∈ ℝ ∣ ( 𝑥 − 𝐶 ) ∈ 𝐴 } )
11	9 10	eleq12d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( 𝑦 − - 𝐶 ) ∈ 𝐵 ↔ ( 𝑦 + 𝐶 ) ∈ { 𝑥 ∈ ℝ ∣ ( 𝑥 − 𝐶 ) ∈ 𝐴 } ) )
12		id	⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℝ )
13		readdcl	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝑦 + 𝐶 ) ∈ ℝ )
14	12 2 13	syl2anr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑦 + 𝐶 ) ∈ ℝ )
15		oveq1	⊢ ( 𝑥 = ( 𝑦 + 𝐶 ) → ( 𝑥 − 𝐶 ) = ( ( 𝑦 + 𝐶 ) − 𝐶 ) )
16	15	eleq1d	⊢ ( 𝑥 = ( 𝑦 + 𝐶 ) → ( ( 𝑥 − 𝐶 ) ∈ 𝐴 ↔ ( ( 𝑦 + 𝐶 ) − 𝐶 ) ∈ 𝐴 ) )
17	16	elrab3	⊢ ( ( 𝑦 + 𝐶 ) ∈ ℝ → ( ( 𝑦 + 𝐶 ) ∈ { 𝑥 ∈ ℝ ∣ ( 𝑥 − 𝐶 ) ∈ 𝐴 } ↔ ( ( 𝑦 + 𝐶 ) − 𝐶 ) ∈ 𝐴 ) )
18	14 17	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( 𝑦 + 𝐶 ) ∈ { 𝑥 ∈ ℝ ∣ ( 𝑥 − 𝐶 ) ∈ 𝐴 } ↔ ( ( 𝑦 + 𝐶 ) − 𝐶 ) ∈ 𝐴 ) )
19		pncan	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝑦 + 𝐶 ) − 𝐶 ) = 𝑦 )
20	6 7 19	syl2anr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( 𝑦 + 𝐶 ) − 𝐶 ) = 𝑦 )
21	20	eleq1d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( ( 𝑦 + 𝐶 ) − 𝐶 ) ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
22	11 18 21	3bitrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( 𝑦 − - 𝐶 ) ∈ 𝐵 ↔ 𝑦 ∈ 𝐴 ) )
23	22	pm5.32da	⊢ ( 𝜑 → ( ( 𝑦 ∈ ℝ ∧ ( 𝑦 − - 𝐶 ) ∈ 𝐵 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝑦 ∈ 𝐴 ) ) )
24	5 23	bitr4d	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↔ ( 𝑦 ∈ ℝ ∧ ( 𝑦 − - 𝐶 ) ∈ 𝐵 ) ) )
25	24	abbi2dv	⊢ ( 𝜑 → 𝐴 = { 𝑦 ∣ ( 𝑦 ∈ ℝ ∧ ( 𝑦 − - 𝐶 ) ∈ 𝐵 ) } )
26		df-rab	⊢ { 𝑦 ∈ ℝ ∣ ( 𝑦 − - 𝐶 ) ∈ 𝐵 } = { 𝑦 ∣ ( 𝑦 ∈ ℝ ∧ ( 𝑦 − - 𝐶 ) ∈ 𝐵 ) }
27	25 26	eqtr4di	⊢ ( 𝜑 → 𝐴 = { 𝑦 ∈ ℝ ∣ ( 𝑦 − - 𝐶 ) ∈ 𝐵 } )