Theorem norm3adifii

Description: Norm of differences around common element. Part of Lemma 3.6 of Beran p. 101. (Contributed by NM, 30-Sep-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	norm3adifii	$$⊢\left|{norm}_{ℎ}\left(A{-}_{ℎ}C\right)-{norm}_{ℎ}\left(B{-}_{ℎ}C\right)\right|\le {norm}_{ℎ}\left(A{-}_{ℎ}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 3	hvsubcli	$$⊢A{-}_{ℎ}C\in \mathscr{H}$$
5	4	normcli	$$⊢{norm}_{ℎ}\left(A{-}_{ℎ}C\right)\in ℝ$$
6	5	recni	$$⊢{norm}_{ℎ}\left(A{-}_{ℎ}C\right)\in ℂ$$
7	2 3	hvsubcli	$$⊢B{-}_{ℎ}C\in \mathscr{H}$$
8	7	normcli	$$⊢{norm}_{ℎ}\left(B{-}_{ℎ}C\right)\in ℝ$$
9	8	recni	$$⊢{norm}_{ℎ}\left(B{-}_{ℎ}C\right)\in ℂ$$
10	6 9	negsubdi2i	$$⊢-\left({norm}_{ℎ}\left(A{-}_{ℎ}C\right)-{norm}_{ℎ}\left(B{-}_{ℎ}C\right)\right)={norm}_{ℎ}\left(B{-}_{ℎ}C\right)-{norm}_{ℎ}\left(A{-}_{ℎ}C\right)$$
11	2 3 1	norm3difi	$$⊢{norm}_{ℎ}\left(B{-}_{ℎ}C\right)\le {norm}_{ℎ}\left(B{-}_{ℎ}A\right)+{norm}_{ℎ}\left(A{-}_{ℎ}C\right)$$
12	2 1	normsubi	$$⊢{norm}_{ℎ}\left(B{-}_{ℎ}A\right)={norm}_{ℎ}\left(A{-}_{ℎ}B\right)$$
13	12	oveq1i	$$⊢{norm}_{ℎ}\left(B{-}_{ℎ}A\right)+{norm}_{ℎ}\left(A{-}_{ℎ}C\right)={norm}_{ℎ}\left(A{-}_{ℎ}B\right)+{norm}_{ℎ}\left(A{-}_{ℎ}C\right)$$
14	11 13	breqtri	$$⊢{norm}_{ℎ}\left(B{-}_{ℎ}C\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}B\right)+{norm}_{ℎ}\left(A{-}_{ℎ}C\right)$$
15	1 2	hvsubcli	$$⊢A{-}_{ℎ}B\in \mathscr{H}$$
16	15	normcli	$$⊢{norm}_{ℎ}\left(A{-}_{ℎ}B\right)\in ℝ$$
17	8 5 16	lesubaddi	$$⊢{norm}_{ℎ}\left(B{-}_{ℎ}C\right)-{norm}_{ℎ}\left(A{-}_{ℎ}C\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}B\right)\leftrightarrow {norm}_{ℎ}\left(B{-}_{ℎ}C\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}B\right)+{norm}_{ℎ}\left(A{-}_{ℎ}C\right)$$
18	14 17	mpbir	$$⊢{norm}_{ℎ}\left(B{-}_{ℎ}C\right)-{norm}_{ℎ}\left(A{-}_{ℎ}C\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}B\right)$$
19	10 18	eqbrtri	$$⊢-\left({norm}_{ℎ}\left(A{-}_{ℎ}C\right)-{norm}_{ℎ}\left(B{-}_{ℎ}C\right)\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}B\right)$$
20	5 8	resubcli	$$⊢{norm}_{ℎ}\left(A{-}_{ℎ}C\right)-{norm}_{ℎ}\left(B{-}_{ℎ}C\right)\in ℝ$$
21	20 16	lenegcon1i	$$⊢-\left({norm}_{ℎ}\left(A{-}_{ℎ}C\right)-{norm}_{ℎ}\left(B{-}_{ℎ}C\right)\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}B\right)\leftrightarrow -{norm}_{ℎ}\left(A{-}_{ℎ}B\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}C\right)-{norm}_{ℎ}\left(B{-}_{ℎ}C\right)$$
22	19 21	mpbi	$$⊢-{norm}_{ℎ}\left(A{-}_{ℎ}B\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}C\right)-{norm}_{ℎ}\left(B{-}_{ℎ}C\right)$$
23	1 3 2	norm3difi	$$⊢{norm}_{ℎ}\left(A{-}_{ℎ}C\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}B\right)+{norm}_{ℎ}\left(B{-}_{ℎ}C\right)$$
24	5 8 16	lesubaddi	$$⊢{norm}_{ℎ}\left(A{-}_{ℎ}C\right)-{norm}_{ℎ}\left(B{-}_{ℎ}C\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}B\right)\leftrightarrow {norm}_{ℎ}\left(A{-}_{ℎ}C\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}B\right)+{norm}_{ℎ}\left(B{-}_{ℎ}C\right)$$
25	23 24	mpbir	$$⊢{norm}_{ℎ}\left(A{-}_{ℎ}C\right)-{norm}_{ℎ}\left(B{-}_{ℎ}C\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}B\right)$$
26	20 16	abslei	$$⊢\left|{norm}_{ℎ}\left(A{-}_{ℎ}C\right)-{norm}_{ℎ}\left(B{-}_{ℎ}C\right)\right|\le {norm}_{ℎ}\left(A{-}_{ℎ}B\right)\leftrightarrow \left(-{norm}_{ℎ}\left(A{-}_{ℎ}B\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}C\right)-{norm}_{ℎ}\left(B{-}_{ℎ}C\right)\wedge {norm}_{ℎ}\left(A{-}_{ℎ}C\right)-{norm}_{ℎ}\left(B{-}_{ℎ}C\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}B\right)\right)$$
27	22 25 26	mpbir2an	$$⊢\left|{norm}_{ℎ}\left(A{-}_{ℎ}C\right)-{norm}_{ℎ}\left(B{-}_{ℎ}C\right)\right|\le {norm}_{ℎ}\left(A{-}_{ℎ}B\right)$$