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