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 
|- A e. ~H
norm3dif.2 
|- B e. ~H
norm3dif.3 
|- C e. ~H
Assertion norm3difi 
|- ( normh ` ( A -h B ) ) <_ ( ( normh ` ( A -h C ) ) + ( normh ` ( C -h B ) ) )

Proof

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