pjhthmo

Description: Projection Theorem, uniqueness part. Any two disjoint subspaces yield a unique decomposition of vectors into each subspace. (Contributed by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

		Ref	Expression
	Assertion	pjhthmo	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ} \land A \cap B = 0_{ℋ}) \to \exists^{*} x (x \in A \land \exists y \in B C = x +_{ℎ} y)$

Proof

Step	Hyp	Ref	Expression
1		an4	$⊢ ((x \in A \land z \in A) \land (\exists y \in B C = x +_{ℎ} y \land \exists w \in B C = z +_{ℎ} w)) \leftrightarrow ((x \in A \land \exists y \in B C = x +_{ℎ} y) \land (z \in A \land \exists w \in B C = z +_{ℎ} w))$
2		reeanv	$⊢ \exists y \in B \exists w \in B (C = x +_{ℎ} y \land C = z +_{ℎ} w) \leftrightarrow (\exists y \in B C = x +_{ℎ} y \land \exists w \in B C = z +_{ℎ} w)$
3		simpll1	$⊢ (((A \in S_{ℋ} \land B \in S_{ℋ} \land A \cap B = 0_{ℋ}) \land (x \in A \land z \in A)) \land ((y \in B \land w \in B) \land (C = x +_{ℎ} y \land C = z +_{ℎ} w))) \to A \in S_{ℋ}$
4		simpll2	$⊢ (((A \in S_{ℋ} \land B \in S_{ℋ} \land A \cap B = 0_{ℋ}) \land (x \in A \land z \in A)) \land ((y \in B \land w \in B) \land (C = x +_{ℎ} y \land C = z +_{ℎ} w))) \to B \in S_{ℋ}$
5		simpll3	$⊢ (((A \in S_{ℋ} \land B \in S_{ℋ} \land A \cap B = 0_{ℋ}) \land (x \in A \land z \in A)) \land ((y \in B \land w \in B) \land (C = x +_{ℎ} y \land C = z +_{ℎ} w))) \to A \cap B = 0_{ℋ}$
6		simplrl	$⊢ (((A \in S_{ℋ} \land B \in S_{ℋ} \land A \cap B = 0_{ℋ}) \land (x \in A \land z \in A)) \land ((y \in B \land w \in B) \land (C = x +_{ℎ} y \land C = z +_{ℎ} w))) \to x \in A$
7		simprll	$⊢ (((A \in S_{ℋ} \land B \in S_{ℋ} \land A \cap B = 0_{ℋ}) \land (x \in A \land z \in A)) \land ((y \in B \land w \in B) \land (C = x +_{ℎ} y \land C = z +_{ℎ} w))) \to y \in B$
8		simplrr	$⊢ (((A \in S_{ℋ} \land B \in S_{ℋ} \land A \cap B = 0_{ℋ}) \land (x \in A \land z \in A)) \land ((y \in B \land w \in B) \land (C = x +_{ℎ} y \land C = z +_{ℎ} w))) \to z \in A$
9		simprlr	$⊢ (((A \in S_{ℋ} \land B \in S_{ℋ} \land A \cap B = 0_{ℋ}) \land (x \in A \land z \in A)) \land ((y \in B \land w \in B) \land (C = x +_{ℎ} y \land C = z +_{ℎ} w))) \to w \in B$
10		simprrl	$⊢ (((A \in S_{ℋ} \land B \in S_{ℋ} \land A \cap B = 0_{ℋ}) \land (x \in A \land z \in A)) \land ((y \in B \land w \in B) \land (C = x +_{ℎ} y \land C = z +_{ℎ} w))) \to C = x +_{ℎ} y$
11		simprrr	$⊢ (((A \in S_{ℋ} \land B \in S_{ℋ} \land A \cap B = 0_{ℋ}) \land (x \in A \land z \in A)) \land ((y \in B \land w \in B) \land (C = x +_{ℎ} y \land C = z +_{ℎ} w))) \to C = z +_{ℎ} w$
12	10 11	eqtr3d	$⊢ (((A \in S_{ℋ} \land B \in S_{ℋ} \land A \cap B = 0_{ℋ}) \land (x \in A \land z \in A)) \land ((y \in B \land w \in B) \land (C = x +_{ℎ} y \land C = z +_{ℎ} w))) \to x +_{ℎ} y = z +_{ℎ} w$
13	3 4 5 6 7 8 9 12	shuni	$⊢ (((A \in S_{ℋ} \land B \in S_{ℋ} \land A \cap B = 0_{ℋ}) \land (x \in A \land z \in A)) \land ((y \in B \land w \in B) \land (C = x +_{ℎ} y \land C = z +_{ℎ} w))) \to (x = z \land y = w)$
14	13	simpld	$⊢ (((A \in S_{ℋ} \land B \in S_{ℋ} \land A \cap B = 0_{ℋ}) \land (x \in A \land z \in A)) \land ((y \in B \land w \in B) \land (C = x +_{ℎ} y \land C = z +_{ℎ} w))) \to x = z$
15	14	exp32	$⊢ ((A \in S_{ℋ} \land B \in S_{ℋ} \land A \cap B = 0_{ℋ}) \land (x \in A \land z \in A)) \to ((y \in B \land w \in B) \to ((C = x +_{ℎ} y \land C = z +_{ℎ} w) \to x = z))$
16	15	rexlimdvv	$⊢ ((A \in S_{ℋ} \land B \in S_{ℋ} \land A \cap B = 0_{ℋ}) \land (x \in A \land z \in A)) \to (\exists y \in B \exists w \in B (C = x +_{ℎ} y \land C = z +_{ℎ} w) \to x = z)$
17	2 16	syl5bir	$⊢ ((A \in S_{ℋ} \land B \in S_{ℋ} \land A \cap B = 0_{ℋ}) \land (x \in A \land z \in A)) \to ((\exists y \in B C = x +_{ℎ} y \land \exists w \in B C = z +_{ℎ} w) \to x = z)$
18	17	expimpd	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ} \land A \cap B = 0_{ℋ}) \to (((x \in A \land z \in A) \land (\exists y \in B C = x +_{ℎ} y \land \exists w \in B C = z +_{ℎ} w)) \to x = z)$
19	1 18	syl5bir	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ} \land A \cap B = 0_{ℋ}) \to (((x \in A \land \exists y \in B C = x +_{ℎ} y) \land (z \in A \land \exists w \in B C = z +_{ℎ} w)) \to x = z)$
20	19	alrimivv	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ} \land A \cap B = 0_{ℋ}) \to \forall x \forall z (((x \in A \land \exists y \in B C = x +_{ℎ} y) \land (z \in A \land \exists w \in B C = z +_{ℎ} w)) \to x = z)$
21		eleq1w	$⊢ x = z \to (x \in A \leftrightarrow z \in A)$
22		oveq1	$⊢ x = z \to x +_{ℎ} y = z +_{ℎ} y$
23	22	eqeq2d	$⊢ x = z \to (C = x +_{ℎ} y \leftrightarrow C = z +_{ℎ} y)$
24	23	rexbidv	$⊢ x = z \to (\exists y \in B C = x +_{ℎ} y \leftrightarrow \exists y \in B C = z +_{ℎ} y)$
25		oveq2	$⊢ y = w \to z +_{ℎ} y = z +_{ℎ} w$
26	25	eqeq2d	$⊢ y = w \to (C = z +_{ℎ} y \leftrightarrow C = z +_{ℎ} w)$
27	26	cbvrexvw	$⊢ \exists y \in B C = z +_{ℎ} y \leftrightarrow \exists w \in B C = z +_{ℎ} w$
28	24 27	bitrdi	$⊢ x = z \to (\exists y \in B C = x +_{ℎ} y \leftrightarrow \exists w \in B C = z +_{ℎ} w)$
29	21 28	anbi12d	$⊢ x = z \to ((x \in A \land \exists y \in B C = x +_{ℎ} y) \leftrightarrow (z \in A \land \exists w \in B C = z +_{ℎ} w))$
30	29	mo4	$⊢ \exists^{*} x (x \in A \land \exists y \in B C = x +_{ℎ} y) \leftrightarrow \forall x \forall z (((x \in A \land \exists y \in B C = x +_{ℎ} y) \land (z \in A \land \exists w \in B C = z +_{ℎ} w)) \to x = z)$
31	20 30	sylibr	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ} \land A \cap B = 0_{ℋ}) \to \exists^{*} x (x \in A \land \exists y \in B C = x +_{ℎ} y)$

Metamath Proof Explorer

Theorem pjhthmo

Proof