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 → ( 𝑥 ∈ ( ⊥ ‘ ℋ ) ↔ ( 𝑥 ∈ ℋ ∧ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih 𝑦 ) = 0 ) ) )
3 1 2 ax-mp ( 𝑥 ∈ ( ⊥ ‘ ℋ ) ↔ ( 𝑥 ∈ ℋ ∧ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih 𝑦 ) = 0 ) )
4 3 simprbi ( 𝑥 ∈ ( ⊥ ‘ ℋ ) → ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih 𝑦 ) = 0 )
5 shocss ( ℋ ∈ S → ( ⊥ ‘ ℋ ) ⊆ ℋ )
6 1 5 ax-mp ( ⊥ ‘ ℋ ) ⊆ ℋ
7 6 sseli ( 𝑥 ∈ ( ⊥ ‘ ℋ ) → 𝑥 ∈ ℋ )
8 hial0 ( 𝑥 ∈ ℋ → ( ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih 𝑦 ) = 0 ↔ 𝑥 = 0 ) )
9 7 8 syl ( 𝑥 ∈ ( ⊥ ‘ ℋ ) → ( ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih 𝑦 ) = 0 ↔ 𝑥 = 0 ) )
10 4 9 mpbid ( 𝑥 ∈ ( ⊥ ‘ ℋ ) → 𝑥 = 0 )
11 elch0 ( 𝑥 ∈ 0𝑥 = 0 )
12 10 11 sylibr ( 𝑥 ∈ ( ⊥ ‘ ℋ ) → 𝑥 ∈ 0 )
13 12 ssriv ( ⊥ ‘ ℋ ) ⊆ 0
14 h0elsh 0S
15 shococss ( 0S → 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