Metamath Proof Explorer

Theorem pjhtheu

Description: Projection Theorem: Any Hilbert space vector A can be decomposed uniquely into a member x of a closed subspace H and a member y of the complement of the subspace. Theorem 3.7(i) of Beran p. 102. See pjhtheu2 for the uniqueness of y . (Contributed by NM, 23-Oct-1999) (Revised by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

Ref Expression
Assertion pjhtheu ⊢ H ∈ C ℋ ∧ A ∈ ℋ → ∃! x ∈ H ∃ y ∈ ⊥ ⁡ H A = x + ℎ y

Proof

Step Hyp Ref Expression
1 pjhth ⊢ H ∈ C ℋ → H + ℋ ⊥ ⁡ H = ℋ
2 1 eleq2d ⊢ H ∈ C ℋ → A ∈ H + ℋ ⊥ ⁡ H ↔ A ∈ ℋ
3 chsh ⊢ H ∈ C ℋ → H ∈ S ℋ
4 shocsh ⊢ H ∈ S ℋ → ⊥ ⁡ H ∈ S ℋ
5 shsel ⊢ H ∈ S ℋ ∧ ⊥ ⁡ H ∈ S ℋ → A ∈ H + ℋ ⊥ ⁡ H ↔ ∃ x ∈ H ∃ y ∈ ⊥ ⁡ H A = x + ℎ y
6 3 4 5 syl2anc2 ⊢ H ∈ C ℋ → A ∈ H + ℋ ⊥ ⁡ H ↔ ∃ x ∈ H ∃ y ∈ ⊥ ⁡ H A = x + ℎ y
7 2 6 bitr3d ⊢ H ∈ C ℋ → A ∈ ℋ ↔ ∃ x ∈ H ∃ y ∈ ⊥ ⁡ H A = x + ℎ y
8 7 biimpa ⊢ H ∈ C ℋ ∧ A ∈ ℋ → ∃ x ∈ H ∃ y ∈ ⊥ ⁡ H A = x + ℎ y
9 3 4 syl ⊢ H ∈ C ℋ → ⊥ ⁡ H ∈ S ℋ
10 ocin ⊢ H ∈ S ℋ → H ∩ ⊥ ⁡ H = 0 ℋ
11 3 10 syl ⊢ H ∈ C ℋ → H ∩ ⊥ ⁡ H = 0 ℋ
12 pjhthmo ⊢ H ∈ S ℋ ∧ ⊥ ⁡ H ∈ S ℋ ∧ H ∩ ⊥ ⁡ H = 0 ℋ → ∃* x x ∈ H ∧ ∃ y ∈ ⊥ ⁡ H A = x + ℎ y
13 3 9 11 12 syl3anc ⊢ H ∈ C ℋ → ∃* x x ∈ H ∧ ∃ y ∈ ⊥ ⁡ H A = x + ℎ y
14 13 adantr ⊢ H ∈ C ℋ ∧ A ∈ ℋ → ∃* x x ∈ H ∧ ∃ y ∈ ⊥ ⁡ H A = x + ℎ y
15 reu5 ⊢ ∃! x ∈ H ∃ y ∈ ⊥ ⁡ H A = x + ℎ y ↔ ∃ x ∈ H ∃ y ∈ ⊥ ⁡ H A = x + ℎ y ∧ ∃* x ∈ H ∃ y ∈ ⊥ ⁡ H A = x + ℎ y
16 df-rmo ⊢ ∃* x ∈ H ∃ y ∈ ⊥ ⁡ H A = x + ℎ y ↔ ∃* x x ∈ H ∧ ∃ y ∈ ⊥ ⁡ H A = x + ℎ y
17 16 anbi2i ⊢ ∃ x ∈ H ∃ y ∈ ⊥ ⁡ H A = x + ℎ y ∧ ∃* x ∈ H ∃ y ∈ ⊥ ⁡ H A = x + ℎ y ↔ ∃ x ∈ H ∃ y ∈ ⊥ ⁡ H A = x + ℎ y ∧ ∃* x x ∈ H ∧ ∃ y ∈ ⊥ ⁡ H A = x + ℎ y
18 15 17 bitri ⊢ ∃! x ∈ H ∃ y ∈ ⊥ ⁡ H A = x + ℎ y ↔ ∃ x ∈ H ∃ y ∈ ⊥ ⁡ H A = x + ℎ y ∧ ∃* x x ∈ H ∧ ∃ y ∈ ⊥ ⁡ H A = x + ℎ y
19 8 14 18 sylanbrc ⊢ H ∈ C ℋ ∧ A ∈ ℋ → ∃! x ∈ H ∃ y ∈ ⊥ ⁡ H A = x + ℎ y