Theorem cdj3 10359

Description: Two ways to express "A and B are completely disjoint subspaces." (1) <=> (3) in Lemma 5 of [Holland] p. 1520.

Hypotheses

Ref	Expression
cdj3.1	|- A e. SH
cdj3.2	|- B e. SH
cdj3.3	|- S = {<.x, y>. | (x e. (A +H B) /\ y = U.{z e. A | E.w e. B x = (z +h w)})}
cdj3.4	|- T = {<.x, y>. | (x e. (A +H B) /\ y = U.{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

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

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

Proof of Theorem cdj3

Step	Hyp	Ref	Expression
1		cdj3.1	. . . 4 |- A e. SH
2		cdj3.2	. . . 4 |- B e. SH
3	1, 2	cdj3lem1 10352	. . 3 |- (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)
4		cdj3.3	. . . . 5 |- S = {<.x, y>. | (x e. (A +H B) /\ y = U.{z e. A | E.w e. B x = (z +h w)})}
5	1, 2, 4	cdj3lem2b 10355	. . . 4 |- (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))))
6		cdj3.5	. . . 4 |- (ph <-> E.v e. RR (0 < v /\ A.u e. (A +H B)(normh` (S` u)) <_ (v x. (normh` u))))
7	5, 6	sylibr 200	. . 3 |- (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)
8		cdj3.4	. . . . 5 |- T = {<.x, y>. | (x e. (A +H B) /\ y = U.{w e. B | E.z e. A x = (z +h w)})}
9	1, 2, 8	cdj3lem3b 10358	. . . 4 |- (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))))
10		cdj3.6	. . . 4 |- (ps <-> E.v e. RR (0 < v /\ A.u e. (A +H B)(normh` (T` u)) <_ (v x. (normh` u))))
11	9, 10	sylibr 200	. . 3 |- (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	3, 7, 11	3jca 818	. 2 |- (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		axaddrcl 5259	. . . . . . . . . 10 |- ((f e. RR /\ g e. RR) -> (f + g) e. RR)
14		breq2 2620	. . . . . . . . . . . . 13 |- (v = (f + g) -> (0 < v <-> 0 < (f + g)))
15		opreq1 3965	. . . . . . . . . . . . . . . 16 |- (v = (f + g) -> (v x. (normh` (t +h h))) = ((f + g) x. (normh` (t +h h))))
16	15	breq2d 2627	. . . . . . . . . . . . . . 15 |- (v = (f + g) -> (((normh` t) + (normh` h)) <_ (v x. (normh` (t +h h))) <-> ((normh` t) + (normh` h)) <_ ((f + g) x. (normh` (t +h h)))))
17	16	2ralbidv 1679	. . . . . . . . . . . . . 14 |- (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)))))
18		fveq2 3721	. . . . . . . . . . . . . . . . 17 |- (x = t -> (normh` x) = (normh` t))
19	18	opreq1d 3972	. . . . . . . . . . . . . . . 16 |- (x = t -> ((normh` x) + (normh` y)) = ((normh` t) + (normh` y)))
20		opreq1 3965	. . . . . . . . . . . . . . . . . 18 |- (x = t -> (x +h y) = (t +h y))
21	20	fveq2d 3725	. . . . . . . . . . . . . . . . 17 |- (x = t -> (normh` (x +h y)) = (normh` (t +h y)))
22	21	opreq2d 3973	. . . . . . . . . . . . . . . 16 |- (x = t -> (v x. (normh` (x +h y))) = (v x. (normh` (t +h y))))
23	19, 22	breq12d 2628	. . . . . . . . . . . . . . 15 |- (x = t -> (((normh` x) + (normh` y)) <_ (v x. (normh` (x +h y))) <-> ((normh` t) + (normh` y)) <_ (v x. (normh` (t +h y)))))
24		fveq2 3721	. . . . . . . . . . . . . . . . 17 |- (y = h -> (normh` y) = (normh` h))
25	24	opreq2d 3973	. . . . . . . . . . . . . . . 16 |- (y = h -> ((normh` t) + (normh` y)) = ((normh` t) + (normh` h)))
26		opreq2 3966	. . . . . . . . . . . . . . . . . 18 |- (y = h -> (t +h y) = (t +h h))
27	26	fveq2d 3725	. . . . . . . . . . . . . . . . 17 |- (y = h -> (normh` (t +h y)) = (normh` (t +h h)))
28	27	opreq2d 3973	. . . . . . . . . . . . . . . 16 |- (y = h -> (v x. (normh` (t +h y))) = (v x. (normh` (t +h h))))
29	25, 28	breq12d 2628	. . . . . . . . . . . . . . 15 |- (y = h -> (((normh` t) + (normh` y)) <_ (v x. (normh` (t +h y))) <-> ((normh` t) + (normh` h)) <_ (v x. (normh` (t +h h)))))
30	23, 29	cbvral2v 1801	. . . . . . . . . . . . . 14 |- (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))))
31	17, 30	syl5bb 531	. . . . . . . . . . . . 13 |- (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)))))
32	14, 31	anbi12d 627	. . . . . . . . . . . 12 |- (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))))))
33	32	rcla4ev 1875	. . . . . . . . . . 11 |- (((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)))))
34	33	ex 373	. . . . . . . . . 10 |- ((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))))))
35	13, 34	syl 10	. . . . . . . . 9 |- ((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))))))
36	35	adantl 388	. . . . . . . 8 |- (((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 +