Theorem cdj3lem1 10361

Description: A property of "A and B are completely disjoint subspaces." Part of Lemma 5 of [Holland] p. 1520.

Hypotheses

Ref	Expression
cdj1.1	|- A e. SH
cdj1.2	|- B e. SH

Assertion

Ref	Expression
cdj3lem1	|- (E.x e. RR (0 < x /\ A.y e. A A.z e. B ((normh` y) + (normh` z)) <_ (x x. (normh` (y +h z)))) -> (A i^i B) = 0H)

Distinct variable groups:   x,y,z,A   x,B,y,z

Proof of Theorem cdj3lem1

Step	Hyp	Ref	Expression
1		elin 2207	. . . . . . . . . . . . . 14 |- (w e. (A i^i B) <-> (w e. A /\ w e. B))
2		ax1cn 5269	. . . . . . . . . . . . . . . . 17 |- 1 e. CC
3	2	negcl 5369	. . . . . . . . . . . . . . . 16 |- -u1 e. CC
4		cdj1.2	. . . . . . . . . . . . . . . . 17 |- B e. SH
5		shmulcltOLD 9088	. . . . . . . . . . . . . . . . 17 |- (B e. SH -> ((-u1 e. CC /\ w e. B) -> (-u1 .h w) e. B))
6	4, 5	ax-mp 7	. . . . . . . . . . . . . . . 16 |- ((-u1 e. CC /\ w e. B) -> (-u1 .h w) e. B)
7	3, 6	mpan 695	. . . . . . . . . . . . . . 15 |- (w e. B -> (-u1 .h w) e. B)
8	7	anim2i 335	. . . . . . . . . . . . . 14 |- ((w e. A /\ w e. B) -> (w e. A /\ (-u1 .h w) e. B))
9	1, 8	sylbi 199	. . . . . . . . . . . . 13 |- (w e. (A i^i B) -> (w e. A /\ (-u1 .h w) e. B))
10		fveq2 3724	. . . . . . . . . . . . . . . 16 |- (y = w -> (normh` y) = (normh` w))
11	10	opreq1d 3975	. . . . . . . . . . . . . . 15 |- (y = w -> ((normh` y) + (normh` z)) = ((normh` w) + (normh` z)))
12		opreq1 3968	. . . . . . . . . . . . . . . . 17 |- (y = w -> (y +h z) = (w +h z))
13	12	fveq2d 3728	. . . . . . . . . . . . . . . 16 |- (y = w -> (normh` (y +h z)) = (normh` (w +h z)))
14	13	opreq2d 3976	. . . . . . . . . . . . . . 15 |- (y = w -> (x x. (normh` (y +h z))) = (x x. (normh` (w +h z))))
15	11, 14	breq12d 2631	. . . . . . . . . . . . . 14 |- (y = w -> (((normh` y) + (normh` z)) <_ (x x. (normh` (y +h z))) <-> ((normh` w) + (normh` z)) <_ (x x. (normh` (w +h z)))))
16		fveq2 3724	. . . . . . . . . . . . . . . 16 |- (z = (-u1 .h w) -> (normh` z) = (normh` (-u1 .h w)))
17	16	opreq2d 3976	. . . . . . . . . . . . . . 15 |- (z = (-u1 .h w) -> ((normh` w) + (normh` z)) = ((normh` w) + (normh` (-u1 .h w))))
18		opreq2 3969	. . . . . . . . . . . . . . . . 17 |- (z = (-u1 .h w) -> (w +h z) = (w +h (-u1 .h w)))
19	18	fveq2d 3728	. . . . . . . . . . . . . . . 16 |- (z = (-u1 .h w) -> (normh` (w +h z)) = (normh` (w +h (-u1 .h w))))
20	19	opreq2d 3976	. . . . . . . . . . . . . . 15 |- (z = (-u1 .h w) -> (x x. (normh` (w +h z))) = (x x. (normh` (w +h (-u1 .h w)))))
21	17, 20	breq12d 2631	. . . . . . . . . . . . . 14 |- (z = (-u1 .h w) -> (((normh` w) + (normh` z)) <_ (x x. (normh` (w +h z))) <-> ((normh` w) + (normh` (-u1 .h w))) <_ (x x. (normh` (w +h (-u1 .h w))))))
22	15, 21	rcla42v 1880	. . . . . . . . . . . . 13 |- ((w e. A /\ (-u1 .h w) e. B) -> (A.y e. A A.z e. B ((normh` y) + (normh` z)) <_ (x x. (normh` (y +h z))) -> ((normh` w) + (normh` (-u1 .h w))) <_ (x x. (normh` (w +h (-u1 .h w))))))
23	9, 22	syl 10	. . . . . . . . . . . 12 |- (w e. (A i^i B) -> (A.y e. A A.z e. B ((normh` y) + (normh` z)) <_ (x x. (normh` (y +h z))) -> ((normh` w) + (normh` (-u1 .h w))) <_ (x x. (normh` (w +h (-u1 .h w))))))
24	23	adantl 388	. . . . . . . . . . 11 |- ((x e. RR /\ w e. (A i^i B)) -> (A.y e. A A.z e. B ((normh` y) + (normh` z)) <_ (x x. (normh` (y +h z))) -> ((normh` w) + (normh` (-u1 .h w))) <_ (x x. (normh` (w +h (-u1 .h w))))))
25		normnegt 9011	. . . . . . . . . . . . . . . . 17 |- (w e. H~ -> (normh` (-u1 .h w)) = (normh` w))
26	25	opreq2d 3976	. . . . . . . . . . . . . . . 16 |- (w e. H~ -> ((normh` w) + (normh` (-u1 .h w))) = ((normh` w) + (normh` w)))
27		normclt 8991	. . . . . . . . . . . . . . . . . 18 |- (w e. H~ -> (normh` w) e. RR)
28	27	recnd 5315	. . . . . . . . . . . . . . . . 17 |- (w e. H~ -> (normh` w) e. CC)
29		2timest 6004	. . . . . . . . . . . . . . . . 17 |- ((normh` w) e. CC -> (2 x. (normh` w)) = ((normh` w) + (normh` w)))
30	28, 29	syl 10	. . . . . . . . . . . . . . . 16 |- (w e. H~ -> (2 x. (normh` w)) = ((normh` w) + (normh` w)))
31	26, 30	eqtr4d 1510	. . . . . . . . . . . . . . 15 |- (w e. H~ -> ((normh` w) + (normh` (-u1 .h w))) = (2 x. (normh` w)))
32	31	adantl 388	. . . . . . . . . . . . . 14 |- ((x e. RR /\ w e. H~) -> ((normh` w) + (normh` (-u1 .h w))) = (2 x. (normh` w)))
33		hvnegidt 8896	. . . . . . . . . . . . . . . . . . 19 |- (w e. H~ -> (w +h (-u1 .h w)) = 0h)
34	33	fveq2d 3728	. . . . . . . . . . . . . . . . . 18 |- (w e. H~ -> (normh` (w +h (-u1 .h w))) = (normh` 0h))
35		norm0 8995	. . . . . . . . . . . . . . . . . 18 |- (normh` 0h) = 0
36	34, 35	syl6eq 1523	. . . . . . . . . . . . . . . . 17 |- (w e. H~ -> (normh` (w +h (-u1 .h w))) = 0)
37	36	opreq2d 3976	. . . . . . . . . . . . . . . 16 |- (w e. H~ -> (x x. (normh` (w +h (-u1 .h w)))) = (x x. 0))
38		recnt 5313	. . . . . . . . . . . . . . . . 17 |- (x e. RR -> x e. CC)
39		mul01t 5443	. . . . . . . . . . . . . . . . 17 |- (x e. CC -> (x x. 0) = 0)
40	38, 39	syl 10	. . . . . . . . . . . . . . . 16 |- (x e. RR -> (x x. 0) = 0)
41	37, 40	sylan9eqr 1529	. . . . . . . . . . . . . . 15 |- ((x e. RR /\ w e. H~) -> (x x. (normh` (w +h (-u1 .h w)))) = 0)
42		2cn 5980	. . . . . . . . . . . . . . . 16 |- 2 e. CC
43	42	mul01 5431	. . . . . . . . . . . . . . 15 |- (2 x. 0) = 0
44	41, 43	syl6eqr 1525	. . . . . . . . . . . . . 14 |- ((x e. RR /\ w e. H~) -> (x x. (normh` (w +h (-u1 .h w)))) = (2 x. 0))
45	32, 44	breq12d 2631	. . . . . . . . . . . . 13 |- ((x e. RR /\ w e. H~) -> (((normh` w) + (normh` (-u1 .h w))) <_ (x x. (normh` (w +h (-u1 .h w)))) <-> (2 x. (normh` w)) <_ (2 x. 0)))
46		0re 5440	. . . . . . . . . . . . . . . . . 18 |- 0 e. RR
47		2re 5979	. . . . . . . . . . . . . . . . . 18 |- 2 e. RR
48		2pos 5989	. . . . . . . . . . . . . . . . . . 19 |- 0 < 2
49		lemul2t 5833	. . . . . . . . . . . . . . . . . . 19 |- ((((normh` w) e. RR /\ 0 e. RR /\ 2 e. RR) /\ 0 < 2) -> ((normh` w) <_ 0 <-> (2 x. (normh` w)) <_ (2 x. 0)))
50	48, 49	mpan2 696	. . . . . . . . . . . . . . . . . 18 |- (((normh` w) e. RR /\ 0 e. RR /\ 2 e. RR) -> ((normh` w) <_ 0 <-> (2 x. (normh` w)) <_ (2 x. 0)))
51	46, 47, 50	mp3an23 908	. . . . . . . . . . . . . . . . 17 |- ((normh` w) e. RR -> ((normh` w) <_ 0 <-> (2 x. (normh` w)) <_ (2 x. 0)))
52	27, 51	syl 10	. . . . . . . . . . . . . . . 16 |- (w e. H~ -> ((normh` w) <_ 0 <-> (2 x. (normh` w)) <_ (2 x. 0)))
53		normge0t 8992	. . . . . . . . . . . . . . . . 17 |- (w e. H~ -> 0 <_ (normh` w))
54	53	biantrud 726	. . . . . . . . . . . . . . . 16 |- (w e. H~ -> ((normh` w) <_ 0 <-> ((normh` w) <_ 0 /\ 0 <_ (normh` w))))
55	52, 54	bitr3d 530	. . . . . . . . . . . . . . 15 |- (w e. H~ -> ((2 x. (normh` w)) <_ (2 x. 0) <-> ((normh` w) <_ 0 /\ 0 <_ (normh` w))))
56		letri3t 5517	. . . . . . . . . . . . . . . . 17 |- (((normh` w) e. RR /\ 0 e. RR) -> ((normh` w) = 0 <-> ((normh` w) <_ 0 /\ 0 <_ (normh` w))))
57	46, 56	mpan2 696	. . . . . . . . . . . . . . . 16 |- ((normh` w) e. RR -> ((normh` w) = 0 <-> ((normh` w) <_ 0 /\ 0 <_ (normh` w))))
58	27, 57	syl 10	. . . . . . . . . . . . . . 15 |- (w e. H~ -> ((normh` w) = 0 <-> ((normh` w) <_ 0 /\ 0 <_ (normh` w))))
59		norm-it 8996	. . . . . . . . . . . . . . 15 |- (w e. H~ -> ((normh` w) = 0 <-> w = 0h))
60	55, 58, 59	3bitr2d 546	. . . . . . . . . . . . . 14 |- (w e. H~ -> ((2 x. (normh` w)) <_ (2 x. 0) <-> w = 0h))
61	60	adantl 388	. . . . . . . . . . . . 13 |- ((x e. RR /\ w e. H~) -> ((2 x. (normh` w)) <_ (2 x. 0) <-> w = 0h))
62	45, 61	bitrd 528	. . . . . . . . . . . 12 |- ((x e. RR /\ w e. H~) -> (((normh` w) + (normh` (-u1 .h w))) <_ (x x.