Metamath Proof Explorer

Theorem cdj3i

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

Ref Expression
Hypotheses cdj3.1 
|- A e. SH
cdj3.2 
|- B e. SH
cdj3.3 
|- S = ( x e. ( A +H B ) |-> ( iota_ z e. A E. w e. B x = ( z +h w ) ) )
cdj3.4 
|- T = ( x e. ( A +H B ) |-> ( iota_ w e. B E. z e. A x = ( z +h w ) ) )
cdj3.5 
|- ( ph <-> E. v e. RR ( 0 < v /\ A. u e. ( A +H B ) ( normh ` ( S ` u ) ) <_ ( v x. ( normh ` u ) ) ) )
cdj3.6 
|- ( ps <-> E. v e. RR ( 0 < v /\ A. u e. ( A +H B ) ( normh ` ( T ` u ) ) <_ ( v x. ( normh ` u ) ) ) )
Assertion cdj3i 
|- ( E. v e. RR ( 0 < v /\ A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) ) <-> ( ( A i^i B ) = 0H /\ ph /\ ps ) )

Proof

Step Hyp Ref Expression
1 cdj3.1 
 |-  A e. SH
2 cdj3.2 
 |-  B e. SH
3 cdj3.3 
 |-  S = ( x e. ( A +H B ) |-> ( iota_ z e. A E. w e. B x = ( z +h w ) ) )
4 cdj3.4 
 |-  T = ( x e. ( A +H B ) |-> ( iota_ w e. B E. z e. A x = ( z +h w ) ) )
5 cdj3.5 
 |-  ( ph <-> E. v e. RR ( 0 < v /\ A. u e. ( A +H B ) ( normh ` ( S ` u ) ) <_ ( v x. ( normh ` u ) ) ) )
6 cdj3.6 
 |-  ( ps <-> E. v e. RR ( 0 < v /\ A. u e. ( A +H B ) ( normh ` ( T ` u ) ) <_ ( v x. ( normh ` u ) ) ) )
7 1 2 cdj3lem1 
 |-  ( E. v e. RR ( 0 < v /\ A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) ) -> ( A i^i B ) = 0H )
8 1 2 3 cdj3lem2b 
 |-  ( 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 ` ( S ` u ) ) <_ ( v x. ( normh ` u ) ) ) )
9 8 5 sylibr 
 |-  ( E. v e. RR ( 0 < v /\ A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) ) -> ph )
10 1 2 4 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 ) ) ) )
11 10 6 sylibr 
 |-  ( E. v e. RR ( 0 < v /\ A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) ) -> ps )
12 7 9 11 3jca 
 |-  ( E. v e. RR ( 0 < v /\ A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) ) -> ( ( A i^i B ) = 0H /\ ph /\ ps ) )
13 breq2 
 |-  ( v = f -> ( 0 < v <-> 0 < f ) )
14 oveq1 
 |-  ( v = f -> ( v x. ( normh ` u ) ) = ( f x. ( normh ` u ) ) )
15 14 breq2d 
 |-  ( v = f -> ( ( normh ` ( S ` u ) ) <_ ( v x. ( normh ` u ) ) <-> ( normh ` ( S ` u ) ) <_ ( f x. ( normh ` u ) ) ) )
16 15 ralbidv 
 |-  ( v = f -> ( A. u e. ( A +H B ) ( normh ` ( S ` u ) ) <_ ( v x. ( normh ` u ) ) <-> A. u e. ( A +H B ) ( normh ` ( S ` u ) ) <_ ( f x. ( normh ` u ) ) ) )
17 13 16 anbi12d 
 |-  ( v = f -> ( ( 0 < v /\ A. u e. ( A +H B ) ( normh ` ( S ` u ) ) <_ ( v x. ( normh ` u ) ) ) <-> ( 0 < f /\ A. u e. ( A +H B ) ( normh ` ( S ` u ) ) <_ ( f x. ( normh ` u ) ) ) ) )
18 17 cbvrexvw 
 |-  ( E. v e. RR ( 0 < v /\ A. u e. ( A +H B ) ( normh ` ( S ` u ) ) <_ ( v x. ( normh ` u ) ) ) <-> E. f e. RR ( 0 < f /\ A. u e. ( A +H B ) ( normh ` ( S ` u ) ) <_ ( f x. ( normh ` u ) ) ) )
19 5 18 bitri 
 |-  ( ph <-> E. f e. RR ( 0 < f /\ A. u e. ( A +H B ) ( normh ` ( S ` u ) ) <_ ( f x. ( normh ` u ) ) ) )
20 breq2 
 |-  ( v = g -> ( 0 < v <-> 0 < g ) )
21 oveq1 
 |-  ( v = g -> ( v x. ( normh ` u ) ) = ( g x. ( normh ` u ) ) )
22 21 breq2d 
 |-  ( v = g -> ( ( normh ` ( T ` u ) ) <_ ( v x. ( normh ` u ) ) <-> ( normh ` ( T ` u ) ) <_ ( g x. ( normh ` u ) ) ) )
23 22 ralbidv 
 |-  ( v = g -> ( A. u e. ( A +H B ) ( normh ` ( T ` u ) ) <_ ( v x. ( normh ` u ) ) <-> A. u e. ( A +H B ) ( normh ` ( T ` u ) ) <_ ( g x. ( normh ` u ) ) ) )
24 20 23 anbi12d 
 |-  ( v = g -> ( ( 0 < v /\ A. u e. ( A +H B ) ( normh ` ( T ` u ) ) <_ ( v x. ( normh ` u ) ) ) <-> ( 0 < g /\ A. u e. ( A +H B ) ( normh ` ( T ` u ) ) <_ ( g x. ( normh ` u ) ) ) ) )
25 24 cbvrexvw 
 |-  ( E. v e. RR ( 0 < v /\ A. u e. ( A +H B ) ( normh ` ( T ` u ) ) <_ ( v x. ( normh ` u ) ) ) <-> E. g e. RR ( 0 < g /\ A. u e. ( A +H B ) ( normh ` ( T ` u ) ) <_ ( g x. ( normh ` u ) ) ) )
26 6 25 bitri 
 |-  ( ps <-> E. g e. RR ( 0 < g /\ A. u e. ( A +H B ) ( normh ` ( T ` u ) ) <_ ( g x. ( normh ` u ) ) ) )
27 19 26 anbi12i 
 |-  ( ( ph /\ ps ) <-> ( E. f e. RR ( 0 < f /\ A. u e. ( A +H B ) ( normh ` ( S ` u ) ) <_ ( f x. ( normh ` u ) ) ) /\ E. g e. RR ( 0 < g /\ A. u e. ( A +H B ) ( normh ` ( T ` u ) ) <_ ( g x. ( normh ` u ) ) ) ) )
28 reeanv 
 |-  ( E. f e. RR E. g e. RR ( ( 0 < f /\ A. u e. ( A +H B ) ( normh ` ( S ` u ) ) <_ ( f x. ( normh ` u ) ) ) /\ ( 0 < g /\ A. u e. ( A +H B ) ( normh ` ( T ` u ) ) <_ ( g x. ( normh ` u ) ) ) ) <-> ( E. f e. RR ( 0 < f /\ A. u e. ( A +H B ) ( normh ` ( S ` u ) ) <_ ( f x. ( normh ` u ) ) ) /\ E. g e. RR ( 0 < g /\ A. u e. ( A +H B ) ( normh ` ( T ` u ) ) <_ ( g x. ( normh ` u ) ) ) ) )
29 27 28 bitr4i 
 |-  ( ( ph /\ ps ) <-> E. f e. RR E. g e. RR ( ( 0 < f /\ A. u e. ( A +H B ) ( normh ` ( S ` u ) ) <_ ( f x. ( normh ` u ) ) ) /\ ( 0 < g /\ A. u e. ( A +H B ) ( normh ` ( T ` u ) ) <_ ( g x. ( normh ` u ) ) ) ) )
30 an4 
 |-  ( ( ( 0 < f /\ A. u e. ( A +H B ) ( normh ` ( S ` u ) ) <_ ( f x. ( normh ` u ) ) ) /\ ( 0 < g /\ A. u e. ( A +H B ) ( normh ` ( T ` u ) ) <_ ( g x. ( normh ` u ) ) ) ) <-> ( ( 0 < f /\ 0 < g ) /\ ( A. u e. ( A +H B ) ( normh ` ( S ` u ) ) <_ ( f x. ( normh ` u ) ) /\ A. u e. ( A +H B ) ( normh ` ( T ` u ) ) <_ ( g x. ( normh ` u ) ) ) ) )
31 addgt0 
 |-  ( ( ( f e. RR /\ g e. RR ) /\ ( 0 < f /\ 0 < g ) ) -> 0 < ( f + g ) )
32 31 ex 
 |-  ( ( f e. RR /\ g e. RR ) -> ( ( 0 < f /\ 0 < g ) -> 0 < ( f + g ) ) )
33 32 adantl 
 |-  ( ( ( A i^i B ) = 0H /\ ( f e. RR /\ g e. RR ) ) -> ( ( 0 < f /\ 0 < g ) -> 0 < ( f + g ) ) )
34 1 2 shsvai 
 |-  ( ( t e. A /\ h e. B ) -> ( t +h h ) e. ( A +H B ) )
35 2fveq3 
 |-  ( u = ( t +h h ) -> ( normh ` ( S ` u ) ) = ( normh ` ( S ` ( t +h h ) ) ) )
36 fveq2 
 |-  ( u = ( t +h h ) -> ( normh ` u ) = ( normh ` ( t +h h ) ) )
37 36 oveq2d 
 |-  ( u = ( t +h h ) -> ( f x. ( normh ` u ) ) = ( f x. ( normh ` ( t +h h ) ) ) )
38 35 37 breq12d 
 |-  ( u = ( t +h h ) -> ( ( normh ` ( S ` u ) ) <_ ( f x. ( normh ` u ) ) <-> ( normh ` ( S ` ( t +h h ) ) ) <_ ( f x. ( normh ` ( t +h h ) ) ) ) )
39 38 rspcv 
 |-  ( ( t +h h ) e. ( A +H B ) -> ( A. u e. ( A +H B ) ( normh ` ( S ` u ) ) <_ ( f x. ( normh ` u ) ) -> ( normh ` ( S ` ( t +h h ) ) ) <_ ( f x. ( normh ` ( t +h h ) ) ) ) )
40 2fveq3 
 |-  ( u = ( t +h h ) -> ( normh ` ( T ` u ) ) = ( normh ` ( T ` ( t +h h ) ) ) )
41 36 oveq2d 
 |-  ( u = ( t +h h ) -> ( g x. ( normh ` u ) ) = ( g x. ( normh ` ( t +h h ) ) ) )
42 40 41 breq12d 
 |-  ( u = ( t +h h ) -> ( ( normh ` ( T ` u ) ) <_ ( g x. ( normh ` u ) ) <-> ( normh ` ( T ` ( t +h h ) ) ) <_ ( g x. ( normh ` ( t +h h ) ) ) ) )
43 42 rspcv 
 |-  ( ( t +h h ) e. ( A +H B ) -> ( A. u e. ( A +H B ) ( normh ` ( T ` u ) ) <_ ( g x. ( normh ` u ) ) -> ( normh ` ( T ` ( t +h h ) ) ) <_ ( g x. ( normh ` ( t +h h ) ) ) ) )
44 39 43 anim12d 
 |-  ( ( t +h h ) e. ( A +H B ) -> ( ( A. u e. ( A +H B ) ( normh ` ( S ` u ) ) <_ ( f x. ( normh ` u ) ) /\ A. u e. ( A +H B ) ( normh ` ( T ` u ) ) <_ ( g x. ( normh ` u ) ) ) -> ( ( normh ` ( S ` ( t +h h ) ) ) <_ ( f x. ( normh ` ( t +h h ) ) ) /\ ( normh ` ( T ` ( t +h h ) ) ) <_ ( g x. ( normh ` ( t +h h ) ) ) ) ) )
45 34 44 syl 
 |-  ( ( t e. A /\ h e. B ) -> ( ( A. u e. ( A +H B ) ( normh ` ( S ` u ) ) <_ ( f x. ( normh ` u ) ) /\ A. u e. ( A +H B ) ( normh ` ( T ` u ) ) <_ ( g x. ( normh ` u ) ) ) -> ( ( normh ` ( S ` ( t +h h ) ) ) <_ ( f x. ( normh ` ( t +h h ) ) ) /\ ( normh ` ( T ` ( t +h h ) ) ) <_ ( g x. ( normh ` ( t +h h ) ) ) ) ) )
46 45 adantl 
 |-  ( ( ( ( A i^i B ) = 0H /\ ( f e. RR /\ g e. RR ) ) /\ ( t e. A /\ h e. B ) ) -> ( ( A. u e. ( A +H B ) ( normh ` ( S ` u ) ) <_ ( f x. ( normh ` u ) ) /\ A. u e. ( A +H B ) ( normh ` ( T ` u ) ) <_ ( g x. ( normh ` u ) ) ) -> ( ( normh ` ( S ` ( t +h h ) ) ) <_ ( f x. ( normh ` ( t +h h ) ) ) /\ ( normh ` ( T ` ( t +h h ) ) ) <_ ( g x. ( normh ` ( t +h h ) ) ) ) ) )
47 1 sheli 
 |-  ( t e. A -> t e. ~H )
48 normcl 
 |-  ( t e. ~H -> ( normh ` t ) e. RR )
49 47 48 syl 
 |-  ( t e. A -> ( normh ` t ) e. RR )
50 2 sheli 
 |-  ( h e. B -> h e. ~H )
51 normcl 
 |-  ( h e. ~H -> ( normh ` h ) e. RR )
52 50 51 syl 
 |-  ( h e. B -> ( normh ` h ) e. RR )
53 49 52 anim12i 
 |-  ( ( t e. A /\ h e. B ) -> ( ( normh ` t ) e. RR /\ ( normh ` h ) e. RR ) )
54 53 adantl 
 |-  ( ( ( f e. RR /\ g e. RR ) /\ ( t e. A /\ h e. B ) ) -> ( ( normh ` t ) e. RR /\ ( normh ` h ) e. RR ) )
55 hvaddcl 
 |-  ( ( t e. ~H /\ h e. ~H ) -> ( t +h h ) e. ~H )
56 47 50 55 syl2an 
 |-  ( ( t e. A /\ h e. B ) -> ( t +h h ) e. ~H )
57 normcl 
 |-  ( ( t +h h ) e. ~H -> ( normh ` ( t +h h ) ) e. RR )
58 56 57 syl 
 |-  ( ( t e. A /\ h e. B ) -> ( normh ` ( t +h h ) ) e. RR )
59 remulcl 
 |-  ( ( f e. RR /\ ( normh ` ( t +h h ) ) e. RR ) -> ( f x. ( normh ` ( t +h h ) ) ) e. RR )
60 58 59 sylan2 
 |-  ( ( f e. RR /\ ( t e. A /\ h e. B ) ) -> ( f x. ( normh ` ( t +h h ) ) ) e. RR )
61 60 adantlr 
 |-  ( ( ( f e. RR /\ g e. RR ) /\ ( t e. A /\ h e. B ) ) -> ( f x. ( normh ` ( t +h h ) ) ) e. RR )
62 remulcl 
 |-  ( ( g e. RR /\ ( normh ` ( t +h h ) ) e. RR ) -> ( g x. ( normh ` ( t +h h ) ) ) e. RR )
63 58 62 sylan2 
 |-  ( ( g e. RR /\ ( t e. A /\ h e. B ) ) -> ( g x. ( normh ` ( t +h h ) ) ) e. RR )
64 63 adantll 
 |-  ( ( ( f e. RR /\ g e. RR ) /\ ( t e. A /\ h e. B ) ) -> ( g x. ( normh ` ( t +h h ) ) ) e. RR )
65 le2add 
 |-  ( ( ( ( normh ` t ) e. RR /\ ( normh ` h ) e. RR ) /\ ( ( f x. ( normh ` ( t +h h ) ) ) e. RR /\ ( g x. ( normh ` ( t +h h ) ) ) e. RR ) ) -> ( ( ( normh ` t ) <_ ( f x. ( normh ` ( t +h h ) ) ) /\ ( normh ` h ) <_ ( g x. ( normh ` ( t +h h ) ) ) ) -> ( ( normh ` t ) + ( normh ` h ) ) <_ ( ( f x. ( normh ` ( t +h h ) ) ) + ( g x. ( normh ` ( t +h h ) ) ) ) ) )
66 54 61 64 65 syl12anc 
 |-  ( ( ( f e. RR /\ g e. RR ) /\ ( t e. A /\ h e. B ) ) -> ( ( ( normh ` t ) <_ ( f x. ( normh ` ( t +h h ) ) ) /\ ( normh ` h ) <_ ( g x. ( normh ` ( t +h h ) ) ) ) -> ( ( normh ` t ) + ( normh ` h ) ) <_ ( ( f x. ( normh ` ( t +h h ) ) ) + ( g x. ( normh ` ( t +h h ) ) ) ) ) )
67 66 adantll 
 |-  ( ( ( ( A i^i B ) = 0H /\ ( f e. RR /\ g e. RR ) ) /\ ( t e. A /\ h e. B ) ) -> ( ( ( normh ` t ) <_ ( f x. ( normh ` ( t +h h ) ) ) /\ ( normh ` h ) <_ ( g x. ( normh ` ( t +h h ) ) ) ) -> ( ( normh ` t ) + ( normh ` h ) ) <_ ( ( f x. ( normh ` ( t +h h ) ) ) + ( g x. ( normh ` ( t +h h ) ) ) ) ) )
68 1 2 3 cdj3lem2 
 |-  ( ( t e. A /\ h e. B /\ ( A i^i B ) = 0H ) -> ( S ` ( t +h h ) ) = t )
69 68 fveq2d 
 |-  ( ( t e. A /\ h e. B /\ ( A i^i B ) = 0H ) -> ( normh ` ( S ` ( t +h h ) ) ) = ( normh ` t ) )
70 69 breq1d 
 |-  ( ( t e. A /\ h e. B /\ ( A i^i B ) = 0H ) -> ( ( normh ` ( S ` ( t +h h ) ) ) <_ ( f x. ( normh ` ( t +h h ) ) ) <-> ( normh ` t ) <_ ( f x. ( normh ` ( t +h h ) ) ) ) )
71 1 2 4 cdj3lem3 
 |-  ( ( t e. A /\ h e. B /\ ( A i^i B ) = 0H ) -> ( T ` ( t +h h ) ) = h )
72 71 fveq2d 
 |-  ( ( t e. A /\ h e. B /\ ( A i^i B ) = 0H ) -> ( normh ` ( T ` ( t +h h ) ) ) = ( normh ` h ) )
73 72 breq1d 
 |-  ( ( t e. A /\ h e. B /\ ( A i^i B ) = 0H ) -> ( ( normh ` ( T ` ( t +h h ) ) ) <_ ( g x. ( normh ` ( t +h h ) ) ) <-> ( normh ` h ) <_ ( g x. ( normh ` ( t +h h ) ) ) ) )
74 70 73 anbi12d 
 |-  ( ( t e. A /\ h e. B /\ ( A i^i B ) = 0H ) -> ( ( ( normh ` ( S ` ( t +h h ) ) ) <_ ( f x. ( normh ` ( t +h h ) ) ) /\ ( normh ` ( T ` ( t +h h ) ) ) <_ ( g x. ( normh ` ( t +h h ) ) ) ) <-> ( ( normh ` t ) <_ ( f x. ( normh ` ( t +h h ) ) ) /\ ( normh ` h ) <_ ( g x. ( normh ` ( t +h h ) ) ) ) ) )
75 74 3expa 
 |-  ( ( ( t e. A /\ h e. B ) /\ ( A i^i B ) = 0H ) -> ( ( ( normh ` ( S ` ( t +h h ) ) ) <_ ( f x. ( normh ` ( t +h h ) ) ) /\ ( normh ` ( T ` ( t +h h ) ) ) <_ ( g x. ( normh ` ( t +h h ) ) ) ) <-> ( ( normh ` t ) <_ ( f x. ( normh ` ( t +h h ) ) ) /\ ( normh ` h ) <_ ( g x. ( normh ` ( t +h h ) ) ) ) ) )
76 75 ancoms 
 |-  ( ( ( A i^i B ) = 0H /\ ( t e. A /\ h e. B ) ) -> ( ( ( normh ` ( S ` ( t +h h ) ) ) <_ ( f x. ( normh ` ( t +h h ) ) ) /\ ( normh ` ( T ` ( t +h h ) ) ) <_ ( g x. ( normh ` ( t +h h ) ) ) ) <-> ( ( normh ` t ) <_ ( f x. ( normh ` ( t +h h ) ) ) /\ ( normh ` h ) <_ ( g x. ( normh ` ( t +h h ) ) ) ) ) )
77 76 adantlr 
 |-  ( ( ( ( A i^i B ) = 0H /\ ( f e. RR /\ g e. RR ) ) /\ ( t e. A /\ h e. B ) ) -> ( ( ( normh ` ( S ` ( t +h h ) ) ) <_ ( f x. ( normh ` ( t +h h ) ) ) /\ ( normh ` ( T ` ( t +h h ) ) ) <_ ( g x. ( normh ` ( t +h h ) ) ) ) <-> ( ( normh ` t ) <_ ( f x. ( normh ` ( t +h h ) ) ) /\ ( normh ` h ) <_ ( g x. ( normh ` ( t +h h ) ) ) ) ) )
78 recn 
 |-  ( f e. RR -> f e. CC )
79 recn 
 |-  ( g e. RR -> g e. CC )
80 58 recnd 
 |-  ( ( t e. A /\ h e. B ) -> ( normh ` ( t +h h ) ) e. CC )
81 adddir 
 |-  ( ( f e. CC /\ g e. CC /\ ( normh ` ( t +h h ) ) e. CC ) -> ( ( f + g ) x. ( normh ` ( t +h h ) ) ) = ( ( f x. ( normh ` ( t +h h ) ) ) + ( g x. ( normh ` ( t +h h ) ) ) ) )
82 78 79 80 81 syl3an 
 |-  ( ( f e. RR /\ g e. RR /\ ( t e. A /\ h e. B ) ) -> ( ( f + g ) x. ( normh ` ( t +h h ) ) ) = ( ( f x. ( normh ` ( t +h h ) ) ) + ( g x. ( normh ` ( t +h h ) ) ) ) )
83 82 3expa 
 |-  ( ( ( f e. RR /\ g e. RR ) /\ ( t e. A /\ h e. B ) ) -> ( ( f + g ) x. ( normh ` ( t +h h ) ) ) = ( ( f x. ( normh ` ( t +h h ) ) ) + ( g x. ( normh ` ( t +h h ) ) ) ) )
84 83 breq2d 
 |-  ( ( ( f e. RR /\ g e. RR ) /\ ( t e. A /\ h e. B ) ) -> ( ( ( normh ` t ) + ( normh ` h ) ) <_ ( ( f + g ) x. ( normh ` ( t +h h ) ) ) <-> ( ( normh ` t ) + ( normh ` h ) ) <_ ( ( f x. ( normh ` ( t +h h ) ) ) + ( g x. ( normh ` ( t +h h ) ) ) ) ) )
85 84 adantll 
 |-  ( ( ( ( A i^i B ) = 0H /\ ( f e. RR /\ g e. RR ) ) /\ ( t e. A /\ h e. B ) ) -> ( ( ( normh ` t ) + ( normh ` h ) ) <_ ( ( f + g ) x. ( normh ` ( t +h h ) ) ) <-> ( ( normh ` t ) + ( normh ` h ) ) <_ ( ( f x. ( normh ` ( t +h h ) ) ) + ( g x. ( normh ` ( t +h h ) ) ) ) ) )
86 67 77 85 3imtr4d 
 |-  ( ( ( ( A i^i B ) = 0H /\ ( f e. RR /\ g e. RR ) ) /\ ( t e. A /\ h e. B ) ) -> ( ( ( normh ` ( S ` ( t +h h ) ) ) <_ ( f x. ( normh ` ( t +h h ) ) ) /\ ( normh ` ( T ` ( t +h h ) ) ) <_ ( g x. ( normh ` ( t +h h ) ) ) ) -> ( ( normh ` t ) + ( normh ` h ) ) <_ ( ( f + g ) x. ( normh ` ( t +h h ) ) ) ) )
87 46 86 syld 
 |-  ( ( ( ( A i^i B ) = 0H /\ ( f e. RR /\ g e. RR ) ) /\ ( t e. A /\ h e. B ) ) -> ( ( A. u e. ( A +H B ) ( normh ` ( S ` u ) ) <_ ( f x. ( normh ` u ) ) /\ A. u e. ( A +H B ) ( normh ` ( T ` u ) ) <_ ( g x. ( normh ` u ) ) ) -> ( ( normh ` t ) + ( normh ` h ) ) <_ ( ( f + g ) x. ( normh ` ( t +h h ) ) ) ) )
88 87 ralrimdvva 
 |-  ( ( ( A i^i B ) = 0H /\ ( f e. RR /\ g e. RR ) ) -> ( ( A. u e. ( A +H B ) ( normh ` ( S ` u ) ) <_ ( f x. ( normh ` u ) ) /\ A. u e. ( A +H B ) ( normh ` ( T ` u ) ) <_ ( g x. ( normh ` u ) ) ) -> A. t e. A A. h e. B ( ( normh ` t ) + ( normh ` h ) ) <_ ( ( f + g ) x. ( normh ` ( t +h h ) ) ) ) )
89 readdcl 
 |-  ( ( f e. RR /\ g e. RR ) -> ( f + g ) e. RR )
90 breq2 
 |-  ( v = ( f + g ) -> ( 0 < v <-> 0 < ( f + g ) ) )
91 fveq2 
 |-  ( x = t -> ( normh ` x ) = ( normh ` t ) )
92 91 oveq1d 
 |-  ( x = t -> ( ( normh ` x ) + ( normh ` y ) ) = ( ( normh ` t ) + ( normh ` y ) ) )
93 fvoveq1 
 |-  ( x = t -> ( normh ` ( x +h y ) ) = ( normh ` ( t +h y ) ) )
94 93 oveq2d 
 |-  ( x = t -> ( v x. ( normh ` ( x +h y ) ) ) = ( v x. ( normh ` ( t +h y ) ) ) )
95 92 94 breq12d 
 |-  ( x = t -> ( ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) <-> ( ( normh ` t ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( t +h y ) ) ) ) )
96 fveq2 
 |-  ( y = h -> ( normh ` y ) = ( normh ` h ) )
97 96 oveq2d 
 |-  ( y = h -> ( ( normh ` t ) + ( normh ` y ) ) = ( ( normh ` t ) + ( normh ` h ) ) )
98 oveq2 
 |-  ( y = h -> ( t +h y ) = ( t +h h ) )
99 98 fveq2d 
 |-  ( y = h -> ( normh ` ( t +h y ) ) = ( normh ` ( t +h h ) ) )
100 99 oveq2d 
 |-  ( y = h -> ( v x. ( normh ` ( t +h y ) ) ) = ( v x. ( normh ` ( t +h h ) ) ) )
101 97 100 breq12d 
 |-  ( y = h -> ( ( ( normh ` t ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( t +h y ) ) ) <-> ( ( normh ` t ) + ( normh ` h ) ) <_ ( v x. ( normh ` ( t +h h ) ) ) ) )
102 95 101 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 ) ) ) )
103 oveq1 
 |-  ( v = ( f + g ) -> ( v x. ( normh ` ( t +h h ) ) ) = ( ( f + g ) x. ( normh ` ( t +h h ) ) ) )
104 103 breq2d 
 |-  ( v = ( f + g ) -> ( ( ( normh ` t ) + ( normh ` h ) ) <_ ( v x. ( normh ` ( t +h h ) ) ) <-> ( ( normh ` t ) + ( normh ` h ) ) <_ ( ( f + g ) x. ( normh ` ( t +h h ) ) ) ) )
105 104 2ralbidv 
 |-  ( v = ( f + g ) -> ( A. t e. A A. h e. B ( ( normh ` t ) + ( normh ` h ) ) <_ ( v x. ( normh ` ( t +h h ) ) ) <-> A. t e. A A. h e. B ( ( normh ` t ) + ( normh ` h ) ) <_ ( ( f + g ) x. ( normh ` ( t +h h ) ) ) ) )
106 102 105 syl5bb 
 |-  ( v = ( f + g ) -> ( 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 ) ) <_ ( ( f + g ) x. ( normh ` ( t +h h ) ) ) ) )
107 90 106 anbi12d 
 |-  ( v = ( f + g ) -> ( ( 0 < v /\ A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) ) <-> ( 0 < ( f + g ) /\ A. t e. A A. h e. B ( ( normh ` t ) + ( normh ` h ) ) <_ ( ( f + g ) x. ( normh ` ( t +h h ) ) ) ) ) )
108 107 rspcev 
 |-  ( ( ( f + g ) e. RR /\ ( 0 < ( f + g ) /\ A. t e. A A. h e. B ( ( normh ` t ) + ( normh ` h ) ) <_ ( ( f + g ) x. ( normh ` ( t +h h ) ) ) ) ) -> E. v e. RR ( 0 < v /\ A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) ) )
109 108 ex 
 |-  ( ( f + g ) e. RR -> ( ( 0 < ( f + g ) /\ A. t e. A A. h e. B ( ( normh ` t ) + ( normh ` h ) ) <_ ( ( f + g ) x. ( normh ` ( t +h h ) ) ) ) -> E. v e. RR ( 0 < v /\ A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) ) ) )
110 89 109 syl 
 |-  ( ( f e. RR /\ g e. RR ) -> ( ( 0 < ( f + g ) /\ A. t e. A A. h e. B ( ( normh ` t ) + ( normh ` h ) ) <_ ( ( f + g ) x. ( normh ` ( t +h h ) ) ) ) -> E. v e. RR ( 0 < v /\ A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) ) ) )
111 110 adantl 
 |-  ( ( ( A i^i B ) = 0H /\ ( f e. RR /\ g e. RR ) ) -> ( ( 0 < ( f + g ) /\ A. t e. A A. h e. B ( ( normh ` t ) + ( normh ` h ) ) <_ ( ( f + g ) x. ( normh ` ( t +h h ) ) ) ) -> E. v e. RR ( 0 < v /\ A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) ) ) )
112 33 88 111 syl2and 
 |-  ( ( ( A i^i B ) = 0H /\ ( f e. RR /\ g e. RR ) ) -> ( ( ( 0 < f /\ 0 < g ) /\ ( A. u e. ( A +H B ) ( normh ` ( S ` u ) ) <_ ( f x. ( normh ` u ) ) /\ A. u e. ( A +H B ) ( normh ` ( T ` u ) ) <_ ( g x. ( normh ` u ) ) ) ) -> E. v e. RR ( 0 < v /\ A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) ) ) )
113 30 112 syl5bi 
 |-  ( ( ( A i^i B ) = 0H /\ ( f e. RR /\ g e. RR ) ) -> ( ( ( 0 < f /\ A. u e. ( A +H B ) ( normh ` ( S ` u ) ) <_ ( f x. ( normh ` u ) ) ) /\ ( 0 < g /\ A. u e. ( A +H B ) ( normh ` ( T ` u ) ) <_ ( g x. ( normh ` u ) ) ) ) -> E. v e. RR ( 0 < v /\ A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) ) ) )
114 113 rexlimdvva 
 |-  ( ( A i^i B ) = 0H -> ( E. f e. RR E. g e. RR ( ( 0 < f /\ A. u e. ( A +H B ) ( normh ` ( S ` u ) ) <_ ( f x. ( normh ` u ) ) ) /\ ( 0 < g /\ A. u e. ( A +H B ) ( normh ` ( T ` u ) ) <_ ( g x. ( normh ` u ) ) ) ) -> E. v e. RR ( 0 < v /\ A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) ) ) )
115 29 114 syl5bi 
 |-  ( ( A i^i B ) = 0H -> ( ( ph /\ ps ) -> E. v e. RR ( 0 < v /\ A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) ) ) )
116 115 3impib 
 |-  ( ( ( A i^i B ) = 0H /\ ph /\ ps ) -> E. v e. RR ( 0 < v /\ A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) ) )
117 12 116 impbii 
 |-  ( E. v e. RR ( 0 < v /\ A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) ) <-> ( ( A i^i B ) = 0H /\ ph /\ ps ) )