Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ocvval Structured version   Unicode version

Theorem ocvval 16894
 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.)
Hypotheses
Ref Expression
ocvfval.v
ocvfval.i
ocvfval.f Scalar
ocvfval.z
ocvfval.o
Assertion
Ref Expression
ocvval
Distinct variable groups:   ,,   ,,   ,,   , ,   ,,
Allowed substitution hints:   (,)   (,)

Proof of Theorem ocvval
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ocvfval.v . . . 4
2 fvex 5742 . . . 4
31, 2eqeltri 2506 . . 3
43elpw2 4364 . 2
5 ocvfval.i . . . . . 6
6 ocvfval.f . . . . . 6 Scalar
7 ocvfval.z . . . . . 6
8 ocvfval.o . . . . . 6
91, 5, 6, 7, 8ocvfval 16893 . . . . 5
109fveq1d 5730 . . . 4
11 raleq 2904 . . . . . 6
1211rabbidv 2948 . . . . 5
13 eqid 2436 . . . . 5
143rabex 4354 . . . . 5
1512, 13, 14fvmpt 5806 . . . 4
1610, 15sylan9eq 2488 . . 3
17 fv01 5763 . . . . 5
18 fvprc 5722 . . . . . . 7
198, 18syl5eq 2480 . . . . . 6
2019fveq1d 5730 . . . . 5
21 ssrab2 3428 . . . . . 6
22 fvprc 5722 . . . . . . 7
231, 22syl5eq 2480 . . . . . 6
24 sseq0 3659 . . . . . 6
2521, 23, 24sylancr 645 . . . . 5
2617, 20, 253eqtr4a 2494 . . . 4