Metamath Proof Explorer

Theorem pjoc2

Description: Projection of a vector in the orthocomplement of the projection subspace. Lemma 4.4(iii) of Beran p. 111. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion pjoc2 ⊢ H ∈ C ℋ ∧ A ∈ ℋ → A ∈ ⊥ ⁡ H ↔ proj ℎ ⁡ H ⁡ A = 0 ℎ

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ H = if H ∈ C ℋ H 0 ℋ → ⊥ ⁡ H = ⊥ ⁡ if H ∈ C ℋ H 0 ℋ
2 1 eleq2d ⊢ H = if H ∈ C ℋ H 0 ℋ → A ∈ ⊥ ⁡ H ↔ A ∈ ⊥ ⁡ if H ∈ C ℋ H 0 ℋ
3 fveq2 ⊢ H = if H ∈ C ℋ H 0 ℋ → proj ℎ ⁡ H = proj ℎ ⁡ if H ∈ C ℋ H 0 ℋ
4 3 fveq1d ⊢ H = if H ∈ C ℋ H 0 ℋ → proj ℎ ⁡ H ⁡ A = proj ℎ ⁡ if H ∈ C ℋ H 0 ℋ ⁡ A
5 4 eqeq1d ⊢ H = if H ∈ C ℋ H 0 ℋ → proj ℎ ⁡ H ⁡ A = 0 ℎ ↔ proj ℎ ⁡ if H ∈ C ℋ H 0 ℋ ⁡ A = 0 ℎ
6 2 5 bibi12d ⊢ H = if H ∈ C ℋ H 0 ℋ → A ∈ ⊥ ⁡ H ↔ proj ℎ ⁡ H ⁡ A = 0 ℎ ↔ A ∈ ⊥ ⁡ if H ∈ C ℋ H 0 ℋ ↔ proj ℎ ⁡ if H ∈ C ℋ H 0 ℋ ⁡ A = 0 ℎ
7 eleq1 ⊢ A = if A ∈ ℋ A 0 ℎ → A ∈ ⊥ ⁡ if H ∈ C ℋ H 0 ℋ ↔ if A ∈ ℋ A 0 ℎ ∈ ⊥ ⁡ if H ∈ C ℋ H 0 ℋ
8 fveqeq2 ⊢ A = if A ∈ ℋ A 0 ℎ → proj ℎ ⁡ if H ∈ C ℋ H 0 ℋ ⁡ A = 0 ℎ ↔ proj ℎ ⁡ if H ∈ C ℋ H 0 ℋ ⁡ if A ∈ ℋ A 0 ℎ = 0 ℎ
9 7 8 bibi12d ⊢ A = if A ∈ ℋ A 0 ℎ → A ∈ ⊥ ⁡ if H ∈ C ℋ H 0 ℋ ↔ proj ℎ ⁡ if H ∈ C ℋ H 0 ℋ ⁡ A = 0 ℎ ↔ if A ∈ ℋ A 0 ℎ ∈ ⊥ ⁡ if H ∈ C ℋ H 0 ℋ ↔ proj ℎ ⁡ if H ∈ C ℋ H 0 ℋ ⁡ if A ∈ ℋ A 0 ℎ = 0 ℎ
10 h0elch ⊢ 0 ℋ ∈ C ℋ
11 10 elimel ⊢ if H ∈ C ℋ H 0 ℋ ∈ C ℋ
12 ifhvhv0 ⊢ if A ∈ ℋ A 0 ℎ ∈ ℋ
13 11 12 pjoc2i ⊢ if A ∈ ℋ A 0 ℎ ∈ ⊥ ⁡ if H ∈ C ℋ H 0 ℋ ↔ proj ℎ ⁡ if H ∈ C ℋ H 0 ℋ ⁡ if A ∈ ℋ A 0 ℎ = 0 ℎ
14 6 9 13 dedth2h ⊢ H ∈ C ℋ ∧ A ∈ ℋ → A ∈ ⊥ ⁡ H ↔ proj ℎ ⁡ H ⁡ A = 0 ℎ