Theorem ocel

Description: Membership in orthogonal complement of H subset. (Contributed by NM, 7-Aug-2000) (New usage is discouraged.)

	Ref	Expression
Assertion	ocel	⊢ ( 𝐻 ⊆ ℋ → ( 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ↔ ( 𝐴 ∈ ℋ ∧ ∀ 𝑥 ∈ 𝐻 ( 𝐴 ·ih 𝑥 ) = 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ocval	⊢ ( 𝐻 ⊆ ℋ → ( ⊥ ‘ 𝐻 ) = { 𝑦 ∈ ℋ ∣ ∀ 𝑥 ∈ 𝐻 ( 𝑦 ·ih 𝑥 ) = 0 } )
2	1	eleq2d	⊢ ( 𝐻 ⊆ ℋ → ( 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ↔ 𝐴 ∈ { 𝑦 ∈ ℋ ∣ ∀ 𝑥 ∈ 𝐻 ( 𝑦 ·ih 𝑥 ) = 0 } ) )
3		oveq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 ·ih 𝑥 ) = ( 𝐴 ·ih 𝑥 ) )
4	3	eqeq1d	⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ·ih 𝑥 ) = 0 ↔ ( 𝐴 ·ih 𝑥 ) = 0 ) )
5	4	ralbidv	⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑥 ∈ 𝐻 ( 𝑦 ·ih 𝑥 ) = 0 ↔ ∀ 𝑥 ∈ 𝐻 ( 𝐴 ·ih 𝑥 ) = 0 ) )
6	5	elrab	⊢ ( 𝐴 ∈ { 𝑦 ∈ ℋ ∣ ∀ 𝑥 ∈ 𝐻 ( 𝑦 ·ih 𝑥 ) = 0 } ↔ ( 𝐴 ∈ ℋ ∧ ∀ 𝑥 ∈ 𝐻 ( 𝐴 ·ih 𝑥 ) = 0 ) )
7	2 6	bitrdi	⊢ ( 𝐻 ⊆ ℋ → ( 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ↔ ( 𝐴 ∈ ℋ ∧ ∀ 𝑥 ∈ 𝐻 ( 𝐴 ·ih 𝑥 ) = 0 ) ) )