Theorem ocvval

Description: Value of the orthocomplement of a subset (normally a subspace) of a pre-Hilbert space. (Contributed by NM, 7-Oct-2011) (Revised by Mario Carneiro, 13-Oct-2015)

	Ref	Expression
Hypotheses	ocvfval.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	ocvfval.i	⊢ , = ( ·𝑖 ‘ 𝑊 )
	ocvfval.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	ocvfval.z	⊢ 0 = ( 0g ‘ 𝐹 )
	ocvfval.o	⊢ ⊥ = ( ocv ‘ 𝑊 )
Assertion	ocvval	⊢ ( 𝑆 ⊆ 𝑉 → ( ⊥ ‘ 𝑆 ) = { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 , 𝑦 ) = 0 } )

Proof

Step	Hyp	Ref	Expression
1		ocvfval.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		ocvfval.i	⊢ , = ( ·𝑖 ‘ 𝑊 )
3		ocvfval.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4		ocvfval.z	⊢ 0 = ( 0g ‘ 𝐹 )
5		ocvfval.o	⊢ ⊥ = ( ocv ‘ 𝑊 )
6	1	fvexi	⊢ 𝑉 ∈ V
7	6	elpw2	⊢ ( 𝑆 ∈ 𝒫 𝑉 ↔ 𝑆 ⊆ 𝑉 )
8	1 2 3 4 5	ocvfval	⊢ ( 𝑊 ∈ V → ⊥ = ( 𝑠 ∈ 𝒫 𝑉 ↦ { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 , 𝑦 ) = 0 } ) )
9	8	fveq1d	⊢ ( 𝑊 ∈ V → ( ⊥ ‘ 𝑆 ) = ( ( 𝑠 ∈ 𝒫 𝑉 ↦ { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 , 𝑦 ) = 0 } ) ‘ 𝑆 ) )
10		raleq	⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑦 ∈ 𝑠 ( 𝑥 , 𝑦 ) = 0 ↔ ∀ 𝑦 ∈ 𝑆 ( 𝑥 , 𝑦 ) = 0 ) )
11	10	rabbidv	⊢ ( 𝑠 = 𝑆 → { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 , 𝑦 ) = 0 } = { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 , 𝑦 ) = 0 } )
12		eqid	⊢ ( 𝑠 ∈ 𝒫 𝑉 ↦ { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 , 𝑦 ) = 0 } ) = ( 𝑠 ∈ 𝒫 𝑉 ↦ { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 , 𝑦 ) = 0 } )
13	6	rabex	⊢ { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 , 𝑦 ) = 0 } ∈ V
14	11 12 13	fvmpt	⊢ ( 𝑆 ∈ 𝒫 𝑉 → ( ( 𝑠 ∈ 𝒫 𝑉 ↦ { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 , 𝑦 ) = 0 } ) ‘ 𝑆 ) = { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 , 𝑦 ) = 0 } )
15	9 14	sylan9eq	⊢ ( ( 𝑊 ∈ V ∧ 𝑆 ∈ 𝒫 𝑉 ) → ( ⊥ ‘ 𝑆 ) = { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 , 𝑦 ) = 0 } )
16		0fv	⊢ ( ∅ ‘ 𝑆 ) = ∅
17		fvprc	⊢ ( ¬ 𝑊 ∈ V → ( ocv ‘ 𝑊 ) = ∅ )
18	5 17	eqtrid	⊢ ( ¬ 𝑊 ∈ V → ⊥ = ∅ )
19	18	fveq1d	⊢ ( ¬ 𝑊 ∈ V → ( ⊥ ‘ 𝑆 ) = ( ∅ ‘ 𝑆 ) )
20		ssrab2	⊢ { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 , 𝑦 ) = 0 } ⊆ 𝑉
21		fvprc	⊢ ( ¬ 𝑊 ∈ V → ( Base ‘ 𝑊 ) = ∅ )
22	1 21	eqtrid	⊢ ( ¬ 𝑊 ∈ V → 𝑉 = ∅ )
23		sseq0	⊢ ( ( { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 , 𝑦 ) = 0 } ⊆ 𝑉 ∧ 𝑉 = ∅ ) → { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 , 𝑦 ) = 0 } = ∅ )
24	20 22 23	sylancr	⊢ ( ¬ 𝑊 ∈ V → { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 , 𝑦 ) = 0 } = ∅ )
25	16 19 24	3eqtr4a	⊢ ( ¬ 𝑊 ∈ V → ( ⊥ ‘ 𝑆 ) = { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 , 𝑦 ) = 0 } )
26	25	adantr	⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝑆 ∈ 𝒫 𝑉 ) → ( ⊥ ‘ 𝑆 ) = { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 , 𝑦 ) = 0 } )
27	15 26	pm2.61ian	⊢ ( 𝑆 ∈ 𝒫 𝑉 → ( ⊥ ‘ 𝑆 ) = { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 , 𝑦 ) = 0 } )
28	7 27	sylbir	⊢ ( 𝑆 ⊆ 𝑉 → ( ⊥ ‘ 𝑆 ) = { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 , 𝑦 ) = 0 } )