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 ⊒ ( πœ‘ β†’ 𝐴 ∈ ( π‘ˆ βŠ• ( 𝑂 β€˜ π‘ˆ ) ) )