Step | Hyp | Ref
| Expression |
1 | | shsel 28173 |
. 2
⊢ ((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
→ (𝐶 ∈ (𝐴 +ℋ 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑧))) |
2 | | id 22 |
. . . . . . . 8
⊢ (𝐶 = (𝑥 +ℎ 𝑧) → 𝐶 = (𝑥 +ℎ 𝑧)) |
3 | | shel 28068 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
Sℋ ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℋ) |
4 | | shel 28068 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈
Sℋ ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ ℋ) |
5 | | hvaddsubval 27890 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑥 +ℎ 𝑧) = (𝑥 −ℎ (-1
·ℎ 𝑧))) |
6 | 3, 4, 5 | syl2an 494 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
Sℋ ∧ 𝑥 ∈ 𝐴) ∧ (𝐵 ∈ Sℋ
∧ 𝑧 ∈ 𝐵)) → (𝑥 +ℎ 𝑧) = (𝑥 −ℎ (-1
·ℎ 𝑧))) |
7 | 6 | an4s 869 |
. . . . . . . . 9
⊢ (((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → (𝑥 +ℎ 𝑧) = (𝑥 −ℎ (-1
·ℎ 𝑧))) |
8 | 7 | anassrs 680 |
. . . . . . . 8
⊢ ((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) → (𝑥 +ℎ 𝑧) = (𝑥 −ℎ (-1
·ℎ 𝑧))) |
9 | 2, 8 | sylan9eqr 2678 |
. . . . . . 7
⊢
(((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝐶 = (𝑥 +ℎ 𝑧)) → 𝐶 = (𝑥 −ℎ (-1
·ℎ 𝑧))) |
10 | | neg1cn 11124 |
. . . . . . . . . . 11
⊢ -1 ∈
ℂ |
11 | | shmulcl 28075 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈
Sℋ ∧ -1 ∈ ℂ ∧ 𝑧 ∈ 𝐵) → (-1
·ℎ 𝑧) ∈ 𝐵) |
12 | 10, 11 | mp3an2 1412 |
. . . . . . . . . 10
⊢ ((𝐵 ∈
Sℋ ∧ 𝑧 ∈ 𝐵) → (-1
·ℎ 𝑧) ∈ 𝐵) |
13 | 12 | adantll 750 |
. . . . . . . . 9
⊢ (((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑧 ∈ 𝐵) → (-1
·ℎ 𝑧) ∈ 𝐵) |
14 | 13 | adantlr 751 |
. . . . . . . 8
⊢ ((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) → (-1
·ℎ 𝑧) ∈ 𝐵) |
15 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑦 = (-1
·ℎ 𝑧) → (𝑥 −ℎ 𝑦) = (𝑥 −ℎ (-1
·ℎ 𝑧))) |
16 | 15 | eqeq2d 2632 |
. . . . . . . . 9
⊢ (𝑦 = (-1
·ℎ 𝑧) → (𝐶 = (𝑥 −ℎ 𝑦) ↔ 𝐶 = (𝑥 −ℎ (-1
·ℎ 𝑧)))) |
17 | 16 | rspcev 3309 |
. . . . . . . 8
⊢ (((-1
·ℎ 𝑧) ∈ 𝐵 ∧ 𝐶 = (𝑥 −ℎ (-1
·ℎ 𝑧))) → ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 −ℎ 𝑦)) |
18 | 14, 17 | sylan 488 |
. . . . . . 7
⊢
(((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝐶 = (𝑥 −ℎ (-1
·ℎ 𝑧))) → ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 −ℎ 𝑦)) |
19 | 9, 18 | syldan 487 |
. . . . . 6
⊢
(((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝐶 = (𝑥 +ℎ 𝑧)) → ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 −ℎ 𝑦)) |
20 | 19 | ex 450 |
. . . . 5
⊢ ((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) → (𝐶 = (𝑥 +ℎ 𝑧) → ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 −ℎ 𝑦))) |
21 | 20 | rexlimdva 3031 |
. . . 4
⊢ (((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑥 ∈ 𝐴) → (∃𝑧 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑧) → ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 −ℎ 𝑦))) |
22 | | id 22 |
. . . . . . . 8
⊢ (𝐶 = (𝑥 −ℎ 𝑦) → 𝐶 = (𝑥 −ℎ 𝑦)) |
23 | | shel 28068 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈
Sℋ ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℋ) |
24 | | hvsubval 27873 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (𝑥 −ℎ
𝑦) = (𝑥 +ℎ (-1
·ℎ 𝑦))) |
25 | 3, 23, 24 | syl2an 494 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
Sℋ ∧ 𝑥 ∈ 𝐴) ∧ (𝐵 ∈ Sℋ
∧ 𝑦 ∈ 𝐵)) → (𝑥 −ℎ 𝑦) = (𝑥 +ℎ (-1
·ℎ 𝑦))) |
26 | 25 | an4s 869 |
. . . . . . . . 9
⊢ (((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥 −ℎ 𝑦) = (𝑥 +ℎ (-1
·ℎ 𝑦))) |
27 | 26 | anassrs 680 |
. . . . . . . 8
⊢ ((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝑥 −ℎ 𝑦) = (𝑥 +ℎ (-1
·ℎ 𝑦))) |
28 | 22, 27 | sylan9eqr 2678 |
. . . . . . 7
⊢
(((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝐶 = (𝑥 −ℎ 𝑦)) → 𝐶 = (𝑥 +ℎ (-1
·ℎ 𝑦))) |
29 | | shmulcl 28075 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈
Sℋ ∧ -1 ∈ ℂ ∧ 𝑦 ∈ 𝐵) → (-1
·ℎ 𝑦) ∈ 𝐵) |
30 | 10, 29 | mp3an2 1412 |
. . . . . . . . . 10
⊢ ((𝐵 ∈
Sℋ ∧ 𝑦 ∈ 𝐵) → (-1
·ℎ 𝑦) ∈ 𝐵) |
31 | 30 | adantll 750 |
. . . . . . . . 9
⊢ (((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑦 ∈ 𝐵) → (-1
·ℎ 𝑦) ∈ 𝐵) |
32 | 31 | adantlr 751 |
. . . . . . . 8
⊢ ((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (-1
·ℎ 𝑦) ∈ 𝐵) |
33 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑧 = (-1
·ℎ 𝑦) → (𝑥 +ℎ 𝑧) = (𝑥 +ℎ (-1
·ℎ 𝑦))) |
34 | 33 | eqeq2d 2632 |
. . . . . . . . 9
⊢ (𝑧 = (-1
·ℎ 𝑦) → (𝐶 = (𝑥 +ℎ 𝑧) ↔ 𝐶 = (𝑥 +ℎ (-1
·ℎ 𝑦)))) |
35 | 34 | rspcev 3309 |
. . . . . . . 8
⊢ (((-1
·ℎ 𝑦) ∈ 𝐵 ∧ 𝐶 = (𝑥 +ℎ (-1
·ℎ 𝑦))) → ∃𝑧 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑧)) |
36 | 32, 35 | sylan 488 |
. . . . . . 7
⊢
(((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝐶 = (𝑥 +ℎ (-1
·ℎ 𝑦))) → ∃𝑧 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑧)) |
37 | 28, 36 | syldan 487 |
. . . . . 6
⊢
(((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝐶 = (𝑥 −ℎ 𝑦)) → ∃𝑧 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑧)) |
38 | 37 | ex 450 |
. . . . 5
⊢ ((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝐶 = (𝑥 −ℎ 𝑦) → ∃𝑧 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑧))) |
39 | 38 | rexlimdva 3031 |
. . . 4
⊢ (((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐵 𝐶 = (𝑥 −ℎ 𝑦) → ∃𝑧 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑧))) |
40 | 21, 39 | impbid 202 |
. . 3
⊢ (((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑥 ∈ 𝐴) → (∃𝑧 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑧) ↔ ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 −ℎ 𝑦))) |
41 | 40 | rexbidva 3049 |
. 2
⊢ ((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
→ (∃𝑥 ∈
𝐴 ∃𝑧 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑧) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 −ℎ 𝑦))) |
42 | 1, 41 | bitrd 268 |
1
⊢ ((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
→ (𝐶 ∈ (𝐴 +ℋ 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 −ℎ 𝑦))) |