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 
|- V = ( Base ` W )
pjthlem.n 
|- N = ( norm ` W )
pjthlem.p 
|- .+ = ( +g ` W )
pjthlem.m 
|- .- = ( -g ` W )
pjthlem.h 
|- ., = ( .i ` W )
pjthlem.l 
|- L = ( LSubSp ` W )
pjthlem.1 
|- ( ph -> W e. CHil )
pjthlem.2 
|- ( ph -> U e. L )
pjthlem.4 
|- ( ph -> A e. V )
pjthlem.j 
|- J = ( TopOpen ` W )
pjthlem.s 
|- .(+) = ( LSSum ` W )
pjthlem.o 
|- O = ( ocv ` W )
pjthlem.3 
|- ( ph -> U e. ( Clsd ` J ) )
Assertion pjthlem2 
|- ( ph -> A e. ( U .(+) ( O ` U ) ) )

Proof

Step Hyp Ref Expression
1 pjthlem.v 
 |-  V = ( Base ` W )
2 pjthlem.n 
 |-  N = ( norm ` W )
3 pjthlem.p 
 |-  .+ = ( +g ` W )
4 pjthlem.m 
 |-  .- = ( -g ` W )
5 pjthlem.h 
 |-  ., = ( .i ` W )
6 pjthlem.l 
 |-  L = ( LSubSp ` W )
7 pjthlem.1 
 |-  ( ph -> W e. CHil )
8 pjthlem.2 
 |-  ( ph -> U e. L )
9 pjthlem.4 
 |-  ( ph -> A e. V )
10 pjthlem.j 
 |-  J = ( TopOpen ` W )
11 pjthlem.s 
 |-  .(+) = ( LSSum ` W )
12 pjthlem.o 
 |-  O = ( ocv ` W )
13 pjthlem.3 
 |-  ( ph -> U e. ( Clsd ` J ) )
14 hlcph 
 |-  ( W e. CHil -> W e. CPreHil )
15 7 14 syl 
 |-  ( ph -> W e. CPreHil )
16 8 6 eleqtrdi 
 |-  ( ph -> U e. ( LSubSp ` W ) )
17 hlcms 
 |-  ( W e. CHil -> W e. CMetSp )
18 7 17 syl 
 |-  ( ph -> W e. CMetSp )
19 1 6 lssss 
 |-  ( U e. L -> U C_ V )
20 8 19 syl 
 |-  ( ph -> U C_ V )
21 eqid 
 |-  ( W |`s U ) = ( W |`s U )
22 21 1 10 cmsss 
 |-  ( ( W e. CMetSp /\ U C_ V ) -> ( ( W |`s U ) e. CMetSp <-> U e. ( Clsd ` J ) ) )
23 18 20 22 syl2anc 
 |-  ( ph -> ( ( W |`s U ) e. CMetSp <-> U e. ( Clsd ` J ) ) )
24 13 23 mpbird 
 |-  ( ph -> ( W |`s U ) e. CMetSp )
25 1 4 2 15 16 24 9 minvec 
 |-  ( ph -> E! x e. U A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) )
26 reurex 
 |-  ( E! x e. U A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) -> E. x e. U A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) )
27 25 26 syl 
 |-  ( ph -> E. x e. U A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) )
28 15 adantr 
 |-  ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) -> W e. CPreHil )
29 cphlmod 
 |-  ( W e. CPreHil -> W e. LMod )
30 28 29 syl 
 |-  ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) -> W e. LMod )
31 lmodabl 
 |-  ( W e. LMod -> W e. Abel )
32 30 31 syl 
 |-  ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) -> W e. Abel )
33 8 adantr 
 |-  ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) -> U e. L )
34 33 19 syl 
 |-  ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) -> U C_ V )
35 simprl 
 |-  ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) -> x e. U )
36 34 35 sseldd 
 |-  ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) -> x e. V )
37 9 adantr 
 |-  ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) -> A e. V )
38 1 3 4 ablpncan3 
 |-  ( ( W e. Abel /\ ( x e. V /\ A e. V ) ) -> ( x .+ ( A .- x ) ) = A )
39 32 36 37 38 syl12anc 
 |-  ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) -> ( x .+ ( A .- x ) ) = A )
40 6 lsssssubg 
 |-  ( W e. LMod -> L C_ ( SubGrp ` W ) )
41 30 40 syl 
 |-  ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) -> L C_ ( SubGrp ` W ) )
42 41 33 sseldd 
 |-  ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) -> U e. ( SubGrp ` W ) )
43 cphphl 
 |-  ( W e. CPreHil -> W e. PreHil )
44 28 43 syl 
 |-  ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) -> W e. PreHil )
45 1 12 6 ocvlss 
 |-  ( ( W e. PreHil /\ U C_ V ) -> ( O ` U ) e. L )
46 44 34 45 syl2anc 
 |-  ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) -> ( O ` U ) e. L )
47 41 46 sseldd 
 |-  ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) -> ( O ` U ) e. ( SubGrp ` W ) )
48 1 4 lmodvsubcl 
 |-  ( ( W e. LMod /\ A e. V /\ x e. V ) -> ( A .- x ) e. V )
49 30 37 36 48 syl3anc 
 |-  ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) -> ( A .- x ) e. V )
50 7 ad2antrr 
 |-  ( ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) /\ z e. U ) -> W e. CHil )
51 33 adantr 
 |-  ( ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) /\ z e. U ) -> U e. L )
52 49 adantr 
 |-  ( ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) /\ z e. U ) -> ( A .- x ) e. V )
53 simpr 
 |-  ( ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) /\ z e. U ) -> z e. U )
54 oveq2 
 |-  ( y = ( w .+ x ) -> ( A .- y ) = ( A .- ( w .+ x ) ) )
55 54 fveq2d 
 |-  ( y = ( w .+ x ) -> ( N ` ( A .- y ) ) = ( N ` ( A .- ( w .+ x ) ) ) )
56 55 breq2d 
 |-  ( y = ( w .+ x ) -> ( ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) <-> ( N ` ( A .- x ) ) <_ ( N ` ( A .- ( w .+ x ) ) ) ) )
57 simplrr 
 |-  ( ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) /\ w e. U ) -> A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) )
58 30 adantr 
 |-  ( ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) /\ w e. U ) -> W e. LMod )
59 33 adantr 
 |-  ( ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) /\ w e. U ) -> U e. L )
60 simpr 
 |-  ( ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) /\ w e. U ) -> w e. U )
61 35 adantr 
 |-  ( ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) /\ w e. U ) -> x e. U )
62 3 6 lssvacl 
 |-  ( ( ( W e. LMod /\ U e. L ) /\ ( w e. U /\ x e. U ) ) -> ( w .+ x ) e. U )
63 58 59 60 61 62 syl22anc 
 |-  ( ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) /\ w e. U ) -> ( w .+ x ) e. U )
64 56 57 63 rspcdva 
 |-  ( ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) /\ w e. U ) -> ( N ` ( A .- x ) ) <_ ( N ` ( A .- ( w .+ x ) ) ) )
65 lmodgrp 
 |-  ( W e. LMod -> W e. Grp )
66 30 65 syl 
 |-  ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) -> W e. Grp )
67 66 adantr 
 |-  ( ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) /\ w e. U ) -> W e. Grp )
68 37 adantr 
 |-  ( ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) /\ w e. U ) -> A e. V )
69 36 adantr 
 |-  ( ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) /\ w e. U ) -> x e. V )
70 34 sselda 
 |-  ( ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) /\ w e. U ) -> w e. V )
71 1 3 4 grpsubsub4 
 |-  ( ( W e. Grp /\ ( A e. V /\ x e. V /\ w e. V ) ) -> ( ( A .- x ) .- w ) = ( A .- ( w .+ x ) ) )
72 67 68 69 70 71 syl13anc 
 |-  ( ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) /\ w e. U ) -> ( ( A .- x ) .- w ) = ( A .- ( w .+ x ) ) )
73 72 fveq2d 
 |-  ( ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) /\ w e. U ) -> ( N ` ( ( A .- x ) .- w ) ) = ( N ` ( A .- ( w .+ x ) ) ) )
74 64 73 breqtrrd 
 |-  ( ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) /\ w e. U ) -> ( N ` ( A .- x ) ) <_ ( N ` ( ( A .- x ) .- w ) ) )
75 74 ralrimiva 
 |-  ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) -> A. w e. U ( N ` ( A .- x ) ) <_ ( N ` ( ( A .- x ) .- w ) ) )
76 75 adantr 
 |-  ( ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) /\ z e. U ) -> A. w e. U ( N ` ( A .- x ) ) <_ ( N ` ( ( A .- x ) .- w ) ) )
77 eqid 
 |-  ( ( ( A .- x ) ., z ) / ( ( z ., z ) + 1 ) ) = ( ( ( A .- x ) ., z ) / ( ( z ., z ) + 1 ) )
78 1 2 3 4 5 6 50 51 52 53 76 77 pjthlem1 
 |-  ( ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) /\ z e. U ) -> ( ( A .- x ) ., z ) = 0 )
79 28 adantr 
 |-  ( ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) /\ z e. U ) -> W e. CPreHil )
80 cphclm 
 |-  ( W e. CPreHil -> W e. CMod )
81 79 80 syl 
 |-  ( ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) /\ z e. U ) -> W e. CMod )
82 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
83 82 clm0 
 |-  ( W e. CMod -> 0 = ( 0g ` ( Scalar ` W ) ) )
84 81 83 syl 
 |-  ( ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) /\ z e. U ) -> 0 = ( 0g ` ( Scalar ` W ) ) )
85 78 84 eqtrd 
 |-  ( ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) /\ z e. U ) -> ( ( A .- x ) ., z ) = ( 0g ` ( Scalar ` W ) ) )
86 85 ralrimiva 
 |-  ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) -> A. z e. U ( ( A .- x ) ., z ) = ( 0g ` ( Scalar ` W ) ) )
87 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
88 1 5 82 87 12 elocv 
 |-  ( ( A .- x ) e. ( O ` U ) <-> ( U C_ V /\ ( A .- x ) e. V /\ A. z e. U ( ( A .- x ) ., z ) = ( 0g ` ( Scalar ` W ) ) ) )
89 34 49 86 88 syl3anbrc 
 |-  ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) -> ( A .- x ) e. ( O ` U ) )
90 3 11 lsmelvali 
 |-  ( ( ( U e. ( SubGrp ` W ) /\ ( O ` U ) e. ( SubGrp ` W ) ) /\ ( x e. U /\ ( A .- x ) e. ( O ` U ) ) ) -> ( x .+ ( A .- x ) ) e. ( U .(+) ( O ` U ) ) )
91 42 47 35 89 90 syl22anc 
 |-  ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) -> ( x .+ ( A .- x ) ) e. ( U .(+) ( O ` U ) ) )
92 39 91 eqeltrrd 
 |-  ( ( ph /\ ( x e. U /\ A. y e. U ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) -> A e. ( U .(+) ( O ` U ) ) )
93 27 92 rexlimddv 
 |-  ( ph -> A e. ( U .(+) ( O ` U ) ) )