Metamath Proof Explorer

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ℎ ‘ 𝑢 ) ) ) )