This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 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ℋ