Theorem norm3difi

Description: Norm of differences around common element. Part of Lemma 3.6 of Beran p. 101. (Contributed by NM, 16-Aug-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	norm3dif.1	$$⊢A\in \mathscr{H}$$
	norm3dif.2	$$⊢B\in \mathscr{H}$$
	norm3dif.3	$$⊢C\in \mathscr{H}$$
Assertion	norm3difi	$$⊢{norm}_{ℎ}\left(A{-}_{ℎ}B\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}C\right)+{norm}_{ℎ}\left(C{-}_{ℎ}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		norm3dif.1	$$⊢A\in \mathscr{H}$$
2		norm3dif.2	$$⊢B\in \mathscr{H}$$
3		norm3dif.3	$$⊢C\in \mathscr{H}$$
4	1 2	hvsubvali	$$⊢A{-}_{ℎ}B=A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)$$
5	1 3	hvsubvali	$$⊢A{-}_{ℎ}C=A{+}_{ℎ}\left(-1{\cdot }_{ℎ}C\right)$$
6	3 2	hvsubvali	$$⊢C{-}_{ℎ}B=C{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)$$
7	5 6	oveq12i	$$⊢\left(A{-}_{ℎ}C\right){+}_{ℎ}\left(C{-}_{ℎ}B\right)=\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}C\right)\right){+}_{ℎ}\left(C{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right)$$
8		neg1cn	$$⊢-1\in ℂ$$
9	8 3	hvmulcli	$$⊢-1{\cdot }_{ℎ}C\in \mathscr{H}$$
10	8 2	hvmulcli	$$⊢-1{\cdot }_{ℎ}B\in \mathscr{H}$$
11	3 10	hvaddcli	$$⊢C{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\in \mathscr{H}$$
12	1 9 11	hvassi	$$⊢\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}C\right)\right){+}_{ℎ}\left(C{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right)=A{+}_{ℎ}\left(\left(-1{\cdot }_{ℎ}C\right){+}_{ℎ}\left(C{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right)\right)$$
13	9 3 10	hvassi	$$⊢\left(\left(-1{\cdot }_{ℎ}C\right){+}_{ℎ}C\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)=\left(-1{\cdot }_{ℎ}C\right){+}_{ℎ}\left(C{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right)$$
14	9 3	hvcomi	$$⊢\left(-1{\cdot }_{ℎ}C\right){+}_{ℎ}C=C{+}_{ℎ}\left(-1{\cdot }_{ℎ}C\right)$$
15	3 3	hvsubvali	$$⊢C{-}_{ℎ}C=C{+}_{ℎ}\left(-1{\cdot }_{ℎ}C\right)$$
16		hvsubid	$$⊢C\in \mathscr{H}\to C{-}_{ℎ}C=0_{ℎ}$$
17	3 16	ax-mp	$$⊢C{-}_{ℎ}C=0_{ℎ}$$
18	14 15 17	3eqtr2i	$$⊢\left(-1{\cdot }_{ℎ}C\right){+}_{ℎ}C=0_{ℎ}$$
19	18	oveq1i	$$⊢\left(\left(-1{\cdot }_{ℎ}C\right){+}_{ℎ}C\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)=0_{ℎ}{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)$$
20		ax-hv0cl	$$⊢0_{ℎ}\in \mathscr{H}$$
21	20 10	hvcomi	$$⊢0_{ℎ}{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)=\left(-1{\cdot }_{ℎ}B\right){+}_{ℎ}{0}_{ℎ}$$
22		ax-hvaddid	$$⊢-1{\cdot }_{ℎ}B\in \mathscr{H}\to \left(-1{\cdot }_{ℎ}B\right){+}_{ℎ}{0}_{ℎ}=-1{\cdot }_{ℎ}B$$
23	10 22	ax-mp	$$⊢\left(-1{\cdot }_{ℎ}B\right){+}_{ℎ}{0}_{ℎ}=-1{\cdot }_{ℎ}B$$
24	19 21 23	3eqtri	$$⊢\left(\left(-1{\cdot }_{ℎ}C\right){+}_{ℎ}C\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)=-1{\cdot }_{ℎ}B$$
25	13 24	eqtr3i	$$⊢\left(-1{\cdot }_{ℎ}C\right){+}_{ℎ}\left(C{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right)=-1{\cdot }_{ℎ}B$$
26	25	oveq2i	$$⊢A{+}_{ℎ}\left(\left(-1{\cdot }_{ℎ}C\right){+}_{ℎ}\left(C{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right)\right)=A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)$$
27	7 12 26	3eqtri	$$⊢\left(A{-}_{ℎ}C\right){+}_{ℎ}\left(C{-}_{ℎ}B\right)=A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)$$
28	4 27	eqtr4i	$$⊢A{-}_{ℎ}B=\left(A{-}_{ℎ}C\right){+}_{ℎ}\left(C{-}_{ℎ}B\right)$$
29	28	fveq2i	$$⊢{norm}_{ℎ}\left(A{-}_{ℎ}B\right)={norm}_{ℎ}\left(\left(A{-}_{ℎ}C\right){+}_{ℎ}\left(C{-}_{ℎ}B\right)\right)$$
30	1 3	hvsubcli	$$⊢A{-}_{ℎ}C\in \mathscr{H}$$
31	3 2	hvsubcli	$$⊢C{-}_{ℎ}B\in \mathscr{H}$$
32	30 31	norm-ii-i	$$⊢{norm}_{ℎ}\left(\left(A{-}_{ℎ}C\right){+}_{ℎ}\left(C{-}_{ℎ}B\right)\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}C\right)+{norm}_{ℎ}\left(C{-}_{ℎ}B\right)$$
33	29 32	eqbrtri	$$⊢{norm}_{ℎ}\left(A{-}_{ℎ}B\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}C\right)+{norm}_{ℎ}\left(C{-}_{ℎ}B\right)$$