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 
|- A C_ ~H
spansnpj.2 
|- B e. ~H
Assertion spansnpji 
|- A C_ ( _|_ ` ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) )

Proof

Step Hyp Ref Expression
1 spansnpj.1 
 |-  A C_ ~H
2 spansnpj.2 
 |-  B e. ~H
3 ococss 
 |-  ( A C_ ~H -> A C_ ( _|_ ` ( _|_ ` A ) ) )
4 1 3 ax-mp 
 |-  A C_ ( _|_ ` ( _|_ ` A ) )
5 occl 
 |-  ( A C_ ~H -> ( _|_ ` A ) e. CH )
6 1 5 ax-mp 
 |-  ( _|_ ` A ) e. CH
7 6 chssii 
 |-  ( _|_ ` A ) C_ ~H
8 6 2 pjclii 
 |-  ( ( projh ` ( _|_ ` A ) ) ` B ) e. ( _|_ ` A )
9 snssi 
 |-  ( ( ( projh ` ( _|_ ` A ) ) ` B ) e. ( _|_ ` A ) -> { ( ( projh ` ( _|_ ` A ) ) ` B ) } C_ ( _|_ ` A ) )
10 8 9 ax-mp 
 |-  { ( ( projh ` ( _|_ ` A ) ) ` B ) } C_ ( _|_ ` A )
11 spanss 
 |-  ( ( ( _|_ ` A ) C_ ~H /\ { ( ( projh ` ( _|_ ` A ) ) ` B ) } C_ ( _|_ ` A ) ) -> ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) C_ ( span ` ( _|_ ` A ) ) )
12 7 10 11 mp2an 
 |-  ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) C_ ( span ` ( _|_ ` A ) )
13 6 chshii 
 |-  ( _|_ ` A ) e. SH
14 spanid 
 |-  ( ( _|_ ` A ) e. SH -> ( span ` ( _|_ ` A ) ) = ( _|_ ` A ) )
15 13 14 ax-mp 
 |-  ( span ` ( _|_ ` A ) ) = ( _|_ ` A )
16 12 15 sseqtri 
 |-  ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) C_ ( _|_ ` A )
17 6 2 pjhclii 
 |-  ( ( projh ` ( _|_ ` A ) ) ` B ) e. ~H
18 17 spansnchi 
 |-  ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) e. CH
19 18 6 chsscon3i 
 |-  ( ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) C_ ( _|_ ` A ) <-> ( _|_ ` ( _|_ ` A ) ) C_ ( _|_ ` ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) )
20 16 19 mpbi 
 |-  ( _|_ ` ( _|_ ` A ) ) C_ ( _|_ ` ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) )
21 4 20 sstri 
 |-  A C_ ( _|_ ` ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) )