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

Metamath Proof Explorer

Theorem ocorth

Description: Members of a subset and its complement are orthogonal. (Contributed by NM, 9-Aug-2000) (New usage is discouraged.)

Ref Expression
Assertion ocorth ( 𝐻 ⊆ ℋ → ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) → ( 𝐴 ·ih 𝐵 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 ocel ⊢ ( 𝐻 ⊆ ℋ → ( 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ↔ ( 𝐵 ∈ ℋ ∧ ∀ 𝑥 ∈ 𝐻 ( 𝐵 ·ih 𝑥 ) = 0 ) ) )
2 1 simplbda ⊢ ( ( 𝐻 ⊆ ℋ ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) → ∀ 𝑥 ∈ 𝐻 ( 𝐵 ·ih 𝑥 ) = 0 )
3 2 adantl ⊢ ( ( ( 𝐻 ⊆ ℋ ∧ 𝐴 ∈ 𝐻 ) ∧ ( 𝐻 ⊆ ℋ ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) ) → ∀ 𝑥 ∈ 𝐻 ( 𝐵 ·ih 𝑥 ) = 0 )
4 oveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐵 ·ih 𝑥 ) = ( 𝐵 ·ih 𝐴 ) )
5 4 eqeq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐵 ·ih 𝑥 ) = 0 ↔ ( 𝐵 ·ih 𝐴 ) = 0 ) )
6 5 rspcv ⊢ ( 𝐴 ∈ 𝐻 → ( ∀ 𝑥 ∈ 𝐻 ( 𝐵 ·ih 𝑥 ) = 0 → ( 𝐵 ·ih 𝐴 ) = 0 ) )
7 6 ad2antlr ⊢ ( ( ( 𝐻 ⊆ ℋ ∧ 𝐴 ∈ 𝐻 ) ∧ ( 𝐻 ⊆ ℋ ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) ) → ( ∀ 𝑥 ∈ 𝐻 ( 𝐵 ·ih 𝑥 ) = 0 → ( 𝐵 ·ih 𝐴 ) = 0 ) )
8 ssel2 ⊢ ( ( 𝐻 ⊆ ℋ ∧ 𝐴 ∈ 𝐻 ) → 𝐴 ∈ ℋ )
9 ocss ⊢ ( 𝐻 ⊆ ℋ → ( ⊥ ‘ 𝐻 ) ⊆ ℋ )
10 9 sselda ⊢ ( ( 𝐻 ⊆ ℋ ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) → 𝐵 ∈ ℋ )
11 orthcom ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 ·ih 𝐵 ) = 0 ↔ ( 𝐵 ·ih 𝐴 ) = 0 ) )
12 8 10 11 syl2an ⊢ ( ( ( 𝐻 ⊆ ℋ ∧ 𝐴 ∈ 𝐻 ) ∧ ( 𝐻 ⊆ ℋ ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) ) → ( ( 𝐴 ·ih 𝐵 ) = 0 ↔ ( 𝐵 ·ih 𝐴 ) = 0 ) )
13 7 12 sylibrd ⊢ ( ( ( 𝐻 ⊆ ℋ ∧ 𝐴 ∈ 𝐻 ) ∧ ( 𝐻 ⊆ ℋ ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) ) → ( ∀ 𝑥 ∈ 𝐻 ( 𝐵 ·ih 𝑥 ) = 0 → ( 𝐴 ·ih 𝐵 ) = 0 ) )
14 3 13 mpd ⊢ ( ( ( 𝐻 ⊆ ℋ ∧ 𝐴 ∈ 𝐻 ) ∧ ( 𝐻 ⊆ ℋ ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) ) → ( 𝐴 ·ih 𝐵 ) = 0 )
15 14 anandis ⊢ ( ( 𝐻 ⊆ ℋ ∧ ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) ) → ( 𝐴 ·ih 𝐵 ) = 0 )
16 15 ex ⊢ ( 𝐻 ⊆ ℋ → ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) → ( 𝐴 ·ih 𝐵 ) = 0 ) )