shsel3

Description: Membership in the subspace sum of two Hilbert subspaces, using vector subtraction. (Contributed by NM, 20-Jan-2007) (New usage is discouraged.)

		Ref	Expression
	Assertion	shsel3	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ}) \to (C \in (A +_{ℋ} B) \leftrightarrow \exists x \in A \exists y \in B C = x -_{ℎ} y)$

Proof

Step	Hyp	Ref	Expression
1		shsel	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ}) \to (C \in (A +_{ℋ} B) \leftrightarrow \exists x \in A \exists z \in B C = x +_{ℎ} z)$
2		id	$⊢ C = x +_{ℎ} z \to C = x +_{ℎ} z$
3		shel	$⊢ (A \in S_{ℋ} \land x \in A) \to x \in ℋ$
4		shel	$⊢ (B \in S_{ℋ} \land z \in B) \to z \in ℋ$
5		hvaddsubval	$⊢ (x \in ℋ \land z \in ℋ) \to x +_{ℎ} z = x -_{ℎ} (-1 \cdot_{ℎ} z)$
6	3 4 5	syl2an	$⊢ ((A \in S_{ℋ} \land x \in A) \land (B \in S_{ℋ} \land z \in B)) \to x +_{ℎ} z = x -_{ℎ} (-1 \cdot_{ℎ} z)$
7	6	an4s	$⊢ ((A \in S_{ℋ} \land B \in S_{ℋ}) \land (x \in A \land z \in B)) \to x +_{ℎ} z = x -_{ℎ} (-1 \cdot_{ℎ} z)$
8	7	anassrs	$⊢ (((A \in S_{ℋ} \land B \in S_{ℋ}) \land x \in A) \land z \in B) \to x +_{ℎ} z = x -_{ℎ} (-1 \cdot_{ℎ} z)$
9	2 8	sylan9eqr	$⊢ ((((A \in S_{ℋ} \land B \in S_{ℋ}) \land x \in A) \land z \in B) \land C = x +_{ℎ} z) \to C = x -_{ℎ} (-1 \cdot_{ℎ} z)$
10		neg1cn	$⊢ - 1 \in ℂ$
11		shmulcl	$⊢ (B \in S_{ℋ} \land - 1 \in ℂ \land z \in B) \to -1 \cdot_{ℎ} z \in B$
12	10 11	mp3an2	$⊢ (B \in S_{ℋ} \land z \in B) \to -1 \cdot_{ℎ} z \in B$
13	12	adantll	$⊢ ((A \in S_{ℋ} \land B \in S_{ℋ}) \land z \in B) \to -1 \cdot_{ℎ} z \in B$
14	13	adantlr	$⊢ (((A \in S_{ℋ} \land B \in S_{ℋ}) \land x \in A) \land z \in B) \to -1 \cdot_{ℎ} z \in B$
15		oveq2	$⊢ y = -1 \cdot_{ℎ} z \to x -_{ℎ} y = x -_{ℎ} (-1 \cdot_{ℎ} z)$
16	15	rspceeqv	$⊢ (-1 \cdot_{ℎ} z \in B \land C = x -_{ℎ} (-1 \cdot_{ℎ} z)) \to \exists y \in B C = x -_{ℎ} y$
17	14 16	sylan	$⊢ ((((A \in S_{ℋ} \land B \in S_{ℋ}) \land x \in A) \land z \in B) \land C = x -_{ℎ} (-1 \cdot_{ℎ} z)) \to \exists y \in B C = x -_{ℎ} y$
18	9 17	syldan	$⊢ ((((A \in S_{ℋ} \land B \in S_{ℋ}) \land x \in A) \land z \in B) \land C = x +_{ℎ} z) \to \exists y \in B C = x -_{ℎ} y$
19	18	rexlimdva2	$⊢ ((A \in S_{ℋ} \land B \in S_{ℋ}) \land x \in A) \to (\exists z \in B C = x +_{ℎ} z \to \exists y \in B C = x -_{ℎ} y)$
20		id	$⊢ C = x -_{ℎ} y \to C = x -_{ℎ} y$
21		shel	$⊢ (B \in S_{ℋ} \land y \in B) \to y \in ℋ$
22		hvsubval	$⊢ (x \in ℋ \land y \in ℋ) \to x -_{ℎ} y = x +_{ℎ} (-1 \cdot_{ℎ} y)$
23	3 21 22	syl2an	$⊢ ((A \in S_{ℋ} \land x \in A) \land (B \in S_{ℋ} \land y \in B)) \to x -_{ℎ} y = x +_{ℎ} (-1 \cdot_{ℎ} y)$
24	23	an4s	$⊢ ((A \in S_{ℋ} \land B \in S_{ℋ}) \land (x \in A \land y \in B)) \to x -_{ℎ} y = x +_{ℎ} (-1 \cdot_{ℎ} y)$
25	24	anassrs	$⊢ (((A \in S_{ℋ} \land B \in S_{ℋ}) \land x \in A) \land y \in B) \to x -_{ℎ} y = x +_{ℎ} (-1 \cdot_{ℎ} y)$
26	20 25	sylan9eqr	$⊢ ((((A \in S_{ℋ} \land B \in S_{ℋ}) \land x \in A) \land y \in B) \land C = x -_{ℎ} y) \to C = x +_{ℎ} (-1 \cdot_{ℎ} y)$
27		shmulcl	$⊢ (B \in S_{ℋ} \land - 1 \in ℂ \land y \in B) \to -1 \cdot_{ℎ} y \in B$
28	10 27	mp3an2	$⊢ (B \in S_{ℋ} \land y \in B) \to -1 \cdot_{ℎ} y \in B$
29	28	adantll	$⊢ ((A \in S_{ℋ} \land B \in S_{ℋ}) \land y \in B) \to -1 \cdot_{ℎ} y \in B$
30	29	adantlr	$⊢ (((A \in S_{ℋ} \land B \in S_{ℋ}) \land x \in A) \land y \in B) \to -1 \cdot_{ℎ} y \in B$
31		oveq2	$⊢ z = -1 \cdot_{ℎ} y \to x +_{ℎ} z = x +_{ℎ} (-1 \cdot_{ℎ} y)$
32	31	rspceeqv	$⊢ (-1 \cdot_{ℎ} y \in B \land C = x +_{ℎ} (-1 \cdot_{ℎ} y)) \to \exists z \in B C = x +_{ℎ} z$
33	30 32	sylan	$⊢ ((((A \in S_{ℋ} \land B \in S_{ℋ}) \land x \in A) \land y \in B) \land C = x +_{ℎ} (-1 \cdot_{ℎ} y)) \to \exists z \in B C = x +_{ℎ} z$
34	26 33	syldan	$⊢ ((((A \in S_{ℋ} \land B \in S_{ℋ}) \land x \in A) \land y \in B) \land C = x -_{ℎ} y) \to \exists z \in B C = x +_{ℎ} z$
35	34	rexlimdva2	$⊢ ((A \in S_{ℋ} \land B \in S_{ℋ}) \land x \in A) \to (\exists y \in B C = x -_{ℎ} y \to \exists z \in B C = x +_{ℎ} z)$
36	19 35	impbid	$⊢ ((A \in S_{ℋ} \land B \in S_{ℋ}) \land x \in A) \to (\exists z \in B C = x +_{ℎ} z \leftrightarrow \exists y \in B C = x -_{ℎ} y)$
37	36	rexbidva	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ}) \to (\exists x \in A \exists z \in B C = x +_{ℎ} z \leftrightarrow \exists x \in A \exists y \in B C = x -_{ℎ} y)$
38	1 37	bitrd	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ}) \to (C \in (A +_{ℋ} B) \leftrightarrow \exists x \in A \exists y \in B C = x -_{ℎ} y)$

Metamath Proof Explorer

Theorem shsel3

Proof