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

Metamath Proof Explorer

Theorem norm3lemt

Description: Lemma involving norm of differences in Hilbert space. (Contributed by NM, 18-Aug-1999) (New usage is discouraged.)

Ref Expression
Assertion norm3lemt ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℝ ) ) → ( ( ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( normℎ ‘ ( 𝐶 −ℎ 𝐵 ) ) < ( 𝐷 / 2 ) ) → ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) < 𝐷 ) )

Proof

Step Hyp Ref Expression
1 fvoveq1 ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) = ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐶 ) ) )
2 1 breq1d ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) < ( 𝐷 / 2 ) ↔ ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐶 ) ) < ( 𝐷 / 2 ) ) )
3 2 anbi1d ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( normℎ ‘ ( 𝐶 −ℎ 𝐵 ) ) < ( 𝐷 / 2 ) ) ↔ ( ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( normℎ ‘ ( 𝐶 −ℎ 𝐵 ) ) < ( 𝐷 / 2 ) ) ) )
4 fvoveq1 ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) = ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐵 ) ) )
5 4 breq1d ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) < 𝐷 ↔ ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐵 ) ) < 𝐷 ) )
6 3 5 imbi12d ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( ( ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( normℎ ‘ ( 𝐶 −ℎ 𝐵 ) ) < ( 𝐷 / 2 ) ) → ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) < 𝐷 ) ↔ ( ( ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( normℎ ‘ ( 𝐶 −ℎ 𝐵 ) ) < ( 𝐷 / 2 ) ) → ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐵 ) ) < 𝐷 ) ) )
7 oveq2 ⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( 𝐶 −ℎ 𝐵 ) = ( 𝐶 −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) )
8 7 fveq2d ⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( normℎ ‘ ( 𝐶 −ℎ 𝐵 ) ) = ( normℎ ‘ ( 𝐶 −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) )
9 8 breq1d ⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( ( normℎ ‘ ( 𝐶 −ℎ 𝐵 ) ) < ( 𝐷 / 2 ) ↔ ( normℎ ‘ ( 𝐶 −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) < ( 𝐷 / 2 ) ) )
10 9 anbi2d ⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( ( ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( normℎ ‘ ( 𝐶 −ℎ 𝐵 ) ) < ( 𝐷 / 2 ) ) ↔ ( ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( normℎ ‘ ( 𝐶 −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) < ( 𝐷 / 2 ) ) ) )
11 oveq2 ⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐵 ) = ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) )
12 11 fveq2d ⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐵 ) ) = ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) )
13 12 breq1d ⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐵 ) ) < 𝐷 ↔ ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) < 𝐷 ) )
14 10 13 imbi12d ⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( ( ( ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( normℎ ‘ ( 𝐶 −ℎ 𝐵 ) ) < ( 𝐷 / 2 ) ) → ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐵 ) ) < 𝐷 ) ↔ ( ( ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( normℎ ‘ ( 𝐶 −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) < ( 𝐷 / 2 ) ) → ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) < 𝐷 ) ) )
15 oveq2 ⊢ ( 𝐶 = if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) → ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐶 ) = ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) ) )
16 15 fveq2d ⊢ ( 𝐶 = if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) → ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐶 ) ) = ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) ) ) )
17 16 breq1d ⊢ ( 𝐶 = if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) → ( ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐶 ) ) < ( 𝐷 / 2 ) ↔ ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) ) ) < ( 𝐷 / 2 ) ) )
18 fvoveq1 ⊢ ( 𝐶 = if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) → ( normℎ ‘ ( 𝐶 −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) = ( normℎ ‘ ( if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) )
19 18 breq1d ⊢ ( 𝐶 = if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) → ( ( normℎ ‘ ( 𝐶 −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) < ( 𝐷 / 2 ) ↔ ( normℎ ‘ ( if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) < ( 𝐷 / 2 ) ) )
20 17 19 anbi12d ⊢ ( 𝐶 = if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) → ( ( ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( normℎ ‘ ( 𝐶 −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) < ( 𝐷 / 2 ) ) ↔ ( ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) ) ) < ( 𝐷 / 2 ) ∧ ( normℎ ‘ ( if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) < ( 𝐷 / 2 ) ) ) )
21 20 imbi1d ⊢ ( 𝐶 = if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) → ( ( ( ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( normℎ ‘ ( 𝐶 −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) < ( 𝐷 / 2 ) ) → ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) < 𝐷 ) ↔ ( ( ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) ) ) < ( 𝐷 / 2 ) ∧ ( normℎ ‘ ( if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) < ( 𝐷 / 2 ) ) → ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) < 𝐷 ) ) )
22 oveq1 ⊢ ( 𝐷 = if ( 𝐷 ∈ ℝ , 𝐷 , 2 ) → ( 𝐷 / 2 ) = ( if ( 𝐷 ∈ ℝ , 𝐷 , 2 ) / 2 ) )
23 22 breq2d ⊢ ( 𝐷 = if ( 𝐷 ∈ ℝ , 𝐷 , 2 ) → ( ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) ) ) < ( 𝐷 / 2 ) ↔ ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) ) ) < ( if ( 𝐷 ∈ ℝ , 𝐷 , 2 ) / 2 ) ) )
24 22 breq2d ⊢ ( 𝐷 = if ( 𝐷 ∈ ℝ , 𝐷 , 2 ) → ( ( normℎ ‘ ( if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) < ( 𝐷 / 2 ) ↔ ( normℎ ‘ ( if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) < ( if ( 𝐷 ∈ ℝ , 𝐷 , 2 ) / 2 ) ) )
25 23 24 anbi12d ⊢ ( 𝐷 = if ( 𝐷 ∈ ℝ , 𝐷 , 2 ) → ( ( ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) ) ) < ( 𝐷 / 2 ) ∧ ( normℎ ‘ ( if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) < ( 𝐷 / 2 ) ) ↔ ( ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) ) ) < ( if ( 𝐷 ∈ ℝ , 𝐷 , 2 ) / 2 ) ∧ ( normℎ ‘ ( if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) < ( if ( 𝐷 ∈ ℝ , 𝐷 , 2 ) / 2 ) ) ) )
26 breq2 ⊢ ( 𝐷 = if ( 𝐷 ∈ ℝ , 𝐷 , 2 ) → ( ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) < 𝐷 ↔ ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) < if ( 𝐷 ∈ ℝ , 𝐷 , 2 ) ) )
27 25 26 imbi12d ⊢ ( 𝐷 = if ( 𝐷 ∈ ℝ , 𝐷 , 2 ) → ( ( ( ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) ) ) < ( 𝐷 / 2 ) ∧ ( normℎ ‘ ( if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) < ( 𝐷 / 2 ) ) → ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) < 𝐷 ) ↔ ( ( ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) ) ) < ( if ( 𝐷 ∈ ℝ , 𝐷 , 2 ) / 2 ) ∧ ( normℎ ‘ ( if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) < ( if ( 𝐷 ∈ ℝ , 𝐷 , 2 ) / 2 ) ) → ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) < if ( 𝐷 ∈ ℝ , 𝐷 , 2 ) ) ) )
28 ifhvhv0 ⊢ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ∈ ℋ
29 ifhvhv0 ⊢ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ∈ ℋ
30 ifhvhv0 ⊢ if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) ∈ ℋ
31 2re ⊢ 2 ∈ ℝ
32 31 elimel ⊢ if ( 𝐷 ∈ ℝ , 𝐷 , 2 ) ∈ ℝ
33 28 29 30 32 norm3lem ⊢ ( ( ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) ) ) < ( if ( 𝐷 ∈ ℝ , 𝐷 , 2 ) / 2 ) ∧ ( normℎ ‘ ( if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) < ( if ( 𝐷 ∈ ℝ , 𝐷 , 2 ) / 2 ) ) → ( normℎ ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) < if ( 𝐷 ∈ ℝ , 𝐷 , 2 ) )
34 6 14 21 27 33 dedth4h ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℝ ) ) → ( ( ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( normℎ ‘ ( 𝐶 −ℎ 𝐵 ) ) < ( 𝐷 / 2 ) ) → ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) < 𝐷 ) )