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ℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) )