Metamath Proof Explorer

Theorem minveclem7

Description: Lemma for minvec . Since any two minimal points are distance zero away from each other, the minimal point is unique. (Contributed by Mario Carneiro, 9-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 minveclem7 ( 𝜑 → ∃! 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )

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 1 2 3 4 5 6 7 8 9 10 11 minveclem5 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
13 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) ∧ ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ∧ ( ( 𝐴 𝐷 𝑤 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ) ) → 𝑈 ∈ ℂPreHil )
14 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) ∧ ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ∧ ( ( 𝐴 𝐷 𝑤 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ) ) → 𝑌 ∈ ( LSubSp ‘ 𝑈 ) )
15 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) ∧ ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ∧ ( ( 𝐴 𝐷 𝑤 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ) ) → ( 𝑈 ↾s 𝑌 ) ∈ CMetSp )
16 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) ∧ ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ∧ ( ( 𝐴 𝐷 𝑤 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ) ) → 𝐴 ∈ 𝑋 )
17 0re ⊢ 0 ∈ ℝ
18 17 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) ∧ ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ∧ ( ( 𝐴 𝐷 𝑤 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ) ) → 0 ∈ ℝ )
19 0le0 ⊢ 0 ≤ 0
20 19 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) ∧ ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ∧ ( ( 𝐴 𝐷 𝑤 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ) ) → 0 ≤ 0 )
21 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) ∧ ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ∧ ( ( 𝐴 𝐷 𝑤 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ) ) → 𝑥 ∈ 𝑌 )
22 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) ∧ ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ∧ ( ( 𝐴 𝐷 𝑤 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ) ) → 𝑤 ∈ 𝑌 )
23 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) ∧ ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ∧ ( ( 𝐴 𝐷 𝑤 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ) ) → ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) )
24 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) ∧ ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ∧ ( ( 𝐴 𝐷 𝑤 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ) ) → ( ( 𝐴 𝐷 𝑤 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) )
25 1 2 3 13 14 15 16 8 9 10 11 18 20 21 22 23 24 minveclem2 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) ∧ ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ∧ ( ( 𝐴 𝐷 𝑤 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ) ) → ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) ≤ ( 4 · 0 ) )
26 25 ex ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ∧ ( ( 𝐴 𝐷 𝑤 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ) → ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) ≤ ( 4 · 0 ) ) )
27 1 2 3 4 5 6 7 8 9 10 11 minveclem6 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ↔ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) )
28 27 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ↔ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) )
29 1 2 3 4 5 6 7 8 9 10 11 minveclem6 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( ( ( 𝐴 𝐷 𝑤 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ↔ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑤 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) )
30 29 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( ( 𝐴 𝐷 𝑤 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ↔ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑤 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) )
31 28 30 anbi12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ∧ ( ( 𝐴 𝐷 𝑤 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ) ↔ ( ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ∧ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑤 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) )
32 4cn ⊢ 4 ∈ ℂ
33 32 mul01i ⊢ ( 4 · 0 ) = 0
34 33 breq2i ⊢ ( ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) ≤ ( 4 · 0 ) ↔ ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) ≤ 0 )
35 cphngp ⊢ ( 𝑈 ∈ ℂPreHil → 𝑈 ∈ NrmGrp )
36 ngpms ⊢ ( 𝑈 ∈ NrmGrp → 𝑈 ∈ MetSp )
37 4 35 36 3syl ⊢ ( 𝜑 → 𝑈 ∈ MetSp )
38 37 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → 𝑈 ∈ MetSp )
39 1 11 msmet ⊢ ( 𝑈 ∈ MetSp → 𝐷 ∈ ( Met ‘ 𝑋 ) )
40 38 39 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
41 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
42 1 41 lssss ⊢ ( 𝑌 ∈ ( LSubSp ‘ 𝑈 ) → 𝑌 ⊆ 𝑋 )
43 5 42 syl ⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
44 43 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → 𝑌 ⊆ 𝑋 )
45 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → 𝑥 ∈ 𝑌 )
46 44 45 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → 𝑥 ∈ 𝑋 )
47 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → 𝑤 ∈ 𝑌 )
48 44 47 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → 𝑤 ∈ 𝑋 )
49 metcl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( 𝑥 𝐷 𝑤 ) ∈ ℝ )
50 40 46 48 49 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( 𝑥 𝐷 𝑤 ) ∈ ℝ )
51 50 sqge0d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → 0 ≤ ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) )
52 51 biantrud ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) ≤ 0 ↔ ( ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) ≤ 0 ∧ 0 ≤ ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) ) ) )
53 50 resqcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) ∈ ℝ )
54 letri3 ⊢ ( ( ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) = 0 ↔ ( ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) ≤ 0 ∧ 0 ≤ ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) ) ) )
55 53 17 54 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) = 0 ↔ ( ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) ≤ 0 ∧ 0 ≤ ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) ) ) )
56 50 recnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( 𝑥 𝐷 𝑤 ) ∈ ℂ )
57 sqeq0 ⊢ ( ( 𝑥 𝐷 𝑤 ) ∈ ℂ → ( ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) = 0 ↔ ( 𝑥 𝐷 𝑤 ) = 0 ) )
58 56 57 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) = 0 ↔ ( 𝑥 𝐷 𝑤 ) = 0 ) )
59 meteq0 ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝑥 𝐷 𝑤 ) = 0 ↔ 𝑥 = 𝑤 ) )
60 40 46 48 59 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( 𝑥 𝐷 𝑤 ) = 0 ↔ 𝑥 = 𝑤 ) )
61 58 60 bitrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) = 0 ↔ 𝑥 = 𝑤 ) )
62 52 55 61 3bitr2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) ≤ 0 ↔ 𝑥 = 𝑤 ) )
63 34 62 syl5bb ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) ≤ ( 4 · 0 ) ↔ 𝑥 = 𝑤 ) )
64 26 31 63 3imtr3d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ∧ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑤 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) → 𝑥 = 𝑤 ) )
65 64 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑌 ∀ 𝑤 ∈ 𝑌 ( ( ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ∧ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑤 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) → 𝑥 = 𝑤 ) )
66 oveq2 ⊢ ( 𝑥 = 𝑤 → ( 𝐴 − 𝑥 ) = ( 𝐴 − 𝑤 ) )
67 66 fveq2d ⊢ ( 𝑥 = 𝑤 → ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) = ( 𝑁 ‘ ( 𝐴 − 𝑤 ) ) )
68 67 breq1d ⊢ ( 𝑥 = 𝑤 → ( ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ↔ ( 𝑁 ‘ ( 𝐴 − 𝑤 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) )
69 68 ralbidv ⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑤 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) )
70 69 reu4 ⊢ ( ∃! 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ↔ ( ∃ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ∧ ∀ 𝑥 ∈ 𝑌 ∀ 𝑤 ∈ 𝑌 ( ( ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ∧ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑤 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) → 𝑥 = 𝑤 ) ) )
71 12 65 70 sylanbrc ⊢ ( 𝜑 → ∃! 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )