This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 ⊆ ℋ
spansnpj.2 ⊢ 𝐵 ∈ ℋ
Assertion spansnpji 𝐴 ⊆ ( ⊥ ‘ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) )

Proof

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