Step | Hyp | Ref
| Expression |
1 | | cdj3lem2.2 |
. . 3
⊢ 𝐵 ∈
Sℋ |
2 | | cdj3lem2.1 |
. . 3
⊢ 𝐴 ∈
Sℋ |
3 | | cdj3lem3.3 |
. . . 4
⊢ 𝑇 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑤 ∈ 𝐵 ∃𝑧 ∈ 𝐴 𝑥 = (𝑧 +ℎ 𝑤))) |
4 | 1, 2 | shscomi 28222 |
. . . . 5
⊢ (𝐵 +ℋ 𝐴) = (𝐴 +ℋ 𝐵) |
5 | 1 | sheli 28071 |
. . . . . . . . 9
⊢ (𝑤 ∈ 𝐵 → 𝑤 ∈ ℋ) |
6 | 2 | sheli 28071 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝐴 → 𝑧 ∈ ℋ) |
7 | | ax-hvcom 27858 |
. . . . . . . . 9
⊢ ((𝑤 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑤 +ℎ 𝑧) = (𝑧 +ℎ 𝑤)) |
8 | 5, 6, 7 | syl2an 494 |
. . . . . . . 8
⊢ ((𝑤 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴) → (𝑤 +ℎ 𝑧) = (𝑧 +ℎ 𝑤)) |
9 | 8 | eqeq2d 2632 |
. . . . . . 7
⊢ ((𝑤 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴) → (𝑥 = (𝑤 +ℎ 𝑧) ↔ 𝑥 = (𝑧 +ℎ 𝑤))) |
10 | 9 | rexbidva 3049 |
. . . . . 6
⊢ (𝑤 ∈ 𝐵 → (∃𝑧 ∈ 𝐴 𝑥 = (𝑤 +ℎ 𝑧) ↔ ∃𝑧 ∈ 𝐴 𝑥 = (𝑧 +ℎ 𝑤))) |
11 | 10 | riotabiia 6628 |
. . . . 5
⊢
(℩𝑤
∈ 𝐵 ∃𝑧 ∈ 𝐴 𝑥 = (𝑤 +ℎ 𝑧)) = (℩𝑤 ∈ 𝐵 ∃𝑧 ∈ 𝐴 𝑥 = (𝑧 +ℎ 𝑤)) |
12 | 4, 11 | mpteq12i 4742 |
. . . 4
⊢ (𝑥 ∈ (𝐵 +ℋ 𝐴) ↦ (℩𝑤 ∈ 𝐵 ∃𝑧 ∈ 𝐴 𝑥 = (𝑤 +ℎ 𝑧))) = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑤 ∈ 𝐵 ∃𝑧 ∈ 𝐴 𝑥 = (𝑧 +ℎ 𝑤))) |
13 | 3, 12 | eqtr4i 2647 |
. . 3
⊢ 𝑇 = (𝑥 ∈ (𝐵 +ℋ 𝐴) ↦ (℩𝑤 ∈ 𝐵 ∃𝑧 ∈ 𝐴 𝑥 = (𝑤 +ℎ 𝑧))) |
14 | 1, 2, 13 | cdj3lem2b 29296 |
. 2
⊢
(∃𝑣 ∈
ℝ (0 < 𝑣 ∧
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐴 ((normℎ‘𝑥) +
(normℎ‘𝑦)) ≤ (𝑣 ·
(normℎ‘(𝑥 +ℎ 𝑦)))) → ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑢 ∈ (𝐵 +ℋ 𝐴)(normℎ‘(𝑇‘𝑢)) ≤ (𝑣 ·
(normℎ‘𝑢)))) |
15 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑥 = 𝑡 → (normℎ‘𝑥) =
(normℎ‘𝑡)) |
16 | 15 | oveq1d 6665 |
. . . . . . 7
⊢ (𝑥 = 𝑡 → ((normℎ‘𝑥) +
(normℎ‘𝑦)) = ((normℎ‘𝑡) +
(normℎ‘𝑦))) |
17 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝑥 = 𝑡 → (𝑥 +ℎ 𝑦) = (𝑡 +ℎ 𝑦)) |
18 | 17 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑥 = 𝑡 → (normℎ‘(𝑥 +ℎ 𝑦)) =
(normℎ‘(𝑡 +ℎ 𝑦))) |
19 | 18 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑥 = 𝑡 → (𝑣 ·
(normℎ‘(𝑥 +ℎ 𝑦))) = (𝑣 ·
(normℎ‘(𝑡 +ℎ 𝑦)))) |
20 | 16, 19 | breq12d 4666 |
. . . . . 6
⊢ (𝑥 = 𝑡 →
(((normℎ‘𝑥) + (normℎ‘𝑦)) ≤ (𝑣 ·
(normℎ‘(𝑥 +ℎ 𝑦))) ↔
((normℎ‘𝑡) + (normℎ‘𝑦)) ≤ (𝑣 ·
(normℎ‘(𝑡 +ℎ 𝑦))))) |
21 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑦 = ℎ → (normℎ‘𝑦) =
(normℎ‘ℎ)) |
22 | 21 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑦 = ℎ → ((normℎ‘𝑡) +
(normℎ‘𝑦)) = ((normℎ‘𝑡) +
(normℎ‘ℎ))) |
23 | | oveq2 6658 |
. . . . . . . . 9
⊢ (𝑦 = ℎ → (𝑡 +ℎ 𝑦) = (𝑡 +ℎ ℎ)) |
24 | 23 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑦 = ℎ → (normℎ‘(𝑡 +ℎ 𝑦)) =
(normℎ‘(𝑡 +ℎ ℎ))) |
25 | 24 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑦 = ℎ → (𝑣 ·
(normℎ‘(𝑡 +ℎ 𝑦))) = (𝑣 ·
(normℎ‘(𝑡 +ℎ ℎ)))) |
26 | 22, 25 | breq12d 4666 |
. . . . . 6
⊢ (𝑦 = ℎ → (((normℎ‘𝑡) +
(normℎ‘𝑦)) ≤ (𝑣 ·
(normℎ‘(𝑡 +ℎ 𝑦))) ↔
((normℎ‘𝑡) + (normℎ‘ℎ)) ≤ (𝑣 ·
(normℎ‘(𝑡 +ℎ ℎ))))) |
27 | 20, 26 | cbvral2v 3179 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 ((normℎ‘𝑥) +
(normℎ‘𝑦)) ≤ (𝑣 ·
(normℎ‘(𝑥 +ℎ 𝑦))) ↔ ∀𝑡 ∈ 𝐴 ∀ℎ ∈ 𝐵 ((normℎ‘𝑡) +
(normℎ‘ℎ)) ≤ (𝑣 ·
(normℎ‘(𝑡 +ℎ ℎ)))) |
28 | | ralcom 3098 |
. . . . 5
⊢
(∀𝑡 ∈
𝐴 ∀ℎ ∈ 𝐵 ((normℎ‘𝑡) +
(normℎ‘ℎ)) ≤ (𝑣 ·
(normℎ‘(𝑡 +ℎ ℎ))) ↔ ∀ℎ ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((normℎ‘𝑡) +
(normℎ‘ℎ)) ≤ (𝑣 ·
(normℎ‘(𝑡 +ℎ ℎ)))) |
29 | 1 | sheli 28071 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐵 → 𝑥 ∈ ℋ) |
30 | | normcl 27982 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℋ →
(normℎ‘𝑥) ∈ ℝ) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐵 → (normℎ‘𝑥) ∈
ℝ) |
32 | 31 | recnd 10068 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐵 → (normℎ‘𝑥) ∈
ℂ) |
33 | 2 | sheli 28071 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝐴 → 𝑦 ∈ ℋ) |
34 | | normcl 27982 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℋ →
(normℎ‘𝑦) ∈ ℝ) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝐴 → (normℎ‘𝑦) ∈
ℝ) |
36 | 35 | recnd 10068 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝐴 → (normℎ‘𝑦) ∈
ℂ) |
37 | | addcom 10222 |
. . . . . . . . . 10
⊢
(((normℎ‘𝑥) ∈ ℂ ∧
(normℎ‘𝑦) ∈ ℂ) →
((normℎ‘𝑥) + (normℎ‘𝑦)) =
((normℎ‘𝑦) + (normℎ‘𝑥))) |
38 | 32, 36, 37 | syl2an 494 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) →
((normℎ‘𝑥) + (normℎ‘𝑦)) =
((normℎ‘𝑦) + (normℎ‘𝑥))) |
39 | | ax-hvcom 27858 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (𝑥 +ℎ 𝑦) = (𝑦 +ℎ 𝑥)) |
40 | 29, 33, 39 | syl2an 494 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) → (𝑥 +ℎ 𝑦) = (𝑦 +ℎ 𝑥)) |
41 | 40 | fveq2d 6195 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) →
(normℎ‘(𝑥 +ℎ 𝑦)) = (normℎ‘(𝑦 +ℎ 𝑥))) |
42 | 41 | oveq2d 6666 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) → (𝑣 ·
(normℎ‘(𝑥 +ℎ 𝑦))) = (𝑣 ·
(normℎ‘(𝑦 +ℎ 𝑥)))) |
43 | 38, 42 | breq12d 4666 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) →
(((normℎ‘𝑥) + (normℎ‘𝑦)) ≤ (𝑣 ·
(normℎ‘(𝑥 +ℎ 𝑦))) ↔
((normℎ‘𝑦) + (normℎ‘𝑥)) ≤ (𝑣 ·
(normℎ‘(𝑦 +ℎ 𝑥))))) |
44 | 43 | ralbidva 2985 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐵 → (∀𝑦 ∈ 𝐴 ((normℎ‘𝑥) +
(normℎ‘𝑦)) ≤ (𝑣 ·
(normℎ‘(𝑥 +ℎ 𝑦))) ↔ ∀𝑦 ∈ 𝐴 ((normℎ‘𝑦) +
(normℎ‘𝑥)) ≤ (𝑣 ·
(normℎ‘(𝑦 +ℎ 𝑥))))) |
45 | 44 | ralbiia 2979 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐴 ((normℎ‘𝑥) +
(normℎ‘𝑦)) ≤ (𝑣 ·
(normℎ‘(𝑥 +ℎ 𝑦))) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐴 ((normℎ‘𝑦) +
(normℎ‘𝑥)) ≤ (𝑣 ·
(normℎ‘(𝑦 +ℎ 𝑥)))) |
46 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑥 = ℎ → (normℎ‘𝑥) =
(normℎ‘ℎ)) |
47 | 46 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝑥 = ℎ → ((normℎ‘𝑦) +
(normℎ‘𝑥)) = ((normℎ‘𝑦) +
(normℎ‘ℎ))) |
48 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑥 = ℎ → (𝑦 +ℎ 𝑥) = (𝑦 +ℎ ℎ)) |
49 | 48 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑥 = ℎ → (normℎ‘(𝑦 +ℎ 𝑥)) =
(normℎ‘(𝑦 +ℎ ℎ))) |
50 | 49 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝑥 = ℎ → (𝑣 ·
(normℎ‘(𝑦 +ℎ 𝑥))) = (𝑣 ·
(normℎ‘(𝑦 +ℎ ℎ)))) |
51 | 47, 50 | breq12d 4666 |
. . . . . . 7
⊢ (𝑥 = ℎ → (((normℎ‘𝑦) +
(normℎ‘𝑥)) ≤ (𝑣 ·
(normℎ‘(𝑦 +ℎ 𝑥))) ↔
((normℎ‘𝑦) + (normℎ‘ℎ)) ≤ (𝑣 ·
(normℎ‘(𝑦 +ℎ ℎ))))) |
52 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑦 = 𝑡 → (normℎ‘𝑦) =
(normℎ‘𝑡)) |
53 | 52 | oveq1d 6665 |
. . . . . . . 8
⊢ (𝑦 = 𝑡 → ((normℎ‘𝑦) +
(normℎ‘ℎ)) = ((normℎ‘𝑡) +
(normℎ‘ℎ))) |
54 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑡 → (𝑦 +ℎ ℎ) = (𝑡 +ℎ ℎ)) |
55 | 54 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑦 = 𝑡 → (normℎ‘(𝑦 +ℎ ℎ)) =
(normℎ‘(𝑡 +ℎ ℎ))) |
56 | 55 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝑦 = 𝑡 → (𝑣 ·
(normℎ‘(𝑦 +ℎ ℎ))) = (𝑣 ·
(normℎ‘(𝑡 +ℎ ℎ)))) |
57 | 53, 56 | breq12d 4666 |
. . . . . . 7
⊢ (𝑦 = 𝑡 →
(((normℎ‘𝑦) + (normℎ‘ℎ)) ≤ (𝑣 ·
(normℎ‘(𝑦 +ℎ ℎ))) ↔
((normℎ‘𝑡) + (normℎ‘ℎ)) ≤ (𝑣 ·
(normℎ‘(𝑡 +ℎ ℎ))))) |
58 | 51, 57 | cbvral2v 3179 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐴 ((normℎ‘𝑦) +
(normℎ‘𝑥)) ≤ (𝑣 ·
(normℎ‘(𝑦 +ℎ 𝑥))) ↔ ∀ℎ ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((normℎ‘𝑡) +
(normℎ‘ℎ)) ≤ (𝑣 ·
(normℎ‘(𝑡 +ℎ ℎ)))) |
59 | 45, 58 | bitr2i 265 |
. . . . 5
⊢
(∀ℎ ∈
𝐵 ∀𝑡 ∈ 𝐴 ((normℎ‘𝑡) +
(normℎ‘ℎ)) ≤ (𝑣 ·
(normℎ‘(𝑡 +ℎ ℎ))) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐴 ((normℎ‘𝑥) +
(normℎ‘𝑦)) ≤ (𝑣 ·
(normℎ‘(𝑥 +ℎ 𝑦)))) |
60 | 27, 28, 59 | 3bitri 286 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 ((normℎ‘𝑥) +
(normℎ‘𝑦)) ≤ (𝑣 ·
(normℎ‘(𝑥 +ℎ 𝑦))) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐴 ((normℎ‘𝑥) +
(normℎ‘𝑦)) ≤ (𝑣 ·
(normℎ‘(𝑥 +ℎ 𝑦)))) |
61 | 60 | anbi2i 730 |
. . 3
⊢ ((0 <
𝑣 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((normℎ‘𝑥) +
(normℎ‘𝑦)) ≤ (𝑣 ·
(normℎ‘(𝑥 +ℎ 𝑦)))) ↔ (0 < 𝑣 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐴 ((normℎ‘𝑥) +
(normℎ‘𝑦)) ≤ (𝑣 ·
(normℎ‘(𝑥 +ℎ 𝑦))))) |
62 | 61 | rexbii 3041 |
. 2
⊢
(∃𝑣 ∈
ℝ (0 < 𝑣 ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((normℎ‘𝑥) +
(normℎ‘𝑦)) ≤ (𝑣 ·
(normℎ‘(𝑥 +ℎ 𝑦)))) ↔ ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐴 ((normℎ‘𝑥) +
(normℎ‘𝑦)) ≤ (𝑣 ·
(normℎ‘(𝑥 +ℎ 𝑦))))) |
63 | 2, 1 | shscomi 28222 |
. . . . 5
⊢ (𝐴 +ℋ 𝐵) = (𝐵 +ℋ 𝐴) |
64 | 63 | raleqi 3142 |
. . . 4
⊢
(∀𝑢 ∈
(𝐴 +ℋ
𝐵)(normℎ‘(𝑇‘𝑢)) ≤ (𝑣 ·
(normℎ‘𝑢)) ↔ ∀𝑢 ∈ (𝐵 +ℋ 𝐴)(normℎ‘(𝑇‘𝑢)) ≤ (𝑣 ·
(normℎ‘𝑢))) |
65 | 64 | anbi2i 730 |
. . 3
⊢ ((0 <
𝑣 ∧ ∀𝑢 ∈ (𝐴 +ℋ 𝐵)(normℎ‘(𝑇‘𝑢)) ≤ (𝑣 ·
(normℎ‘𝑢))) ↔ (0 < 𝑣 ∧ ∀𝑢 ∈ (𝐵 +ℋ 𝐴)(normℎ‘(𝑇‘𝑢)) ≤ (𝑣 ·
(normℎ‘𝑢)))) |
66 | 65 | rexbii 3041 |
. 2
⊢
(∃𝑣 ∈
ℝ (0 < 𝑣 ∧
∀𝑢 ∈ (𝐴 +ℋ 𝐵)(normℎ‘(𝑇‘𝑢)) ≤ (𝑣 ·
(normℎ‘𝑢))) ↔ ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑢 ∈ (𝐵 +ℋ 𝐴)(normℎ‘(𝑇‘𝑢)) ≤ (𝑣 ·
(normℎ‘𝑢)))) |
67 | 14, 62, 66 | 3imtr4i 281 |
1
⊢
(∃𝑣 ∈
ℝ (0 < 𝑣 ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((normℎ‘𝑥) +
(normℎ‘𝑦)) ≤ (𝑣 ·
(normℎ‘(𝑥 +ℎ 𝑦)))) → ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑢 ∈ (𝐴 +ℋ 𝐵)(normℎ‘(𝑇‘𝑢)) ≤ (𝑣 ·
(normℎ‘𝑢)))) |