# Metamath Proof Explorer

## Theorem nvtri

Description: Triangle inequality for the norm of a normed complex vector space. (Contributed by NM, 11-Nov-2006) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses nvtri.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
nvtri.2 ${⊢}{G}={+}_{v}\left({U}\right)$
nvtri.6 ${⊢}{N}={norm}_{CV}\left({U}\right)$
Assertion nvtri ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {N}\left({A}{G}{B}\right)\le {N}\left({A}\right)+{N}\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 nvtri.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 nvtri.2 ${⊢}{G}={+}_{v}\left({U}\right)$
3 nvtri.6 ${⊢}{N}={norm}_{CV}\left({U}\right)$
4 eqid ${⊢}{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$
5 4 smfval ${⊢}{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)={2}^{nd}\left({1}^{st}\left({U}\right)\right)$
6 5 eqcomi ${⊢}{2}^{nd}\left({1}^{st}\left({U}\right)\right)={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$
7 eqid ${⊢}{0}_{\mathrm{vec}}\left({U}\right)={0}_{\mathrm{vec}}\left({U}\right)$
8 1 2 6 7 3 nvi ${⊢}{U}\in \mathrm{NrmCVec}\to \left(⟨{G},{2}^{nd}\left({1}^{st}\left({U}\right)\right)⟩\in {CVec}_{\mathrm{OLD}}\wedge {N}:{X}⟶ℝ\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({N}\left({x}\right)=0\to {x}={0}_{\mathrm{vec}}\left({U}\right)\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{N}\left({y}{2}^{nd}\left({1}^{st}\left({U}\right)\right){x}\right)=\left|{y}\right|{N}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({x}{G}{y}\right)\le {N}\left({x}\right)+{N}\left({y}\right)\right)\right)$
9 8 simp3d ${⊢}{U}\in \mathrm{NrmCVec}\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({N}\left({x}\right)=0\to {x}={0}_{\mathrm{vec}}\left({U}\right)\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{N}\left({y}{2}^{nd}\left({1}^{st}\left({U}\right)\right){x}\right)=\left|{y}\right|{N}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({x}{G}{y}\right)\le {N}\left({x}\right)+{N}\left({y}\right)\right)$
10 simp3 ${⊢}\left(\left({N}\left({x}\right)=0\to {x}={0}_{\mathrm{vec}}\left({U}\right)\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{N}\left({y}{2}^{nd}\left({1}^{st}\left({U}\right)\right){x}\right)=\left|{y}\right|{N}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({x}{G}{y}\right)\le {N}\left({x}\right)+{N}\left({y}\right)\right)\to \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({x}{G}{y}\right)\le {N}\left({x}\right)+{N}\left({y}\right)$
11 10 ralimi ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({N}\left({x}\right)=0\to {x}={0}_{\mathrm{vec}}\left({U}\right)\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{N}\left({y}{2}^{nd}\left({1}^{st}\left({U}\right)\right){x}\right)=\left|{y}\right|{N}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({x}{G}{y}\right)\le {N}\left({x}\right)+{N}\left({y}\right)\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({x}{G}{y}\right)\le {N}\left({x}\right)+{N}\left({y}\right)$
12 9 11 syl ${⊢}{U}\in \mathrm{NrmCVec}\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({x}{G}{y}\right)\le {N}\left({x}\right)+{N}\left({y}\right)$
13 fvoveq1 ${⊢}{x}={A}\to {N}\left({x}{G}{y}\right)={N}\left({A}{G}{y}\right)$
14 fveq2 ${⊢}{x}={A}\to {N}\left({x}\right)={N}\left({A}\right)$
15 14 oveq1d ${⊢}{x}={A}\to {N}\left({x}\right)+{N}\left({y}\right)={N}\left({A}\right)+{N}\left({y}\right)$
16 13 15 breq12d ${⊢}{x}={A}\to \left({N}\left({x}{G}{y}\right)\le {N}\left({x}\right)+{N}\left({y}\right)↔{N}\left({A}{G}{y}\right)\le {N}\left({A}\right)+{N}\left({y}\right)\right)$
17 oveq2 ${⊢}{y}={B}\to {A}{G}{y}={A}{G}{B}$
18 17 fveq2d ${⊢}{y}={B}\to {N}\left({A}{G}{y}\right)={N}\left({A}{G}{B}\right)$
19 fveq2 ${⊢}{y}={B}\to {N}\left({y}\right)={N}\left({B}\right)$
20 19 oveq2d ${⊢}{y}={B}\to {N}\left({A}\right)+{N}\left({y}\right)={N}\left({A}\right)+{N}\left({B}\right)$
21 18 20 breq12d ${⊢}{y}={B}\to \left({N}\left({A}{G}{y}\right)\le {N}\left({A}\right)+{N}\left({y}\right)↔{N}\left({A}{G}{B}\right)\le {N}\left({A}\right)+{N}\left({B}\right)\right)$
22 16 21 rspc2v ${⊢}\left({A}\in {X}\wedge {B}\in {X}\right)\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({x}{G}{y}\right)\le {N}\left({x}\right)+{N}\left({y}\right)\to {N}\left({A}{G}{B}\right)\le {N}\left({A}\right)+{N}\left({B}\right)\right)$
23 12 22 syl5 ${⊢}\left({A}\in {X}\wedge {B}\in {X}\right)\to \left({U}\in \mathrm{NrmCVec}\to {N}\left({A}{G}{B}\right)\le {N}\left({A}\right)+{N}\left({B}\right)\right)$
24 23 3impia ${⊢}\left({A}\in {X}\wedge {B}\in {X}\wedge {U}\in \mathrm{NrmCVec}\right)\to {N}\left({A}{G}{B}\right)\le {N}\left({A}\right)+{N}\left({B}\right)$
25 24 3comr ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {N}\left({A}{G}{B}\right)\le {N}\left({A}\right)+{N}\left({B}\right)$