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⋅ihB=0

Proof

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