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

Metamath Proof Explorer

Theorem shocorth

Description: Members of a subspace and its complement are orthogonal. (Contributed by NM, 10-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion shocorth ⊢ H ∈ S ℋ → A ∈ H ∧ B ∈ ⊥ ⁡ H → A ⋅ ih B = 0

Proof

Step Hyp Ref Expression
1 shss ⊢ H ∈ S ℋ → H ⊆ ℋ
2 ocorth ⊢ H ⊆ ℋ → A ∈ H ∧ B ∈ ⊥ ⁡ H → A ⋅ ih B = 0
3 1 2 syl ⊢ H ∈ S ℋ → A ∈ H ∧ B ∈ ⊥ ⁡ H → A ⋅ ih B = 0