| Step | Hyp | Ref
| Expression |
| 1 | | shsel 31333 |
. 2
⊢ ((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
→ (𝐶 ∈ (𝐴 +ℋ 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑧))) |
| 2 | | id 22 |
. . . . . . 7
⊢ (𝐶 = (𝑥 +ℎ 𝑧) → 𝐶 = (𝑥 +ℎ 𝑧)) |
| 3 | | shel 31230 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
Sℋ ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℋ) |
| 4 | | shel 31230 |
. . . . . . . . . 10
⊢ ((𝐵 ∈
Sℋ ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ ℋ) |
| 5 | | hvaddsubval 31052 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑥 +ℎ 𝑧) = (𝑥 −ℎ (-1
·ℎ 𝑧))) |
| 6 | 3, 4, 5 | syl2an 596 |
. . . . . . . . 9
⊢ (((𝐴 ∈
Sℋ ∧ 𝑥 ∈ 𝐴) ∧ (𝐵 ∈ Sℋ
∧ 𝑧 ∈ 𝐵)) → (𝑥 +ℎ 𝑧) = (𝑥 −ℎ (-1
·ℎ 𝑧))) |
| 7 | 6 | an4s 660 |
. . . . . . . 8
⊢ (((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → (𝑥 +ℎ 𝑧) = (𝑥 −ℎ (-1
·ℎ 𝑧))) |
| 8 | 7 | anassrs 467 |
. . . . . . 7
⊢ ((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) → (𝑥 +ℎ 𝑧) = (𝑥 −ℎ (-1
·ℎ 𝑧))) |
| 9 | 2, 8 | sylan9eqr 2799 |
. . . . . 6
⊢
(((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝐶 = (𝑥 +ℎ 𝑧)) → 𝐶 = (𝑥 −ℎ (-1
·ℎ 𝑧))) |
| 10 | | neg1cn 12380 |
. . . . . . . . . 10
⊢ -1 ∈
ℂ |
| 11 | | shmulcl 31237 |
. . . . . . . . . 10
⊢ ((𝐵 ∈
Sℋ ∧ -1 ∈ ℂ ∧ 𝑧 ∈ 𝐵) → (-1
·ℎ 𝑧) ∈ 𝐵) |
| 12 | 10, 11 | mp3an2 1451 |
. . . . . . . . 9
⊢ ((𝐵 ∈
Sℋ ∧ 𝑧 ∈ 𝐵) → (-1
·ℎ 𝑧) ∈ 𝐵) |
| 13 | 12 | adantll 714 |
. . . . . . . 8
⊢ (((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑧 ∈ 𝐵) → (-1
·ℎ 𝑧) ∈ 𝐵) |
| 14 | 13 | adantlr 715 |
. . . . . . 7
⊢ ((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) → (-1
·ℎ 𝑧) ∈ 𝐵) |
| 15 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑦 = (-1
·ℎ 𝑧) → (𝑥 −ℎ 𝑦) = (𝑥 −ℎ (-1
·ℎ 𝑧))) |
| 16 | 15 | rspceeqv 3645 |
. . . . . . 7
⊢ (((-1
·ℎ 𝑧) ∈ 𝐵 ∧ 𝐶 = (𝑥 −ℎ (-1
·ℎ 𝑧))) → ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 −ℎ 𝑦)) |
| 17 | 14, 16 | sylan 580 |
. . . . . 6
⊢
(((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝐶 = (𝑥 −ℎ (-1
·ℎ 𝑧))) → ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 −ℎ 𝑦)) |
| 18 | 9, 17 | syldan 591 |
. . . . 5
⊢
(((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝐶 = (𝑥 +ℎ 𝑧)) → ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 −ℎ 𝑦)) |
| 19 | 18 | rexlimdva2 3157 |
. . . 4
⊢ (((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑥 ∈ 𝐴) → (∃𝑧 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑧) → ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 −ℎ 𝑦))) |
| 20 | | id 22 |
. . . . . . 7
⊢ (𝐶 = (𝑥 −ℎ 𝑦) → 𝐶 = (𝑥 −ℎ 𝑦)) |
| 21 | | shel 31230 |
. . . . . . . . . 10
⊢ ((𝐵 ∈
Sℋ ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℋ) |
| 22 | | hvsubval 31035 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (𝑥 −ℎ
𝑦) = (𝑥 +ℎ (-1
·ℎ 𝑦))) |
| 23 | 3, 21, 22 | syl2an 596 |
. . . . . . . . 9
⊢ (((𝐴 ∈
Sℋ ∧ 𝑥 ∈ 𝐴) ∧ (𝐵 ∈ Sℋ
∧ 𝑦 ∈ 𝐵)) → (𝑥 −ℎ 𝑦) = (𝑥 +ℎ (-1
·ℎ 𝑦))) |
| 24 | 23 | an4s 660 |
. . . . . . . 8
⊢ (((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥 −ℎ 𝑦) = (𝑥 +ℎ (-1
·ℎ 𝑦))) |
| 25 | 24 | anassrs 467 |
. . . . . . 7
⊢ ((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝑥 −ℎ 𝑦) = (𝑥 +ℎ (-1
·ℎ 𝑦))) |
| 26 | 20, 25 | sylan9eqr 2799 |
. . . . . 6
⊢
(((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝐶 = (𝑥 −ℎ 𝑦)) → 𝐶 = (𝑥 +ℎ (-1
·ℎ 𝑦))) |
| 27 | | shmulcl 31237 |
. . . . . . . . . 10
⊢ ((𝐵 ∈
Sℋ ∧ -1 ∈ ℂ ∧ 𝑦 ∈ 𝐵) → (-1
·ℎ 𝑦) ∈ 𝐵) |
| 28 | 10, 27 | mp3an2 1451 |
. . . . . . . . 9
⊢ ((𝐵 ∈
Sℋ ∧ 𝑦 ∈ 𝐵) → (-1
·ℎ 𝑦) ∈ 𝐵) |
| 29 | 28 | adantll 714 |
. . . . . . . 8
⊢ (((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑦 ∈ 𝐵) → (-1
·ℎ 𝑦) ∈ 𝐵) |
| 30 | 29 | adantlr 715 |
. . . . . . 7
⊢ ((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (-1
·ℎ 𝑦) ∈ 𝐵) |
| 31 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑧 = (-1
·ℎ 𝑦) → (𝑥 +ℎ 𝑧) = (𝑥 +ℎ (-1
·ℎ 𝑦))) |
| 32 | 31 | rspceeqv 3645 |
. . . . . . 7
⊢ (((-1
·ℎ 𝑦) ∈ 𝐵 ∧ 𝐶 = (𝑥 +ℎ (-1
·ℎ 𝑦))) → ∃𝑧 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑧)) |
| 33 | 30, 32 | sylan 580 |
. . . . . 6
⊢
(((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝐶 = (𝑥 +ℎ (-1
·ℎ 𝑦))) → ∃𝑧 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑧)) |
| 34 | 26, 33 | syldan 591 |
. . . . 5
⊢
(((((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝐶 = (𝑥 −ℎ 𝑦)) → ∃𝑧 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑧)) |
| 35 | 34 | rexlimdva2 3157 |
. . . 4
⊢ (((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐵 𝐶 = (𝑥 −ℎ 𝑦) → ∃𝑧 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑧))) |
| 36 | 19, 35 | impbid 212 |
. . 3
⊢ (((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
∧ 𝑥 ∈ 𝐴) → (∃𝑧 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑧) ↔ ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 −ℎ 𝑦))) |
| 37 | 36 | rexbidva 3177 |
. 2
⊢ ((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
→ (∃𝑥 ∈
𝐴 ∃𝑧 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑧) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 −ℎ 𝑦))) |
| 38 | 1, 37 | bitrd 279 |
1
⊢ ((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
→ (𝐶 ∈ (𝐴 +ℋ 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 −ℎ 𝑦))) |