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

Metamath Proof Explorer

Theorem choc0

Description: The orthocomplement of the zero subspace is the unit subspace. (Contributed by NM, 15-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion choc0 ( ⊥ ‘ 0ℋ ) = ℋ

Proof

Step Hyp Ref Expression
1 h0elsh ⊢ 0ℋ ∈ Sℋ
2 shocel ⊢ ( 0ℋ ∈ Sℋ → ( 𝑥 ∈ ( ⊥ ‘ 0ℋ ) ↔ ( 𝑥 ∈ ℋ ∧ ∀ 𝑦 ∈ 0ℋ ( 𝑥 ·ih 𝑦 ) = 0 ) ) )
3 1 2 ax-mp ⊢ ( 𝑥 ∈ ( ⊥ ‘ 0ℋ ) ↔ ( 𝑥 ∈ ℋ ∧ ∀ 𝑦 ∈ 0ℋ ( 𝑥 ·ih 𝑦 ) = 0 ) )
4 hi02 ⊢ ( 𝑥 ∈ ℋ → ( 𝑥 ·ih 0ℎ ) = 0 )
5 df-ral ⊢ ( ∀ 𝑦 ∈ 0ℋ ( 𝑥 ·ih 𝑦 ) = 0 ↔ ∀ 𝑦 ( 𝑦 ∈ 0ℋ → ( 𝑥 ·ih 𝑦 ) = 0 ) )
6 elch0 ⊢ ( 𝑦 ∈ 0ℋ ↔ 𝑦 = 0ℎ )
7 6 imbi1i ⊢ ( ( 𝑦 ∈ 0ℋ → ( 𝑥 ·ih 𝑦 ) = 0 ) ↔ ( 𝑦 = 0ℎ → ( 𝑥 ·ih 𝑦 ) = 0 ) )
8 7 albii ⊢ ( ∀ 𝑦 ( 𝑦 ∈ 0ℋ → ( 𝑥 ·ih 𝑦 ) = 0 ) ↔ ∀ 𝑦 ( 𝑦 = 0ℎ → ( 𝑥 ·ih 𝑦 ) = 0 ) )
9 ax-hv0cl ⊢ 0ℎ ∈ ℋ
10 9 elexi ⊢ 0ℎ ∈ V
11 oveq2 ⊢ ( 𝑦 = 0ℎ → ( 𝑥 ·ih 𝑦 ) = ( 𝑥 ·ih 0ℎ ) )
12 11 eqeq1d ⊢ ( 𝑦 = 0ℎ → ( ( 𝑥 ·ih 𝑦 ) = 0 ↔ ( 𝑥 ·ih 0ℎ ) = 0 ) )
13 10 12 ceqsalv ⊢ ( ∀ 𝑦 ( 𝑦 = 0ℎ → ( 𝑥 ·ih 𝑦 ) = 0 ) ↔ ( 𝑥 ·ih 0ℎ ) = 0 )
14 8 13 bitri ⊢ ( ∀ 𝑦 ( 𝑦 ∈ 0ℋ → ( 𝑥 ·ih 𝑦 ) = 0 ) ↔ ( 𝑥 ·ih 0ℎ ) = 0 )
15 5 14 bitri ⊢ ( ∀ 𝑦 ∈ 0ℋ ( 𝑥 ·ih 𝑦 ) = 0 ↔ ( 𝑥 ·ih 0ℎ ) = 0 )
16 4 15 sylibr ⊢ ( 𝑥 ∈ ℋ → ∀ 𝑦 ∈ 0ℋ ( 𝑥 ·ih 𝑦 ) = 0 )
17 abai ⊢ ( ( 𝑥 ∈ ℋ ∧ ∀ 𝑦 ∈ 0ℋ ( 𝑥 ·ih 𝑦 ) = 0 ) ↔ ( 𝑥 ∈ ℋ ∧ ( 𝑥 ∈ ℋ → ∀ 𝑦 ∈ 0ℋ ( 𝑥 ·ih 𝑦 ) = 0 ) ) )
18 16 17 mpbiran2 ⊢ ( ( 𝑥 ∈ ℋ ∧ ∀ 𝑦 ∈ 0ℋ ( 𝑥 ·ih 𝑦 ) = 0 ) ↔ 𝑥 ∈ ℋ )
19 3 18 bitri ⊢ ( 𝑥 ∈ ( ⊥ ‘ 0ℋ ) ↔ 𝑥 ∈ ℋ )
20 19 eqriv ⊢ ( ⊥ ‘ 0ℋ ) = ℋ