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 V = Base W
ocvfval.i , ˙ = 𝑖 W
ocvfval.f F = Scalar W
ocvfval.z 0 ˙ = 0 F
ocvfval.o ˙ = ocv W
Assertion elocv A ˙ S S V A V x S A , ˙ x = 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 elfvdm A ˙ S S dom ˙
7 n0i A ˙ S ¬ ˙ S =
8 fvprc ¬ W V ocv W =
9 5 8 syl5eq ¬ W V ˙ =
10 9 fveq1d ¬ W V ˙ S = S
11 0fv S =
12 10 11 eqtrdi ¬ W V ˙ S =
13 7 12 nsyl2 A ˙ S W V
14 1 2 3 4 5 ocvfval W V ˙ = s 𝒫 V y V | x s y , ˙ x = 0 ˙
15 13 14 syl A ˙ S ˙ = s 𝒫 V y V | x s y , ˙ x = 0 ˙
16 15 dmeqd A ˙ S dom ˙ = dom s 𝒫 V y V | x s y , ˙ x = 0 ˙
17 1 fvexi V V
18 17 rabex y V | x s y , ˙ x = 0 ˙ V
19 eqid s 𝒫 V y V | x s y , ˙ x = 0 ˙ = s 𝒫 V y V | x s y , ˙ x = 0 ˙
20 18 19 dmmpti dom s 𝒫 V y V | x s y , ˙ x = 0 ˙ = 𝒫 V
21 16 20 eqtrdi A ˙ S dom ˙ = 𝒫 V
22 6 21 eleqtrd A ˙ S S 𝒫 V
23 22 elpwid A ˙ S S V
24 1 2 3 4 5 ocvval S V ˙ S = y V | x S y , ˙ x = 0 ˙
25 24 eleq2d S V A ˙ S A y V | x S y , ˙ x = 0 ˙
26 oveq1 y = A y , ˙ x = A , ˙ x
27 26 eqeq1d y = A y , ˙ x = 0 ˙ A , ˙ x = 0 ˙
28 27 ralbidv y = A x S y , ˙ x = 0 ˙ x S A , ˙ x = 0 ˙
29 28 elrab A y V | x S y , ˙ x = 0 ˙ A V x S A , ˙ x = 0 ˙
30 25 29 syl6bb S V A ˙ S A V x S A , ˙ x = 0 ˙
31 23 30 biadanii A ˙ S S V A V x S A , ˙ x = 0 ˙
32 3anass S V A V x S A , ˙ x = 0 ˙ S V A V x S A , ˙ x = 0 ˙
33 31 32 bitr4i A ˙ S S V A V x S A , ˙ x = 0 ˙