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 ) } ) )