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 𝐴 ∈ ℋ
norm3dif.2 𝐵 ∈ ℋ
norm3dif.3 𝐶 ∈ ℋ
Assertion norm3difi ( norm ‘ ( 𝐴 𝐵 ) ) ≤ ( ( norm ‘ ( 𝐴 𝐶 ) ) + ( norm ‘ ( 𝐶 𝐵 ) ) )

Proof

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