Metamath Proof Explorer

Theorem cdj3lem3b

Description: Lemma for cdj3i . The second-component function T is bounded if the subspaces are completely disjoint. (Contributed by NM, 31-May-2005) (New usage is discouraged.)

Ref Expression
Hypotheses cdj3lem2.1 
|- A e. SH
cdj3lem2.2 
|- B e. SH
cdj3lem3.3 
|- T = ( x e. ( A +H B ) |-> ( iota_ w e. B E. z e. A x = ( z +h w ) ) )
Assertion cdj3lem3b 
|- ( E. v e. RR ( 0 < v /\ A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) ) -> E. v e. RR ( 0 < v /\ A. u e. ( A +H B ) ( normh ` ( T ` u ) ) <_ ( v x. ( normh ` u ) ) ) )

Proof

Step Hyp Ref Expression
1 cdj3lem2.1 
 |-  A e. SH
2 cdj3lem2.2 
 |-  B e. SH
3 cdj3lem3.3 
 |-  T = ( x e. ( A +H B ) |-> ( iota_ w e. B E. z e. A x = ( z +h w ) ) )
4 2 1 shscomi 
 |-  ( B +H A ) = ( A +H B )
5 2 sheli 
 |-  ( w e. B -> w e. ~H )
6 1 sheli 
 |-  ( z e. A -> z e. ~H )
7 ax-hvcom 
 |-  ( ( w e. ~H /\ z e. ~H ) -> ( w +h z ) = ( z +h w ) )
8 5 6 7 syl2an 
 |-  ( ( w e. B /\ z e. A ) -> ( w +h z ) = ( z +h w ) )
9 8 eqeq2d 
 |-  ( ( w e. B /\ z e. A ) -> ( x = ( w +h z ) <-> x = ( z +h w ) ) )
10 9 rexbidva 
 |-  ( w e. B -> ( E. z e. A x = ( w +h z ) <-> E. z e. A x = ( z +h w ) ) )
11 10 riotabiia 
 |-  ( iota_ w e. B E. z e. A x = ( w +h z ) ) = ( iota_ w e. B E. z e. A x = ( z +h w ) )
12 4 11 mpteq12i 
 |-  ( x e. ( B +H A ) |-> ( iota_ w e. B E. z e. A x = ( w +h z ) ) ) = ( x e. ( A +H B ) |-> ( iota_ w e. B E. z e. A x = ( z +h w ) ) )
13 3 12 eqtr4i 
 |-  T = ( x e. ( B +H A ) |-> ( iota_ w e. B E. z e. A x = ( w +h z ) ) )
14 2 1 13 cdj3lem2b 
 |-  ( E. v e. RR ( 0 < v /\ A. x e. B A. y e. A ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) ) -> E. v e. RR ( 0 < v /\ A. u e. ( B +H A ) ( normh ` ( T ` u ) ) <_ ( v x. ( normh ` u ) ) ) )
15 fveq2 
 |-  ( x = t -> ( normh ` x ) = ( normh ` t ) )
16 15 oveq1d 
 |-  ( x = t -> ( ( normh ` x ) + ( normh ` y ) ) = ( ( normh ` t ) + ( normh ` y ) ) )
17 fvoveq1 
 |-  ( x = t -> ( normh ` ( x +h y ) ) = ( normh ` ( t +h y ) ) )
18 17 oveq2d 
 |-  ( x = t -> ( v x. ( normh ` ( x +h y ) ) ) = ( v x. ( normh ` ( t +h y ) ) ) )
19 16 18 breq12d 
 |-  ( x = t -> ( ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) <-> ( ( normh ` t ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( t +h y ) ) ) ) )
20 fveq2 
 |-  ( y = h -> ( normh ` y ) = ( normh ` h ) )
21 20 oveq2d 
 |-  ( y = h -> ( ( normh ` t ) + ( normh ` y ) ) = ( ( normh ` t ) + ( normh ` h ) ) )
22 oveq2 
 |-  ( y = h -> ( t +h y ) = ( t +h h ) )
23 22 fveq2d 
 |-  ( y = h -> ( normh ` ( t +h y ) ) = ( normh ` ( t +h h ) ) )
24 23 oveq2d 
 |-  ( y = h -> ( v x. ( normh ` ( t +h y ) ) ) = ( v x. ( normh ` ( t +h h ) ) ) )
25 21 24 breq12d 
 |-  ( y = h -> ( ( ( normh ` t ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( t +h y ) ) ) <-> ( ( normh ` t ) + ( normh ` h ) ) <_ ( v x. ( normh ` ( t +h h ) ) ) ) )
26 19 25 cbvral2vw 
 |-  ( A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) <-> A. t e. A A. h e. B ( ( normh ` t ) + ( normh ` h ) ) <_ ( v x. ( normh ` ( t +h h ) ) ) )
27 ralcom 
 |-  ( A. t e. A A. h e. B ( ( normh ` t ) + ( normh ` h ) ) <_ ( v x. ( normh ` ( t +h h ) ) ) <-> A. h e. B A. t e. A ( ( normh ` t ) + ( normh ` h ) ) <_ ( v x. ( normh ` ( t +h h ) ) ) )
28 2 sheli 
 |-  ( x e. B -> x e. ~H )
29 normcl 
 |-  ( x e. ~H -> ( normh ` x ) e. RR )
30 28 29 syl 
 |-  ( x e. B -> ( normh ` x ) e. RR )
31 30 recnd 
 |-  ( x e. B -> ( normh ` x ) e. CC )
32 1 sheli 
 |-  ( y e. A -> y e. ~H )
33 normcl 
 |-  ( y e. ~H -> ( normh ` y ) e. RR )
34 32 33 syl 
 |-  ( y e. A -> ( normh ` y ) e. RR )
35 34 recnd 
 |-  ( y e. A -> ( normh ` y ) e. CC )
36 addcom 
 |-  ( ( ( normh ` x ) e. CC /\ ( normh ` y ) e. CC ) -> ( ( normh ` x ) + ( normh ` y ) ) = ( ( normh ` y ) + ( normh ` x ) ) )
37 31 35 36 syl2an 
 |-  ( ( x e. B /\ y e. A ) -> ( ( normh ` x ) + ( normh ` y ) ) = ( ( normh ` y ) + ( normh ` x ) ) )
38 ax-hvcom 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( x +h y ) = ( y +h x ) )
39 28 32 38 syl2an 
 |-  ( ( x e. B /\ y e. A ) -> ( x +h y ) = ( y +h x ) )
40 39 fveq2d 
 |-  ( ( x e. B /\ y e. A ) -> ( normh ` ( x +h y ) ) = ( normh ` ( y +h x ) ) )
41 40 oveq2d 
 |-  ( ( x e. B /\ y e. A ) -> ( v x. ( normh ` ( x +h y ) ) ) = ( v x. ( normh ` ( y +h x ) ) ) )
42 37 41 breq12d 
 |-  ( ( x e. B /\ y e. A ) -> ( ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) <-> ( ( normh ` y ) + ( normh ` x ) ) <_ ( v x. ( normh ` ( y +h x ) ) ) ) )
43 42 ralbidva 
 |-  ( x e. B -> ( A. y e. A ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) <-> A. y e. A ( ( normh ` y ) + ( normh ` x ) ) <_ ( v x. ( normh ` ( y +h x ) ) ) ) )
44 43 ralbiia 
 |-  ( A. x e. B A. y e. A ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) <-> A. x e. B A. y e. A ( ( normh ` y ) + ( normh ` x ) ) <_ ( v x. ( normh ` ( y +h x ) ) ) )
45 fveq2 
 |-  ( x = h -> ( normh ` x ) = ( normh ` h ) )
46 45 oveq2d 
 |-  ( x = h -> ( ( normh ` y ) + ( normh ` x ) ) = ( ( normh ` y ) + ( normh ` h ) ) )
47 oveq2 
 |-  ( x = h -> ( y +h x ) = ( y +h h ) )
48 47 fveq2d 
 |-  ( x = h -> ( normh ` ( y +h x ) ) = ( normh ` ( y +h h ) ) )
49 48 oveq2d 
 |-  ( x = h -> ( v x. ( normh ` ( y +h x ) ) ) = ( v x. ( normh ` ( y +h h ) ) ) )
50 46 49 breq12d 
 |-  ( x = h -> ( ( ( normh ` y ) + ( normh ` x ) ) <_ ( v x. ( normh ` ( y +h x ) ) ) <-> ( ( normh ` y ) + ( normh ` h ) ) <_ ( v x. ( normh ` ( y +h h ) ) ) ) )
51 fveq2 
 |-  ( y = t -> ( normh ` y ) = ( normh ` t ) )
52 51 oveq1d 
 |-  ( y = t -> ( ( normh ` y ) + ( normh ` h ) ) = ( ( normh ` t ) + ( normh ` h ) ) )
53 fvoveq1 
 |-  ( y = t -> ( normh ` ( y +h h ) ) = ( normh ` ( t +h h ) ) )
54 53 oveq2d 
 |-  ( y = t -> ( v x. ( normh ` ( y +h h ) ) ) = ( v x. ( normh ` ( t +h h ) ) ) )
55 52 54 breq12d 
 |-  ( y = t -> ( ( ( normh ` y ) + ( normh ` h ) ) <_ ( v x. ( normh ` ( y +h h ) ) ) <-> ( ( normh ` t ) + ( normh ` h ) ) <_ ( v x. ( normh ` ( t +h h ) ) ) ) )
56 50 55 cbvral2vw 
 |-  ( A. x e. B A. y e. A ( ( normh ` y ) + ( normh ` x ) ) <_ ( v x. ( normh ` ( y +h x ) ) ) <-> A. h e. B A. t e. A ( ( normh ` t ) + ( normh ` h ) ) <_ ( v x. ( normh ` ( t +h h ) ) ) )
57 44 56 bitr2i 
 |-  ( A. h e. B A. t e. A ( ( normh ` t ) + ( normh ` h ) ) <_ ( v x. ( normh ` ( t +h h ) ) ) <-> A. x e. B A. y e. A ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) )
58 26 27 57 3bitri 
 |-  ( A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) <-> A. x e. B A. y e. A ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) )
59 58 anbi2i 
 |-  ( ( 0 < v /\ A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) ) <-> ( 0 < v /\ A. x e. B A. y e. A ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) ) )
60 59 rexbii 
 |-  ( E. v e. RR ( 0 < v /\ A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) ) <-> E. v e. RR ( 0 < v /\ A. x e. B A. y e. A ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) ) )
61 1 2 shscomi 
 |-  ( A +H B ) = ( B +H A )
62 61 raleqi 
 |-  ( A. u e. ( A +H B ) ( normh ` ( T ` u ) ) <_ ( v x. ( normh ` u ) ) <-> A. u e. ( B +H A ) ( normh ` ( T ` u ) ) <_ ( v x. ( normh ` u ) ) )
63 62 anbi2i 
 |-  ( ( 0 < v /\ A. u e. ( A +H B ) ( normh ` ( T ` u ) ) <_ ( v x. ( normh ` u ) ) ) <-> ( 0 < v /\ A. u e. ( B +H A ) ( normh ` ( T ` u ) ) <_ ( v x. ( normh ` u ) ) ) )
64 63 rexbii 
 |-  ( E. v e. RR ( 0 < v /\ A. u e. ( A +H B ) ( normh ` ( T ` u ) ) <_ ( v x. ( normh ` u ) ) ) <-> E. v e. RR ( 0 < v /\ A. u e. ( B +H A ) ( normh ` ( T ` u ) ) <_ ( v x. ( normh ` u ) ) ) )
65 14 60 64 3imtr4i 
 |-  ( E. v e. RR ( 0 < v /\ A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) ) -> E. v e. RR ( 0 < v /\ A. u e. ( A +H B ) ( normh ` ( T ` u ) ) <_ ( v x. ( normh ` u ) ) ) )