Metamath Proof Explorer

Theorem spansnpji

Description: A subset of Hilbert space is orthogonal to the span of the singleton of a projection onto its orthocomplement. (Contributed by NM, 4-Jun-2004) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses spansnpj.1 ⊢ A ⊆ ℋ
spansnpj.2 ⊢ B ∈ ℋ
Assertion spansnpji ⊢ A ⊆ ⊥ ⁡ span ⁡ proj ℎ ⁡ ⊥ ⁡ A ⁡ B

Proof

Step Hyp Ref Expression
1 spansnpj.1 ⊢ A ⊆ ℋ
2 spansnpj.2 ⊢ B ∈ ℋ
3 ococss ⊢ A ⊆ ℋ → A ⊆ ⊥ ⁡ ⊥ ⁡ A
4 1 3 ax-mp ⊢ A ⊆ ⊥ ⁡ ⊥ ⁡ A
5 occl ⊢ A ⊆ ℋ → ⊥ ⁡ A ∈ C ℋ
6 1 5 ax-mp ⊢ ⊥ ⁡ A ∈ C ℋ
7 6 chssii ⊢ ⊥ ⁡ A ⊆ ℋ
8 6 2 pjclii ⊢ proj ℎ ⁡ ⊥ ⁡ A ⁡ B ∈ ⊥ ⁡ A
9 snssi ⊢ proj ℎ ⁡ ⊥ ⁡ A ⁡ B ∈ ⊥ ⁡ A → proj ℎ ⁡ ⊥ ⁡ A ⁡ B ⊆ ⊥ ⁡ A
10 8 9 ax-mp ⊢ proj ℎ ⁡ ⊥ ⁡ A ⁡ B ⊆ ⊥ ⁡ A
11 spanss ⊢ ⊥ ⁡ A ⊆ ℋ ∧ proj ℎ ⁡ ⊥ ⁡ A ⁡ B ⊆ ⊥ ⁡ A → span ⁡ proj ℎ ⁡ ⊥ ⁡ A ⁡ B ⊆ span ⁡ ⊥ ⁡ A
12 7 10 11 mp2an ⊢ span ⁡ proj ℎ ⁡ ⊥ ⁡ A ⁡ B ⊆ span ⁡ ⊥ ⁡ A
13 6 chshii ⊢ ⊥ ⁡ A ∈ S ℋ
14 spanid ⊢ ⊥ ⁡ A ∈ S ℋ → span ⁡ ⊥ ⁡ A = ⊥ ⁡ A
15 13 14 ax-mp ⊢ span ⁡ ⊥ ⁡ A = ⊥ ⁡ A
16 12 15 sseqtri ⊢ span ⁡ proj ℎ ⁡ ⊥ ⁡ A ⁡ B ⊆ ⊥ ⁡ A
17 6 2 pjhclii ⊢ proj ℎ ⁡ ⊥ ⁡ A ⁡ B ∈ ℋ
18 17 spansnchi ⊢ span ⁡ proj ℎ ⁡ ⊥ ⁡ A ⁡ B ∈ C ℋ
19 18 6 chsscon3i ⊢ span ⁡ proj ℎ ⁡ ⊥ ⁡ A ⁡ B ⊆ ⊥ ⁡ A ↔ ⊥ ⁡ ⊥ ⁡ A ⊆ ⊥ ⁡ span ⁡ proj ℎ ⁡ ⊥ ⁡ A ⁡ B
20 16 19 mpbi ⊢ ⊥ ⁡ ⊥ ⁡ A ⊆ ⊥ ⁡ span ⁡ proj ℎ ⁡ ⊥ ⁡ A ⁡ B
21 4 20 sstri ⊢ A ⊆ ⊥ ⁡ span ⁡ proj ℎ ⁡ ⊥ ⁡ A ⁡ B