Theorem cdj3lem3b

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

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

Proof

Step	Hyp	Ref	Expression
1		cdj3lem2.1	⊢ 𝐴 ∈ Sℋ
2		cdj3lem2.2	⊢ 𝐵 ∈ Sℋ
3		cdj3lem3.3	⊢ 𝑇 = ( 𝑥 ∈ ( 𝐴 +ℋ 𝐵 ) ↦ ( ℩ 𝑤 ∈ 𝐵 ∃ 𝑧 ∈ 𝐴 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) )
4	2 1	shscomi	⊢ ( 𝐵 +ℋ 𝐴 ) = ( 𝐴 +ℋ 𝐵 )
5	2	sheli	⊢ ( 𝑤 ∈ 𝐵 → 𝑤 ∈ ℋ )
6	1	sheli	⊢ ( 𝑧 ∈ 𝐴 → 𝑧 ∈ ℋ )
7		ax-hvcom	⊢ ( ( 𝑤 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( 𝑤 +ℎ 𝑧 ) = ( 𝑧 +ℎ 𝑤 ) )
8	5 6 7	syl2an	⊢ ( ( 𝑤 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑤 +ℎ 𝑧 ) = ( 𝑧 +ℎ 𝑤 ) )
9	8	eqeq2d	⊢ ( ( 𝑤 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 = ( 𝑤 +ℎ 𝑧 ) ↔ 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) )
10	9	rexbidva	⊢ ( 𝑤 ∈ 𝐵 → ( ∃ 𝑧 ∈ 𝐴 𝑥 = ( 𝑤 +ℎ 𝑧 ) ↔ ∃ 𝑧 ∈ 𝐴 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) )
11	10	riotabiia	⊢ ( ℩ 𝑤 ∈ 𝐵 ∃ 𝑧 ∈ 𝐴 𝑥 = ( 𝑤 +ℎ 𝑧 ) ) = ( ℩ 𝑤 ∈ 𝐵 ∃ 𝑧 ∈ 𝐴 𝑥 = ( 𝑧 +ℎ 𝑤 ) )
12	4 11	mpteq12i	⊢ ( 𝑥 ∈ ( 𝐵 +ℋ 𝐴 ) ↦ ( ℩ 𝑤 ∈ 𝐵 ∃ 𝑧 ∈ 𝐴 𝑥 = ( 𝑤 +ℎ 𝑧 ) ) ) = ( 𝑥 ∈ ( 𝐴 +ℋ 𝐵 ) ↦ ( ℩ 𝑤 ∈ 𝐵 ∃ 𝑧 ∈ 𝐴 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) )
13	3 12	eqtr4i	⊢ 𝑇 = ( 𝑥 ∈ ( 𝐵 +ℋ 𝐴 ) ↦ ( ℩ 𝑤 ∈ 𝐵 ∃ 𝑧 ∈ 𝐴 𝑥 = ( 𝑤 +ℎ 𝑧 ) ) )
14	2 1 13	cdj3lem2b	⊢ ( ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐴 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) → ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑢 ∈ ( 𝐵 +ℋ 𝐴 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) )
15		fveq2	⊢ ( 𝑥 = 𝑡 → ( normℎ ‘ 𝑥 ) = ( normℎ ‘ 𝑡 ) )
16	15	oveq1d	⊢ ( 𝑥 = 𝑡 → ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) = ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ 𝑦 ) ) )
17		fvoveq1	⊢ ( 𝑥 = 𝑡 → ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) = ( normℎ ‘ ( 𝑡 +ℎ 𝑦 ) ) )
18	17	oveq2d	⊢ ( 𝑥 = 𝑡 → ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) = ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ 𝑦 ) ) ) )
19	16 18	breq12d	⊢ ( 𝑥 = 𝑡 → ( ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ↔ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ 𝑦 ) ) ) ) )
20		fveq2	⊢ ( 𝑦 = ℎ → ( normℎ ‘ 𝑦 ) = ( normℎ ‘ ℎ ) )
21	20	oveq2d	⊢ ( 𝑦 = ℎ → ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ 𝑦 ) ) = ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) )
22		oveq2	⊢ ( 𝑦 = ℎ → ( 𝑡 +ℎ 𝑦 ) = ( 𝑡 +ℎ ℎ ) )
23	22	fveq2d	⊢ ( 𝑦 = ℎ → ( normℎ ‘ ( 𝑡 +ℎ 𝑦 ) ) = ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) )
24	23	oveq2d	⊢ ( 𝑦 = ℎ → ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ 𝑦 ) ) ) = ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) )
25	21 24	breq12d	⊢ ( 𝑦 = ℎ → ( ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ 𝑦 ) ) ) ↔ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) )
26	19 25	cbvral2vw	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ↔ ∀ 𝑡 ∈ 𝐴 ∀ ℎ ∈ 𝐵 ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) )
27		ralcom	⊢ ( ∀ 𝑡 ∈ 𝐴 ∀ ℎ ∈ 𝐵 ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ↔ ∀ ℎ ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) )
28	2	sheli	⊢ ( 𝑥 ∈ 𝐵 → 𝑥 ∈ ℋ )
29		normcl	⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ 𝑥 ) ∈ ℝ )
30	28 29	syl	⊢ ( 𝑥 ∈ 𝐵 → ( normℎ ‘ 𝑥 ) ∈ ℝ )
31	30	recnd	⊢ ( 𝑥 ∈ 𝐵 → ( normℎ ‘ 𝑥 ) ∈ ℂ )
32	1	sheli	⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ℋ )
33		normcl	⊢ ( 𝑦 ∈ ℋ → ( normℎ ‘ 𝑦 ) ∈ ℝ )
34	32 33	syl	⊢ ( 𝑦 ∈ 𝐴 → ( normℎ ‘ 𝑦 ) ∈ ℝ )
35	34	recnd	⊢ ( 𝑦 ∈ 𝐴 → ( normℎ ‘ 𝑦 ) ∈ ℂ )
36		addcom	⊢ ( ( ( normℎ ‘ 𝑥 ) ∈ ℂ ∧ ( normℎ ‘ 𝑦 ) ∈ ℂ ) → ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) = ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑥 ) ) )
37	31 35 36	syl2an	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) → ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) = ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑥 ) ) )
38		ax-hvcom	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 +ℎ 𝑦 ) = ( 𝑦 +ℎ 𝑥 ) )
39	28 32 38	syl2an	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 +ℎ 𝑦 ) = ( 𝑦 +ℎ 𝑥 ) )
40	39	fveq2d	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) → ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) = ( normℎ ‘ ( 𝑦 +ℎ 𝑥 ) ) )
41	40	oveq2d	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) = ( 𝑣 · ( normℎ ‘ ( 𝑦 +ℎ 𝑥 ) ) ) )
42	37 41	breq12d	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) → ( ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ↔ ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑥 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑦 +ℎ 𝑥 ) ) ) ) )
43	42	ralbidva	⊢ ( 𝑥 ∈ 𝐵 → ( ∀ 𝑦 ∈ 𝐴 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ 𝐴 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑥 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑦 +ℎ 𝑥 ) ) ) ) )
44	43	ralbiia	⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐴 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐴 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑥 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑦 +ℎ 𝑥 ) ) ) )
45		fveq2	⊢ ( 𝑥 = ℎ → ( normℎ ‘ 𝑥 ) = ( normℎ ‘ ℎ ) )
46	45	oveq2d	⊢ ( 𝑥 = ℎ → ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑥 ) ) = ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ ℎ ) ) )
47		oveq2	⊢ ( 𝑥 = ℎ → ( 𝑦 +ℎ 𝑥 ) = ( 𝑦 +ℎ ℎ ) )
48	47	fveq2d	⊢ ( 𝑥 = ℎ → ( normℎ ‘ ( 𝑦 +ℎ 𝑥 ) ) = ( normℎ ‘ ( 𝑦 +ℎ ℎ ) ) )
49	48	oveq2d	⊢ ( 𝑥 = ℎ → ( 𝑣 · ( normℎ ‘ ( 𝑦 +ℎ 𝑥 ) ) ) = ( 𝑣 · ( normℎ ‘ ( 𝑦 +ℎ ℎ ) ) ) )
50	46 49	breq12d	⊢ ( 𝑥 = ℎ → ( ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑥 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑦 +ℎ 𝑥 ) ) ) ↔ ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑦 +ℎ ℎ ) ) ) ) )
51		fveq2	⊢ ( 𝑦 = 𝑡 → ( normℎ ‘ 𝑦 ) = ( normℎ ‘ 𝑡 ) )
52	51	oveq1d	⊢ ( 𝑦 = 𝑡 → ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ ℎ ) ) = ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) )
53		fvoveq1	⊢ ( 𝑦 = 𝑡 → ( normℎ ‘ ( 𝑦 +ℎ ℎ ) ) = ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) )
54	53	oveq2d	⊢ ( 𝑦 = 𝑡 → ( 𝑣 · ( normℎ ‘ ( 𝑦 +ℎ ℎ ) ) ) = ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) )
55	52 54	breq12d	⊢ ( 𝑦 = 𝑡 → ( ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑦 +ℎ ℎ ) ) ) ↔ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) )
56	50 55	cbvral2vw	⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐴 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑥 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑦 +ℎ 𝑥 ) ) ) ↔ ∀ ℎ ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) )
57	44 56	bitr2i	⊢ ( ∀ ℎ ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐴 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) )
58	26 27 57	3bitri	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐴 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) )
59	58	anbi2i	⊢ ( ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) ↔ ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐴 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) )
60	59	rexbii	⊢ ( ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) ↔ ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐴 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) )
61	1 2	shscomi	⊢ ( 𝐴 +ℋ 𝐵 ) = ( 𝐵 +ℋ 𝐴 )
62	61	raleqi	⊢ ( ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ↔ ∀ 𝑢 ∈ ( 𝐵 +ℋ 𝐴 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) )
63	62	anbi2i	⊢ ( ( 0 < 𝑣 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) ↔ ( 0 < 𝑣 ∧ ∀ 𝑢 ∈ ( 𝐵 +ℋ 𝐴 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) )
64	63	rexbii	⊢ ( ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) ↔ ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑢 ∈ ( 𝐵 +ℋ 𝐴 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) )
65	14 60 64	3imtr4i	⊢ ( ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) → ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) )