Theorem cdj3lem2b

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

	Ref	Expression
Hypotheses	cdj3lem2.1	|- A e. SH
	cdj3lem2.2	|- B e. SH
	cdj3lem2.3	|- S = ( x e. ( A +H B ) |-> ( iota_ z e. A E. w e. B x = ( z +h w ) ) )
Assertion	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 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cdj3lem2.1	|- A e. SH
2		cdj3lem2.2	|- B e. SH
3		cdj3lem2.3	|- S = ( x e. ( A +H B ) |-> ( iota_ z e. A E. w e. B x = ( z +h w ) ) )
4	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 )
5	1 2	shseli	|- ( u e. ( A +H B ) <-> E. t e. A E. h e. B u = ( t +h h ) )
6	5	biimpi	|- ( u e. ( A +H B ) -> E. t e. A E. h e. B u = ( t +h h ) )
7		fveq2	|- ( x = t -> ( normh ` x ) = ( normh ` t ) )
8	7	oveq1d	|- ( x = t -> ( ( normh ` x ) + ( normh ` y ) ) = ( ( normh ` t ) + ( normh ` y ) ) )
9		fvoveq1	|- ( x = t -> ( normh ` ( x +h y ) ) = ( normh ` ( t +h y ) ) )
10	9	oveq2d	|- ( x = t -> ( v x. ( normh ` ( x +h y ) ) ) = ( v x. ( normh ` ( t +h y ) ) ) )
11	8 10	breq12d	|- ( x = t -> ( ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) <-> ( ( normh ` t ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( t +h y ) ) ) ) )
12		fveq2	|- ( y = h -> ( normh ` y ) = ( normh ` h ) )
13	12	oveq2d	|- ( y = h -> ( ( normh ` t ) + ( normh ` y ) ) = ( ( normh ` t ) + ( normh ` h ) ) )
14		oveq2	|- ( y = h -> ( t +h y ) = ( t +h h ) )
15	14	fveq2d	|- ( y = h -> ( normh ` ( t +h y ) ) = ( normh ` ( t +h h ) ) )
16	15	oveq2d	|- ( y = h -> ( v x. ( normh ` ( t +h y ) ) ) = ( v x. ( normh ` ( t +h h ) ) ) )
17	13 16	breq12d	|- ( y = h -> ( ( ( normh ` t ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( t +h y ) ) ) <-> ( ( normh ` t ) + ( normh ` h ) ) <_ ( v x. ( normh ` ( t +h h ) ) ) ) )
18	11 17	rspc2v	|- ( ( t e. A /\ h e. B ) -> ( A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) -> ( ( normh ` t ) + ( normh ` h ) ) <_ ( v x. ( normh ` ( t +h h ) ) ) ) )
19	1 2 3	cdj3lem2	|- ( ( t e. A /\ h e. B /\ ( A i^i B ) = 0H ) -> ( S ` ( t +h h ) ) = t )
20	19	3expa	|- ( ( ( t e. A /\ h e. B ) /\ ( A i^i B ) = 0H ) -> ( S ` ( t +h h ) ) = t )
21	20	fveq2d	|- ( ( ( t e. A /\ h e. B ) /\ ( A i^i B ) = 0H ) -> ( normh ` ( S ` ( t +h h ) ) ) = ( normh ` t ) )
22	21	ad2ant2r	|- ( ( ( ( t e. A /\ h e. B ) /\ ( ( normh ` t ) + ( normh ` h ) ) <_ ( v x. ( normh ` ( t +h h ) ) ) ) /\ ( ( A i^i B ) = 0H /\ v e. RR ) ) -> ( normh ` ( S ` ( t +h h ) ) ) = ( normh ` t ) )
23	2	sheli	|- ( h e. B -> h e. ~H )
24		normge0	|- ( h e. ~H -> 0 <_ ( normh ` h ) )
25	23 24	syl	|- ( h e. B -> 0 <_ ( normh ` h ) )
26	25	adantl	|- ( ( t e. A /\ h e. B ) -> 0 <_ ( normh ` h ) )
27	1	sheli	|- ( t e. A -> t e. ~H )
28		normcl	|- ( t e. ~H -> ( normh ` t ) e. RR )
29	27 28	syl	|- ( t e. A -> ( normh ` t ) e. RR )
30		normcl	|- ( h e. ~H -> ( normh ` h ) e. RR )
31	23 30	syl	|- ( h e. B -> ( normh ` h ) e. RR )
32		addge01	|- ( ( ( normh ` t ) e. RR /\ ( normh ` h ) e. RR ) -> ( 0 <_ ( normh ` h ) <-> ( normh ` t ) <_ ( ( normh ` t ) + ( normh ` h ) ) ) )
33	29 31 32	syl2an	|- ( ( t e. A /\ h e. B ) -> ( 0 <_ ( normh ` h ) <-> ( normh ` t ) <_ ( ( normh ` t ) + ( normh ` h ) ) ) )
34	26 33	mpbid	|- ( ( t e. A /\ h e. B ) -> ( normh ` t ) <_ ( ( normh ` t ) + ( normh ` h ) ) )
35	34	adantr	|- ( ( ( t e. A /\ h e. B ) /\ v e. RR ) -> ( normh ` t ) <_ ( ( normh ` t ) + ( normh ` h ) ) )
36	29	ad2antrr	|- ( ( ( t e. A /\ h e. B ) /\ v e. RR ) -> ( normh ` t ) e. RR )
37		readdcl	|- ( ( ( normh ` t ) e. RR /\ ( normh ` h ) e. RR ) -> ( ( normh ` t ) + ( normh ` h ) ) e. RR )
38	29 31 37	syl2an	|- ( ( t e. A /\ h e. B ) -> ( ( normh ` t ) + ( normh ` h ) ) e. RR )
39	38	adantr	|- ( ( ( t e. A /\ h e. B ) /\ v e. RR ) -> ( ( normh ` t ) + ( normh ` h ) ) e. RR )
40		hvaddcl	|- ( ( t e. ~H /\ h e. ~H ) -> ( t +h h ) e. ~H )
41	27 23 40	syl2an	|- ( ( t e. A /\ h e. B ) -> ( t +h h ) e. ~H )
42		normcl	|- ( ( t +h h ) e. ~H -> ( normh ` ( t +h h ) ) e. RR )
43	41 42	syl	|- ( ( t e. A /\ h e. B ) -> ( normh ` ( t +h h ) ) e. RR )
44		remulcl	|- ( ( v e. RR /\ ( normh ` ( t +h h ) ) e. RR ) -> ( v x. ( normh ` ( t +h h ) ) ) e. RR )
45	43 44	sylan2	|- ( ( v e. RR /\ ( t e. A /\ h e. B ) ) -> ( v x. ( normh ` ( t +h h ) ) ) e. RR )
46	45	ancoms	|- ( ( ( t e. A /\ h e. B ) /\ v e. RR ) -> ( v x. ( normh ` ( t +h h ) ) ) e. RR )
47		letr	|- ( ( ( normh ` t ) e. RR /\ ( ( normh ` t ) + ( normh ` h ) ) e. RR /\ ( v x. ( normh ` ( t +h h ) ) ) e. RR ) -> ( ( ( normh ` t ) <_ ( ( normh ` t ) + ( normh ` h ) ) /\ ( ( normh ` t ) + ( normh ` h ) ) <_ ( v x. ( normh ` ( t +h h ) ) ) ) -> ( normh ` t ) <_ ( v x. ( normh ` ( t +h h ) ) ) ) )
48	36 39 46 47	syl3anc	|- ( ( ( t e. A /\ h e. B ) /\ v e. RR ) -> ( ( ( normh ` t ) <_ ( ( normh ` t ) + ( normh ` h ) ) /\ ( ( normh ` t ) + ( normh ` h ) ) <_ ( v x. ( normh ` ( t +h h ) ) ) ) -> ( normh ` t ) <_ ( v x. ( normh ` ( t +h h ) ) ) ) )
49	35 48	mpand	|- ( ( ( t e. A /\ h e. B ) /\ v e. RR ) -> ( ( ( normh ` t ) + ( normh ` h ) ) <_ ( v x. ( normh ` ( t +h h ) ) ) -> ( normh ` t ) <_ ( v x. ( normh ` ( t +h h ) ) ) ) )
50	49	imp	|- ( ( ( ( t e. A /\ h e. B ) /\ v e. RR ) /\ ( ( normh ` t ) + ( normh ` h ) ) <_ ( v x. ( normh ` ( t +h h ) ) ) ) -> ( normh ` t ) <_ ( v x. ( normh ` ( t +h h ) ) ) )
51	50	an32s	|- ( ( ( ( t e. A /\ h e. B ) /\ ( ( normh ` t ) + ( normh ` h ) ) <_ ( v x. ( normh ` ( t +h h ) ) ) ) /\ v e. RR ) -> ( normh ` t ) <_ ( v x. ( normh ` ( t +h h ) ) ) )
52	51	adantrl	|- ( ( ( ( t e. A /\ h e. B ) /\ ( ( normh ` t ) + ( normh ` h ) ) <_ ( v x. ( normh ` ( t +h h ) ) ) ) /\ ( ( A i^i B ) = 0H /\ v e. RR ) ) -> ( normh ` t ) <_ ( v x. ( normh ` ( t +h h ) ) ) )
53	22 52	eqbrtrd	|- ( ( ( ( t e. A /\ h e. B ) /\ ( ( normh ` t ) + ( normh ` h ) ) <_ ( v x. ( normh ` ( t +h h ) ) ) ) /\ ( ( A i^i B ) = 0H /\ v e. RR ) ) -> ( normh ` ( S ` ( t +h h ) ) ) <_ ( v x. ( normh ` ( t +h h ) ) ) )
54		2fveq3	|- ( u = ( t +h h ) -> ( normh ` ( S ` u ) ) = ( normh ` ( S ` ( t +h h ) ) ) )
55		fveq2	|- ( u = ( t +h h ) -> ( normh ` u ) = ( normh ` ( t +h h ) ) )
56	55	oveq2d	|- ( u = ( t +h h ) -> ( v x. ( normh ` u ) ) = ( v x. ( normh ` ( t +h h ) ) ) )
57	54 56	breq12d	|- ( u = ( t +h h ) -> ( ( normh ` ( S ` u ) ) <_ ( v x. ( normh ` u ) ) <-> ( normh ` ( S ` ( t +h h ) ) ) <_ ( v x. ( normh ` ( t +h h ) ) ) ) )
58	53 57	syl5ibrcom	|- ( ( ( ( t e. A /\ h e. B ) /\ ( ( normh ` t ) + ( normh ` h ) ) <_ ( v x. ( normh ` ( t +h h ) ) ) ) /\ ( ( A i^i B ) = 0H /\ v e. RR ) ) -> ( u = ( t +h h ) -> ( normh ` ( S ` u ) ) <_ ( v x. ( normh ` u ) ) ) )
59	58	exp31	|- ( ( t e. A /\ h e. B ) -> ( ( ( normh ` t ) + ( normh ` h ) ) <_ ( v x. ( normh ` ( t +h h ) ) ) -> ( ( ( A i^i B ) = 0H /\ v e. RR ) -> ( u = ( t +h h ) -> ( normh ` ( S ` u ) ) <_ ( v x. ( normh ` u ) ) ) ) ) )
60	18 59	syld	|- ( ( t e. A /\ h e. B ) -> ( A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) -> ( ( ( A i^i B ) = 0H /\ v e. RR ) -> ( u = ( t +h h ) -> ( normh ` ( S ` u ) ) <_ ( v x. ( normh ` u ) ) ) ) ) )
61	60	com14	|- ( u = ( t +h h ) -> ( A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) -> ( ( ( A i^i B ) = 0H /\ v e. RR ) -> ( ( t e. A /\ h e. B ) -> ( normh ` ( S ` u ) ) <_ ( v x. ( normh ` u ) ) ) ) ) )
62	61	com4t	|- ( ( ( A i^i B ) = 0H /\ v e. RR ) -> ( ( t e. A /\ h e. B ) -> ( u = ( t +h h ) -> ( A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) -> ( normh ` ( S ` u ) ) <_ ( v x. ( normh ` u ) ) ) ) ) )
63	62	rexlimdvv	|- ( ( ( A i^i B ) = 0H /\ v e. RR ) -> ( E. t e. A E. h e. B u = ( t +h h ) -> ( A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) -> ( normh ` ( S ` u ) ) <_ ( v x. ( normh ` u ) ) ) ) )
64	6 63	syl5com	|- ( u e. ( A +H B ) -> ( ( ( A i^i B ) = 0H /\ v e. RR ) -> ( A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) -> ( normh ` ( S ` u ) ) <_ ( v x. ( normh ` u ) ) ) ) )
65	64	com3l	|- ( ( ( A i^i B ) = 0H /\ v e. RR ) -> ( A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) -> ( u e. ( A +H B ) -> ( normh ` ( S ` u ) ) <_ ( v x. ( normh ` u ) ) ) ) )
66	65	ralrimdv	|- ( ( ( A i^i B ) = 0H /\ v e. RR ) -> ( A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) -> A. u e. ( A +H B ) ( normh ` ( S ` u ) ) <_ ( v x. ( normh ` u ) ) ) )
67	66	anim2d	|- ( ( ( A i^i B ) = 0H /\ v e. RR ) -> ( ( 0 < v /\ A. x e. A A. y e. B ( ( normh ` x ) + ( normh ` y ) ) <_ ( v x. ( normh ` ( x +h y ) ) ) ) -> ( 0 < v /\ A. u e. ( A +H B ) ( normh ` ( S ` u ) ) <_ ( v x. ( normh ` u ) ) ) ) )
68	67	reximdva	|- ( ( A i^i B ) = 0H -> ( 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 ) ) ) ) )
69	4 68	mpcom	|- ( 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 ) ) ) )