Theorem cdj3lem2b

Description: Lemma for cdj3i . The first-component function S is bounded if the subspaces are completely disjoint. (Contributed by NM, 26-May-2005) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cdj3lem2.1	⊢ 𝐴 ∈ Sℋ
	cdj3lem2.2	⊢ 𝐵 ∈ Sℋ
	cdj3lem2.3	⊢ 𝑆 = ( 𝑥 ∈ ( 𝐴 +ℋ 𝐵 ) ↦ ( ℩ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) )
Assertion	cdj3lem2b	⊢ ( ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) → ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cdj3lem2.1	⊢ 𝐴 ∈ Sℋ
2		cdj3lem2.2	⊢ 𝐵 ∈ Sℋ
3		cdj3lem2.3	⊢ 𝑆 = ( 𝑥 ∈ ( 𝐴 +ℋ 𝐵 ) ↦ ( ℩ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) )
4	1 2	cdj3lem1	⊢ ( ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) → ( 𝐴 ∩ 𝐵 ) = 0ℋ )
5	1 2	shseli	⊢ ( 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ↔ ∃ 𝑡 ∈ 𝐴 ∃ ℎ ∈ 𝐵 𝑢 = ( 𝑡 +ℎ ℎ ) )
6	5	biimpi	⊢ ( 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) → ∃ 𝑡 ∈ 𝐴 ∃ ℎ ∈ 𝐵 𝑢 = ( 𝑡 +ℎ ℎ ) )
7		fveq2	⊢ ( 𝑥 = 𝑡 → ( normℎ ‘ 𝑥 ) = ( normℎ ‘ 𝑡 ) )
8	7	oveq1d	⊢ ( 𝑥 = 𝑡 → ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) = ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ 𝑦 ) ) )
9		fvoveq1	⊢ ( 𝑥 = 𝑡 → ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) = ( normℎ ‘ ( 𝑡 +ℎ 𝑦 ) ) )
10	9	oveq2d	⊢ ( 𝑥 = 𝑡 → ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) = ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ 𝑦 ) ) ) )
11	8 10	breq12d	⊢ ( 𝑥 = 𝑡 → ( ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ↔ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ 𝑦 ) ) ) ) )
12		fveq2	⊢ ( 𝑦 = ℎ → ( normℎ ‘ 𝑦 ) = ( normℎ ‘ ℎ ) )
13	12	oveq2d	⊢ ( 𝑦 = ℎ → ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ 𝑦 ) ) = ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) )
14		oveq2	⊢ ( 𝑦 = ℎ → ( 𝑡 +ℎ 𝑦 ) = ( 𝑡 +ℎ ℎ ) )
15	14	fveq2d	⊢ ( 𝑦 = ℎ → ( normℎ ‘ ( 𝑡 +ℎ 𝑦 ) ) = ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) )
16	15	oveq2d	⊢ ( 𝑦 = ℎ → ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ 𝑦 ) ) ) = ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) )
17	13 16	breq12d	⊢ ( 𝑦 = ℎ → ( ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ 𝑦 ) ) ) ↔ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) )
18	11 17	rspc2v	⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) → ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) )
19	1 2 3	cdj3lem2	⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( 𝑆 ‘ ( 𝑡 +ℎ ℎ ) ) = 𝑡 )
20	19	3expa	⊢ ( ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( 𝑆 ‘ ( 𝑡 +ℎ ℎ ) ) = 𝑡 )
21	20	fveq2d	⊢ ( ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( normℎ ‘ ( 𝑆 ‘ ( 𝑡 +ℎ ℎ ) ) ) = ( normℎ ‘ 𝑡 ) )
22	21	ad2ant2r	⊢ ( ( ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ∧ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) ∧ ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ 𝑣 ∈ ℝ ) ) → ( normℎ ‘ ( 𝑆 ‘ ( 𝑡 +ℎ ℎ ) ) ) = ( normℎ ‘ 𝑡 ) )
23	2	sheli	⊢ ( ℎ ∈ 𝐵 → ℎ ∈ ℋ )
24		normge0	⊢ ( ℎ ∈ ℋ → 0 ≤ ( normℎ ‘ ℎ ) )
25	23 24	syl	⊢ ( ℎ ∈ 𝐵 → 0 ≤ ( normℎ ‘ ℎ ) )
26	25	adantl	⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → 0 ≤ ( normℎ ‘ ℎ ) )
27	1	sheli	⊢ ( 𝑡 ∈ 𝐴 → 𝑡 ∈ ℋ )
28		normcl	⊢ ( 𝑡 ∈ ℋ → ( normℎ ‘ 𝑡 ) ∈ ℝ )
29	27 28	syl	⊢ ( 𝑡 ∈ 𝐴 → ( normℎ ‘ 𝑡 ) ∈ ℝ )
30		normcl	⊢ ( ℎ ∈ ℋ → ( normℎ ‘ ℎ ) ∈ ℝ )
31	23 30	syl	⊢ ( ℎ ∈ 𝐵 → ( normℎ ‘ ℎ ) ∈ ℝ )
32		addge01	⊢ ( ( ( normℎ ‘ 𝑡 ) ∈ ℝ ∧ ( normℎ ‘ ℎ ) ∈ ℝ ) → ( 0 ≤ ( normℎ ‘ ℎ ) ↔ ( normℎ ‘ 𝑡 ) ≤ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ) )
33	29 31 32	syl2an	⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( 0 ≤ ( normℎ ‘ ℎ ) ↔ ( normℎ ‘ 𝑡 ) ≤ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ) )
34	26 33	mpbid	⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( normℎ ‘ 𝑡 ) ≤ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) )
35	34	adantr	⊢ ( ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ∧ 𝑣 ∈ ℝ ) → ( normℎ ‘ 𝑡 ) ≤ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) )
36	29	ad2antrr	⊢ ( ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ∧ 𝑣 ∈ ℝ ) → ( normℎ ‘ 𝑡 ) ∈ ℝ )
37		readdcl	⊢ ( ( ( normℎ ‘ 𝑡 ) ∈ ℝ ∧ ( normℎ ‘ ℎ ) ∈ ℝ ) → ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ∈ ℝ )
38	29 31 37	syl2an	⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ∈ ℝ )
39	38	adantr	⊢ ( ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ∧ 𝑣 ∈ ℝ ) → ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ∈ ℝ )
40		hvaddcl	⊢ ( ( 𝑡 ∈ ℋ ∧ ℎ ∈ ℋ ) → ( 𝑡 +ℎ ℎ ) ∈ ℋ )
41	27 23 40	syl2an	⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( 𝑡 +ℎ ℎ ) ∈ ℋ )
42		normcl	⊢ ( ( 𝑡 +ℎ ℎ ) ∈ ℋ → ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ∈ ℝ )
43	41 42	syl	⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ∈ ℝ )
44		remulcl	⊢ ( ( 𝑣 ∈ ℝ ∧ ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ∈ ℝ ) → ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ∈ ℝ )
45	43 44	sylan2	⊢ ( ( 𝑣 ∈ ℝ ∧ ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ) → ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ∈ ℝ )
46	45	ancoms	⊢ ( ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ∧ 𝑣 ∈ ℝ ) → ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ∈ ℝ )
47		letr	⊢ ( ( ( normℎ ‘ 𝑡 ) ∈ ℝ ∧ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ∈ ℝ ∧ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ∈ ℝ ) → ( ( ( normℎ ‘ 𝑡 ) ≤ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ∧ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) → ( normℎ ‘ 𝑡 ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) )
48	36 39 46 47	syl3anc	⊢ ( ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ∧ 𝑣 ∈ ℝ ) → ( ( ( normℎ ‘ 𝑡 ) ≤ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ∧ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) → ( normℎ ‘ 𝑡 ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) )
49	35 48	mpand	⊢ ( ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ∧ 𝑣 ∈ ℝ ) → ( ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) → ( normℎ ‘ 𝑡 ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) )
50	49	imp	⊢ ( ( ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ∧ 𝑣 ∈ ℝ ) ∧ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) → ( normℎ ‘ 𝑡 ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) )
51	50	an32s	⊢ ( ( ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ∧ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) ∧ 𝑣 ∈ ℝ ) → ( normℎ ‘ 𝑡 ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) )
52	51	adantrl	⊢ ( ( ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ∧ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) ∧ ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ 𝑣 ∈ ℝ ) ) → ( normℎ ‘ 𝑡 ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) )
53	22 52	eqbrtrd	⊢ ( ( ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ∧ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) ∧ ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ 𝑣 ∈ ℝ ) ) → ( normℎ ‘ ( 𝑆 ‘ ( 𝑡 +ℎ ℎ ) ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) )
54		2fveq3	⊢ ( 𝑢 = ( 𝑡 +ℎ ℎ ) → ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) = ( normℎ ‘ ( 𝑆 ‘ ( 𝑡 +ℎ ℎ ) ) ) )
55		fveq2	⊢ ( 𝑢 = ( 𝑡 +ℎ ℎ ) → ( normℎ ‘ 𝑢 ) = ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) )
56	55	oveq2d	⊢ ( 𝑢 = ( 𝑡 +ℎ ℎ ) → ( 𝑣 · ( normℎ ‘ 𝑢 ) ) = ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) )
57	54 56	breq12d	⊢ ( 𝑢 = ( 𝑡 +ℎ ℎ ) → ( ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ↔ ( normℎ ‘ ( 𝑆 ‘ ( 𝑡 +ℎ ℎ ) ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) )
58	53 57	syl5ibrcom	⊢ ( ( ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ∧ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) ∧ ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ 𝑣 ∈ ℝ ) ) → ( 𝑢 = ( 𝑡 +ℎ ℎ ) → ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) )
59	58	exp31	⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) → ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ 𝑣 ∈ ℝ ) → ( 𝑢 = ( 𝑡 +ℎ ℎ ) → ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) ) ) )
60	18 59	syld	⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) → ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ 𝑣 ∈ ℝ ) → ( 𝑢 = ( 𝑡 +ℎ ℎ ) → ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) ) ) )
61	60	com14	⊢ ( 𝑢 = ( 𝑡 +ℎ ℎ ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) → ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ 𝑣 ∈ ℝ ) → ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) ) ) )
62	61	com4t	⊢ ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ 𝑣 ∈ ℝ ) → ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( 𝑢 = ( 𝑡 +ℎ ℎ ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) → ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) ) ) )
63	62	rexlimdvv	⊢ ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ 𝑣 ∈ ℝ ) → ( ∃ 𝑡 ∈ 𝐴 ∃ ℎ ∈ 𝐵 𝑢 = ( 𝑡 +ℎ ℎ ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) → ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) ) )
64	6 63	syl5com	⊢ ( 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) → ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ 𝑣 ∈ ℝ ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) → ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) ) )
65	64	com3l	⊢ ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ 𝑣 ∈ ℝ ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) → ( 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) → ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) ) )
66	65	ralrimdv	⊢ ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ 𝑣 ∈ ℝ ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) → ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) )
67	66	anim2d	⊢ ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ 𝑣 ∈ ℝ ) → ( ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) → ( 0 < 𝑣 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) ) )
68	67	reximdva	⊢ ( ( 𝐴 ∩ 𝐵 ) = 0ℋ → ( ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) → ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) ) )
69	4 68	mpcom	⊢ ( ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) → ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) )