This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( ¬ 𝐴 ∈ 𝐻 ↔ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) < ( normℎ ‘ 𝐴 ) ) )

Proof

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