Step | Hyp | Ref
| Expression |
1 | | an4 646 |
. . . 4
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ∧ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤))) ↔ ((𝑥 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦)) ∧ (𝑧 ∈ 𝐴 ∧ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤)))) |
2 | | reeanv 3292 |
. . . . . 6
⊢
(∃𝑦 ∈
𝐵 ∃𝑤 ∈ 𝐵 (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)) ↔ (∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ∧ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤))) |
3 | | simpll1 1226 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ
∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧
(𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)))) → 𝐴 ∈ Sℋ
) |
4 | | simpll2 1228 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ
∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧
(𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)))) → 𝐵 ∈ Sℋ
) |
5 | | simpll3 1230 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ
∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧
(𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)))) → (𝐴 ∩ 𝐵) = 0ℋ) |
6 | | simplrl 767 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ
∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧
(𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)))) → 𝑥 ∈ 𝐴) |
7 | | simprll 769 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ
∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧
(𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)))) → 𝑦 ∈ 𝐵) |
8 | | simplrr 768 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ
∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧
(𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)))) → 𝑧 ∈ 𝐴) |
9 | | simprlr 770 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ
∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧
(𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)))) → 𝑤 ∈ 𝐵) |
10 | | simprrl 771 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ
∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧
(𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)))) → 𝐶 = (𝑥 +ℎ 𝑦)) |
11 | | simprrr 772 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ
∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧
(𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)))) → 𝐶 = (𝑧 +ℎ 𝑤)) |
12 | 10, 11 | eqtr3d 2815 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ
∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧
(𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)))) → (𝑥 +ℎ 𝑦) = (𝑧 +ℎ 𝑤)) |
13 | 3, 4, 5, 6, 7, 8, 9, 12 | shuni 28745 |
. . . . . . . . 9
⊢ ((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ
∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧
(𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)))) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) |
14 | 13 | simpld 490 |
. . . . . . . 8
⊢ ((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ
∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧
(𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)))) → 𝑥 = 𝑧) |
15 | 14 | exp32 413 |
. . . . . . 7
⊢ (((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ
∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧
(𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) → ((𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)) → 𝑥 = 𝑧))) |
16 | 15 | rexlimdvv 3219 |
. . . . . 6
⊢ (((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ
∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧
(𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (∃𝑦 ∈ 𝐵 ∃𝑤 ∈ 𝐵 (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)) → 𝑥 = 𝑧)) |
17 | 2, 16 | syl5bir 235 |
. . . . 5
⊢ (((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ
∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧
(𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ∧ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤)) → 𝑥 = 𝑧)) |
18 | 17 | expimpd 447 |
. . . 4
⊢ ((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ
∧ (𝐴 ∩ 𝐵) = 0ℋ) →
(((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ∧ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤))) → 𝑥 = 𝑧)) |
19 | 1, 18 | syl5bir 235 |
. . 3
⊢ ((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ
∧ (𝐴 ∩ 𝐵) = 0ℋ) →
(((𝑥 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦)) ∧ (𝑧 ∈ 𝐴 ∧ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤))) → 𝑥 = 𝑧)) |
20 | 19 | alrimivv 1971 |
. 2
⊢ ((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ
∧ (𝐴 ∩ 𝐵) = 0ℋ) →
∀𝑥∀𝑧(((𝑥 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦)) ∧ (𝑧 ∈ 𝐴 ∧ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤))) → 𝑥 = 𝑧)) |
21 | | eleq1w 2841 |
. . . 4
⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) |
22 | | oveq1 6929 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝑥 +ℎ 𝑦) = (𝑧 +ℎ 𝑦)) |
23 | 22 | eqeq2d 2787 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (𝐶 = (𝑥 +ℎ 𝑦) ↔ 𝐶 = (𝑧 +ℎ 𝑦))) |
24 | 23 | rexbidv 3236 |
. . . . 5
⊢ (𝑥 = 𝑧 → (∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ↔ ∃𝑦 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑦))) |
25 | | oveq2 6930 |
. . . . . . 7
⊢ (𝑦 = 𝑤 → (𝑧 +ℎ 𝑦) = (𝑧 +ℎ 𝑤)) |
26 | 25 | eqeq2d 2787 |
. . . . . 6
⊢ (𝑦 = 𝑤 → (𝐶 = (𝑧 +ℎ 𝑦) ↔ 𝐶 = (𝑧 +ℎ 𝑤))) |
27 | 26 | cbvrexv 3367 |
. . . . 5
⊢
(∃𝑦 ∈
𝐵 𝐶 = (𝑧 +ℎ 𝑦) ↔ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤)) |
28 | 24, 27 | syl6bb 279 |
. . . 4
⊢ (𝑥 = 𝑧 → (∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ↔ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤))) |
29 | 21, 28 | anbi12d 624 |
. . 3
⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤)))) |
30 | 29 | mo4 2584 |
. 2
⊢
(∃*𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦)) ↔ ∀𝑥∀𝑧(((𝑥 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦)) ∧ (𝑧 ∈ 𝐴 ∧ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤))) → 𝑥 = 𝑧)) |
31 | 20, 30 | sylibr 226 |
1
⊢ ((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ
∧ (𝐴 ∩ 𝐵) = 0ℋ) →
∃*𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦))) |