Metamath Proof Explorer

Theorem pjnel

Description: If a vector does not belong to subspace, the norm of its projection is less than its norm. (Contributed by NM, 2-Nov-1999) (New usage is discouraged.)

Ref Expression
Assertion pjnel ⊢ H ∈ C ℋ ∧ A ∈ ℋ → ¬ A ∈ H ↔ norm ℎ ⁡ proj ℎ ⁡ H ⁡ A < norm ℎ ⁡ A

Proof

Step Hyp Ref Expression
1 eleq2 ⊢ H = if H ∈ C ℋ H ℋ → A ∈ H ↔ A ∈ if H ∈ C ℋ H ℋ
2 1 notbid ⊢ H = if H ∈ C ℋ H ℋ → ¬ A ∈ H ↔ ¬ A ∈ if H ∈ C ℋ H ℋ
3 fveq2 ⊢ H = if H ∈ C ℋ H ℋ → proj ℎ ⁡ H = proj ℎ ⁡ if H ∈ C ℋ H ℋ
4 3 fveq1d ⊢ H = if H ∈ C ℋ H ℋ → proj ℎ ⁡ H ⁡ A = proj ℎ ⁡ if H ∈ C ℋ H ℋ ⁡ A
5 4 fveq2d ⊢ H = if H ∈ C ℋ H ℋ → norm ℎ ⁡ proj ℎ ⁡ H ⁡ A = norm ℎ ⁡ proj ℎ ⁡ if H ∈ C ℋ H ℋ ⁡ A
6 5 breq1d ⊢ H = if H ∈ C ℋ H ℋ → norm ℎ ⁡ proj ℎ ⁡ H ⁡ A < norm ℎ ⁡ A ↔ norm ℎ ⁡ proj ℎ ⁡ if H ∈ C ℋ H ℋ ⁡ A < norm ℎ ⁡ A
7 2 6 bibi12d ⊢ H = if H ∈ C ℋ H ℋ → ¬ A ∈ H ↔ norm ℎ ⁡ proj ℎ ⁡ H ⁡ A < norm ℎ ⁡ A ↔ ¬ A ∈ if H ∈ C ℋ H ℋ ↔ norm ℎ ⁡ proj ℎ ⁡ if H ∈ C ℋ H ℋ ⁡ A < norm ℎ ⁡ A
8 eleq1 ⊢ A = if A ∈ ℋ A 0 ℎ → A ∈ if H ∈ C ℋ H ℋ ↔ if A ∈ ℋ A 0 ℎ ∈ if H ∈ C ℋ H ℋ
9 8 notbid ⊢ A = if A ∈ ℋ A 0 ℎ → ¬ A ∈ if H ∈ C ℋ H ℋ ↔ ¬ if A ∈ ℋ A 0 ℎ ∈ if H ∈ C ℋ H ℋ
10 2fveq3 ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ proj ℎ ⁡ if H ∈ C ℋ H ℋ ⁡ A = norm ℎ ⁡ proj ℎ ⁡ if H ∈ C ℋ H ℋ ⁡ if A ∈ ℋ A 0 ℎ
11 fveq2 ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ
12 10 11 breq12d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ proj ℎ ⁡ if H ∈ C ℋ H ℋ ⁡ A < norm ℎ ⁡ A ↔ norm ℎ ⁡ proj ℎ ⁡ if H ∈ C ℋ H ℋ ⁡ if A ∈ ℋ A 0 ℎ < norm ℎ ⁡ if A ∈ ℋ A 0 ℎ
13 9 12 bibi12d ⊢ A = if A ∈ ℋ A 0 ℎ → ¬ A ∈ if H ∈ C ℋ H ℋ ↔ norm ℎ ⁡ proj ℎ ⁡ if H ∈ C ℋ H ℋ ⁡ A < norm ℎ ⁡ A ↔ ¬ if A ∈ ℋ A 0 ℎ ∈ if H ∈ C ℋ H ℋ ↔ norm ℎ ⁡ proj ℎ ⁡ if H ∈ C ℋ H ℋ ⁡ if A ∈ ℋ A 0 ℎ < norm ℎ ⁡ if A ∈ ℋ A 0 ℎ
14 ifchhv ⊢ if H ∈ C ℋ H ℋ ∈ C ℋ
15 ifhvhv0 ⊢ if A ∈ ℋ A 0 ℎ ∈ ℋ
16 14 15 pjneli ⊢ ¬ if A ∈ ℋ A 0 ℎ ∈ if H ∈ C ℋ H ℋ ↔ norm ℎ ⁡ proj ℎ ⁡ if H ∈ C ℋ H ℋ ⁡ if A ∈ ℋ A 0 ℎ < norm ℎ ⁡ if A ∈ ℋ A 0 ℎ
17 7 13 16 dedth2h ⊢ H ∈ C ℋ ∧ A ∈ ℋ → ¬ A ∈ H ↔ norm ℎ ⁡ proj ℎ ⁡ H ⁡ A < norm ℎ ⁡ A