pjpjpre

Description: Decomposition of a vector into projections. This formulation of axpjpj avoids pjhth . (Contributed by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjpjpre.1	$⊢ φ \to H \in C_{ℋ}$
	pjpjpre.2	$⊢ φ \to A \in (H +_{ℋ} ⊥ (H))$
Assertion	pjpjpre	$⊢ φ \to A = {proj}_{ℎ} (H) (A) +_{ℎ} {proj}_{ℎ} (⊥ (H)) (A)$

Proof

Step	Hyp	Ref	Expression
1		pjpjpre.1	$⊢ φ \to H \in C_{ℋ}$
2		pjpjpre.2	$⊢ φ \to A \in (H +_{ℋ} ⊥ (H))$
3		chsh	$⊢ H \in C_{ℋ} \to H \in S_{ℋ}$
4	1 3	syl	$⊢ φ \to H \in S_{ℋ}$
5		shocsh	$⊢ H \in S_{ℋ} \to ⊥ (H) \in S_{ℋ}$
6	4 5	syl	$⊢ φ \to ⊥ (H) \in S_{ℋ}$
7		shsel	$⊢ (H \in S_{ℋ} \land ⊥ (H) \in S_{ℋ}) \to (A \in (H +_{ℋ} ⊥ (H)) \leftrightarrow \exists x \in H \exists y \in ⊥ (H) A = x +_{ℎ} y)$
8	4 6 7	syl2anc	$⊢ φ \to (A \in (H +_{ℋ} ⊥ (H)) \leftrightarrow \exists x \in H \exists y \in ⊥ (H) A = x +_{ℎ} y)$
9	2 8	mpbid	$⊢ φ \to \exists x \in H \exists y \in ⊥ (H) A = x +_{ℎ} y$
10		simprr	$⊢ (φ \land ((x \in H \land y \in ⊥ (H)) \land A = x +_{ℎ} y)) \to A = x +_{ℎ} y$
11		simprll	$⊢ (φ \land ((x \in H \land y \in ⊥ (H)) \land A = x +_{ℎ} y)) \to x \in H$
12		simprlr	$⊢ (φ \land ((x \in H \land y \in ⊥ (H)) \land A = x +_{ℎ} y)) \to y \in ⊥ (H)$
13		rspe	$⊢ (y \in ⊥ (H) \land A = x +_{ℎ} y) \to \exists y \in ⊥ (H) A = x +_{ℎ} y$
14	12 10 13	syl2anc	$⊢ (φ \land ((x \in H \land y \in ⊥ (H)) \land A = x +_{ℎ} y)) \to \exists y \in ⊥ (H) A = x +_{ℎ} y$
15		pjpreeq	$⊢ (H \in C_{ℋ} \land A \in (H +_{ℋ} ⊥ (H))) \to ({proj}_{ℎ} (H) (A) = x \leftrightarrow (x \in H \land \exists y \in ⊥ (H) A = x +_{ℎ} y))$
16	1 2 15	syl2anc	$⊢ φ \to ({proj}_{ℎ} (H) (A) = x \leftrightarrow (x \in H \land \exists y \in ⊥ (H) A = x +_{ℎ} y))$
17	16	adantr	$⊢ (φ \land ((x \in H \land y \in ⊥ (H)) \land A = x +_{ℎ} y)) \to ({proj}_{ℎ} (H) (A) = x \leftrightarrow (x \in H \land \exists y \in ⊥ (H) A = x +_{ℎ} y))$
18	11 14 17	mpbir2and	$⊢ (φ \land ((x \in H \land y \in ⊥ (H)) \land A = x +_{ℎ} y)) \to {proj}_{ℎ} (H) (A) = x$
19		shococss	$⊢ H \in S_{ℋ} \to H \subseteq ⊥ (⊥ (H))$
20	4 19	syl	$⊢ φ \to H \subseteq ⊥ (⊥ (H))$
21	20	adantr	$⊢ (φ \land ((x \in H \land y \in ⊥ (H)) \land A = x +_{ℎ} y)) \to H \subseteq ⊥ (⊥ (H))$
22	21 11	sseldd	$⊢ (φ \land ((x \in H \land y \in ⊥ (H)) \land A = x +_{ℎ} y)) \to x \in ⊥ (⊥ (H))$
23	1	adantr	$⊢ (φ \land ((x \in H \land y \in ⊥ (H)) \land A = x +_{ℎ} y)) \to H \in C_{ℋ}$
24	23 3	syl	$⊢ (φ \land ((x \in H \land y \in ⊥ (H)) \land A = x +_{ℎ} y)) \to H \in S_{ℋ}$
25		shel	$⊢ (H \in S_{ℋ} \land x \in H) \to x \in ℋ$
26	24 11 25	syl2anc	$⊢ (φ \land ((x \in H \land y \in ⊥ (H)) \land A = x +_{ℎ} y)) \to x \in ℋ$
27	24 5	syl	$⊢ (φ \land ((x \in H \land y \in ⊥ (H)) \land A = x +_{ℎ} y)) \to ⊥ (H) \in S_{ℋ}$
28		shel	$⊢ (⊥ (H) \in S_{ℋ} \land y \in ⊥ (H)) \to y \in ℋ$
29	27 12 28	syl2anc	$⊢ (φ \land ((x \in H \land y \in ⊥ (H)) \land A = x +_{ℎ} y)) \to y \in ℋ$
30		ax-hvcom	$⊢ (x \in ℋ \land y \in ℋ) \to x +_{ℎ} y = y +_{ℎ} x$
31	26 29 30	syl2anc	$⊢ (φ \land ((x \in H \land y \in ⊥ (H)) \land A = x +_{ℎ} y)) \to x +_{ℎ} y = y +_{ℎ} x$
32	10 31	eqtrd	$⊢ (φ \land ((x \in H \land y \in ⊥ (H)) \land A = x +_{ℎ} y)) \to A = y +_{ℎ} x$
33		rspe	$⊢ (x \in ⊥ (⊥ (H)) \land A = y +_{ℎ} x) \to \exists x \in ⊥ (⊥ (H)) A = y +_{ℎ} x$
34	22 32 33	syl2anc	$⊢ (φ \land ((x \in H \land y \in ⊥ (H)) \land A = x +_{ℎ} y)) \to \exists x \in ⊥ (⊥ (H)) A = y +_{ℎ} x$
35		choccl	$⊢ H \in C_{ℋ} \to ⊥ (H) \in C_{ℋ}$
36	1 35	syl	$⊢ φ \to ⊥ (H) \in C_{ℋ}$
37		shocsh	$⊢ ⊥ (H) \in S_{ℋ} \to ⊥ (⊥ (H)) \in S_{ℋ}$
38	6 37	syl	$⊢ φ \to ⊥ (⊥ (H)) \in S_{ℋ}$
39		shless	$⊢ ((H \in S_{ℋ} \land ⊥ (⊥ (H)) \in S_{ℋ} \land ⊥ (H) \in S_{ℋ}) \land H \subseteq ⊥ (⊥ (H))) \to H +_{ℋ} ⊥ (H) \subseteq ⊥ (⊥ (H)) +_{ℋ} ⊥ (H)$
40	4 38 6 20 39	syl31anc	$⊢ φ \to H +_{ℋ} ⊥ (H) \subseteq ⊥ (⊥ (H)) +_{ℋ} ⊥ (H)$
41		shscom	$⊢ (⊥ (H) \in S_{ℋ} \land ⊥ (⊥ (H)) \in S_{ℋ}) \to ⊥ (H) +_{ℋ} ⊥ (⊥ (H)) = ⊥ (⊥ (H)) +_{ℋ} ⊥ (H)$
42	6 38 41	syl2anc	$⊢ φ \to ⊥ (H) +_{ℋ} ⊥ (⊥ (H)) = ⊥ (⊥ (H)) +_{ℋ} ⊥ (H)$
43	40 42	sseqtrrd	$⊢ φ \to H +_{ℋ} ⊥ (H) \subseteq ⊥ (H) +_{ℋ} ⊥ (⊥ (H))$
44	43 2	sseldd	$⊢ φ \to A \in (⊥ (H) +_{ℋ} ⊥ (⊥ (H)))$
45		pjpreeq	$⊢ (⊥ (H) \in C_{ℋ} \land A \in (⊥ (H) +_{ℋ} ⊥ (⊥ (H)))) \to ({proj}_{ℎ} (⊥ (H)) (A) = y \leftrightarrow (y \in ⊥ (H) \land \exists x \in ⊥ (⊥ (H)) A = y +_{ℎ} x))$
46	36 44 45	syl2anc	$⊢ φ \to ({proj}_{ℎ} (⊥ (H)) (A) = y \leftrightarrow (y \in ⊥ (H) \land \exists x \in ⊥ (⊥ (H)) A = y +_{ℎ} x))$
47	46	adantr	$⊢ (φ \land ((x \in H \land y \in ⊥ (H)) \land A = x +_{ℎ} y)) \to ({proj}_{ℎ} (⊥ (H)) (A) = y \leftrightarrow (y \in ⊥ (H) \land \exists x \in ⊥ (⊥ (H)) A = y +_{ℎ} x))$
48	12 34 47	mpbir2and	$⊢ (φ \land ((x \in H \land y \in ⊥ (H)) \land A = x +_{ℎ} y)) \to {proj}_{ℎ} (⊥ (H)) (A) = y$
49	18 48	oveq12d	$⊢ (φ \land ((x \in H \land y \in ⊥ (H)) \land A = x +_{ℎ} y)) \to {proj}_{ℎ} (H) (A) +_{ℎ} {proj}_{ℎ} (⊥ (H)) (A) = x +_{ℎ} y$
50	10 49	eqtr4d	$⊢ (φ \land ((x \in H \land y \in ⊥ (H)) \land A = x +_{ℎ} y)) \to A = {proj}_{ℎ} (H) (A) +_{ℎ} {proj}_{ℎ} (⊥ (H)) (A)$
51	50	exp32	$⊢ φ \to ((x \in H \land y \in ⊥ (H)) \to (A = x +_{ℎ} y \to A = {proj}_{ℎ} (H) (A) +_{ℎ} {proj}_{ℎ} (⊥ (H)) (A)))$
52	51	rexlimdvv	$⊢ φ \to (\exists x \in H \exists y \in ⊥ (H) A = x +_{ℎ} y \to A = {proj}_{ℎ} (H) (A) +_{ℎ} {proj}_{ℎ} (⊥ (H)) (A))$
53	9 52	mpd	$⊢ φ \to A = {proj}_{ℎ} (H) (A) +_{ℎ} {proj}_{ℎ} (⊥ (H)) (A)$

Metamath Proof Explorer

Theorem pjpjpre

Proof