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	⊢ 𝐴 ∈ Sℋ
	cdj1.2	⊢ 𝐵 ∈ Sℋ
Assertion	cdj3lem1	⊢ ( ∃ 𝑥 ∈ ℝ ( 0 < 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑧 ) ) ≤ ( 𝑥 · ( normℎ ‘ ( 𝑦 +ℎ 𝑧 ) ) ) ) → ( 𝐴 ∩ 𝐵 ) = 0ℋ )

Proof

Step	Hyp	Ref	Expression
1		cdj1.1	⊢ 𝐴 ∈ Sℋ
2		cdj1.2	⊢ 𝐵 ∈ Sℋ
3		elin	⊢ ( 𝑤 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑤 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) )
4		neg1cn	⊢ - 1 ∈ ℂ
5		shmulcl	⊢ ( ( 𝐵 ∈ Sℋ ∧ - 1 ∈ ℂ ∧ 𝑤 ∈ 𝐵 ) → ( - 1 ·ℎ 𝑤 ) ∈ 𝐵 )
6	2 4 5	mp3an12	⊢ ( 𝑤 ∈ 𝐵 → ( - 1 ·ℎ 𝑤 ) ∈ 𝐵 )
7	6	anim2i	⊢ ( ( 𝑤 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) → ( 𝑤 ∈ 𝐴 ∧ ( - 1 ·ℎ 𝑤 ) ∈ 𝐵 ) )
8	3 7	sylbi	⊢ ( 𝑤 ∈ ( 𝐴 ∩ 𝐵 ) → ( 𝑤 ∈ 𝐴 ∧ ( - 1 ·ℎ 𝑤 ) ∈ 𝐵 ) )
9		fveq2	⊢ ( 𝑦 = 𝑤 → ( normℎ ‘ 𝑦 ) = ( normℎ ‘ 𝑤 ) )
10	9	oveq1d	⊢ ( 𝑦 = 𝑤 → ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑧 ) ) = ( ( normℎ ‘ 𝑤 ) + ( normℎ ‘ 𝑧 ) ) )
11		fvoveq1	⊢ ( 𝑦 = 𝑤 → ( normℎ ‘ ( 𝑦 +ℎ 𝑧 ) ) = ( normℎ ‘ ( 𝑤 +ℎ 𝑧 ) ) )
12	11	oveq2d	⊢ ( 𝑦 = 𝑤 → ( 𝑥 · ( normℎ ‘ ( 𝑦 +ℎ 𝑧 ) ) ) = ( 𝑥 · ( normℎ ‘ ( 𝑤 +ℎ 𝑧 ) ) ) )
13	10 12	breq12d	⊢ ( 𝑦 = 𝑤 → ( ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑧 ) ) ≤ ( 𝑥 · ( normℎ ‘ ( 𝑦 +ℎ 𝑧 ) ) ) ↔ ( ( normℎ ‘ 𝑤 ) + ( normℎ ‘ 𝑧 ) ) ≤ ( 𝑥 · ( normℎ ‘ ( 𝑤 +ℎ 𝑧 ) ) ) ) )
14		fveq2	⊢ ( 𝑧 = ( - 1 ·ℎ 𝑤 ) → ( normℎ ‘ 𝑧 ) = ( normℎ ‘ ( - 1 ·ℎ 𝑤 ) ) )
15	14	oveq2d	⊢ ( 𝑧 = ( - 1 ·ℎ 𝑤 ) → ( ( normℎ ‘ 𝑤 ) + ( normℎ ‘ 𝑧 ) ) = ( ( normℎ ‘ 𝑤 ) + ( normℎ ‘ ( - 1 ·ℎ 𝑤 ) ) ) )
16		oveq2	⊢ ( 𝑧 = ( - 1 ·ℎ 𝑤 ) → ( 𝑤 +ℎ 𝑧 ) = ( 𝑤 +ℎ ( - 1 ·ℎ 𝑤 ) ) )
17	16	fveq2d	⊢ ( 𝑧 = ( - 1 ·ℎ 𝑤 ) → ( normℎ ‘ ( 𝑤 +ℎ 𝑧 ) ) = ( normℎ ‘ ( 𝑤 +ℎ ( - 1 ·ℎ 𝑤 ) ) ) )
18	17	oveq2d	⊢ ( 𝑧 = ( - 1 ·ℎ 𝑤 ) → ( 𝑥 · ( normℎ ‘ ( 𝑤 +ℎ 𝑧 ) ) ) = ( 𝑥 · ( normℎ ‘ ( 𝑤 +ℎ ( - 1 ·ℎ 𝑤 ) ) ) ) )
19	15 18	breq12d	⊢ ( 𝑧 = ( - 1 ·ℎ 𝑤 ) → ( ( ( normℎ ‘ 𝑤 ) + ( normℎ ‘ 𝑧 ) ) ≤ ( 𝑥 · ( normℎ ‘ ( 𝑤 +ℎ 𝑧 ) ) ) ↔ ( ( normℎ ‘ 𝑤 ) + ( normℎ ‘ ( - 1 ·ℎ 𝑤 ) ) ) ≤ ( 𝑥 · ( normℎ ‘ ( 𝑤 +ℎ ( - 1 ·ℎ 𝑤 ) ) ) ) ) )
20	13 19	rspc2v	⊢ ( ( 𝑤 ∈ 𝐴 ∧ ( - 1 ·ℎ 𝑤 ) ∈ 𝐵 ) → ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑧 ) ) ≤ ( 𝑥 · ( normℎ ‘ ( 𝑦 +ℎ 𝑧 ) ) ) → ( ( normℎ ‘ 𝑤 ) + ( normℎ ‘ ( - 1 ·ℎ 𝑤 ) ) ) ≤ ( 𝑥 · ( normℎ ‘ ( 𝑤 +ℎ ( - 1 ·ℎ 𝑤 ) ) ) ) ) )
21	8 20	syl	⊢ ( 𝑤 ∈ ( 𝐴 ∩ 𝐵 ) → ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑧 ) ) ≤ ( 𝑥 · ( normℎ ‘ ( 𝑦 +ℎ 𝑧 ) ) ) → ( ( normℎ ‘ 𝑤 ) + ( normℎ ‘ ( - 1 ·ℎ 𝑤 ) ) ) ≤ ( 𝑥 · ( normℎ ‘ ( 𝑤 +ℎ ( - 1 ·ℎ 𝑤 ) ) ) ) ) )
22	21	adantl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ ( 𝐴 ∩ 𝐵 ) ) → ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑧 ) ) ≤ ( 𝑥 · ( normℎ ‘ ( 𝑦 +ℎ 𝑧 ) ) ) → ( ( normℎ ‘ 𝑤 ) + ( normℎ ‘ ( - 1 ·ℎ 𝑤 ) ) ) ≤ ( 𝑥 · ( normℎ ‘ ( 𝑤 +ℎ ( - 1 ·ℎ 𝑤 ) ) ) ) ) )
23	1 2	shincli	⊢ ( 𝐴 ∩ 𝐵 ) ∈ Sℋ
24	23	sheli	⊢ ( 𝑤 ∈ ( 𝐴 ∩ 𝐵 ) → 𝑤 ∈ ℋ )
25		normneg	⊢ ( 𝑤 ∈ ℋ → ( normℎ ‘ ( - 1 ·ℎ 𝑤 ) ) = ( normℎ ‘ 𝑤 ) )
26	25	oveq2d	⊢ ( 𝑤 ∈ ℋ → ( ( normℎ ‘ 𝑤 ) + ( normℎ ‘ ( - 1 ·ℎ 𝑤 ) ) ) = ( ( normℎ ‘ 𝑤 ) + ( normℎ ‘ 𝑤 ) ) )
27		normcl	⊢ ( 𝑤 ∈ ℋ → ( normℎ ‘ 𝑤 ) ∈ ℝ )
28	27	recnd	⊢ ( 𝑤 ∈ ℋ → ( normℎ ‘ 𝑤 ) ∈ ℂ )
29	28	2timesd	⊢ ( 𝑤 ∈ ℋ → ( 2 · ( normℎ ‘ 𝑤 ) ) = ( ( normℎ ‘ 𝑤 ) + ( normℎ ‘ 𝑤 ) ) )
30	26 29	eqtr4d	⊢ ( 𝑤 ∈ ℋ → ( ( normℎ ‘ 𝑤 ) + ( normℎ ‘ ( - 1 ·ℎ 𝑤 ) ) ) = ( 2 · ( normℎ ‘ 𝑤 ) ) )
31	30	adantl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ ℋ ) → ( ( normℎ ‘ 𝑤 ) + ( normℎ ‘ ( - 1 ·ℎ 𝑤 ) ) ) = ( 2 · ( normℎ ‘ 𝑤 ) ) )
32		hvnegid	⊢ ( 𝑤 ∈ ℋ → ( 𝑤 +ℎ ( - 1 ·ℎ 𝑤 ) ) = 0ℎ )
33	32	fveq2d	⊢ ( 𝑤 ∈ ℋ → ( normℎ ‘ ( 𝑤 +ℎ ( - 1 ·ℎ 𝑤 ) ) ) = ( normℎ ‘ 0ℎ ) )
34		norm0	⊢ ( normℎ ‘ 0ℎ ) = 0
35	33 34	eqtrdi	⊢ ( 𝑤 ∈ ℋ → ( normℎ ‘ ( 𝑤 +ℎ ( - 1 ·ℎ 𝑤 ) ) ) = 0 )
36	35	oveq2d	⊢ ( 𝑤 ∈ ℋ → ( 𝑥 · ( normℎ ‘ ( 𝑤 +ℎ ( - 1 ·ℎ 𝑤 ) ) ) ) = ( 𝑥 · 0 ) )
37		recn	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
38	37	mul01d	⊢ ( 𝑥 ∈ ℝ → ( 𝑥 · 0 ) = 0 )
39	36 38	sylan9eqr	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ ℋ ) → ( 𝑥 · ( normℎ ‘ ( 𝑤 +ℎ ( - 1 ·ℎ 𝑤 ) ) ) ) = 0 )
40		2t0e0	⊢ ( 2 · 0 ) = 0
41	39 40	eqtr4di	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ ℋ ) → ( 𝑥 · ( normℎ ‘ ( 𝑤 +ℎ ( - 1 ·ℎ 𝑤 ) ) ) ) = ( 2 · 0 ) )
42	31 41	breq12d	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ ℋ ) → ( ( ( normℎ ‘ 𝑤 ) + ( normℎ ‘ ( - 1 ·ℎ 𝑤 ) ) ) ≤ ( 𝑥 · ( normℎ ‘ ( 𝑤 +ℎ ( - 1 ·ℎ 𝑤 ) ) ) ) ↔ ( 2 · ( normℎ ‘ 𝑤 ) ) ≤ ( 2 · 0 ) ) )
43		0re	⊢ 0 ∈ ℝ
44		letri3	⊢ ( ( ( normℎ ‘ 𝑤 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( normℎ ‘ 𝑤 ) = 0 ↔ ( ( normℎ ‘ 𝑤 ) ≤ 0 ∧ 0 ≤ ( normℎ ‘ 𝑤 ) ) ) )
45	27 43 44	sylancl	⊢ ( 𝑤 ∈ ℋ → ( ( normℎ ‘ 𝑤 ) = 0 ↔ ( ( normℎ ‘ 𝑤 ) ≤ 0 ∧ 0 ≤ ( normℎ ‘ 𝑤 ) ) ) )
46		normge0	⊢ ( 𝑤 ∈ ℋ → 0 ≤ ( normℎ ‘ 𝑤 ) )
47	46	biantrud	⊢ ( 𝑤 ∈ ℋ → ( ( normℎ ‘ 𝑤 ) ≤ 0 ↔ ( ( normℎ ‘ 𝑤 ) ≤ 0 ∧ 0 ≤ ( normℎ ‘ 𝑤 ) ) ) )
48		2re	⊢ 2 ∈ ℝ
49		2pos	⊢ 0 < 2
50	48 49	pm3.2i	⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
51		lemul2	⊢ ( ( ( normℎ ‘ 𝑤 ) ∈ ℝ ∧ 0 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( normℎ ‘ 𝑤 ) ≤ 0 ↔ ( 2 · ( normℎ ‘ 𝑤 ) ) ≤ ( 2 · 0 ) ) )
52	43 50 51	mp3an23	⊢ ( ( normℎ ‘ 𝑤 ) ∈ ℝ → ( ( normℎ ‘ 𝑤 ) ≤ 0 ↔ ( 2 · ( normℎ ‘ 𝑤 ) ) ≤ ( 2 · 0 ) ) )
53	27 52	syl	⊢ ( 𝑤 ∈ ℋ → ( ( normℎ ‘ 𝑤 ) ≤ 0 ↔ ( 2 · ( normℎ ‘ 𝑤 ) ) ≤ ( 2 · 0 ) ) )
54	45 47 53	3bitr2rd	⊢ ( 𝑤 ∈ ℋ → ( ( 2 · ( normℎ ‘ 𝑤 ) ) ≤ ( 2 · 0 ) ↔ ( normℎ ‘ 𝑤 ) = 0 ) )
55		norm-i	⊢ ( 𝑤 ∈ ℋ → ( ( normℎ ‘ 𝑤 ) = 0 ↔ 𝑤 = 0ℎ ) )
56	54 55	bitrd	⊢ ( 𝑤 ∈ ℋ → ( ( 2 · ( normℎ ‘ 𝑤 ) ) ≤ ( 2 · 0 ) ↔ 𝑤 = 0ℎ ) )
57	56	adantl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ ℋ ) → ( ( 2 · ( normℎ ‘ 𝑤 ) ) ≤ ( 2 · 0 ) ↔ 𝑤 = 0ℎ ) )
58	42 57	bitrd	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ ℋ ) → ( ( ( normℎ ‘ 𝑤 ) + ( normℎ ‘ ( - 1 ·ℎ 𝑤 ) ) ) ≤ ( 𝑥 · ( normℎ ‘ ( 𝑤 +ℎ ( - 1 ·ℎ 𝑤 ) ) ) ) ↔ 𝑤 = 0ℎ ) )
59	24 58	sylan2	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ ( 𝐴 ∩ 𝐵 ) ) → ( ( ( normℎ ‘ 𝑤 ) + ( normℎ ‘ ( - 1 ·ℎ 𝑤 ) ) ) ≤ ( 𝑥 · ( normℎ ‘ ( 𝑤 +ℎ ( - 1 ·ℎ 𝑤 ) ) ) ) ↔ 𝑤 = 0ℎ ) )
60	22 59	sylibd	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ ( 𝐴 ∩ 𝐵 ) ) → ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑧 ) ) ≤ ( 𝑥 · ( normℎ ‘ ( 𝑦 +ℎ 𝑧 ) ) ) → 𝑤 = 0ℎ ) )
61	60	impancom	⊢ ( ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑧 ) ) ≤ ( 𝑥 · ( normℎ ‘ ( 𝑦 +ℎ 𝑧 ) ) ) ) → ( 𝑤 ∈ ( 𝐴 ∩ 𝐵 ) → 𝑤 = 0ℎ ) )
62		elch0	⊢ ( 𝑤 ∈ 0ℋ ↔ 𝑤 = 0ℎ )
63	61 62	imbitrrdi	⊢ ( ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑧 ) ) ≤ ( 𝑥 · ( normℎ ‘ ( 𝑦 +ℎ 𝑧 ) ) ) ) → ( 𝑤 ∈ ( 𝐴 ∩ 𝐵 ) → 𝑤 ∈ 0ℋ ) )
64	63	ssrdv	⊢ ( ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑧 ) ) ≤ ( 𝑥 · ( normℎ ‘ ( 𝑦 +ℎ 𝑧 ) ) ) ) → ( 𝐴 ∩ 𝐵 ) ⊆ 0ℋ )
65	64	ex	⊢ ( 𝑥 ∈ ℝ → ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑧 ) ) ≤ ( 𝑥 · ( normℎ ‘ ( 𝑦 +ℎ 𝑧 ) ) ) → ( 𝐴 ∩ 𝐵 ) ⊆ 0ℋ ) )
66		shle0	⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ Sℋ → ( ( 𝐴 ∩ 𝐵 ) ⊆ 0ℋ ↔ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) )
67	23 66	ax-mp	⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ 0ℋ ↔ ( 𝐴 ∩ 𝐵 ) = 0ℋ )
68	65 67	imbitrdi	⊢ ( 𝑥 ∈ ℝ → ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑧 ) ) ≤ ( 𝑥 · ( normℎ ‘ ( 𝑦 +ℎ 𝑧 ) ) ) → ( 𝐴 ∩ 𝐵 ) = 0ℋ ) )
69	68	adantld	⊢ ( 𝑥 ∈ ℝ → ( ( 0 < 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑧 ) ) ≤ ( 𝑥 · ( normℎ ‘ ( 𝑦 +ℎ 𝑧 ) ) ) ) → ( 𝐴 ∩ 𝐵 ) = 0ℋ ) )
70	69	rexlimiv	⊢ ( ∃ 𝑥 ∈ ℝ ( 0 < 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑧 ) ) ≤ ( 𝑥 · ( normℎ ‘ ( 𝑦 +ℎ 𝑧 ) ) ) ) → ( 𝐴 ∩ 𝐵 ) = 0ℋ )