This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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ℎ ‘ ( 𝐶 −ℎ 𝐵 ) ) )