Metamath Proof Explorer


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
norm3dif.2 B
norm3dif.3 C
Assertion norm3difi norm A - B norm A - C + norm C - B

Proof

Step Hyp Ref Expression
1 norm3dif.1 A
2 norm3dif.2 B
3 norm3dif.3 C
4 1 2 hvsubvali A - B = A + -1 B
5 1 3 hvsubvali A - C = A + -1 C
6 3 2 hvsubvali C - B = C + -1 B
7 5 6 oveq12i A - C + C - B = A + -1 C + C + -1 B
8 neg1cn 1
9 8 3 hvmulcli -1 C
10 8 2 hvmulcli -1 B
11 3 10 hvaddcli C + -1 B
12 1 9 11 hvassi A + -1 C + C + -1 B = A + -1 C + C + -1 B
13 9 3 10 hvassi -1 C + C + -1 B = -1 C + C + -1 B
14 9 3 hvcomi -1 C + C = C + -1 C
15 3 3 hvsubvali C - C = C + -1 C
16 hvsubid C C - C = 0
17 3 16 ax-mp C - C = 0
18 14 15 17 3eqtr2i -1 C + C = 0
19 18 oveq1i -1 C + C + -1 B = 0 + -1 B
20 ax-hv0cl 0
21 20 10 hvcomi 0 + -1 B = -1 B + 0
22 ax-hvaddid -1 B -1 B + 0 = -1 B
23 10 22 ax-mp -1 B + 0 = -1 B
24 19 21 23 3eqtri -1 C + C + -1 B = -1 B
25 13 24 eqtr3i -1 C + C + -1 B = -1 B
26 25 oveq2i A + -1 C + C + -1 B = A + -1 B
27 7 12 26 3eqtri A - C + C - B = A + -1 B
28 4 27 eqtr4i A - B = A - C + C - B
29 28 fveq2i norm A - B = norm A - C + C - B
30 1 3 hvsubcli A - C
31 3 2 hvsubcli C - B
32 30 31 norm-ii-i norm A - C + C - B norm A - C + norm C - B
33 29 32 eqbrtri norm A - B norm A - C + norm C - B