Metamath Proof Explorer

Theorem minveclem3a

Description: Lemma for minvec . D is a complete metric when restricted to Y . (Contributed by Mario Carneiro, 7-May-2014) (Revised by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypotheses minvec.x ⊢ 𝑋 = ( Base ‘ 𝑈 )
minvec.m ⊢ − = ( -g ‘ 𝑈 )
minvec.n ⊢ 𝑁 = ( norm ‘ 𝑈 )
minvec.u ⊢ ( 𝜑 → 𝑈 ∈ ℂPreHil )
minvec.y ⊢ ( 𝜑 → 𝑌 ∈ ( LSubSp ‘ 𝑈 ) )
minvec.w ⊢ ( 𝜑 → ( 𝑈 ↾s 𝑌 ) ∈ CMetSp )
minvec.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
minvec.j ⊢ 𝐽 = ( TopOpen ‘ 𝑈 )
minvec.r ⊢ 𝑅 = ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
minvec.s ⊢ 𝑆 = inf ( 𝑅 , ℝ , < )
minvec.d ⊢ 𝐷 = ( ( dist ‘ 𝑈 ) ↾ ( 𝑋 × 𝑋 ) )
Assertion minveclem3a ( 𝜑 → ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 minvec.x ⊢ 𝑋 = ( Base ‘ 𝑈 )
2 minvec.m ⊢ − = ( -g ‘ 𝑈 )
3 minvec.n ⊢ 𝑁 = ( norm ‘ 𝑈 )
4 minvec.u ⊢ ( 𝜑 → 𝑈 ∈ ℂPreHil )
5 minvec.y ⊢ ( 𝜑 → 𝑌 ∈ ( LSubSp ‘ 𝑈 ) )
6 minvec.w ⊢ ( 𝜑 → ( 𝑈 ↾s 𝑌 ) ∈ CMetSp )
7 minvec.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
8 minvec.j ⊢ 𝐽 = ( TopOpen ‘ 𝑈 )
9 minvec.r ⊢ 𝑅 = ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
10 minvec.s ⊢ 𝑆 = inf ( 𝑅 , ℝ , < )
11 minvec.d ⊢ 𝐷 = ( ( dist ‘ 𝑈 ) ↾ ( 𝑋 × 𝑋 ) )
12 eqid ⊢ ( Base ‘ ( 𝑈 ↾s 𝑌 ) ) = ( Base ‘ ( 𝑈 ↾s 𝑌 ) )
13 eqid ⊢ ( ( dist ‘ ( 𝑈 ↾s 𝑌 ) ) ↾ ( ( Base ‘ ( 𝑈 ↾s 𝑌 ) ) × ( Base ‘ ( 𝑈 ↾s 𝑌 ) ) ) ) = ( ( dist ‘ ( 𝑈 ↾s 𝑌 ) ) ↾ ( ( Base ‘ ( 𝑈 ↾s 𝑌 ) ) × ( Base ‘ ( 𝑈 ↾s 𝑌 ) ) ) )
14 12 13 cmscmet ⊢ ( ( 𝑈 ↾s 𝑌 ) ∈ CMetSp → ( ( dist ‘ ( 𝑈 ↾s 𝑌 ) ) ↾ ( ( Base ‘ ( 𝑈 ↾s 𝑌 ) ) × ( Base ‘ ( 𝑈 ↾s 𝑌 ) ) ) ) ∈ ( CMet ‘ ( Base ‘ ( 𝑈 ↾s 𝑌 ) ) ) )
15 6 14 syl ⊢ ( 𝜑 → ( ( dist ‘ ( 𝑈 ↾s 𝑌 ) ) ↾ ( ( Base ‘ ( 𝑈 ↾s 𝑌 ) ) × ( Base ‘ ( 𝑈 ↾s 𝑌 ) ) ) ) ∈ ( CMet ‘ ( Base ‘ ( 𝑈 ↾s 𝑌 ) ) ) )
16 11 reseq1i ⊢ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) = ( ( ( dist ‘ 𝑈 ) ↾ ( 𝑋 × 𝑋 ) ) ↾ ( 𝑌 × 𝑌 ) )
17 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
18 1 17 lssss ⊢ ( 𝑌 ∈ ( LSubSp ‘ 𝑈 ) → 𝑌 ⊆ 𝑋 )
19 5 18 syl ⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
20 xpss12 ⊢ ( ( 𝑌 ⊆ 𝑋 ∧ 𝑌 ⊆ 𝑋 ) → ( 𝑌 × 𝑌 ) ⊆ ( 𝑋 × 𝑋 ) )
21 19 19 20 syl2anc ⊢ ( 𝜑 → ( 𝑌 × 𝑌 ) ⊆ ( 𝑋 × 𝑋 ) )
22 21 resabs1d ⊢ ( 𝜑 → ( ( ( dist ‘ 𝑈 ) ↾ ( 𝑋 × 𝑋 ) ) ↾ ( 𝑌 × 𝑌 ) ) = ( ( dist ‘ 𝑈 ) ↾ ( 𝑌 × 𝑌 ) ) )
23 eqid ⊢ ( 𝑈 ↾s 𝑌 ) = ( 𝑈 ↾s 𝑌 )
24 eqid ⊢ ( dist ‘ 𝑈 ) = ( dist ‘ 𝑈 )
25 23 24 ressds ⊢ ( 𝑌 ∈ ( LSubSp ‘ 𝑈 ) → ( dist ‘ 𝑈 ) = ( dist ‘ ( 𝑈 ↾s 𝑌 ) ) )
26 5 25 syl ⊢ ( 𝜑 → ( dist ‘ 𝑈 ) = ( dist ‘ ( 𝑈 ↾s 𝑌 ) ) )
27 23 1 ressbas2 ⊢ ( 𝑌 ⊆ 𝑋 → 𝑌 = ( Base ‘ ( 𝑈 ↾s 𝑌 ) ) )
28 19 27 syl ⊢ ( 𝜑 → 𝑌 = ( Base ‘ ( 𝑈 ↾s 𝑌 ) ) )
29 28 sqxpeqd ⊢ ( 𝜑 → ( 𝑌 × 𝑌 ) = ( ( Base ‘ ( 𝑈 ↾s 𝑌 ) ) × ( Base ‘ ( 𝑈 ↾s 𝑌 ) ) ) )
30 26 29 reseq12d ⊢ ( 𝜑 → ( ( dist ‘ 𝑈 ) ↾ ( 𝑌 × 𝑌 ) ) = ( ( dist ‘ ( 𝑈 ↾s 𝑌 ) ) ↾ ( ( Base ‘ ( 𝑈 ↾s 𝑌 ) ) × ( Base ‘ ( 𝑈 ↾s 𝑌 ) ) ) ) )
31 22 30 eqtrd ⊢ ( 𝜑 → ( ( ( dist ‘ 𝑈 ) ↾ ( 𝑋 × 𝑋 ) ) ↾ ( 𝑌 × 𝑌 ) ) = ( ( dist ‘ ( 𝑈 ↾s 𝑌 ) ) ↾ ( ( Base ‘ ( 𝑈 ↾s 𝑌 ) ) × ( Base ‘ ( 𝑈 ↾s 𝑌 ) ) ) ) )
32 16 31 syl5eq ⊢ ( 𝜑 → ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) = ( ( dist ‘ ( 𝑈 ↾s 𝑌 ) ) ↾ ( ( Base ‘ ( 𝑈 ↾s 𝑌 ) ) × ( Base ‘ ( 𝑈 ↾s 𝑌 ) ) ) ) )
33 28 fveq2d ⊢ ( 𝜑 → ( CMet ‘ 𝑌 ) = ( CMet ‘ ( Base ‘ ( 𝑈 ↾s 𝑌 ) ) ) )
34 15 32 33 3eltr4d ⊢ ( 𝜑 → ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) )