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 bitrid ⊒ ( ( πœ‘ ∧ ( π‘₯ ∈ π‘Œ ∧ 𝑀 ∈ π‘Œ ) ) β†’ ( ( ( π‘₯ 𝐷 𝑀 ) ↑ 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 ⊒ ( πœ‘ β†’ βˆƒ! π‘₯ ∈ π‘Œ βˆ€ 𝑦 ∈ π‘Œ ( 𝑁 β€˜ ( 𝐴 βˆ’ π‘₯ ) ) ≀ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) )