Metamath Proof Explorer

Theorem pjhthlem2

Description: Lemma for pjhth . (Contributed by NM, 10-Oct-1999) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses pjhth.1 
|- H e. CH
pjhth.2 
|- ( ph -> A e. ~H )
Assertion pjhthlem2 
|- ( ph -> E. x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) )

Proof

Step Hyp Ref Expression
1 pjhth.1 
 |-  H e. CH
2 pjhth.2 
 |-  ( ph -> A e. ~H )
3 2 adantr 
 |-  ( ( ph /\ ( x e. H /\ A. z e. H ( normh ` ( A -h x ) ) <_ ( normh ` ( A -h z ) ) ) ) -> A e. ~H )
4 1 cheli 
 |-  ( x e. H -> x e. ~H )
5 4 ad2antrl 
 |-  ( ( ph /\ ( x e. H /\ A. z e. H ( normh ` ( A -h x ) ) <_ ( normh ` ( A -h z ) ) ) ) -> x e. ~H )
6 hvsubcl 
 |-  ( ( A e. ~H /\ x e. ~H ) -> ( A -h x ) e. ~H )
7 3 5 6 syl2anc 
 |-  ( ( ph /\ ( x e. H /\ A. z e. H ( normh ` ( A -h x ) ) <_ ( normh ` ( A -h z ) ) ) ) -> ( A -h x ) e. ~H )
8 3 adantr 
 |-  ( ( ( ph /\ ( x e. H /\ A. z e. H ( normh ` ( A -h x ) ) <_ ( normh ` ( A -h z ) ) ) ) /\ y e. H ) -> A e. ~H )
9 simplrl 
 |-  ( ( ( ph /\ ( x e. H /\ A. z e. H ( normh ` ( A -h x ) ) <_ ( normh ` ( A -h z ) ) ) ) /\ y e. H ) -> x e. H )
10 simpr 
 |-  ( ( ( ph /\ ( x e. H /\ A. z e. H ( normh ` ( A -h x ) ) <_ ( normh ` ( A -h z ) ) ) ) /\ y e. H ) -> y e. H )
11 simplrr 
 |-  ( ( ( ph /\ ( x e. H /\ A. z e. H ( normh ` ( A -h x ) ) <_ ( normh ` ( A -h z ) ) ) ) /\ y e. H ) -> A. z e. H ( normh ` ( A -h x ) ) <_ ( normh ` ( A -h z ) ) )
12 eqid 
 |-  ( ( ( A -h x ) .ih y ) / ( ( y .ih y ) + 1 ) ) = ( ( ( A -h x ) .ih y ) / ( ( y .ih y ) + 1 ) )
13 1 8 9 10 11 12 pjhthlem1 
 |-  ( ( ( ph /\ ( x e. H /\ A. z e. H ( normh ` ( A -h x ) ) <_ ( normh ` ( A -h z ) ) ) ) /\ y e. H ) -> ( ( A -h x ) .ih y ) = 0 )
14 13 ralrimiva 
 |-  ( ( ph /\ ( x e. H /\ A. z e. H ( normh ` ( A -h x ) ) <_ ( normh ` ( A -h z ) ) ) ) -> A. y e. H ( ( A -h x ) .ih y ) = 0 )
15 1 chshii 
 |-  H e. SH
16 shocel 
 |-  ( H e. SH -> ( ( A -h x ) e. ( _|_ ` H ) <-> ( ( A -h x ) e. ~H /\ A. y e. H ( ( A -h x ) .ih y ) = 0 ) ) )
17 15 16 ax-mp 
 |-  ( ( A -h x ) e. ( _|_ ` H ) <-> ( ( A -h x ) e. ~H /\ A. y e. H ( ( A -h x ) .ih y ) = 0 ) )
18 7 14 17 sylanbrc 
 |-  ( ( ph /\ ( x e. H /\ A. z e. H ( normh ` ( A -h x ) ) <_ ( normh ` ( A -h z ) ) ) ) -> ( A -h x ) e. ( _|_ ` H ) )
19 hvpncan3 
 |-  ( ( x e. ~H /\ A e. ~H ) -> ( x +h ( A -h x ) ) = A )
20 5 3 19 syl2anc 
 |-  ( ( ph /\ ( x e. H /\ A. z e. H ( normh ` ( A -h x ) ) <_ ( normh ` ( A -h z ) ) ) ) -> ( x +h ( A -h x ) ) = A )
21 20 eqcomd 
 |-  ( ( ph /\ ( x e. H /\ A. z e. H ( normh ` ( A -h x ) ) <_ ( normh ` ( A -h z ) ) ) ) -> A = ( x +h ( A -h x ) ) )
22 oveq2 
 |-  ( y = ( A -h x ) -> ( x +h y ) = ( x +h ( A -h x ) ) )
23 22 rspceeqv 
 |-  ( ( ( A -h x ) e. ( _|_ ` H ) /\ A = ( x +h ( A -h x ) ) ) -> E. y e. ( _|_ ` H ) A = ( x +h y ) )
24 18 21 23 syl2anc 
 |-  ( ( ph /\ ( x e. H /\ A. z e. H ( normh ` ( A -h x ) ) <_ ( normh ` ( A -h z ) ) ) ) -> E. y e. ( _|_ ` H ) A = ( x +h y ) )
25 df-hba 
 |-  ~H = ( BaseSet ` <. <. +h , .h >. , normh >. )
26 eqid 
 |-  <. <. +h , .h >. , normh >. = <. <. +h , .h >. , normh >.
27 26 hhvs 
 |-  -h = ( -v ` <. <. +h , .h >. , normh >. )
28 26 hhnm 
 |-  normh = ( normCV ` <. <. +h , .h >. , normh >. )
29 eqid 
 |-  <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >. = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >.
30 29 15 hhssba 
 |-  H = ( BaseSet ` <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >. )
31 26 hhph 
 |-  <. <. +h , .h >. , normh >. e. CPreHilOLD
32 31 a1i 
 |-  ( ph -> <. <. +h , .h >. , normh >. e. CPreHilOLD )
33 26 29 hhsst 
 |-  ( H e. SH -> <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >. e. ( SubSp ` <. <. +h , .h >. , normh >. ) )
34 15 33 ax-mp 
 |-  <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >. e. ( SubSp ` <. <. +h , .h >. , normh >. )
35 29 1 hhssbnOLD 
 |-  <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >. e. CBan
36 elin 
 |-  ( <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >. e. ( ( SubSp ` <. <. +h , .h >. , normh >. ) i^i CBan ) <-> ( <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >. e. ( SubSp ` <. <. +h , .h >. , normh >. ) /\ <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >. e. CBan ) )
37 34 35 36 mpbir2an 
 |-  <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >. e. ( ( SubSp ` <. <. +h , .h >. , normh >. ) i^i CBan )
38 37 a1i 
 |-  ( ph -> <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >. e. ( ( SubSp ` <. <. +h , .h >. , normh >. ) i^i CBan ) )
39 25 27 28 30 32 38 2 minveco 
 |-  ( ph -> E! x e. H A. z e. H ( normh ` ( A -h x ) ) <_ ( normh ` ( A -h z ) ) )
40 reurex 
 |-  ( E! x e. H A. z e. H ( normh ` ( A -h x ) ) <_ ( normh ` ( A -h z ) ) -> E. x e. H A. z e. H ( normh ` ( A -h x ) ) <_ ( normh ` ( A -h z ) ) )
41 39 40 syl 
 |-  ( ph -> E. x e. H A. z e. H ( normh ` ( A -h x ) ) <_ ( normh ` ( A -h z ) ) )
42 24 41 reximddv 
 |-  ( ph -> E. x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) )