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