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