Metamath Proof Explorer

Theorem pjoc1

Description: Projection of a vector in the orthocomplement of the projection subspace. (Contributed by NM, 6-Nov-1999) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 eleq2 ⊢ H = if H ∈ C ℋ H ℋ → A ∈ H ↔ A ∈ if H ∈ C ℋ H ℋ
2 2fveq3 ⊢ H = if H ∈ C ℋ H ℋ → proj ℎ ⁡ ⊥ ⁡ H = proj ℎ ⁡ ⊥ ⁡ if H ∈ C ℋ H ℋ
3 2 fveq1d ⊢ H = if H ∈ C ℋ H ℋ → proj ℎ ⁡ ⊥ ⁡ H ⁡ A = proj ℎ ⁡ ⊥ ⁡ if H ∈ C ℋ H ℋ ⁡ A
4 3 eqeq1d ⊢ H = if H ∈ C ℋ H ℋ → proj ℎ ⁡ ⊥ ⁡ H ⁡ A = 0 ℎ ↔ proj ℎ ⁡ ⊥ ⁡ if H ∈ C ℋ H ℋ ⁡ A = 0 ℎ
5 1 4 bibi12d ⊢ H = if H ∈ C ℋ H ℋ → A ∈ H ↔ proj ℎ ⁡ ⊥ ⁡ H ⁡ A = 0 ℎ ↔ A ∈ if H ∈ C ℋ H ℋ ↔ proj ℎ ⁡ ⊥ ⁡ if H ∈ C ℋ H ℋ ⁡ A = 0 ℎ
6 eleq1 ⊢ A = if A ∈ ℋ A 0 ℎ → A ∈ if H ∈ C ℋ H ℋ ↔ if A ∈ ℋ A 0 ℎ ∈ if H ∈ C ℋ H ℋ
7 fveqeq2 ⊢ A = if A ∈ ℋ A 0 ℎ → proj ℎ ⁡ ⊥ ⁡ if H ∈ C ℋ H ℋ ⁡ A = 0 ℎ ↔ proj ℎ ⁡ ⊥ ⁡ if H ∈ C ℋ H ℋ ⁡ if A ∈ ℋ A 0 ℎ = 0 ℎ
8 6 7 bibi12d ⊢ A = if A ∈ ℋ A 0 ℎ → A ∈ if H ∈ C ℋ H ℋ ↔ proj ℎ ⁡ ⊥ ⁡ if H ∈ C ℋ H ℋ ⁡ A = 0 ℎ ↔ if A ∈ ℋ A 0 ℎ ∈ if H ∈ C ℋ H ℋ ↔ proj ℎ ⁡ ⊥ ⁡ if H ∈ C ℋ H ℋ ⁡ if A ∈ ℋ A 0 ℎ = 0 ℎ
9 ifchhv ⊢ if H ∈ C ℋ H ℋ ∈ C ℋ
10 ifhvhv0 ⊢ if A ∈ ℋ A 0 ℎ ∈ ℋ
11 9 10 pjoc1i ⊢ if A ∈ ℋ A 0 ℎ ∈ if H ∈ C ℋ H ℋ ↔ proj ℎ ⁡ ⊥ ⁡ if H ∈ C ℋ H ℋ ⁡ if A ∈ ℋ A 0 ℎ = 0 ℎ
12 5 8 11 dedth2h ⊢ H ∈ C ℋ ∧ A ∈ ℋ → A ∈ H ↔ proj ℎ ⁡ ⊥ ⁡ H ⁡ A = 0 ℎ