Metamath Proof Explorer

Theorem cdj1i

Description: Two ways to express " A and B are completely disjoint subspaces." (1) => (2) in Lemma 5 of Holland p. 1520. (Contributed by NM, 21-May-2005) (New usage is discouraged.)

Ref Expression
Hypotheses cdj1.1 
|- A e. SH
cdj1.2 
|- B e. SH
Assertion cdj1i 
|- ( E. w e. RR ( 0 < w /\ A. y e. A A. v e. B ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) ) -> E. x e. RR ( 0 < x /\ A. y e. A A. z e. B ( ( normh ` y ) = 1 -> x <_ ( normh ` ( y -h z ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cdj1.1 
 |-  A e. SH
2 cdj1.2 
 |-  B e. SH
3 gt0ne0 
 |-  ( ( w e. RR /\ 0 < w ) -> w =/= 0 )
4 rereccl 
 |-  ( ( w e. RR /\ w =/= 0 ) -> ( 1 / w ) e. RR )
5 3 4 syldan 
 |-  ( ( w e. RR /\ 0 < w ) -> ( 1 / w ) e. RR )
6 5 adantrr 
 |-  ( ( w e. RR /\ ( 0 < w /\ A. y e. A A. v e. B ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) ) ) -> ( 1 / w ) e. RR )
7 recgt0 
 |-  ( ( w e. RR /\ 0 < w ) -> 0 < ( 1 / w ) )
8 7 adantrr 
 |-  ( ( w e. RR /\ ( 0 < w /\ A. y e. A A. v e. B ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) ) ) -> 0 < ( 1 / w ) )
9 1red 
 |-  ( ( ( ( w e. RR /\ y e. A ) /\ z e. B ) /\ ( A. v e. B ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) /\ ( normh ` y ) = 1 ) ) -> 1 e. RR )
10 1re 
 |-  1 e. RR
11 neg1cn 
 |-  -u 1 e. CC
12 2 sheli 
 |-  ( z e. B -> z e. ~H )
13 hvmulcl 
 |-  ( ( -u 1 e. CC /\ z e. ~H ) -> ( -u 1 .h z ) e. ~H )
14 11 12 13 sylancr 
 |-  ( z e. B -> ( -u 1 .h z ) e. ~H )
15 normcl 
 |-  ( ( -u 1 .h z ) e. ~H -> ( normh ` ( -u 1 .h z ) ) e. RR )
16 14 15 syl 
 |-  ( z e. B -> ( normh ` ( -u 1 .h z ) ) e. RR )
17 16 adantl 
 |-  ( ( ( w e. RR /\ y e. A ) /\ z e. B ) -> ( normh ` ( -u 1 .h z ) ) e. RR )
18 readdcl 
 |-  ( ( 1 e. RR /\ ( normh ` ( -u 1 .h z ) ) e. RR ) -> ( 1 + ( normh ` ( -u 1 .h z ) ) ) e. RR )
19 10 17 18 sylancr 
 |-  ( ( ( w e. RR /\ y e. A ) /\ z e. B ) -> ( 1 + ( normh ` ( -u 1 .h z ) ) ) e. RR )
20 19 adantr 
 |-  ( ( ( ( w e. RR /\ y e. A ) /\ z e. B ) /\ ( A. v e. B ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) /\ ( normh ` y ) = 1 ) ) -> ( 1 + ( normh ` ( -u 1 .h z ) ) ) e. RR )
21 1 sheli 
 |-  ( y e. A -> y e. ~H )
22 hvsubcl 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( y -h z ) e. ~H )
23 21 12 22 syl2an 
 |-  ( ( y e. A /\ z e. B ) -> ( y -h z ) e. ~H )
24 normcl 
 |-  ( ( y -h z ) e. ~H -> ( normh ` ( y -h z ) ) e. RR )
25 23 24 syl 
 |-  ( ( y e. A /\ z e. B ) -> ( normh ` ( y -h z ) ) e. RR )
26 remulcl 
 |-  ( ( w e. RR /\ ( normh ` ( y -h z ) ) e. RR ) -> ( w x. ( normh ` ( y -h z ) ) ) e. RR )
27 25 26 sylan2 
 |-  ( ( w e. RR /\ ( y e. A /\ z e. B ) ) -> ( w x. ( normh ` ( y -h z ) ) ) e. RR )
28 27 anassrs 
 |-  ( ( ( w e. RR /\ y e. A ) /\ z e. B ) -> ( w x. ( normh ` ( y -h z ) ) ) e. RR )
29 28 adantr 
 |-  ( ( ( ( w e. RR /\ y e. A ) /\ z e. B ) /\ ( A. v e. B ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) /\ ( normh ` y ) = 1 ) ) -> ( w x. ( normh ` ( y -h z ) ) ) e. RR )
30 normge0 
 |-  ( ( -u 1 .h z ) e. ~H -> 0 <_ ( normh ` ( -u 1 .h z ) ) )
31 14 30 syl 
 |-  ( z e. B -> 0 <_ ( normh ` ( -u 1 .h z ) ) )
32 addge01 
 |-  ( ( 1 e. RR /\ ( normh ` ( -u 1 .h z ) ) e. RR ) -> ( 0 <_ ( normh ` ( -u 1 .h z ) ) <-> 1 <_ ( 1 + ( normh ` ( -u 1 .h z ) ) ) ) )
33 10 32 mpan 
 |-  ( ( normh ` ( -u 1 .h z ) ) e. RR -> ( 0 <_ ( normh ` ( -u 1 .h z ) ) <-> 1 <_ ( 1 + ( normh ` ( -u 1 .h z ) ) ) ) )
34 33 biimpa 
 |-  ( ( ( normh ` ( -u 1 .h z ) ) e. RR /\ 0 <_ ( normh ` ( -u 1 .h z ) ) ) -> 1 <_ ( 1 + ( normh ` ( -u 1 .h z ) ) ) )
35 16 31 34 syl2anc 
 |-  ( z e. B -> 1 <_ ( 1 + ( normh ` ( -u 1 .h z ) ) ) )
36 35 ad2antlr 
 |-  ( ( ( ( w e. RR /\ y e. A ) /\ z e. B ) /\ ( A. v e. B ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) /\ ( normh ` y ) = 1 ) ) -> 1 <_ ( 1 + ( normh ` ( -u 1 .h z ) ) ) )
37 shmulcl 
 |-  ( ( B e. SH /\ -u 1 e. CC /\ z e. B ) -> ( -u 1 .h z ) e. B )
38 2 11 37 mp3an12 
 |-  ( z e. B -> ( -u 1 .h z ) e. B )
39 fveq2 
 |-  ( v = ( -u 1 .h z ) -> ( normh ` v ) = ( normh ` ( -u 1 .h z ) ) )
40 39 oveq2d 
 |-  ( v = ( -u 1 .h z ) -> ( ( normh ` y ) + ( normh ` v ) ) = ( ( normh ` y ) + ( normh ` ( -u 1 .h z ) ) ) )
41 oveq2 
 |-  ( v = ( -u 1 .h z ) -> ( y +h v ) = ( y +h ( -u 1 .h z ) ) )
42 41 fveq2d 
 |-  ( v = ( -u 1 .h z ) -> ( normh ` ( y +h v ) ) = ( normh ` ( y +h ( -u 1 .h z ) ) ) )
43 42 oveq2d 
 |-  ( v = ( -u 1 .h z ) -> ( w x. ( normh ` ( y +h v ) ) ) = ( w x. ( normh ` ( y +h ( -u 1 .h z ) ) ) ) )
44 40 43 breq12d 
 |-  ( v = ( -u 1 .h z ) -> ( ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) <-> ( ( normh ` y ) + ( normh ` ( -u 1 .h z ) ) ) <_ ( w x. ( normh ` ( y +h ( -u 1 .h z ) ) ) ) ) )
45 44 rspcv 
 |-  ( ( -u 1 .h z ) e. B -> ( A. v e. B ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) -> ( ( normh ` y ) + ( normh ` ( -u 1 .h z ) ) ) <_ ( w x. ( normh ` ( y +h ( -u 1 .h z ) ) ) ) ) )
46 38 45 syl 
 |-  ( z e. B -> ( A. v e. B ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) -> ( ( normh ` y ) + ( normh ` ( -u 1 .h z ) ) ) <_ ( w x. ( normh ` ( y +h ( -u 1 .h z ) ) ) ) ) )
47 46 imp 
 |-  ( ( z e. B /\ A. v e. B ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) ) -> ( ( normh ` y ) + ( normh ` ( -u 1 .h z ) ) ) <_ ( w x. ( normh ` ( y +h ( -u 1 .h z ) ) ) ) )
48 47 ad2ant2lr 
 |-  ( ( ( ( w e. RR /\ y e. A ) /\ z e. B ) /\ ( A. v e. B ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) /\ ( normh ` y ) = 1 ) ) -> ( ( normh ` y ) + ( normh ` ( -u 1 .h z ) ) ) <_ ( w x. ( normh ` ( y +h ( -u 1 .h z ) ) ) ) )
49 oveq1 
 |-  ( 1 = ( normh ` y ) -> ( 1 + ( normh ` ( -u 1 .h z ) ) ) = ( ( normh ` y ) + ( normh ` ( -u 1 .h z ) ) ) )
50 49 eqcoms 
 |-  ( ( normh ` y ) = 1 -> ( 1 + ( normh ` ( -u 1 .h z ) ) ) = ( ( normh ` y ) + ( normh ` ( -u 1 .h z ) ) ) )
51 50 ad2antll 
 |-  ( ( ( ( w e. RR /\ y e. A ) /\ z e. B ) /\ ( A. v e. B ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) /\ ( normh ` y ) = 1 ) ) -> ( 1 + ( normh ` ( -u 1 .h z ) ) ) = ( ( normh ` y ) + ( normh ` ( -u 1 .h z ) ) ) )
52 hvsubval 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( y -h z ) = ( y +h ( -u 1 .h z ) ) )
53 21 12 52 syl2an 
 |-  ( ( y e. A /\ z e. B ) -> ( y -h z ) = ( y +h ( -u 1 .h z ) ) )
54 53 fveq2d 
 |-  ( ( y e. A /\ z e. B ) -> ( normh ` ( y -h z ) ) = ( normh ` ( y +h ( -u 1 .h z ) ) ) )
55 54 oveq2d 
 |-  ( ( y e. A /\ z e. B ) -> ( w x. ( normh ` ( y -h z ) ) ) = ( w x. ( normh ` ( y +h ( -u 1 .h z ) ) ) ) )
56 55 adantll 
 |-  ( ( ( w e. RR /\ y e. A ) /\ z e. B ) -> ( w x. ( normh ` ( y -h z ) ) ) = ( w x. ( normh ` ( y +h ( -u 1 .h z ) ) ) ) )
57 56 adantr 
 |-  ( ( ( ( w e. RR /\ y e. A ) /\ z e. B ) /\ ( A. v e. B ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) /\ ( normh ` y ) = 1 ) ) -> ( w x. ( normh ` ( y -h z ) ) ) = ( w x. ( normh ` ( y +h ( -u 1 .h z ) ) ) ) )
58 48 51 57 3brtr4d 
 |-  ( ( ( ( w e. RR /\ y e. A ) /\ z e. B ) /\ ( A. v e. B ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) /\ ( normh ` y ) = 1 ) ) -> ( 1 + ( normh ` ( -u 1 .h z ) ) ) <_ ( w x. ( normh ` ( y -h z ) ) ) )
59 9 20 29 36 58 letrd 
 |-  ( ( ( ( w e. RR /\ y e. A ) /\ z e. B ) /\ ( A. v e. B ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) /\ ( normh ` y ) = 1 ) ) -> 1 <_ ( w x. ( normh ` ( y -h z ) ) ) )
60 59 ex 
 |-  ( ( ( w e. RR /\ y e. A ) /\ z e. B ) -> ( ( A. v e. B ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) /\ ( normh ` y ) = 1 ) -> 1 <_ ( w x. ( normh ` ( y -h z ) ) ) ) )
61 60 adantllr 
 |-  ( ( ( ( w e. RR /\ 0 < w ) /\ y e. A ) /\ z e. B ) -> ( ( A. v e. B ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) /\ ( normh ` y ) = 1 ) -> 1 <_ ( w x. ( normh ` ( y -h z ) ) ) ) )
62 simplll 
 |-  ( ( ( ( w e. RR /\ 0 < w ) /\ y e. A ) /\ z e. B ) -> w e. RR )
63 23 adantll 
 |-  ( ( ( ( w e. RR /\ 0 < w ) /\ y e. A ) /\ z e. B ) -> ( y -h z ) e. ~H )
64 63 24 syl 
 |-  ( ( ( ( w e. RR /\ 0 < w ) /\ y e. A ) /\ z e. B ) -> ( normh ` ( y -h z ) ) e. RR )
65 62 64 26 syl2anc 
 |-  ( ( ( ( w e. RR /\ 0 < w ) /\ y e. A ) /\ z e. B ) -> ( w x. ( normh ` ( y -h z ) ) ) e. RR )
66 simpllr 
 |-  ( ( ( ( w e. RR /\ 0 < w ) /\ y e. A ) /\ z e. B ) -> 0 < w )
67 lediv1 
 |-  ( ( 1 e. RR /\ ( w x. ( normh ` ( y -h z ) ) ) e. RR /\ ( w e. RR /\ 0 < w ) ) -> ( 1 <_ ( w x. ( normh ` ( y -h z ) ) ) <-> ( 1 / w ) <_ ( ( w x. ( normh ` ( y -h z ) ) ) / w ) ) )
68 10 67 mp3an1 
 |-  ( ( ( w x. ( normh ` ( y -h z ) ) ) e. RR /\ ( w e. RR /\ 0 < w ) ) -> ( 1 <_ ( w x. ( normh ` ( y -h z ) ) ) <-> ( 1 / w ) <_ ( ( w x. ( normh ` ( y -h z ) ) ) / w ) ) )
69 65 62 66 68 syl12anc 
 |-  ( ( ( ( w e. RR /\ 0 < w ) /\ y e. A ) /\ z e. B ) -> ( 1 <_ ( w x. ( normh ` ( y -h z ) ) ) <-> ( 1 / w ) <_ ( ( w x. ( normh ` ( y -h z ) ) ) / w ) ) )
70 61 69 sylibd 
 |-  ( ( ( ( w e. RR /\ 0 < w ) /\ y e. A ) /\ z e. B ) -> ( ( A. v e. B ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) /\ ( normh ` y ) = 1 ) -> ( 1 / w ) <_ ( ( w x. ( normh ` ( y -h z ) ) ) / w ) ) )
71 70 imp 
 |-  ( ( ( ( ( w e. RR /\ 0 < w ) /\ y e. A ) /\ z e. B ) /\ ( A. v e. B ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) /\ ( normh ` y ) = 1 ) ) -> ( 1 / w ) <_ ( ( w x. ( normh ` ( y -h z ) ) ) / w ) )
72 25 recnd 
 |-  ( ( y e. A /\ z e. B ) -> ( normh ` ( y -h z ) ) e. CC )
73 72 adantll 
 |-  ( ( ( ( w e. RR /\ 0 < w ) /\ y e. A ) /\ z e. B ) -> ( normh ` ( y -h z ) ) e. CC )
74 recn 
 |-  ( w e. RR -> w e. CC )
75 74 ad3antrrr 
 |-  ( ( ( ( w e. RR /\ 0 < w ) /\ y e. A ) /\ z e. B ) -> w e. CC )
76 3 ad2antrr 
 |-  ( ( ( ( w e. RR /\ 0 < w ) /\ y e. A ) /\ z e. B ) -> w =/= 0 )
77 73 75 76 divcan3d 
 |-  ( ( ( ( w e. RR /\ 0 < w ) /\ y e. A ) /\ z e. B ) -> ( ( w x. ( normh ` ( y -h z ) ) ) / w ) = ( normh ` ( y -h z ) ) )
78 77 adantr 
 |-  ( ( ( ( ( w e. RR /\ 0 < w ) /\ y e. A ) /\ z e. B ) /\ ( A. v e. B ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) /\ ( normh ` y ) = 1 ) ) -> ( ( w x. ( normh ` ( y -h z ) ) ) / w ) = ( normh ` ( y -h z ) ) )
79 71 78 breqtrd 
 |-  ( ( ( ( ( w e. RR /\ 0 < w ) /\ y e. A ) /\ z e. B ) /\ ( A. v e. B ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) /\ ( normh ` y ) = 1 ) ) -> ( 1 / w ) <_ ( normh ` ( y -h z ) ) )
80 79 exp43 
 |-  ( ( ( w e. RR /\ 0 < w ) /\ y e. A ) -> ( z e. B -> ( A. v e. B ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) -> ( ( normh ` y ) = 1 -> ( 1 / w ) <_ ( normh ` ( y -h z ) ) ) ) ) )
81 80 com23 
 |-  ( ( ( w e. RR /\ 0 < w ) /\ y e. A ) -> ( A. v e. B ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) -> ( z e. B -> ( ( normh ` y ) = 1 -> ( 1 / w ) <_ ( normh ` ( y -h z ) ) ) ) ) )
82 81 ralrimdv 
 |-  ( ( ( w e. RR /\ 0 < w ) /\ y e. A ) -> ( A. v e. B ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) -> A. z e. B ( ( normh ` y ) = 1 -> ( 1 / w ) <_ ( normh ` ( y -h z ) ) ) ) )
83 82 ralimdva 
 |-  ( ( w e. RR /\ 0 < w ) -> ( A. y e. A A. v e. B ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) -> A. y e. A A. z e. B ( ( normh ` y ) = 1 -> ( 1 / w ) <_ ( normh ` ( y -h z ) ) ) ) )
84 83 impr 
 |-  ( ( w e. RR /\ ( 0 < w /\ A. y e. A A. v e. B ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) ) ) -> A. y e. A A. z e. B ( ( normh ` y ) = 1 -> ( 1 / w ) <_ ( normh ` ( y -h z ) ) ) )
85 6 8 84 jca32 
 |-  ( ( w e. RR /\ ( 0 < w /\ A. y e. A A. v e. B ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) ) ) -> ( ( 1 / w ) e. RR /\ ( 0 < ( 1 / w ) /\ A. y e. A A. z e. B ( ( normh ` y ) = 1 -> ( 1 / w ) <_ ( normh ` ( y -h z ) ) ) ) ) )
86 85 ex 
 |-  ( w e. RR -> ( ( 0 < w /\ A. y e. A A. v e. B ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) ) -> ( ( 1 / w ) e. RR /\ ( 0 < ( 1 / w ) /\ A. y e. A A. z e. B ( ( normh ` y ) = 1 -> ( 1 / w ) <_ ( normh ` ( y -h z ) ) ) ) ) ) )
87 breq2 
 |-  ( x = ( 1 / w ) -> ( 0 < x <-> 0 < ( 1 / w ) ) )
88 breq1 
 |-  ( x = ( 1 / w ) -> ( x <_ ( normh ` ( y -h z ) ) <-> ( 1 / w ) <_ ( normh ` ( y -h z ) ) ) )
89 88 imbi2d 
 |-  ( x = ( 1 / w ) -> ( ( ( normh ` y ) = 1 -> x <_ ( normh ` ( y -h z ) ) ) <-> ( ( normh ` y ) = 1 -> ( 1 / w ) <_ ( normh ` ( y -h z ) ) ) ) )
90 89 2ralbidv 
 |-  ( x = ( 1 / w ) -> ( A. y e. A A. z e. B ( ( normh ` y ) = 1 -> x <_ ( normh ` ( y -h z ) ) ) <-> A. y e. A A. z e. B ( ( normh ` y ) = 1 -> ( 1 / w ) <_ ( normh ` ( y -h z ) ) ) ) )
91 87 90 anbi12d 
 |-  ( x = ( 1 / w ) -> ( ( 0 < x /\ A. y e. A A. z e. B ( ( normh ` y ) = 1 -> x <_ ( normh ` ( y -h z ) ) ) ) <-> ( 0 < ( 1 / w ) /\ A. y e. A A. z e. B ( ( normh ` y ) = 1 -> ( 1 / w ) <_ ( normh ` ( y -h z ) ) ) ) ) )
92 91 rspcev 
 |-  ( ( ( 1 / w ) e. RR /\ ( 0 < ( 1 / w ) /\ A. y e. A A. z e. B ( ( normh ` y ) = 1 -> ( 1 / w ) <_ ( normh ` ( y -h z ) ) ) ) ) -> E. x e. RR ( 0 < x /\ A. y e. A A. z e. B ( ( normh ` y ) = 1 -> x <_ ( normh ` ( y -h z ) ) ) ) )
93 86 92 syl6 
 |-  ( w e. RR -> ( ( 0 < w /\ A. y e. A A. v e. B ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) ) -> E. x e. RR ( 0 < x /\ A. y e. A A. z e. B ( ( normh ` y ) = 1 -> x <_ ( normh ` ( y -h z ) ) ) ) ) )
94 93 rexlimiv 
 |-  ( E. w e. RR ( 0 < w /\ A. y e. A A. v e. B ( ( normh ` y ) + ( normh ` v ) ) <_ ( w x. ( normh ` ( y +h v ) ) ) ) -> E. x e. RR ( 0 < x /\ A. y e. A A. z e. B ( ( normh ` y ) = 1 -> x <_ ( normh ` ( y -h z ) ) ) ) )