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 ) )