Metamath Proof Explorer


Theorem choc1

Description: The orthocomplement of the unit subspace is the zero subspace. Does not require Axiom of Choice. (Contributed by NM, 24-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion choc1 = 0

Proof

Step Hyp Ref Expression
1 helsh S
2 shocel S x x y x ih y = 0
3 1 2 ax-mp x x y x ih y = 0
4 3 simprbi x y x ih y = 0
5 shocss S
6 1 5 ax-mp
7 6 sseli x x
8 hial0 x y x ih y = 0 x = 0
9 7 8 syl x y x ih y = 0 x = 0
10 4 9 mpbid x x = 0
11 elch0 x 0 x = 0
12 10 11 sylibr x x 0
13 12 ssriv 0
14 h0elsh 0 S
15 shococss 0 S 0 0
16 14 15 ax-mp 0 0
17 choc0 0 =
18 17 fveq2i 0 =
19 16 18 sseqtri 0
20 13 19 eqssi = 0