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 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧D∈ℝ→normℎ⁡A-ℎC<D2∧normℎ⁡C-ℎB<D2→normℎ⁡A-ℎB<D

Proof

Step Hyp Ref Expression
1 fvoveq1 ⊢A=ifA∈ℋA0ℎ→normℎ⁡A-ℎC=normℎ⁡ifA∈ℋA0ℎ-ℎC
2 1 breq1d ⊢A=ifA∈ℋA0ℎ→normℎ⁡A-ℎC<D2↔normℎ⁡ifA∈ℋA0ℎ-ℎC<D2
3 2 anbi1d ⊢A=ifA∈ℋA0ℎ→normℎ⁡A-ℎC<D2∧normℎ⁡C-ℎB<D2↔normℎ⁡ifA∈ℋA0ℎ-ℎC<D2∧normℎ⁡C-ℎB<D2
4 fvoveq1 ⊢A=ifA∈ℋA0ℎ→normℎ⁡A-ℎB=normℎ⁡ifA∈ℋA0ℎ-ℎB
5 4 breq1d ⊢A=ifA∈ℋA0ℎ→normℎ⁡A-ℎB<D↔normℎ⁡ifA∈ℋA0ℎ-ℎB<D
6 3 5 imbi12d ⊢A=ifA∈ℋA0ℎ→normℎ⁡A-ℎC<D2∧normℎ⁡C-ℎB<D2→normℎ⁡A-ℎB<D↔normℎ⁡ifA∈ℋA0ℎ-ℎC<D2∧normℎ⁡C-ℎB<D2→normℎ⁡ifA∈ℋA0ℎ-ℎB<D
7 oveq2 ⊢B=ifB∈ℋB0ℎ→C-ℎB=C-ℎifB∈ℋB0ℎ
8 7 fveq2d ⊢B=ifB∈ℋB0ℎ→normℎ⁡C-ℎB=normℎ⁡C-ℎifB∈ℋB0ℎ
9 8 breq1d ⊢B=ifB∈ℋB0ℎ→normℎ⁡C-ℎB<D2↔normℎ⁡C-ℎifB∈ℋB0ℎ<D2
10 9 anbi2d ⊢B=ifB∈ℋB0ℎ→normℎ⁡ifA∈ℋA0ℎ-ℎC<D2∧normℎ⁡C-ℎB<D2↔normℎ⁡ifA∈ℋA0ℎ-ℎC<D2∧normℎ⁡C-ℎifB∈ℋB0ℎ<D2
11 oveq2 ⊢B=ifB∈ℋB0ℎ→ifA∈ℋA0ℎ-ℎB=ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ
12 11 fveq2d ⊢B=ifB∈ℋB0ℎ→normℎ⁡ifA∈ℋA0ℎ-ℎB=normℎ⁡ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ
13 12 breq1d ⊢B=ifB∈ℋB0ℎ→normℎ⁡ifA∈ℋA0ℎ-ℎB<D↔normℎ⁡ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ<D
14 10 13 imbi12d ⊢B=ifB∈ℋB0ℎ→normℎ⁡ifA∈ℋA0ℎ-ℎC<D2∧normℎ⁡C-ℎB<D2→normℎ⁡ifA∈ℋA0ℎ-ℎB<D↔normℎ⁡ifA∈ℋA0ℎ-ℎC<D2∧normℎ⁡C-ℎifB∈ℋB0ℎ<D2→normℎ⁡ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ<D
15 oveq2 ⊢C=ifC∈ℋC0ℎ→ifA∈ℋA0ℎ-ℎC=ifA∈ℋA0ℎ-ℎifC∈ℋC0ℎ
16 15 fveq2d ⊢C=ifC∈ℋC0ℎ→normℎ⁡ifA∈ℋA0ℎ-ℎC=normℎ⁡ifA∈ℋA0ℎ-ℎifC∈ℋC0ℎ
17 16 breq1d ⊢C=ifC∈ℋC0ℎ→normℎ⁡ifA∈ℋA0ℎ-ℎC<D2↔normℎ⁡ifA∈ℋA0ℎ-ℎifC∈ℋC0ℎ<D2
18 fvoveq1 ⊢C=ifC∈ℋC0ℎ→normℎ⁡C-ℎifB∈ℋB0ℎ=normℎ⁡ifC∈ℋC0ℎ-ℎifB∈ℋB0ℎ
19 18 breq1d ⊢C=ifC∈ℋC0ℎ→normℎ⁡C-ℎifB∈ℋB0ℎ<D2↔normℎ⁡ifC∈ℋC0ℎ-ℎifB∈ℋB0ℎ<D2
20 17 19 anbi12d ⊢C=ifC∈ℋC0ℎ→normℎ⁡ifA∈ℋA0ℎ-ℎC<D2∧normℎ⁡C-ℎifB∈ℋB0ℎ<D2↔normℎ⁡ifA∈ℋA0ℎ-ℎifC∈ℋC0ℎ<D2∧normℎ⁡ifC∈ℋC0ℎ-ℎifB∈ℋB0ℎ<D2
21 20 imbi1d ⊢C=ifC∈ℋC0ℎ→normℎ⁡ifA∈ℋA0ℎ-ℎC<D2∧normℎ⁡C-ℎifB∈ℋB0ℎ<D2→normℎ⁡ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ<D↔normℎ⁡ifA∈ℋA0ℎ-ℎifC∈ℋC0ℎ<D2∧normℎ⁡ifC∈ℋC0ℎ-ℎifB∈ℋB0ℎ<D2→normℎ⁡ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ<D
22 oveq1 ⊢D=ifD∈ℝD2→D2=ifD∈ℝD22
23 22 breq2d ⊢D=ifD∈ℝD2→normℎ⁡ifA∈ℋA0ℎ-ℎifC∈ℋC0ℎ<D2↔normℎ⁡ifA∈ℋA0ℎ-ℎifC∈ℋC0ℎ<ifD∈ℝD22
24 22 breq2d ⊢D=ifD∈ℝD2→normℎ⁡ifC∈ℋC0ℎ-ℎifB∈ℋB0ℎ<D2↔normℎ⁡ifC∈ℋC0ℎ-ℎifB∈ℋB0ℎ<ifD∈ℝD22
25 23 24 anbi12d ⊢D=ifD∈ℝD2→normℎ⁡ifA∈ℋA0ℎ-ℎifC∈ℋC0ℎ<D2∧normℎ⁡ifC∈ℋC0ℎ-ℎifB∈ℋB0ℎ<D2↔normℎ⁡ifA∈ℋA0ℎ-ℎifC∈ℋC0ℎ<ifD∈ℝD22∧normℎ⁡ifC∈ℋC0ℎ-ℎifB∈ℋB0ℎ<ifD∈ℝD22
26 breq2 ⊢D=ifD∈ℝD2→normℎ⁡ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ<D↔normℎ⁡ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ<ifD∈ℝD2
27 25 26 imbi12d ⊢D=ifD∈ℝD2→normℎ⁡ifA∈ℋA0ℎ-ℎifC∈ℋC0ℎ<D2∧normℎ⁡ifC∈ℋC0ℎ-ℎifB∈ℋB0ℎ<D2→normℎ⁡ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ<D↔normℎ⁡ifA∈ℋA0ℎ-ℎifC∈ℋC0ℎ<ifD∈ℝD22∧normℎ⁡ifC∈ℋC0ℎ-ℎifB∈ℋB0ℎ<ifD∈ℝD22→normℎ⁡ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ<ifD∈ℝD2
28 ifhvhv0 ⊢ifA∈ℋA0ℎ∈ℋ
29 ifhvhv0 ⊢ifB∈ℋB0ℎ∈ℋ
30 ifhvhv0 ⊢ifC∈ℋC0ℎ∈ℋ
31 2re ⊢2∈ℝ
32 31 elimel ⊢ifD∈ℝD2∈ℝ
33 28 29 30 32 norm3lem ⊢normℎ⁡ifA∈ℋA0ℎ-ℎifC∈ℋC0ℎ<ifD∈ℝD22∧normℎ⁡ifC∈ℋC0ℎ-ℎifB∈ℋB0ℎ<ifD∈ℝD22→normℎ⁡ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ<ifD∈ℝD2
34 6 14 21 27 33 dedth4h ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧D∈ℝ→normℎ⁡A-ℎC<D2∧normℎ⁡C-ℎB<D2→normℎ⁡A-ℎB<D