Metamath Proof Explorer

Theorem norm-ii

Description: Triangle inequality for norms. Theorem 3.3(ii) of Beran p. 97. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion norm-ii ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( norm ‘ ( 𝐴 + 𝐵 ) ) ≤ ( ( norm𝐴 ) + ( norm𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 fvoveq1 ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( norm ‘ ( 𝐴 + 𝐵 ) ) = ( norm ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) + 𝐵 ) ) )
2 fveq2 ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( norm𝐴 ) = ( norm ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) )
3 2 oveq1d ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( ( norm𝐴 ) + ( norm𝐵 ) ) = ( ( norm ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) + ( norm𝐵 ) ) )
4 1 3 breq12d ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( ( norm ‘ ( 𝐴 + 𝐵 ) ) ≤ ( ( norm𝐴 ) + ( norm𝐵 ) ) ↔ ( norm ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) + 𝐵 ) ) ≤ ( ( norm ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) + ( norm𝐵 ) ) ) )
5 oveq2 ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) → ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) + 𝐵 ) = ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) + if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) )
6 5 fveq2d ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) → ( norm ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) + 𝐵 ) ) = ( norm ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) + if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) ) )
7 fveq2 ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) → ( norm𝐵 ) = ( norm ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) )
8 7 oveq2d ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) → ( ( norm ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) + ( norm𝐵 ) ) = ( ( norm ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) + ( norm ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) ) )
9 6 8 breq12d ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) → ( ( norm ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) + 𝐵 ) ) ≤ ( ( norm ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) + ( norm𝐵 ) ) ↔ ( norm ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) + if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) ) ≤ ( ( norm ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) + ( norm ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) ) ) )
10 ifhvhv0 if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ∈ ℋ
11 ifhvhv0 if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ∈ ℋ
12 10 11 norm-ii-i ( norm ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) + if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) ) ≤ ( ( norm ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) + ( norm ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) )
13 4 9 12 dedth2h ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( norm ‘ ( 𝐴 + 𝐵 ) ) ≤ ( ( norm𝐴 ) + ( norm𝐵 ) ) )