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 ⊢A∈ℋ∧B∈ℋ→normℎ⁡A+ℎB≤normℎ⁡A+normℎ⁡B

Proof

Step Hyp Ref Expression
1 fvoveq1 ⊢A=ifA∈ℋA0ℎ→normℎ⁡A+ℎB=normℎ⁡ifA∈ℋA0ℎ+ℎB
2 fveq2 ⊢A=ifA∈ℋA0ℎ→normℎ⁡A=normℎ⁡ifA∈ℋA0ℎ
3 2 oveq1d ⊢A=ifA∈ℋA0ℎ→normℎ⁡A+normℎ⁡B=normℎ⁡ifA∈ℋA0ℎ+normℎ⁡B
4 1 3 breq12d ⊢A=ifA∈ℋA0ℎ→normℎ⁡A+ℎB≤normℎ⁡A+normℎ⁡B↔normℎ⁡ifA∈ℋA0ℎ+ℎB≤normℎ⁡ifA∈ℋA0ℎ+normℎ⁡B
5 oveq2 ⊢B=ifB∈ℋB0ℎ→ifA∈ℋA0ℎ+ℎB=ifA∈ℋA0ℎ+ℎifB∈ℋB0ℎ
6 5 fveq2d ⊢B=ifB∈ℋB0ℎ→normℎ⁡ifA∈ℋA0ℎ+ℎB=normℎ⁡ifA∈ℋA0ℎ+ℎifB∈ℋB0ℎ
7 fveq2 ⊢B=ifB∈ℋB0ℎ→normℎ⁡B=normℎ⁡ifB∈ℋB0ℎ
8 7 oveq2d ⊢B=ifB∈ℋB0ℎ→normℎ⁡ifA∈ℋA0ℎ+normℎ⁡B=normℎ⁡ifA∈ℋA0ℎ+normℎ⁡ifB∈ℋB0ℎ
9 6 8 breq12d ⊢B=ifB∈ℋB0ℎ→normℎ⁡ifA∈ℋA0ℎ+ℎB≤normℎ⁡ifA∈ℋA0ℎ+normℎ⁡B↔normℎ⁡ifA∈ℋA0ℎ+ℎifB∈ℋB0ℎ≤normℎ⁡ifA∈ℋA0ℎ+normℎ⁡ifB∈ℋB0ℎ
10 ifhvhv0 ⊢ifA∈ℋA0ℎ∈ℋ
11 ifhvhv0 ⊢ifB∈ℋB0ℎ∈ℋ
12 10 11 norm-ii-i ⊢normℎ⁡ifA∈ℋA0ℎ+ℎifB∈ℋB0ℎ≤normℎ⁡ifA∈ℋA0ℎ+normℎ⁡ifB∈ℋB0ℎ
13 4 9 12 dedth2h ⊢A∈ℋ∧B∈ℋ→normℎ⁡A+ℎB≤normℎ⁡A+normℎ⁡B