Metamath Proof Explorer

Theorem pjthlem2

Description: Lemma for pjth . (Contributed by NM, 10-Oct-1999) (Revised by Mario Carneiro, 15-May-2014)

Ref Expression
Hypotheses pjthlem.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
pjthlem.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
pjthlem.p ⊢ + = ( +g ‘ 𝑊 )
pjthlem.m ⊢ − = ( -g ‘ 𝑊 )
pjthlem.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
pjthlem.l ⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
pjthlem.1 ⊢ ( 𝜑 → 𝑊 ∈ ℂHil )
pjthlem.2 ⊢ ( 𝜑 → 𝑈 ∈ 𝐿 )
pjthlem.4 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
pjthlem.j ⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
pjthlem.s ⊢ ⊕ = ( LSSum ‘ 𝑊 )
pjthlem.o ⊢ 𝑂 = ( ocv ‘ 𝑊 )
pjthlem.3 ⊢ ( 𝜑 → 𝑈 ∈ ( Clsd ‘ 𝐽 ) )
Assertion pjthlem2 ( 𝜑 → 𝐴 ∈ ( 𝑈 ⊕ ( 𝑂 ‘ 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 pjthlem.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 pjthlem.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
3 pjthlem.p ⊢ + = ( +g ‘ 𝑊 )
4 pjthlem.m ⊢ − = ( -g ‘ 𝑊 )
5 pjthlem.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
6 pjthlem.l ⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
7 pjthlem.1 ⊢ ( 𝜑 → 𝑊 ∈ ℂHil )
8 pjthlem.2 ⊢ ( 𝜑 → 𝑈 ∈ 𝐿 )
9 pjthlem.4 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
10 pjthlem.j ⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
11 pjthlem.s ⊢ ⊕ = ( LSSum ‘ 𝑊 )
12 pjthlem.o ⊢ 𝑂 = ( ocv ‘ 𝑊 )
13 pjthlem.3 ⊢ ( 𝜑 → 𝑈 ∈ ( Clsd ‘ 𝐽 ) )
14 hlcph ⊢ ( 𝑊 ∈ ℂHil → 𝑊 ∈ ℂPreHil )
15 7 14 syl ⊢ ( 𝜑 → 𝑊 ∈ ℂPreHil )
16 8 6 eleqtrdi ⊢ ( 𝜑 → 𝑈 ∈ ( LSubSp ‘ 𝑊 ) )
17 hlcms ⊢ ( 𝑊 ∈ ℂHil → 𝑊 ∈ CMetSp )
18 7 17 syl ⊢ ( 𝜑 → 𝑊 ∈ CMetSp )
19 1 6 lssss ⊢ ( 𝑈 ∈ 𝐿 → 𝑈 ⊆ 𝑉 )
20 8 19 syl ⊢ ( 𝜑 → 𝑈 ⊆ 𝑉 )
21 eqid ⊢ ( 𝑊 ↾s 𝑈 ) = ( 𝑊 ↾s 𝑈 )
22 21 1 10 cmsss ⊢ ( ( 𝑊 ∈ CMetSp ∧ 𝑈 ⊆ 𝑉 ) → ( ( 𝑊 ↾s 𝑈 ) ∈ CMetSp ↔ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) )
23 18 20 22 syl2anc ⊢ ( 𝜑 → ( ( 𝑊 ↾s 𝑈 ) ∈ CMetSp ↔ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) )
24 13 23 mpbird ⊢ ( 𝜑 → ( 𝑊 ↾s 𝑈 ) ∈ CMetSp )
25 1 4 2 15 16 24 9 minvec ⊢ ( 𝜑 → ∃! 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
26 reurex ⊢ ( ∃! 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) → ∃ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
27 25 26 syl ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
28 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) → 𝑊 ∈ ℂPreHil )
29 cphlmod ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ LMod )
30 28 29 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) → 𝑊 ∈ LMod )
31 lmodabl ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
32 30 31 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) → 𝑊 ∈ Abel )
33 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) → 𝑈 ∈ 𝐿 )
34 33 19 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) → 𝑈 ⊆ 𝑉 )
35 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) → 𝑥 ∈ 𝑈 )
36 34 35 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) → 𝑥 ∈ 𝑉 )
37 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) → 𝐴 ∈ 𝑉 )
38 1 3 4 ablpncan3 ⊢ ( ( 𝑊 ∈ Abel ∧ ( 𝑥 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ) → ( 𝑥 + ( 𝐴 − 𝑥 ) ) = 𝐴 )
39 32 36 37 38 syl12anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) → ( 𝑥 + ( 𝐴 − 𝑥 ) ) = 𝐴 )
40 6 lsssssubg ⊢ ( 𝑊 ∈ LMod → 𝐿 ⊆ ( SubGrp ‘ 𝑊 ) )
41 30 40 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) → 𝐿 ⊆ ( SubGrp ‘ 𝑊 ) )
42 41 33 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
43 cphphl ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil )
44 28 43 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) → 𝑊 ∈ PreHil )
45 1 12 6 ocvlss ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑈 ⊆ 𝑉 ) → ( 𝑂 ‘ 𝑈 ) ∈ 𝐿 )
46 44 34 45 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) → ( 𝑂 ‘ 𝑈 ) ∈ 𝐿 )
47 41 46 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) → ( 𝑂 ‘ 𝑈 ) ∈ ( SubGrp ‘ 𝑊 ) )
48 1 4 lmodvsubcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐴 − 𝑥 ) ∈ 𝑉 )
49 30 37 36 48 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) → ( 𝐴 − 𝑥 ) ∈ 𝑉 )
50 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) ∧ 𝑧 ∈ 𝑈 ) → 𝑊 ∈ ℂHil )
51 33 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) ∧ 𝑧 ∈ 𝑈 ) → 𝑈 ∈ 𝐿 )
52 49 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) ∧ 𝑧 ∈ 𝑈 ) → ( 𝐴 − 𝑥 ) ∈ 𝑉 )
53 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ∈ 𝑈 )
54 oveq2 ⊢ ( 𝑦 = ( 𝑤 + 𝑥 ) → ( 𝐴 − 𝑦 ) = ( 𝐴 − ( 𝑤 + 𝑥 ) ) )
55 54 fveq2d ⊢ ( 𝑦 = ( 𝑤 + 𝑥 ) → ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) = ( 𝑁 ‘ ( 𝐴 − ( 𝑤 + 𝑥 ) ) ) )
56 55 breq2d ⊢ ( 𝑦 = ( 𝑤 + 𝑥 ) → ( ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ↔ ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − ( 𝑤 + 𝑥 ) ) ) ) )
57 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) ∧ 𝑤 ∈ 𝑈 ) → ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
58 30 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) ∧ 𝑤 ∈ 𝑈 ) → 𝑊 ∈ LMod )
59 33 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) ∧ 𝑤 ∈ 𝑈 ) → 𝑈 ∈ 𝐿 )
60 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) ∧ 𝑤 ∈ 𝑈 ) → 𝑤 ∈ 𝑈 )
61 35 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) ∧ 𝑤 ∈ 𝑈 ) → 𝑥 ∈ 𝑈 )
62 3 6 lssvacl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ) ∧ ( 𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ) → ( 𝑤 + 𝑥 ) ∈ 𝑈 )
63 58 59 60 61 62 syl22anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) ∧ 𝑤 ∈ 𝑈 ) → ( 𝑤 + 𝑥 ) ∈ 𝑈 )
64 56 57 63 rspcdva ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) ∧ 𝑤 ∈ 𝑈 ) → ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − ( 𝑤 + 𝑥 ) ) ) )
65 lmodgrp ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
66 30 65 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) → 𝑊 ∈ Grp )
67 66 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) ∧ 𝑤 ∈ 𝑈 ) → 𝑊 ∈ Grp )
68 37 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) ∧ 𝑤 ∈ 𝑈 ) → 𝐴 ∈ 𝑉 )
69 36 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) ∧ 𝑤 ∈ 𝑈 ) → 𝑥 ∈ 𝑉 )
70 34 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) ∧ 𝑤 ∈ 𝑈 ) → 𝑤 ∈ 𝑉 )
71 1 3 4 grpsubsub4 ⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉 ) ) → ( ( 𝐴 − 𝑥 ) − 𝑤 ) = ( 𝐴 − ( 𝑤 + 𝑥 ) ) )
72 67 68 69 70 71 syl13anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) ∧ 𝑤 ∈ 𝑈 ) → ( ( 𝐴 − 𝑥 ) − 𝑤 ) = ( 𝐴 − ( 𝑤 + 𝑥 ) ) )
73 72 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) ∧ 𝑤 ∈ 𝑈 ) → ( 𝑁 ‘ ( ( 𝐴 − 𝑥 ) − 𝑤 ) ) = ( 𝑁 ‘ ( 𝐴 − ( 𝑤 + 𝑥 ) ) ) )
74 64 73 breqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) ∧ 𝑤 ∈ 𝑈 ) → ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( ( 𝐴 − 𝑥 ) − 𝑤 ) ) )
75 74 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) → ∀ 𝑤 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( ( 𝐴 − 𝑥 ) − 𝑤 ) ) )
76 75 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) ∧ 𝑧 ∈ 𝑈 ) → ∀ 𝑤 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( ( 𝐴 − 𝑥 ) − 𝑤 ) ) )
77 eqid ⊢ ( ( ( 𝐴 − 𝑥 ) , 𝑧 ) / ( ( 𝑧 , 𝑧 ) + 1 ) ) = ( ( ( 𝐴 − 𝑥 ) , 𝑧 ) / ( ( 𝑧 , 𝑧 ) + 1 ) )
78 1 2 3 4 5 6 50 51 52 53 76 77 pjthlem1 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) ∧ 𝑧 ∈ 𝑈 ) → ( ( 𝐴 − 𝑥 ) , 𝑧 ) = 0 )
79 28 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) ∧ 𝑧 ∈ 𝑈 ) → 𝑊 ∈ ℂPreHil )
80 cphclm ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ ℂMod )
81 79 80 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) ∧ 𝑧 ∈ 𝑈 ) → 𝑊 ∈ ℂMod )
82 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
83 82 clm0 ⊢ ( 𝑊 ∈ ℂMod → 0 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
84 81 83 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) ∧ 𝑧 ∈ 𝑈 ) → 0 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
85 78 84 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) ∧ 𝑧 ∈ 𝑈 ) → ( ( 𝐴 − 𝑥 ) , 𝑧 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
86 85 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) → ∀ 𝑧 ∈ 𝑈 ( ( 𝐴 − 𝑥 ) , 𝑧 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
87 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
88 1 5 82 87 12 elocv ⊢ ( ( 𝐴 − 𝑥 ) ∈ ( 𝑂 ‘ 𝑈 ) ↔ ( 𝑈 ⊆ 𝑉 ∧ ( 𝐴 − 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑈 ( ( 𝐴 − 𝑥 ) , 𝑧 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
89 34 49 86 88 syl3anbrc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) → ( 𝐴 − 𝑥 ) ∈ ( 𝑂 ‘ 𝑈 ) )
90 3 11 lsmelvali ⊢ ( ( ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑂 ‘ 𝑈 ) ∈ ( SubGrp ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ( 𝐴 − 𝑥 ) ∈ ( 𝑂 ‘ 𝑈 ) ) ) → ( 𝑥 + ( 𝐴 − 𝑥 ) ) ∈ ( 𝑈 ⊕ ( 𝑂 ‘ 𝑈 ) ) )
91 42 47 35 89 90 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) → ( 𝑥 + ( 𝐴 − 𝑥 ) ) ∈ ( 𝑈 ⊕ ( 𝑂 ‘ 𝑈 ) ) )
92 39 91 eqeltrrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ) → 𝐴 ∈ ( 𝑈 ⊕ ( 𝑂 ‘ 𝑈 ) ) )
93 27 92 rexlimddv ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑈 ⊕ ( 𝑂 ‘ 𝑈 ) ) )