This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elocv

Description: Elementhood in the orthocomplement of a subset (normally a subspace) of a pre-Hilbert space. (Contributed 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 elocv ( 𝐴 ∈ ( ⊥ ‘ 𝑆 ) ↔ ( 𝑆 ⊆ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐴 , 𝑥 ) = 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 elfvdm ⊢ ( 𝐴 ∈ ( ⊥ ‘ 𝑆 ) → 𝑆 ∈ dom ⊥ )
7 n0i ⊢ ( 𝐴 ∈ ( ⊥ ‘ 𝑆 ) → ¬ ( ⊥ ‘ 𝑆 ) = ∅ )
8 fvprc ⊢ ( ¬ 𝑊 ∈ V → ( ocv ‘ 𝑊 ) = ∅ )
9 5 8 eqtrid ⊢ ( ¬ 𝑊 ∈ V → ⊥ = ∅ )
10 9 fveq1d ⊢ ( ¬ 𝑊 ∈ V → ( ⊥ ‘ 𝑆 ) = ( ∅ ‘ 𝑆 ) )
11 0fv ⊢ ( ∅ ‘ 𝑆 ) = ∅
12 10 11 eqtrdi ⊢ ( ¬ 𝑊 ∈ V → ( ⊥ ‘ 𝑆 ) = ∅ )
13 7 12 nsyl2 ⊢ ( 𝐴 ∈ ( ⊥ ‘ 𝑆 ) → 𝑊 ∈ V )
14 1 2 3 4 5 ocvfval ⊢ ( 𝑊 ∈ V → ⊥ = ( 𝑠 ∈ 𝒫 𝑉 ↦ { 𝑦 ∈ 𝑉 ∣ ∀ 𝑥 ∈ 𝑠 ( 𝑦 , 𝑥 ) = 0 } ) )
15 13 14 syl ⊢ ( 𝐴 ∈ ( ⊥ ‘ 𝑆 ) → ⊥ = ( 𝑠 ∈ 𝒫 𝑉 ↦ { 𝑦 ∈ 𝑉 ∣ ∀ 𝑥 ∈ 𝑠 ( 𝑦 , 𝑥 ) = 0 } ) )
16 15 dmeqd ⊢ ( 𝐴 ∈ ( ⊥ ‘ 𝑆 ) → dom ⊥ = dom ( 𝑠 ∈ 𝒫 𝑉 ↦ { 𝑦 ∈ 𝑉 ∣ ∀ 𝑥 ∈ 𝑠 ( 𝑦 , 𝑥 ) = 0 } ) )
17 1 fvexi ⊢ 𝑉 ∈ V
18 17 rabex ⊢ { 𝑦 ∈ 𝑉 ∣ ∀ 𝑥 ∈ 𝑠 ( 𝑦 , 𝑥 ) = 0 } ∈ V
19 eqid ⊢ ( 𝑠 ∈ 𝒫 𝑉 ↦ { 𝑦 ∈ 𝑉 ∣ ∀ 𝑥 ∈ 𝑠 ( 𝑦 , 𝑥 ) = 0 } ) = ( 𝑠 ∈ 𝒫 𝑉 ↦ { 𝑦 ∈ 𝑉 ∣ ∀ 𝑥 ∈ 𝑠 ( 𝑦 , 𝑥 ) = 0 } )
20 18 19 dmmpti ⊢ dom ( 𝑠 ∈ 𝒫 𝑉 ↦ { 𝑦 ∈ 𝑉 ∣ ∀ 𝑥 ∈ 𝑠 ( 𝑦 , 𝑥 ) = 0 } ) = 𝒫 𝑉
21 16 20 eqtrdi ⊢ ( 𝐴 ∈ ( ⊥ ‘ 𝑆 ) → dom ⊥ = 𝒫 𝑉 )
22 6 21 eleqtrd ⊢ ( 𝐴 ∈ ( ⊥ ‘ 𝑆 ) → 𝑆 ∈ 𝒫 𝑉 )
23 22 elpwid ⊢ ( 𝐴 ∈ ( ⊥ ‘ 𝑆 ) → 𝑆 ⊆ 𝑉 )
24 1 2 3 4 5 ocvval ⊢ ( 𝑆 ⊆ 𝑉 → ( ⊥ ‘ 𝑆 ) = { 𝑦 ∈ 𝑉 ∣ ∀ 𝑥 ∈ 𝑆 ( 𝑦 , 𝑥 ) = 0 } )
25 24 eleq2d ⊢ ( 𝑆 ⊆ 𝑉 → ( 𝐴 ∈ ( ⊥ ‘ 𝑆 ) ↔ 𝐴 ∈ { 𝑦 ∈ 𝑉 ∣ ∀ 𝑥 ∈ 𝑆 ( 𝑦 , 𝑥 ) = 0 } ) )
26 oveq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 , 𝑥 ) = ( 𝐴 , 𝑥 ) )
27 26 eqeq1d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 , 𝑥 ) = 0 ↔ ( 𝐴 , 𝑥 ) = 0 ) )
28 27 ralbidv ⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑥 ∈ 𝑆 ( 𝑦 , 𝑥 ) = 0 ↔ ∀ 𝑥 ∈ 𝑆 ( 𝐴 , 𝑥 ) = 0 ) )
29 28 elrab ⊢ ( 𝐴 ∈ { 𝑦 ∈ 𝑉 ∣ ∀ 𝑥 ∈ 𝑆 ( 𝑦 , 𝑥 ) = 0 } ↔ ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐴 , 𝑥 ) = 0 ) )
30 25 29 bitrdi ⊢ ( 𝑆 ⊆ 𝑉 → ( 𝐴 ∈ ( ⊥ ‘ 𝑆 ) ↔ ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐴 , 𝑥 ) = 0 ) ) )
31 23 30 biadanii ⊢ ( 𝐴 ∈ ( ⊥ ‘ 𝑆 ) ↔ ( 𝑆 ⊆ 𝑉 ∧ ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐴 , 𝑥 ) = 0 ) ) )
32 3anass ⊢ ( ( 𝑆 ⊆ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐴 , 𝑥 ) = 0 ) ↔ ( 𝑆 ⊆ 𝑉 ∧ ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐴 , 𝑥 ) = 0 ) ) )
33 31 32 bitr4i ⊢ ( 𝐴 ∈ ( ⊥ ‘ 𝑆 ) ↔ ( 𝑆 ⊆ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐴 , 𝑥 ) = 0 ) )