Theorem cdj3lem1

Description: A property of " A and B are completely disjoint subspaces." Part of Lemma 5 of Holland p. 1520. (Contributed by NM, 23-May-2005) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cdj1.1	|- A e. SH
	cdj1.2	|- B e. SH
Assertion	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 )

Proof

Step	Hyp	Ref	Expression
1		cdj1.1	|- A e. SH
2		cdj1.2	|- B e. SH
3		elin	|- ( w e. ( A i^i B ) <-> ( w e. A /\ w e. B ) )
4		neg1cn	|- -u 1 e. CC
5		shmulcl	|- ( ( B e. SH /\ -u 1 e. CC /\ w e. B ) -> ( -u 1 .h w ) e. B )
6	2 4 5	mp3an12	|- ( w e. B -> ( -u 1 .h w ) e. B )
7	6	anim2i	|- ( ( w e. A /\ w e. B ) -> ( w e. A /\ ( -u 1 .h w ) e. B ) )
8	3 7	sylbi	|- ( w e. ( A i^i B ) -> ( w e. A /\ ( -u 1 .h w ) e. B ) )
9		fveq2	|- ( y = w -> ( normh ` y ) = ( normh ` w ) )
10	9	oveq1d	|- ( y = w -> ( ( normh ` y ) + ( normh ` z ) ) = ( ( normh ` w ) + ( normh ` z ) ) )
11		fvoveq1	|- ( y = w -> ( normh ` ( y +h z ) ) = ( normh ` ( w +h z ) ) )
12	11	oveq2d	|- ( y = w -> ( x x. ( normh ` ( y +h z ) ) ) = ( x x. ( normh ` ( w +h z ) ) ) )
13	10 12	breq12d	|- ( y = w -> ( ( ( normh ` y ) + ( normh ` z ) ) <_ ( x x. ( normh ` ( y +h z ) ) ) <-> ( ( normh ` w ) + ( normh ` z ) ) <_ ( x x. ( normh ` ( w +h z ) ) ) ) )
14		fveq2	|- ( z = ( -u 1 .h w ) -> ( normh ` z ) = ( normh ` ( -u 1 .h w ) ) )
15	14	oveq2d	|- ( z = ( -u 1 .h w ) -> ( ( normh ` w ) + ( normh ` z ) ) = ( ( normh ` w ) + ( normh ` ( -u 1 .h w ) ) ) )
16		oveq2	|- ( z = ( -u 1 .h w ) -> ( w +h z ) = ( w +h ( -u 1 .h w ) ) )
17	16	fveq2d	|- ( z = ( -u 1 .h w ) -> ( normh ` ( w +h z ) ) = ( normh ` ( w +h ( -u 1 .h w ) ) ) )
18	17	oveq2d	|- ( z = ( -u 1 .h w ) -> ( x x. ( normh ` ( w +h z ) ) ) = ( x x. ( normh ` ( w +h ( -u 1 .h w ) ) ) ) )
19	15 18	breq12d	|- ( z = ( -u 1 .h w ) -> ( ( ( normh ` w ) + ( normh ` z ) ) <_ ( x x. ( normh ` ( w +h z ) ) ) <-> ( ( normh ` w ) + ( normh ` ( -u 1 .h w ) ) ) <_ ( x x. ( normh ` ( w +h ( -u 1 .h w ) ) ) ) ) )
20	13 19	rspc2v	|- ( ( w e. A /\ ( -u 1 .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 ` ( -u 1 .h w ) ) ) <_ ( x x. ( normh ` ( w +h ( -u 1 .h w ) ) ) ) ) )
21	8 20	syl	|- ( 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 ` ( -u 1 .h w ) ) ) <_ ( x x. ( normh ` ( w +h ( -u 1 .h w ) ) ) ) ) )
22	21	adantl	|- ( ( 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 ` ( -u 1 .h w ) ) ) <_ ( x x. ( normh ` ( w +h ( -u 1 .h w ) ) ) ) ) )
23	1 2	shincli	|- ( A i^i B ) e. SH
24	23	sheli	|- ( w e. ( A i^i B ) -> w e. ~H )
25		normneg	|- ( w e. ~H -> ( normh ` ( -u 1 .h w ) ) = ( normh ` w ) )
26	25	oveq2d	|- ( w e. ~H -> ( ( normh ` w ) + ( normh ` ( -u 1 .h w ) ) ) = ( ( normh ` w ) + ( normh ` w ) ) )
27		normcl	|- ( w e. ~H -> ( normh ` w ) e. RR )
28	27	recnd	|- ( w e. ~H -> ( normh ` w ) e. CC )
29	28	2timesd	|- ( w e. ~H -> ( 2 x. ( normh ` w ) ) = ( ( normh ` w ) + ( normh ` w ) ) )
30	26 29	eqtr4d	|- ( w e. ~H -> ( ( normh ` w ) + ( normh ` ( -u 1 .h w ) ) ) = ( 2 x. ( normh ` w ) ) )
31	30	adantl	|- ( ( x e. RR /\ w e. ~H ) -> ( ( normh ` w ) + ( normh ` ( -u 1 .h w ) ) ) = ( 2 x. ( normh ` w ) ) )
32		hvnegid	|- ( w e. ~H -> ( w +h ( -u 1 .h w ) ) = 0h )
33	32	fveq2d	|- ( w e. ~H -> ( normh ` ( w +h ( -u 1 .h w ) ) ) = ( normh ` 0h ) )
34		norm0	|- ( normh ` 0h ) = 0
35	33 34	eqtrdi	|- ( w e. ~H -> ( normh ` ( w +h ( -u 1 .h w ) ) ) = 0 )
36	35	oveq2d	|- ( w e. ~H -> ( x x. ( normh ` ( w +h ( -u 1 .h w ) ) ) ) = ( x x. 0 ) )
37		recn	|- ( x e. RR -> x e. CC )
38	37	mul01d	|- ( x e. RR -> ( x x. 0 ) = 0 )
39	36 38	sylan9eqr	|- ( ( x e. RR /\ w e. ~H ) -> ( x x. ( normh ` ( w +h ( -u 1 .h w ) ) ) ) = 0 )
40		2t0e0	|- ( 2 x. 0 ) = 0
41	39 40	eqtr4di	|- ( ( x e. RR /\ w e. ~H ) -> ( x x. ( normh ` ( w +h ( -u 1 .h w ) ) ) ) = ( 2 x. 0 ) )
42	31 41	breq12d	|- ( ( x e. RR /\ w e. ~H ) -> ( ( ( normh ` w ) + ( normh ` ( -u 1 .h w ) ) ) <_ ( x x. ( normh ` ( w +h ( -u 1 .h w ) ) ) ) <-> ( 2 x. ( normh ` w ) ) <_ ( 2 x. 0 ) ) )
43		0re	|- 0 e. RR
44		letri3	|- ( ( ( normh ` w ) e. RR /\ 0 e. RR ) -> ( ( normh ` w ) = 0 <-> ( ( normh ` w ) <_ 0 /\ 0 <_ ( normh ` w ) ) ) )
45	27 43 44	sylancl	|- ( w e. ~H -> ( ( normh ` w ) = 0 <-> ( ( normh ` w ) <_ 0 /\ 0 <_ ( normh ` w ) ) ) )
46		normge0	|- ( w e. ~H -> 0 <_ ( normh ` w ) )
47	46	biantrud	|- ( w e. ~H -> ( ( normh ` w ) <_ 0 <-> ( ( normh ` w ) <_ 0 /\ 0 <_ ( normh ` w ) ) ) )
48		2re	|- 2 e. RR
49		2pos	|- 0 < 2
50	48 49	pm3.2i	|- ( 2 e. RR /\ 0 < 2 )
51		lemul2	|- ( ( ( normh ` w ) e. RR /\ 0 e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( normh ` w ) <_ 0 <-> ( 2 x. ( normh ` w ) ) <_ ( 2 x. 0 ) ) )
52	43 50 51	mp3an23	|- ( ( normh ` w ) e. RR -> ( ( normh ` w ) <_ 0 <-> ( 2 x. ( normh ` w ) ) <_ ( 2 x. 0 ) ) )
53	27 52	syl	|- ( w e. ~H -> ( ( normh ` w ) <_ 0 <-> ( 2 x. ( normh ` w ) ) <_ ( 2 x. 0 ) ) )
54	45 47 53	3bitr2rd	|- ( w e. ~H -> ( ( 2 x. ( normh ` w ) ) <_ ( 2 x. 0 ) <-> ( normh ` w ) = 0 ) )
55		norm-i	|- ( w e. ~H -> ( ( normh ` w ) = 0 <-> w = 0h ) )
56	54 55	bitrd	|- ( w e. ~H -> ( ( 2 x. ( normh ` w ) ) <_ ( 2 x. 0 ) <-> w = 0h ) )
57	56	adantl	|- ( ( x e. RR /\ w e. ~H ) -> ( ( 2 x. ( normh ` w ) ) <_ ( 2 x. 0 ) <-> w = 0h ) )
58	42 57	bitrd	|- ( ( x e. RR /\ w e. ~H ) -> ( ( ( normh ` w ) + ( normh ` ( -u 1 .h w ) ) ) <_ ( x x. ( normh ` ( w +h ( -u 1 .h w ) ) ) ) <-> w = 0h ) )
59	24 58	sylan2	|- ( ( x e. RR /\ w e. ( A i^i B ) ) -> ( ( ( normh ` w ) + ( normh ` ( -u 1 .h w ) ) ) <_ ( x x. ( normh ` ( w +h ( -u 1 .h w ) ) ) ) <-> w = 0h ) )
60	22 59	sylibd	|- ( ( 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 ) ) ) -> w = 0h ) )
61	60	impancom	|- ( ( x e. RR /\ A. y e. A A. z e. B ( ( normh ` y ) + ( normh ` z ) ) <_ ( x x. ( normh ` ( y +h z ) ) ) ) -> ( w e. ( A i^i B ) -> w = 0h ) )
62		elch0	|- ( w e. 0H <-> w = 0h )
63	61 62	imbitrrdi	|- ( ( x e. RR /\ A. y e. A A. z e. B ( ( normh ` y ) + ( normh ` z ) ) <_ ( x x. ( normh ` ( y +h z ) ) ) ) -> ( w e. ( A i^i B ) -> w e. 0H ) )
64	63	ssrdv	|- ( ( x e. RR /\ A. y e. A A. z e. B ( ( normh ` y ) + ( normh ` z ) ) <_ ( x x. ( normh ` ( y +h z ) ) ) ) -> ( A i^i B ) C_ 0H )
65	64	ex	|- ( x e. RR -> ( A. y e. A A. z e. B ( ( normh ` y ) + ( normh ` z ) ) <_ ( x x. ( normh ` ( y +h z ) ) ) -> ( A i^i B ) C_ 0H ) )
66		shle0	|- ( ( A i^i B ) e. SH -> ( ( A i^i B ) C_ 0H <-> ( A i^i B ) = 0H ) )
67	23 66	ax-mp	|- ( ( A i^i B ) C_ 0H <-> ( A i^i B ) = 0H )
68	65 67	imbitrdi	|- ( x e. RR -> ( A. y e. A A. z e. B ( ( normh ` y ) + ( normh ` z ) ) <_ ( x x. ( normh ` ( y +h z ) ) ) -> ( A i^i B ) = 0H ) )
69	68	adantld	|- ( 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 ) )
70	69	rexlimiv	|- ( 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 )