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 V = Base W
ocvfval.i , ˙ = 𝑖 W
ocvfval.f F = Scalar W
ocvfval.z 0 ˙ = 0 F
ocvfval.o ˙ = ocv W
Assertion ocvval S V ˙ S = x V | y S x , ˙ y = 0 ˙

Proof

Step Hyp Ref Expression
1 ocvfval.v V = Base W
2 ocvfval.i , ˙ = 𝑖 W
3 ocvfval.f F = Scalar W
4 ocvfval.z 0 ˙ = 0 F
5 ocvfval.o ˙ = ocv W
6 1 fvexi V V
7 6 elpw2 S 𝒫 V S V
8 1 2 3 4 5 ocvfval W V ˙ = s 𝒫 V x V | y s x , ˙ y = 0 ˙
9 8 fveq1d W V ˙ S = s 𝒫 V x V | y s x , ˙ y = 0 ˙ S
10 raleq s = S y s x , ˙ y = 0 ˙ y S x , ˙ y = 0 ˙
11 10 rabbidv s = S x V | y s x , ˙ y = 0 ˙ = x V | y S x , ˙ y = 0 ˙
12 eqid s 𝒫 V x V | y s x , ˙ y = 0 ˙ = s 𝒫 V x V | y s x , ˙ y = 0 ˙
13 6 rabex x V | y S x , ˙ y = 0 ˙ V
14 11 12 13 fvmpt S 𝒫 V s 𝒫 V x V | y s x , ˙ y = 0 ˙ S = x V | y S x , ˙ y = 0 ˙
15 9 14 sylan9eq W V S 𝒫 V ˙ S = x V | y S x , ˙ y = 0 ˙
16 0fv S =
17 fvprc ¬ W V ocv W =
18 5 17 syl5eq ¬ W V ˙ =
19 18 fveq1d ¬ W V ˙ S = S
20 ssrab2 x V | y S x , ˙ y = 0 ˙ V
21 fvprc ¬ W V Base W =
22 1 21 syl5eq ¬ W V V =
23 sseq0 x V | y S x , ˙ y = 0 ˙ V V = x V | y S x , ˙ y = 0 ˙ =
24 20 22 23 sylancr ¬ W V x V | y S x , ˙ y = 0 ˙ =
25 16 19 24 3eqtr4a ¬ W V ˙ S = x V | y S x , ˙ y = 0 ˙
26 25 adantr ¬ W V S 𝒫 V ˙ S = x V | y S x , ˙ y = 0 ˙
27 15 26 pm2.61ian S 𝒫 V ˙ S = x V | y S x , ˙ y = 0 ˙
28 7 27 sylbir S V ˙ S = x V | y S x , ˙ y = 0 ˙