Theorem cdj1i

Description: Two ways to express " A and B are completely disjoint subspaces." (1) => (2) in Lemma 5 of Holland p. 1520. (Contributed by NM, 21-May-2005) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cdj1.1	⊢ 𝐴 ∈ Sℋ
	cdj1.2	⊢ 𝐵 ∈ Sℋ
Assertion	cdj1i	⊢ ( ∃ 𝑤 ∈ ℝ ( 0 < 𝑤 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) ) → ∃ 𝑥 ∈ ℝ ( 0 < 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) = 1 → 𝑥 ≤ ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cdj1.1	⊢ 𝐴 ∈ Sℋ
2		cdj1.2	⊢ 𝐵 ∈ Sℋ
3		gt0ne0	⊢ ( ( 𝑤 ∈ ℝ ∧ 0 < 𝑤 ) → 𝑤 ≠ 0 )
4		rereccl	⊢ ( ( 𝑤 ∈ ℝ ∧ 𝑤 ≠ 0 ) → ( 1 / 𝑤 ) ∈ ℝ )
5	3 4	syldan	⊢ ( ( 𝑤 ∈ ℝ ∧ 0 < 𝑤 ) → ( 1 / 𝑤 ) ∈ ℝ )
6	5	adantrr	⊢ ( ( 𝑤 ∈ ℝ ∧ ( 0 < 𝑤 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) ) ) → ( 1 / 𝑤 ) ∈ ℝ )
7		recgt0	⊢ ( ( 𝑤 ∈ ℝ ∧ 0 < 𝑤 ) → 0 < ( 1 / 𝑤 ) )
8	7	adantrr	⊢ ( ( 𝑤 ∈ ℝ ∧ ( 0 < 𝑤 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) ) ) → 0 < ( 1 / 𝑤 ) )
9		1red	⊢ ( ( ( ( 𝑤 ∈ ℝ ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( ∀ 𝑣 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) ∧ ( normℎ ‘ 𝑦 ) = 1 ) ) → 1 ∈ ℝ )
10		1re	⊢ 1 ∈ ℝ
11		neg1cn	⊢ - 1 ∈ ℂ
12	2	sheli	⊢ ( 𝑧 ∈ 𝐵 → 𝑧 ∈ ℋ )
13		hvmulcl	⊢ ( ( - 1 ∈ ℂ ∧ 𝑧 ∈ ℋ ) → ( - 1 ·ℎ 𝑧 ) ∈ ℋ )
14	11 12 13	sylancr	⊢ ( 𝑧 ∈ 𝐵 → ( - 1 ·ℎ 𝑧 ) ∈ ℋ )
15		normcl	⊢ ( ( - 1 ·ℎ 𝑧 ) ∈ ℋ → ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) ∈ ℝ )
16	14 15	syl	⊢ ( 𝑧 ∈ 𝐵 → ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) ∈ ℝ )
17	16	adantl	⊢ ( ( ( 𝑤 ∈ ℝ ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) → ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) ∈ ℝ )
18		readdcl	⊢ ( ( 1 ∈ ℝ ∧ ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) ∈ ℝ ) → ( 1 + ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) ) ∈ ℝ )
19	10 17 18	sylancr	⊢ ( ( ( 𝑤 ∈ ℝ ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) → ( 1 + ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) ) ∈ ℝ )
20	19	adantr	⊢ ( ( ( ( 𝑤 ∈ ℝ ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( ∀ 𝑣 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) ∧ ( normℎ ‘ 𝑦 ) = 1 ) ) → ( 1 + ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) ) ∈ ℝ )
21	1	sheli	⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ℋ )
22		hvsubcl	⊢ ( ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( 𝑦 −ℎ 𝑧 ) ∈ ℋ )
23	21 12 22	syl2an	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑦 −ℎ 𝑧 ) ∈ ℋ )
24		normcl	⊢ ( ( 𝑦 −ℎ 𝑧 ) ∈ ℋ → ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ∈ ℝ )
25	23 24	syl	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ∈ ℝ )
26		remulcl	⊢ ( ( 𝑤 ∈ ℝ ∧ ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ∈ ℝ ) → ( 𝑤 · ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) ∈ ℝ )
27	25 26	sylan2	⊢ ( ( 𝑤 ∈ ℝ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑤 · ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) ∈ ℝ )
28	27	anassrs	⊢ ( ( ( 𝑤 ∈ ℝ ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑤 · ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) ∈ ℝ )
29	28	adantr	⊢ ( ( ( ( 𝑤 ∈ ℝ ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( ∀ 𝑣 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) ∧ ( normℎ ‘ 𝑦 ) = 1 ) ) → ( 𝑤 · ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) ∈ ℝ )
30		normge0	⊢ ( ( - 1 ·ℎ 𝑧 ) ∈ ℋ → 0 ≤ ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) )
31	14 30	syl	⊢ ( 𝑧 ∈ 𝐵 → 0 ≤ ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) )
32		addge01	⊢ ( ( 1 ∈ ℝ ∧ ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) ∈ ℝ ) → ( 0 ≤ ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) ↔ 1 ≤ ( 1 + ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) ) ) )
33	10 32	mpan	⊢ ( ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) ∈ ℝ → ( 0 ≤ ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) ↔ 1 ≤ ( 1 + ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) ) ) )
34	33	biimpa	⊢ ( ( ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) ∈ ℝ ∧ 0 ≤ ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) ) → 1 ≤ ( 1 + ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) ) )
35	16 31 34	syl2anc	⊢ ( 𝑧 ∈ 𝐵 → 1 ≤ ( 1 + ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) ) )
36	35	ad2antlr	⊢ ( ( ( ( 𝑤 ∈ ℝ ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( ∀ 𝑣 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) ∧ ( normℎ ‘ 𝑦 ) = 1 ) ) → 1 ≤ ( 1 + ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) ) )
37		shmulcl	⊢ ( ( 𝐵 ∈ Sℋ ∧ - 1 ∈ ℂ ∧ 𝑧 ∈ 𝐵 ) → ( - 1 ·ℎ 𝑧 ) ∈ 𝐵 )
38	2 11 37	mp3an12	⊢ ( 𝑧 ∈ 𝐵 → ( - 1 ·ℎ 𝑧 ) ∈ 𝐵 )
39		fveq2	⊢ ( 𝑣 = ( - 1 ·ℎ 𝑧 ) → ( normℎ ‘ 𝑣 ) = ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) )
40	39	oveq2d	⊢ ( 𝑣 = ( - 1 ·ℎ 𝑧 ) → ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) = ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) ) )
41		oveq2	⊢ ( 𝑣 = ( - 1 ·ℎ 𝑧 ) → ( 𝑦 +ℎ 𝑣 ) = ( 𝑦 +ℎ ( - 1 ·ℎ 𝑧 ) ) )
42	41	fveq2d	⊢ ( 𝑣 = ( - 1 ·ℎ 𝑧 ) → ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) = ( normℎ ‘ ( 𝑦 +ℎ ( - 1 ·ℎ 𝑧 ) ) ) )
43	42	oveq2d	⊢ ( 𝑣 = ( - 1 ·ℎ 𝑧 ) → ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) = ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ ( - 1 ·ℎ 𝑧 ) ) ) ) )
44	40 43	breq12d	⊢ ( 𝑣 = ( - 1 ·ℎ 𝑧 ) → ( ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) ↔ ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ ( - 1 ·ℎ 𝑧 ) ) ) ) ) )
45	44	rspcv	⊢ ( ( - 1 ·ℎ 𝑧 ) ∈ 𝐵 → ( ∀ 𝑣 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) → ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ ( - 1 ·ℎ 𝑧 ) ) ) ) ) )
46	38 45	syl	⊢ ( 𝑧 ∈ 𝐵 → ( ∀ 𝑣 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) → ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ ( - 1 ·ℎ 𝑧 ) ) ) ) ) )
47	46	imp	⊢ ( ( 𝑧 ∈ 𝐵 ∧ ∀ 𝑣 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) ) → ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ ( - 1 ·ℎ 𝑧 ) ) ) ) )
48	47	ad2ant2lr	⊢ ( ( ( ( 𝑤 ∈ ℝ ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( ∀ 𝑣 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) ∧ ( normℎ ‘ 𝑦 ) = 1 ) ) → ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ ( - 1 ·ℎ 𝑧 ) ) ) ) )
49		oveq1	⊢ ( 1 = ( normℎ ‘ 𝑦 ) → ( 1 + ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) ) = ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) ) )
50	49	eqcoms	⊢ ( ( normℎ ‘ 𝑦 ) = 1 → ( 1 + ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) ) = ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) ) )
51	50	ad2antll	⊢ ( ( ( ( 𝑤 ∈ ℝ ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( ∀ 𝑣 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) ∧ ( normℎ ‘ 𝑦 ) = 1 ) ) → ( 1 + ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) ) = ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) ) )
52		hvsubval	⊢ ( ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( 𝑦 −ℎ 𝑧 ) = ( 𝑦 +ℎ ( - 1 ·ℎ 𝑧 ) ) )
53	21 12 52	syl2an	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑦 −ℎ 𝑧 ) = ( 𝑦 +ℎ ( - 1 ·ℎ 𝑧 ) ) )
54	53	fveq2d	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) = ( normℎ ‘ ( 𝑦 +ℎ ( - 1 ·ℎ 𝑧 ) ) ) )
55	54	oveq2d	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑤 · ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) = ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ ( - 1 ·ℎ 𝑧 ) ) ) ) )
56	55	adantll	⊢ ( ( ( 𝑤 ∈ ℝ ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑤 · ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) = ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ ( - 1 ·ℎ 𝑧 ) ) ) ) )
57	56	adantr	⊢ ( ( ( ( 𝑤 ∈ ℝ ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( ∀ 𝑣 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) ∧ ( normℎ ‘ 𝑦 ) = 1 ) ) → ( 𝑤 · ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) = ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ ( - 1 ·ℎ 𝑧 ) ) ) ) )
58	48 51 57	3brtr4d	⊢ ( ( ( ( 𝑤 ∈ ℝ ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( ∀ 𝑣 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) ∧ ( normℎ ‘ 𝑦 ) = 1 ) ) → ( 1 + ( normℎ ‘ ( - 1 ·ℎ 𝑧 ) ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) )
59	9 20 29 36 58	letrd	⊢ ( ( ( ( 𝑤 ∈ ℝ ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( ∀ 𝑣 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) ∧ ( normℎ ‘ 𝑦 ) = 1 ) ) → 1 ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) )
60	59	ex	⊢ ( ( ( 𝑤 ∈ ℝ ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( ∀ 𝑣 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) ∧ ( normℎ ‘ 𝑦 ) = 1 ) → 1 ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) ) )
61	60	adantllr	⊢ ( ( ( ( 𝑤 ∈ ℝ ∧ 0 < 𝑤 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( ∀ 𝑣 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) ∧ ( normℎ ‘ 𝑦 ) = 1 ) → 1 ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) ) )
62		simplll	⊢ ( ( ( ( 𝑤 ∈ ℝ ∧ 0 < 𝑤 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑤 ∈ ℝ )
63	23	adantll	⊢ ( ( ( ( 𝑤 ∈ ℝ ∧ 0 < 𝑤 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑦 −ℎ 𝑧 ) ∈ ℋ )
64	63 24	syl	⊢ ( ( ( ( 𝑤 ∈ ℝ ∧ 0 < 𝑤 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) → ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ∈ ℝ )
65	62 64 26	syl2anc	⊢ ( ( ( ( 𝑤 ∈ ℝ ∧ 0 < 𝑤 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑤 · ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) ∈ ℝ )
66		simpllr	⊢ ( ( ( ( 𝑤 ∈ ℝ ∧ 0 < 𝑤 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) → 0 < 𝑤 )
67		lediv1	⊢ ( ( 1 ∈ ℝ ∧ ( 𝑤 · ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) ∈ ℝ ∧ ( 𝑤 ∈ ℝ ∧ 0 < 𝑤 ) ) → ( 1 ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) ↔ ( 1 / 𝑤 ) ≤ ( ( 𝑤 · ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) / 𝑤 ) ) )
68	10 67	mp3an1	⊢ ( ( ( 𝑤 · ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) ∈ ℝ ∧ ( 𝑤 ∈ ℝ ∧ 0 < 𝑤 ) ) → ( 1 ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) ↔ ( 1 / 𝑤 ) ≤ ( ( 𝑤 · ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) / 𝑤 ) ) )
69	65 62 66 68	syl12anc	⊢ ( ( ( ( 𝑤 ∈ ℝ ∧ 0 < 𝑤 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) → ( 1 ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) ↔ ( 1 / 𝑤 ) ≤ ( ( 𝑤 · ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) / 𝑤 ) ) )
70	61 69	sylibd	⊢ ( ( ( ( 𝑤 ∈ ℝ ∧ 0 < 𝑤 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( ∀ 𝑣 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) ∧ ( normℎ ‘ 𝑦 ) = 1 ) → ( 1 / 𝑤 ) ≤ ( ( 𝑤 · ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) / 𝑤 ) ) )
71	70	imp	⊢ ( ( ( ( ( 𝑤 ∈ ℝ ∧ 0 < 𝑤 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( ∀ 𝑣 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) ∧ ( normℎ ‘ 𝑦 ) = 1 ) ) → ( 1 / 𝑤 ) ≤ ( ( 𝑤 · ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) / 𝑤 ) )
72	25	recnd	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ∈ ℂ )
73	72	adantll	⊢ ( ( ( ( 𝑤 ∈ ℝ ∧ 0 < 𝑤 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) → ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ∈ ℂ )
74		recn	⊢ ( 𝑤 ∈ ℝ → 𝑤 ∈ ℂ )
75	74	ad3antrrr	⊢ ( ( ( ( 𝑤 ∈ ℝ ∧ 0 < 𝑤 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑤 ∈ ℂ )
76	3	ad2antrr	⊢ ( ( ( ( 𝑤 ∈ ℝ ∧ 0 < 𝑤 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑤 ≠ 0 )
77	73 75 76	divcan3d	⊢ ( ( ( ( 𝑤 ∈ ℝ ∧ 0 < 𝑤 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑤 · ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) / 𝑤 ) = ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) )
78	77	adantr	⊢ ( ( ( ( ( 𝑤 ∈ ℝ ∧ 0 < 𝑤 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( ∀ 𝑣 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) ∧ ( normℎ ‘ 𝑦 ) = 1 ) ) → ( ( 𝑤 · ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) / 𝑤 ) = ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) )
79	71 78	breqtrd	⊢ ( ( ( ( ( 𝑤 ∈ ℝ ∧ 0 < 𝑤 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( ∀ 𝑣 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) ∧ ( normℎ ‘ 𝑦 ) = 1 ) ) → ( 1 / 𝑤 ) ≤ ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) )
80	79	exp43	⊢ ( ( ( 𝑤 ∈ ℝ ∧ 0 < 𝑤 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑧 ∈ 𝐵 → ( ∀ 𝑣 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) → ( ( normℎ ‘ 𝑦 ) = 1 → ( 1 / 𝑤 ) ≤ ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) ) ) )
81	80	com23	⊢ ( ( ( 𝑤 ∈ ℝ ∧ 0 < 𝑤 ) ∧ 𝑦 ∈ 𝐴 ) → ( ∀ 𝑣 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) → ( 𝑧 ∈ 𝐵 → ( ( normℎ ‘ 𝑦 ) = 1 → ( 1 / 𝑤 ) ≤ ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) ) ) )
82	81	ralrimdv	⊢ ( ( ( 𝑤 ∈ ℝ ∧ 0 < 𝑤 ) ∧ 𝑦 ∈ 𝐴 ) → ( ∀ 𝑣 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) → ∀ 𝑧 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) = 1 → ( 1 / 𝑤 ) ≤ ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) ) )
83	82	ralimdva	⊢ ( ( 𝑤 ∈ ℝ ∧ 0 < 𝑤 ) → ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) → ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) = 1 → ( 1 / 𝑤 ) ≤ ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) ) )
84	83	impr	⊢ ( ( 𝑤 ∈ ℝ ∧ ( 0 < 𝑤 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) ) ) → ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) = 1 → ( 1 / 𝑤 ) ≤ ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) )
85	6 8 84	jca32	⊢ ( ( 𝑤 ∈ ℝ ∧ ( 0 < 𝑤 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) ) ) → ( ( 1 / 𝑤 ) ∈ ℝ ∧ ( 0 < ( 1 / 𝑤 ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) = 1 → ( 1 / 𝑤 ) ≤ ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) ) ) )
86	85	ex	⊢ ( 𝑤 ∈ ℝ → ( ( 0 < 𝑤 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) ) → ( ( 1 / 𝑤 ) ∈ ℝ ∧ ( 0 < ( 1 / 𝑤 ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) = 1 → ( 1 / 𝑤 ) ≤ ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) ) ) ) )
87		breq2	⊢ ( 𝑥 = ( 1 / 𝑤 ) → ( 0 < 𝑥 ↔ 0 < ( 1 / 𝑤 ) ) )
88		breq1	⊢ ( 𝑥 = ( 1 / 𝑤 ) → ( 𝑥 ≤ ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ↔ ( 1 / 𝑤 ) ≤ ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) )
89	88	imbi2d	⊢ ( 𝑥 = ( 1 / 𝑤 ) → ( ( ( normℎ ‘ 𝑦 ) = 1 → 𝑥 ≤ ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) ↔ ( ( normℎ ‘ 𝑦 ) = 1 → ( 1 / 𝑤 ) ≤ ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) ) )
90	89	2ralbidv	⊢ ( 𝑥 = ( 1 / 𝑤 ) → ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) = 1 → 𝑥 ≤ ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) = 1 → ( 1 / 𝑤 ) ≤ ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) ) )
91	87 90	anbi12d	⊢ ( 𝑥 = ( 1 / 𝑤 ) → ( ( 0 < 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) = 1 → 𝑥 ≤ ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) ) ↔ ( 0 < ( 1 / 𝑤 ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) = 1 → ( 1 / 𝑤 ) ≤ ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) ) ) )
92	91	rspcev	⊢ ( ( ( 1 / 𝑤 ) ∈ ℝ ∧ ( 0 < ( 1 / 𝑤 ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) = 1 → ( 1 / 𝑤 ) ≤ ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) ) ) → ∃ 𝑥 ∈ ℝ ( 0 < 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) = 1 → 𝑥 ≤ ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) ) )
93	86 92	syl6	⊢ ( 𝑤 ∈ ℝ → ( ( 0 < 𝑤 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) ) → ∃ 𝑥 ∈ ℝ ( 0 < 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) = 1 → 𝑥 ≤ ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) ) ) )
94	93	rexlimiv	⊢ ( ∃ 𝑤 ∈ ℝ ( 0 < 𝑤 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑣 ) ) ≤ ( 𝑤 · ( normℎ ‘ ( 𝑦 +ℎ 𝑣 ) ) ) ) → ∃ 𝑥 ∈ ℝ ( 0 < 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) = 1 → 𝑥 ≤ ( normℎ ‘ ( 𝑦 −ℎ 𝑧 ) ) ) ) )