Database
BASIC ALGEBRAIC STRUCTURES
Generalized pre-Hilbert and Hilbert spaces
Orthocomplements and closed subspaces
ocv1
Next ⟩
unocv
Metamath Proof Explorer
Ascii
Unicode
Theorem
ocv1
Description:
The orthocomplement of the base set.
(Contributed by
Mario Carneiro
, 23-Oct-2015)
Ref
Expression
Hypotheses
ocvz.v
⊢
V
=
Base
W
ocvz.o
⊢
⊥
˙
=
ocv
⁡
W
ocvz.z
⊢
0
˙
=
0
W
Assertion
ocv1
⊢
W
∈
PreHil
→
⊥
˙
⁡
V
=
0
˙
Proof
Step
Hyp
Ref
Expression
1
ocvz.v
⊢
V
=
Base
W
2
ocvz.o
⊢
⊥
˙
=
ocv
⁡
W
3
ocvz.z
⊢
0
˙
=
0
W
4
1
2
ocvss
⊢
⊥
˙
⁡
V
⊆
V
5
sseqin2
⊢
⊥
˙
⁡
V
⊆
V
↔
V
∩
⊥
˙
⁡
V
=
⊥
˙
⁡
V
6
4
5
mpbi
⊢
V
∩
⊥
˙
⁡
V
=
⊥
˙
⁡
V
7
phllmod
⊢
W
∈
PreHil
→
W
∈
LMod
8
eqid
⊢
LSubSp
⁡
W
=
LSubSp
⁡
W
9
1
8
lss1
⊢
W
∈
LMod
→
V
∈
LSubSp
⁡
W
10
7
9
syl
⊢
W
∈
PreHil
→
V
∈
LSubSp
⁡
W
11
2
8
3
ocvin
⊢
W
∈
PreHil
∧
V
∈
LSubSp
⁡
W
→
V
∩
⊥
˙
⁡
V
=
0
˙
12
10
11
mpdan
⊢
W
∈
PreHil
→
V
∩
⊥
˙
⁡
V
=
0
˙
13
6
12
syl5eqr
⊢
W
∈
PreHil
→
⊥
˙
⁡
V
=
0
˙