Step | Hyp | Ref
| Expression |
1 | | cdjreu.1 |
. . . . 5
⊢ 𝐴 ∈
Sℋ |
2 | | cdjreu.2 |
. . . . 5
⊢ 𝐵 ∈
Sℋ |
3 | 1, 2 | shseli 29251 |
. . . 4
⊢ (𝐶 ∈ (𝐴 +ℋ 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦)) |
4 | 3 | biimpi 219 |
. . 3
⊢ (𝐶 ∈ (𝐴 +ℋ 𝐵) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦)) |
5 | | reeanv 3270 |
. . . . 5
⊢
(∃𝑦 ∈
𝐵 ∃𝑤 ∈ 𝐵 (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)) ↔ (∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ∧ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤))) |
6 | | eqtr2 2759 |
. . . . . . 7
⊢ ((𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)) → (𝑥 +ℎ 𝑦) = (𝑧 +ℎ 𝑤)) |
7 | 1 | sheli 29149 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℋ) |
8 | 2 | sheli 29149 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝐵 → 𝑦 ∈ ℋ) |
9 | 7, 8 | anim12i 616 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) |
10 | 1 | sheli 29149 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝐴 → 𝑧 ∈ ℋ) |
11 | 2 | sheli 29149 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ 𝐵 → 𝑤 ∈ ℋ) |
12 | 10, 11 | anim12i 616 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) → (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)) |
13 | | hvaddsub4 29013 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)) → ((𝑥 +ℎ 𝑦) = (𝑧 +ℎ 𝑤) ↔ (𝑥 −ℎ 𝑧) = (𝑤 −ℎ 𝑦))) |
14 | 9, 12, 13 | syl2an 599 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → ((𝑥 +ℎ 𝑦) = (𝑧 +ℎ 𝑤) ↔ (𝑥 −ℎ 𝑧) = (𝑤 −ℎ 𝑦))) |
15 | 14 | an4s 660 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑥 +ℎ 𝑦) = (𝑧 +ℎ 𝑤) ↔ (𝑥 −ℎ 𝑧) = (𝑤 −ℎ 𝑦))) |
16 | 15 | adantll 714 |
. . . . . . . 8
⊢ ((((𝐴 ∩ 𝐵) = 0ℋ ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑥 +ℎ 𝑦) = (𝑧 +ℎ 𝑤) ↔ (𝑥 −ℎ 𝑧) = (𝑤 −ℎ 𝑦))) |
17 | | shsubcl 29155 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈
Sℋ ∧ 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑤 −ℎ 𝑦) ∈ 𝐵) |
18 | 2, 17 | mp3an1 1449 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑤 −ℎ 𝑦) ∈ 𝐵) |
19 | 18 | ancoms 462 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) → (𝑤 −ℎ 𝑦) ∈ 𝐵) |
20 | | eleq1 2820 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 −ℎ
𝑧) = (𝑤 −ℎ 𝑦) → ((𝑥 −ℎ 𝑧) ∈ 𝐵 ↔ (𝑤 −ℎ 𝑦) ∈ 𝐵)) |
21 | 19, 20 | syl5ibrcom 250 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) → ((𝑥 −ℎ 𝑧) = (𝑤 −ℎ 𝑦) → (𝑥 −ℎ 𝑧) ∈ 𝐵)) |
22 | 21 | adantl 485 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑥 −ℎ 𝑧) = (𝑤 −ℎ 𝑦) → (𝑥 −ℎ 𝑧) ∈ 𝐵)) |
23 | | shsubcl 29155 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
Sℋ ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (𝑥 −ℎ 𝑧) ∈ 𝐴) |
24 | 1, 23 | mp3an1 1449 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (𝑥 −ℎ 𝑧) ∈ 𝐴) |
25 | 24 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑥 −ℎ 𝑧) ∈ 𝐴) |
26 | 22, 25 | jctild 529 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑥 −ℎ 𝑧) = (𝑤 −ℎ 𝑦) → ((𝑥 −ℎ 𝑧) ∈ 𝐴 ∧ (𝑥 −ℎ 𝑧) ∈ 𝐵))) |
27 | 26 | adantll 714 |
. . . . . . . . . 10
⊢ ((((𝐴 ∩ 𝐵) = 0ℋ ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑥 −ℎ 𝑧) = (𝑤 −ℎ 𝑦) → ((𝑥 −ℎ 𝑧) ∈ 𝐴 ∧ (𝑥 −ℎ 𝑧) ∈ 𝐵))) |
28 | | elin 3859 |
. . . . . . . . . . . 12
⊢ ((𝑥 −ℎ
𝑧) ∈ (𝐴 ∩ 𝐵) ↔ ((𝑥 −ℎ 𝑧) ∈ 𝐴 ∧ (𝑥 −ℎ 𝑧) ∈ 𝐵)) |
29 | | eleq2 2821 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∩ 𝐵) = 0ℋ → ((𝑥 −ℎ
𝑧) ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 −ℎ 𝑧) ∈
0ℋ)) |
30 | 28, 29 | bitr3id 288 |
. . . . . . . . . . 11
⊢ ((𝐴 ∩ 𝐵) = 0ℋ → (((𝑥 −ℎ
𝑧) ∈ 𝐴 ∧ (𝑥 −ℎ 𝑧) ∈ 𝐵) ↔ (𝑥 −ℎ 𝑧) ∈
0ℋ)) |
31 | 30 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝐴 ∩ 𝐵) = 0ℋ ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (((𝑥 −ℎ 𝑧) ∈ 𝐴 ∧ (𝑥 −ℎ 𝑧) ∈ 𝐵) ↔ (𝑥 −ℎ 𝑧) ∈
0ℋ)) |
32 | 27, 31 | sylibd 242 |
. . . . . . . . 9
⊢ ((((𝐴 ∩ 𝐵) = 0ℋ ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑥 −ℎ 𝑧) = (𝑤 −ℎ 𝑦) → (𝑥 −ℎ 𝑧) ∈
0ℋ)) |
33 | | elch0 29189 |
. . . . . . . . . . . 12
⊢ ((𝑥 −ℎ
𝑧) ∈
0ℋ ↔ (𝑥 −ℎ 𝑧) =
0ℎ) |
34 | | hvsubeq0 29003 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑥 −ℎ
𝑧) = 0ℎ
↔ 𝑥 = 𝑧)) |
35 | 33, 34 | syl5bb 286 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑥 −ℎ
𝑧) ∈
0ℋ ↔ 𝑥 = 𝑧)) |
36 | 7, 10, 35 | syl2an 599 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → ((𝑥 −ℎ 𝑧) ∈ 0ℋ
↔ 𝑥 = 𝑧)) |
37 | 36 | ad2antlr 727 |
. . . . . . . . 9
⊢ ((((𝐴 ∩ 𝐵) = 0ℋ ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑥 −ℎ 𝑧) ∈ 0ℋ
↔ 𝑥 = 𝑧)) |
38 | 32, 37 | sylibd 242 |
. . . . . . . 8
⊢ ((((𝐴 ∩ 𝐵) = 0ℋ ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑥 −ℎ 𝑧) = (𝑤 −ℎ 𝑦) → 𝑥 = 𝑧)) |
39 | 16, 38 | sylbid 243 |
. . . . . . 7
⊢ ((((𝐴 ∩ 𝐵) = 0ℋ ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑥 +ℎ 𝑦) = (𝑧 +ℎ 𝑤) → 𝑥 = 𝑧)) |
40 | 6, 39 | syl5 34 |
. . . . . 6
⊢ ((((𝐴 ∩ 𝐵) = 0ℋ ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)) → 𝑥 = 𝑧)) |
41 | 40 | rexlimdvva 3204 |
. . . . 5
⊢ (((𝐴 ∩ 𝐵) = 0ℋ ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (∃𝑦 ∈ 𝐵 ∃𝑤 ∈ 𝐵 (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)) → 𝑥 = 𝑧)) |
42 | 5, 41 | syl5bir 246 |
. . . 4
⊢ (((𝐴 ∩ 𝐵) = 0ℋ ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ∧ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤)) → 𝑥 = 𝑧)) |
43 | 42 | ralrimivva 3103 |
. . 3
⊢ ((𝐴 ∩ 𝐵) = 0ℋ → ∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ∧ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤)) → 𝑥 = 𝑧)) |
44 | 4, 43 | anim12i 616 |
. 2
⊢ ((𝐶 ∈ (𝐴 +ℋ 𝐵) ∧ (𝐴 ∩ 𝐵) = 0ℋ) →
(∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ∧ ∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ∧ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤)) → 𝑥 = 𝑧))) |
45 | | oveq1 7177 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (𝑥 +ℎ 𝑦) = (𝑧 +ℎ 𝑦)) |
46 | 45 | eqeq2d 2749 |
. . . . 5
⊢ (𝑥 = 𝑧 → (𝐶 = (𝑥 +ℎ 𝑦) ↔ 𝐶 = (𝑧 +ℎ 𝑦))) |
47 | 46 | rexbidv 3207 |
. . . 4
⊢ (𝑥 = 𝑧 → (∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ↔ ∃𝑦 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑦))) |
48 | | oveq2 7178 |
. . . . . 6
⊢ (𝑦 = 𝑤 → (𝑧 +ℎ 𝑦) = (𝑧 +ℎ 𝑤)) |
49 | 48 | eqeq2d 2749 |
. . . . 5
⊢ (𝑦 = 𝑤 → (𝐶 = (𝑧 +ℎ 𝑦) ↔ 𝐶 = (𝑧 +ℎ 𝑤))) |
50 | 49 | cbvrexvw 3350 |
. . . 4
⊢
(∃𝑦 ∈
𝐵 𝐶 = (𝑧 +ℎ 𝑦) ↔ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤)) |
51 | 47, 50 | bitrdi 290 |
. . 3
⊢ (𝑥 = 𝑧 → (∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ↔ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤))) |
52 | 51 | reu4 3630 |
. 2
⊢
(∃!𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ∧ ∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ∧ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤)) → 𝑥 = 𝑧))) |
53 | 44, 52 | sylibr 237 |
1
⊢ ((𝐶 ∈ (𝐴 +ℋ 𝐵) ∧ (𝐴 ∩ 𝐵) = 0ℋ) →
∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦)) |