Theorem cdj3lem3b 10367

Description: Lemma for cdj3 10368. The second-component function T is bounded if the subspaces are completely disjoint.

Hypotheses

Ref	Expression
cdj3lem2.1	|- A e. SH
cdj3lem2.2	|- B e. SH
cdj3lem3.3	|- T = {<.x, y>. | (x e. (A +H B) /\ y = U.{w e. B | E.z e. A x = (z +h w)})}

Assertion

Ref	Expression
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))))

Distinct variable groups:   x,y,z,w,v,u,A   x,B,y,z,w,v,u   v,T,u

Proof of Theorem cdj3lem3b

Step	Hyp	Ref	Expression
1		cdj3lem2.2	. . 3 |- B e. SH
2		cdj3lem2.1	. . 3 |- A e. SH
3		cdj3lem3.3	. . . 4 |- T = {<.x, y>. | (x e. (A +H B) /\ y = U.{w e. B | E.z e. A x = (z +h w)})}
4	1, 2	shscom 9332	. . . . . . 7 |- (B +H A) = (A +H B)
5	4	eleq2i 1538	. . . . . 6 |- (x e. (B +H A) <-> x e. (A +H B))
6		ax-hvcom 8871	. . . . . . . . . . . 12 |- ((w e. H~ /\ z e. H~) -> (w +h z) = (z +h w))
7	1	shel 9082	. . . . . . . . . . . 12 |- (w e. B -> w e. H~)
8	2	shel 9082	. . . . . . . . . . . 12 |- (z e. A -> z e. H~)
9	6, 7, 8	syl2an 454	. . . . . . . . . . 11 |- ((w e. B /\ z e. A) -> (w +h z) = (z +h w))
10	9	eqeq2d 1486	. . . . . . . . . 10 |- ((w e. B /\ z e. A) -> (x = (w +h z) <-> x = (z +h w)))
11	10	rexbidva 1660	. . . . . . . . 9 |- (w e. B -> (E.z e. A x = (w +h z) <-> E.z e. A x = (z +h w)))
12	11	rabbii 1805	. . . . . . . 8 |- {w e. B | E.z e. A x = (w +h z)} = {w e. B | E.z e. A x = (z +h w)}
13	12	unieqi 2511	. . . . . . 7 |- U.{w e. B | E.z e. A x = (w +h z)} = U.{w e. B | E.z e. A x = (z +h w)}
14	13	eqeq2i 1485	. . . . . 6 |- (y = U.{w e. B | E.z e. A x = (w +h z)} <-> y = U.{w e. B | E.z e. A x = (z +h w)})
15	5, 14	anbi12i 482	. . . . 5 |- ((x e. (B +H A) /\ y = U.{w e. B | E.z e. A x = (w +h z)}) <-> (x e. (A +H B) /\ y = U.{w e. B | E.z e. A x = (z +h w)}))
16	15	opabbii 2671	. . . 4 |- {<.x, y>. | (x e. (B +H A) /\ y = U.{w e. B | E.z e. A x = (w +h z)})} = {<.x, y>. | (x e. (A +H B) /\ y = U.{w e. B | E.z e. A x = (z +h w)})}
17	3, 16	eqtr4 1498	. . 3 |- T = {<.x, y>. | (x e. (B +H A) /\ y = U.{w e. B | E.z e. A x = (w +h z)})}
18	1, 2, 17	cdj3lem2b 10364	. 2 |- (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))))
19		fveq2 3724	. . . . . . . 8 |- (x = t -> (normh` x) = (normh` t))
20	19	opreq1d 3975	. . . . . . 7 |- (x = t -> ((normh` x) + (normh` y)) = ((normh` t) + (normh` y)))
21		opreq1 3968	. . . . . . . . 9 |- (x = t -> (x +h y) = (t +h y))
22	21	fveq2d 3728	. . . . . . . 8 |- (x = t -> (normh` (x +h y)) = (normh` (t +h y)))
23	22	opreq2d 3976	. . . . . . 7 |- (x = t -> (v x. (normh` (x +h y))) = (v x. (normh` (t +h y))))
24	20, 23	breq12d 2631	. . . . . 6 |- (x = t -> (((normh` x) + (normh` y)) <_ (v x. (normh` (x +h y))) <-> ((normh` t) + (normh` y)) <_ (v x. (normh` (t +h y)))))
25		fveq2 3724	. . . . . . . 8 |- (y = h -> (normh` y) = (normh` h))
26	25	opreq2d 3976	. . . . . . 7 |- (y = h -> ((normh` t) + (normh` y)) = ((normh` t) + (normh` h)))
27		opreq2 3969	. . . . . . . . 9 |- (y = h -> (t +h y) = (t +h h))
28	27	fveq2d 3728	. . . . . . . 8 |- (y = h -> (normh` (t +h y)) = (normh` (t +h h)))
29	28	opreq2d 3976	. . . . . . 7 |- (y = h -> (v x. (normh` (t +h y))) = (v x. (normh` (t +h h))))
30	26, 29	breq12d 2631	. . . . . 6 |- (y = h -> (((normh` t) + (normh` y)) <_ (v x. (normh` (t +h y))) <-> ((normh` t) + (normh` h)) <_ (v x. (normh` (t +h h)))))
31	24, 30	cbvral2v 1803	. . . . 5 |- (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))))
32		ralcom 1774	. . . . 5 |- (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))))
33		axaddcom 5275	. . . . . . . . . 10 |- (((normh` x) e. CC /\ (normh` y) e. CC) -> ((normh` x) + (normh` y)) = ((normh` y) + (normh` x)))
34	1	shel 9082	. . . . . . . . . . . 12 |- (x e. B -> x e. H~)
35		normclt 8991	. . . . . . . . . . . 12 |- (x e. H~ -> (normh` x) e. RR)
36	34, 35	syl 10	. . . . . . . . . . 11 |- (x e. B -> (normh` x) e. RR)
37	36	recnd 5315	. . . . . . . . . 10 |- (x e. B -> (normh` x) e. CC)
38	2	shel 9082	. . . . . . . . . . . 12 |- (y e. A -> y e. H~)
39		normclt 8991	. . . . . . . . . . . 12 |- (y e. H~ -> (normh` y) e. RR)
40	38, 39	syl 10	. . . . . . . . . . 11 |- (y e. A -> (normh` y) e. RR)
41	40	recnd 5315	. . . . . . . . . 10 |- (y e. A -> (normh` y) e. CC)
42	33, 37, 41	syl2an 454	. . . . . . . . 9 |- ((x e. B /\ y e. A) -> ((normh` x) + (normh` y)) = ((normh` y) + (normh` x)))
43		ax-hvcom 8871	. . . . . . . . . . . 12 |- ((x e. H~ /\ y e. H~) -> (x +h y) = (y +h x))
44	43, 34, 38	syl2an 454	. . . . . . . . . . 11 |- ((x e. B /\ y e. A) -> (x +h y) = (y +h x))
45	44	fveq2d 3728	. . . . . . . . . 10 |- ((x e. B /\ y e. A) -> (normh` (x +h y)) = (normh` (y +h x)))
46	45	opreq2d 3976	. . . . . . . . 9 |- ((x e. B /\ y e. A) -> (v x. (normh` (x +h y))) = (v x. (normh` (y +h x))))
47	42, 46	breq12d 2631	. . . . . . . 8 |- ((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)))))
48	47	ralbidva 1659	. . . . . . 7 |- (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)))))
49	48	ralbiia 1673	. . . . . 6 |- (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))))
50		fveq2 3724	. . . . . . . . 9 |- (x = h -> (normh` x) = (normh` h))
51	50	opreq2d 3976	. . . . . . . 8 |- (x = h -> ((normh` y) + (normh` x)) = ((normh` y) + (normh` h)))
52		opreq2 3969	. . . . . . . . . 10 |- (x = h -> (y +h x) = (y +h h))
53	52	fveq2d 3728	. . . . . . . . 9 |- (x = h -> (normh` (y +h x)) = (normh` (y +h h)))
54	53	opreq2d 3976	. . . . . . . 8 |- (x = h -> (v x. (normh` (y +h x))) = (v x. (normh` (y +h h))))
55	51, 54	breq12d 2631	. . . . . . 7 |- (x = h -> (((normh` y) + (normh` x)) <_ (v x. (normh` (y +h x))) <-> ((normh` y) + (normh` h)) <_ (v x. (normh` (y +h h)))))
56		fveq2 3724	. . . . . . . . 9 |- (y = t -> (normh` y) = (normh` t