Theorem ocvlsp

Description: The orthocomplement of a linear span. (Contributed by Mario Carneiro, 23-Oct-2015)

	Ref	Expression
Hypotheses	ocvlsp.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	ocvlsp.o	⊢ ⊥ = ( ocv ‘ 𝑊 )
	ocvlsp.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
Assertion	ocvlsp	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( ⊥ ‘ ( 𝑁 ‘ 𝑆 ) ) = ( ⊥ ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		ocvlsp.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		ocvlsp.o	⊢ ⊥ = ( ocv ‘ 𝑊 )
3		ocvlsp.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4		phllmod	⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod )
5	1 3	lspssid	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ⊆ 𝑉 ) → 𝑆 ⊆ ( 𝑁 ‘ 𝑆 ) )
6	4 5	sylan	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → 𝑆 ⊆ ( 𝑁 ‘ 𝑆 ) )
7	2	ocv2ss	⊢ ( 𝑆 ⊆ ( 𝑁 ‘ 𝑆 ) → ( ⊥ ‘ ( 𝑁 ‘ 𝑆 ) ) ⊆ ( ⊥ ‘ 𝑆 ) )
8	6 7	syl	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( ⊥ ‘ ( 𝑁 ‘ 𝑆 ) ) ⊆ ( ⊥ ‘ 𝑆 ) )
9	1 2	ocvss	⊢ ( ⊥ ‘ 𝑆 ) ⊆ 𝑉
10	9	a1i	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑆 ) ⊆ 𝑉 )
11	1 2	ocvocv	⊢ ( ( 𝑊 ∈ PreHil ∧ ( ⊥ ‘ 𝑆 ) ⊆ 𝑉 ) → ( ⊥ ‘ 𝑆 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) )
12	10 11	syldan	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑆 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) )
13	4	adantr	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → 𝑊 ∈ LMod )
14		eqid	⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
15	1 2 14	ocvlss	⊢ ( ( 𝑊 ∈ PreHil ∧ ( ⊥ ‘ 𝑆 ) ⊆ 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ∈ ( LSubSp ‘ 𝑊 ) )
16	10 15	syldan	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ∈ ( LSubSp ‘ 𝑊 ) )
17	1 2	ocvocv	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → 𝑆 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) )
18	14 3	lspssp	⊢ ( ( 𝑊 ∈ LMod ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑆 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) → ( 𝑁 ‘ 𝑆 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) )
19	13 16 17 18	syl3anc	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( 𝑁 ‘ 𝑆 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) )
20	2	ocv2ss	⊢ ( ( 𝑁 ‘ 𝑆 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) ⊆ ( ⊥ ‘ ( 𝑁 ‘ 𝑆 ) ) )
21	19 20	syl	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) ⊆ ( ⊥ ‘ ( 𝑁 ‘ 𝑆 ) ) )
22	12 21	sstrd	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑆 ) ⊆ ( ⊥ ‘ ( 𝑁 ‘ 𝑆 ) ) )
23	8 22	eqssd	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( ⊥ ‘ ( 𝑁 ‘ 𝑆 ) ) = ( ⊥ ‘ 𝑆 ) )