Metamath Proof Explorer

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