shftlem

Description: Two ways to write a shifted set ( B + A ) . (Contributed by Mario Carneiro, 3-Nov-2013)

		Ref	Expression
	Assertion	shftlem	$⊢ (A \in ℂ \land B \subseteq ℂ) \to \{x \in ℂ \| x - A \in B\} = \{x \| \exists y \in B x = y + A\}$

Proof

Step	Hyp	Ref	Expression
1		df-rab	$⊢ \{x \in ℂ \| x - A \in B\} = \{x \| (x \in ℂ \land x - A \in B)\}$
2		npcan	$⊢ (x \in ℂ \land A \in ℂ) \to x - A + A = x$
3	2	ancoms	$⊢ (A \in ℂ \land x \in ℂ) \to x - A + A = x$
4	3	eqcomd	$⊢ (A \in ℂ \land x \in ℂ) \to x = x - A + A$
5		oveq1	$⊢ y = x - A \to y + A = x - A + A$
6	5	rspceeqv	$⊢ (x - A \in B \land x = x - A + A) \to \exists y \in B x = y + A$
7	6	expcom	$⊢ x = x - A + A \to (x - A \in B \to \exists y \in B x = y + A)$
8	4 7	syl	$⊢ (A \in ℂ \land x \in ℂ) \to (x - A \in B \to \exists y \in B x = y + A)$
9	8	expimpd	$⊢ A \in ℂ \to ((x \in ℂ \land x - A \in B) \to \exists y \in B x = y + A)$
10	9	adantr	$⊢ (A \in ℂ \land B \subseteq ℂ) \to ((x \in ℂ \land x - A \in B) \to \exists y \in B x = y + A)$
11		ssel2	$⊢ (B \subseteq ℂ \land y \in B) \to y \in ℂ$
12		addcl	$⊢ (y \in ℂ \land A \in ℂ) \to y + A \in ℂ$
13	11 12	sylan	$⊢ ((B \subseteq ℂ \land y \in B) \land A \in ℂ) \to y + A \in ℂ$
14		pncan	$⊢ (y \in ℂ \land A \in ℂ) \to y + A - A = y$
15	11 14	sylan	$⊢ ((B \subseteq ℂ \land y \in B) \land A \in ℂ) \to y + A - A = y$
16		simplr	$⊢ ((B \subseteq ℂ \land y \in B) \land A \in ℂ) \to y \in B$
17	15 16	eqeltrd	$⊢ ((B \subseteq ℂ \land y \in B) \land A \in ℂ) \to y + A - A \in B$
18	13 17	jca	$⊢ ((B \subseteq ℂ \land y \in B) \land A \in ℂ) \to (y + A \in ℂ \land y + A - A \in B)$
19	18	ancoms	$⊢ (A \in ℂ \land (B \subseteq ℂ \land y \in B)) \to (y + A \in ℂ \land y + A - A \in B)$
20	19	anassrs	$⊢ ((A \in ℂ \land B \subseteq ℂ) \land y \in B) \to (y + A \in ℂ \land y + A - A \in B)$
21		eleq1	$⊢ x = y + A \to (x \in ℂ \leftrightarrow y + A \in ℂ)$
22		oveq1	$⊢ x = y + A \to x - A = y + A - A$
23	22	eleq1d	$⊢ x = y + A \to (x - A \in B \leftrightarrow y + A - A \in B)$
24	21 23	anbi12d	$⊢ x = y + A \to ((x \in ℂ \land x - A \in B) \leftrightarrow (y + A \in ℂ \land y + A - A \in B))$
25	20 24	syl5ibrcom	$⊢ ((A \in ℂ \land B \subseteq ℂ) \land y \in B) \to (x = y + A \to (x \in ℂ \land x - A \in B))$
26	25	rexlimdva	$⊢ (A \in ℂ \land B \subseteq ℂ) \to (\exists y \in B x = y + A \to (x \in ℂ \land x - A \in B))$
27	10 26	impbid	$⊢ (A \in ℂ \land B \subseteq ℂ) \to ((x \in ℂ \land x - A \in B) \leftrightarrow \exists y \in B x = y + A)$
28	27	abbidv	$⊢ (A \in ℂ \land B \subseteq ℂ) \to \{x \| (x \in ℂ \land x - A \in B)\} = \{x \| \exists y \in B x = y + A\}$
29	1 28	eqtrid	$⊢ (A \in ℂ \land B \subseteq ℂ) \to \{x \in ℂ \| x - A \in B\} = \{x \| \exists y \in B x = y + A\}$

Metamath Proof Explorer

Theorem shftlem

Proof