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 ⊢ H ⊆ ℋ → A ∈ H ∧ B ∈ ⊥ ⁡ H → A ⋅ ih B = 0

Proof

Step Hyp Ref Expression
1 ocel ⊢ H ⊆ ℋ → B ∈ ⊥ ⁡ H ↔ B ∈ ℋ ∧ ∀ x ∈ H B ⋅ ih x = 0
2 1 simplbda ⊢ H ⊆ ℋ ∧ B ∈ ⊥ ⁡ H → ∀ x ∈ H B ⋅ ih x = 0
3 2 adantl ⊢ H ⊆ ℋ ∧ A ∈ H ∧ H ⊆ ℋ ∧ B ∈ ⊥ ⁡ H → ∀ x ∈ H B ⋅ ih x = 0
4 oveq2 ⊢ x = A → B ⋅ ih x = B ⋅ ih A
5 4 eqeq1d ⊢ x = A → B ⋅ ih x = 0 ↔ B ⋅ ih A = 0
6 5 rspcv ⊢ A ∈ H → ∀ x ∈ H B ⋅ ih x = 0 → B ⋅ ih A = 0
7 6 ad2antlr ⊢ H ⊆ ℋ ∧ A ∈ H ∧ H ⊆ ℋ ∧ B ∈ ⊥ ⁡ H → ∀ x ∈ H B ⋅ ih x = 0 → B ⋅ ih A = 0
8 ssel2 ⊢ H ⊆ ℋ ∧ A ∈ H → A ∈ ℋ
9 ocss ⊢ H ⊆ ℋ → ⊥ ⁡ H ⊆ ℋ
10 9 sselda ⊢ H ⊆ ℋ ∧ B ∈ ⊥ ⁡ H → B ∈ ℋ
11 orthcom ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih B = 0 ↔ B ⋅ ih A = 0
12 8 10 11 syl2an ⊢ H ⊆ ℋ ∧ A ∈ H ∧ H ⊆ ℋ ∧ B ∈ ⊥ ⁡ H → A ⋅ ih B = 0 ↔ B ⋅ ih A = 0
13 7 12 sylibrd ⊢ H ⊆ ℋ ∧ A ∈ H ∧ H ⊆ ℋ ∧ B ∈ ⊥ ⁡ H → ∀ x ∈ H B ⋅ ih x = 0 → A ⋅ ih B = 0
14 3 13 mpd ⊢ H ⊆ ℋ ∧ A ∈ H ∧ H ⊆ ℋ ∧ B ∈ ⊥ ⁡ H → A ⋅ ih B = 0
15 14 anandis ⊢ H ⊆ ℋ ∧ A ∈ H ∧ B ∈ ⊥ ⁡ H → A ⋅ ih B = 0
16 15 ex ⊢ H ⊆ ℋ → A ∈ H ∧ B ∈ ⊥ ⁡ H → A ⋅ ih B = 0