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

Metamath Proof Explorer

Theorem chocin

Description: Intersection of a closed subspace and its orthocomplement. Part of Proposition 1 of Kalmbach p. 65. (Contributed by NM, 13-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion chocin ⊢ A ∈ C ℋ → A ∩ ⊥ ⁡ A = 0 ℋ

Proof

Step Hyp Ref Expression
1 id ⊢ A = if A ∈ C ℋ A 0 ℋ → A = if A ∈ C ℋ A 0 ℋ
2 fveq2 ⊢ A = if A ∈ C ℋ A 0 ℋ → ⊥ ⁡ A = ⊥ ⁡ if A ∈ C ℋ A 0 ℋ
3 1 2 ineq12d ⊢ A = if A ∈ C ℋ A 0 ℋ → A ∩ ⊥ ⁡ A = if A ∈ C ℋ A 0 ℋ ∩ ⊥ ⁡ if A ∈ C ℋ A 0 ℋ
4 3 eqeq1d ⊢ A = if A ∈ C ℋ A 0 ℋ → A ∩ ⊥ ⁡ A = 0 ℋ ↔ if A ∈ C ℋ A 0 ℋ ∩ ⊥ ⁡ if A ∈ C ℋ A 0 ℋ = 0 ℋ
5 h0elch ⊢ 0 ℋ ∈ C ℋ
6 5 elimel ⊢ if A ∈ C ℋ A 0 ℋ ∈ C ℋ
7 6 chocini ⊢ if A ∈ C ℋ A 0 ℋ ∩ ⊥ ⁡ if A ∈ C ℋ A 0 ℋ = 0 ℋ
8 4 7 dedth ⊢ A ∈ C ℋ → A ∩ ⊥ ⁡ A = 0 ℋ