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 eqtrid ⊒ ( πœ‘ β†’ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) = ( ( dist β€˜ ( π‘ˆ β†Ύs π‘Œ ) ) β†Ύ ( ( Base β€˜ ( π‘ˆ β†Ύs π‘Œ ) ) Γ— ( Base β€˜ ( π‘ˆ β†Ύs π‘Œ ) ) ) ) )
33 28 fveq2d ⊒ ( πœ‘ β†’ ( CMet β€˜ π‘Œ ) = ( CMet β€˜ ( Base β€˜ ( π‘ˆ β†Ύs π‘Œ ) ) ) )
34 15 32 33 3eltr4d ⊒ ( πœ‘ β†’ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ∈ ( CMet β€˜ π‘Œ ) )