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 syl5eq ( ¬ 𝑊 ∈ 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 ) )