| Step | Hyp | Ref
| Expression |
| 1 | | cdjreu.1 |
. . . . 5
⊢ 𝐴 ∈
Sℋ |
| 2 | | cdjreu.2 |
. . . . 5
⊢ 𝐵 ∈
Sℋ |
| 3 | 1, 2 | shseli 31335 |
. . . 4
⊢ (𝐶 ∈ (𝐴 +ℋ 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦)) |
| 4 | 3 | biimpi 216 |
. . 3
⊢ (𝐶 ∈ (𝐴 +ℋ 𝐵) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦)) |
| 5 | | reeanv 3229 |
. . . . 5
⊢
(∃𝑦 ∈
𝐵 ∃𝑤 ∈ 𝐵 (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)) ↔ (∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ∧ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤))) |
| 6 | | eqtr2 2761 |
. . . . . . 7
⊢ ((𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)) → (𝑥 +ℎ 𝑦) = (𝑧 +ℎ 𝑤)) |
| 7 | 1 | sheli 31233 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℋ) |
| 8 | 2 | sheli 31233 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝐵 → 𝑦 ∈ ℋ) |
| 9 | 7, 8 | anim12i 613 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) |
| 10 | 1 | sheli 31233 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝐴 → 𝑧 ∈ ℋ) |
| 11 | 2 | sheli 31233 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ 𝐵 → 𝑤 ∈ ℋ) |
| 12 | 10, 11 | anim12i 613 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) → (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)) |
| 13 | | hvaddsub4 31097 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)) → ((𝑥 +ℎ 𝑦) = (𝑧 +ℎ 𝑤) ↔ (𝑥 −ℎ 𝑧) = (𝑤 −ℎ 𝑦))) |
| 14 | 9, 12, 13 | syl2an 596 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → ((𝑥 +ℎ 𝑦) = (𝑧 +ℎ 𝑤) ↔ (𝑥 −ℎ 𝑧) = (𝑤 −ℎ 𝑦))) |
| 15 | 14 | an4s 660 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑥 +ℎ 𝑦) = (𝑧 +ℎ 𝑤) ↔ (𝑥 −ℎ 𝑧) = (𝑤 −ℎ 𝑦))) |
| 16 | 15 | adantll 714 |
. . . . . . . 8
⊢ ((((𝐴 ∩ 𝐵) = 0ℋ ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑥 +ℎ 𝑦) = (𝑧 +ℎ 𝑤) ↔ (𝑥 −ℎ 𝑧) = (𝑤 −ℎ 𝑦))) |
| 17 | | shsubcl 31239 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈
Sℋ ∧ 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑤 −ℎ 𝑦) ∈ 𝐵) |
| 18 | 2, 17 | mp3an1 1450 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑤 −ℎ 𝑦) ∈ 𝐵) |
| 19 | 18 | ancoms 458 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) → (𝑤 −ℎ 𝑦) ∈ 𝐵) |
| 20 | | eleq1 2829 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 −ℎ
𝑧) = (𝑤 −ℎ 𝑦) → ((𝑥 −ℎ 𝑧) ∈ 𝐵 ↔ (𝑤 −ℎ 𝑦) ∈ 𝐵)) |
| 21 | 19, 20 | syl5ibrcom 247 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) → ((𝑥 −ℎ 𝑧) = (𝑤 −ℎ 𝑦) → (𝑥 −ℎ 𝑧) ∈ 𝐵)) |
| 22 | 21 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑥 −ℎ 𝑧) = (𝑤 −ℎ 𝑦) → (𝑥 −ℎ 𝑧) ∈ 𝐵)) |
| 23 | | shsubcl 31239 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
Sℋ ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (𝑥 −ℎ 𝑧) ∈ 𝐴) |
| 24 | 1, 23 | mp3an1 1450 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (𝑥 −ℎ 𝑧) ∈ 𝐴) |
| 25 | 24 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑥 −ℎ 𝑧) ∈ 𝐴) |
| 26 | 22, 25 | jctild 525 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑥 −ℎ 𝑧) = (𝑤 −ℎ 𝑦) → ((𝑥 −ℎ 𝑧) ∈ 𝐴 ∧ (𝑥 −ℎ 𝑧) ∈ 𝐵))) |
| 27 | 26 | adantll 714 |
. . . . . . . . . 10
⊢ ((((𝐴 ∩ 𝐵) = 0ℋ ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑥 −ℎ 𝑧) = (𝑤 −ℎ 𝑦) → ((𝑥 −ℎ 𝑧) ∈ 𝐴 ∧ (𝑥 −ℎ 𝑧) ∈ 𝐵))) |
| 28 | | elin 3967 |
. . . . . . . . . . . 12
⊢ ((𝑥 −ℎ
𝑧) ∈ (𝐴 ∩ 𝐵) ↔ ((𝑥 −ℎ 𝑧) ∈ 𝐴 ∧ (𝑥 −ℎ 𝑧) ∈ 𝐵)) |
| 29 | | eleq2 2830 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∩ 𝐵) = 0ℋ → ((𝑥 −ℎ
𝑧) ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 −ℎ 𝑧) ∈
0ℋ)) |
| 30 | 28, 29 | bitr3id 285 |
. . . . . . . . . . 11
⊢ ((𝐴 ∩ 𝐵) = 0ℋ → (((𝑥 −ℎ
𝑧) ∈ 𝐴 ∧ (𝑥 −ℎ 𝑧) ∈ 𝐵) ↔ (𝑥 −ℎ 𝑧) ∈
0ℋ)) |
| 31 | 30 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝐴 ∩ 𝐵) = 0ℋ ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (((𝑥 −ℎ 𝑧) ∈ 𝐴 ∧ (𝑥 −ℎ 𝑧) ∈ 𝐵) ↔ (𝑥 −ℎ 𝑧) ∈
0ℋ)) |
| 32 | 27, 31 | sylibd 239 |
. . . . . . . . 9
⊢ ((((𝐴 ∩ 𝐵) = 0ℋ ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑥 −ℎ 𝑧) = (𝑤 −ℎ 𝑦) → (𝑥 −ℎ 𝑧) ∈
0ℋ)) |
| 33 | | elch0 31273 |
. . . . . . . . . . . 12
⊢ ((𝑥 −ℎ
𝑧) ∈
0ℋ ↔ (𝑥 −ℎ 𝑧) =
0ℎ) |
| 34 | | hvsubeq0 31087 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑥 −ℎ
𝑧) = 0ℎ
↔ 𝑥 = 𝑧)) |
| 35 | 33, 34 | bitrid 283 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑥 −ℎ
𝑧) ∈
0ℋ ↔ 𝑥 = 𝑧)) |
| 36 | 7, 10, 35 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → ((𝑥 −ℎ 𝑧) ∈ 0ℋ
↔ 𝑥 = 𝑧)) |
| 37 | 36 | ad2antlr 727 |
. . . . . . . . 9
⊢ ((((𝐴 ∩ 𝐵) = 0ℋ ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑥 −ℎ 𝑧) ∈ 0ℋ
↔ 𝑥 = 𝑧)) |
| 38 | 32, 37 | sylibd 239 |
. . . . . . . 8
⊢ ((((𝐴 ∩ 𝐵) = 0ℋ ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑥 −ℎ 𝑧) = (𝑤 −ℎ 𝑦) → 𝑥 = 𝑧)) |
| 39 | 16, 38 | sylbid 240 |
. . . . . . 7
⊢ ((((𝐴 ∩ 𝐵) = 0ℋ ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑥 +ℎ 𝑦) = (𝑧 +ℎ 𝑤) → 𝑥 = 𝑧)) |
| 40 | 6, 39 | syl5 34 |
. . . . . 6
⊢ ((((𝐴 ∩ 𝐵) = 0ℋ ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)) → 𝑥 = 𝑧)) |
| 41 | 40 | rexlimdvva 3213 |
. . . . 5
⊢ (((𝐴 ∩ 𝐵) = 0ℋ ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (∃𝑦 ∈ 𝐵 ∃𝑤 ∈ 𝐵 (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)) → 𝑥 = 𝑧)) |
| 42 | 5, 41 | biimtrrid 243 |
. . . 4
⊢ (((𝐴 ∩ 𝐵) = 0ℋ ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ∧ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤)) → 𝑥 = 𝑧)) |
| 43 | 42 | ralrimivva 3202 |
. . 3
⊢ ((𝐴 ∩ 𝐵) = 0ℋ → ∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ∧ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤)) → 𝑥 = 𝑧)) |
| 44 | 4, 43 | anim12i 613 |
. 2
⊢ ((𝐶 ∈ (𝐴 +ℋ 𝐵) ∧ (𝐴 ∩ 𝐵) = 0ℋ) →
(∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ∧ ∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ∧ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤)) → 𝑥 = 𝑧))) |
| 45 | | oveq1 7438 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (𝑥 +ℎ 𝑦) = (𝑧 +ℎ 𝑦)) |
| 46 | 45 | eqeq2d 2748 |
. . . . 5
⊢ (𝑥 = 𝑧 → (𝐶 = (𝑥 +ℎ 𝑦) ↔ 𝐶 = (𝑧 +ℎ 𝑦))) |
| 47 | 46 | rexbidv 3179 |
. . . 4
⊢ (𝑥 = 𝑧 → (∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ↔ ∃𝑦 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑦))) |
| 48 | | oveq2 7439 |
. . . . . 6
⊢ (𝑦 = 𝑤 → (𝑧 +ℎ 𝑦) = (𝑧 +ℎ 𝑤)) |
| 49 | 48 | eqeq2d 2748 |
. . . . 5
⊢ (𝑦 = 𝑤 → (𝐶 = (𝑧 +ℎ 𝑦) ↔ 𝐶 = (𝑧 +ℎ 𝑤))) |
| 50 | 49 | cbvrexvw 3238 |
. . . 4
⊢
(∃𝑦 ∈
𝐵 𝐶 = (𝑧 +ℎ 𝑦) ↔ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤)) |
| 51 | 47, 50 | bitrdi 287 |
. . 3
⊢ (𝑥 = 𝑧 → (∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ↔ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤))) |
| 52 | 51 | reu4 3737 |
. 2
⊢
(∃!𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ∧ ∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ∧ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤)) → 𝑥 = 𝑧))) |
| 53 | 44, 52 | sylibr 234 |
1
⊢ ((𝐶 ∈ (𝐴 +ℋ 𝐵) ∧ (𝐴 ∩ 𝐵) = 0ℋ) →
∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦)) |