Proof of Theorem hvaddsub4
| Step | Hyp | Ref
| Expression |
| 1 | | hvaddcl 31031 |
. . . 4
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) ∈
ℋ) |
| 2 | 1 | adantr 480 |
. . 3
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → (𝐴 +ℎ 𝐵) ∈
ℋ) |
| 3 | | hvaddcl 31031 |
. . . 4
⊢ ((𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ) → (𝐶 +ℎ 𝐷) ∈
ℋ) |
| 4 | 3 | adantl 481 |
. . 3
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → (𝐶 +ℎ 𝐷) ∈
ℋ) |
| 5 | | hvaddcl 31031 |
. . . . 5
⊢ ((𝐶 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐶 +ℎ 𝐵) ∈
ℋ) |
| 6 | 5 | ancoms 458 |
. . . 4
⊢ ((𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐶 +ℎ 𝐵) ∈
ℋ) |
| 7 | 6 | ad2ant2lr 748 |
. . 3
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → (𝐶 +ℎ 𝐵) ∈
ℋ) |
| 8 | | hvsubcan2 31094 |
. . 3
⊢ (((𝐴 +ℎ 𝐵) ∈ ℋ ∧ (𝐶 +ℎ 𝐷) ∈ ℋ ∧ (𝐶 +ℎ 𝐵) ∈ ℋ) →
(((𝐴 +ℎ
𝐵)
−ℎ (𝐶 +ℎ 𝐵)) = ((𝐶 +ℎ 𝐷) −ℎ (𝐶 +ℎ 𝐵)) ↔ (𝐴 +ℎ 𝐵) = (𝐶 +ℎ 𝐷))) |
| 9 | 2, 4, 7, 8 | syl3anc 1373 |
. 2
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) →
(((𝐴 +ℎ
𝐵)
−ℎ (𝐶 +ℎ 𝐵)) = ((𝐶 +ℎ 𝐷) −ℎ (𝐶 +ℎ 𝐵)) ↔ (𝐴 +ℎ 𝐵) = (𝐶 +ℎ 𝐷))) |
| 10 | | simpr 484 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → 𝐵 ∈
ℋ) |
| 11 | 10 | anim2i 617 |
. . . . . . 7
⊢ ((𝐶 ∈ ℋ ∧ (𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ)) → (𝐶 ∈ ℋ ∧ 𝐵 ∈
ℋ)) |
| 12 | 11 | ancoms 458 |
. . . . . 6
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ 𝐶 ∈ ℋ) → (𝐶 ∈ ℋ ∧ 𝐵 ∈
ℋ)) |
| 13 | | hvsub4 31056 |
. . . . . 6
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐵 ∈ ℋ)) → ((𝐴 +ℎ 𝐵) −ℎ
(𝐶 +ℎ
𝐵)) = ((𝐴 −ℎ 𝐶) +ℎ (𝐵 −ℎ
𝐵))) |
| 14 | 12, 13 | syldan 591 |
. . . . 5
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) −ℎ
(𝐶 +ℎ
𝐵)) = ((𝐴 −ℎ 𝐶) +ℎ (𝐵 −ℎ
𝐵))) |
| 15 | | hvsubid 31045 |
. . . . . . 7
⊢ (𝐵 ∈ ℋ → (𝐵 −ℎ
𝐵) =
0ℎ) |
| 16 | 15 | ad2antlr 727 |
. . . . . 6
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ 𝐶 ∈ ℋ) → (𝐵 −ℎ
𝐵) =
0ℎ) |
| 17 | 16 | oveq2d 7447 |
. . . . 5
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ 𝐶 ∈ ℋ) → ((𝐴 −ℎ
𝐶) +ℎ
(𝐵
−ℎ 𝐵)) = ((𝐴 −ℎ 𝐶) +ℎ
0ℎ)) |
| 18 | | hvsubcl 31036 |
. . . . . . 7
⊢ ((𝐴 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 −ℎ
𝐶) ∈
ℋ) |
| 19 | | ax-hvaddid 31023 |
. . . . . . 7
⊢ ((𝐴 −ℎ
𝐶) ∈ ℋ →
((𝐴
−ℎ 𝐶) +ℎ 0ℎ)
= (𝐴
−ℎ 𝐶)) |
| 20 | 18, 19 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 −ℎ
𝐶) +ℎ
0ℎ) = (𝐴
−ℎ 𝐶)) |
| 21 | 20 | adantlr 715 |
. . . . 5
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ 𝐶 ∈ ℋ) → ((𝐴 −ℎ
𝐶) +ℎ
0ℎ) = (𝐴
−ℎ 𝐶)) |
| 22 | 14, 17, 21 | 3eqtrd 2781 |
. . . 4
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) −ℎ
(𝐶 +ℎ
𝐵)) = (𝐴 −ℎ 𝐶)) |
| 23 | 22 | adantrr 717 |
. . 3
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 +ℎ 𝐵) −ℎ
(𝐶 +ℎ
𝐵)) = (𝐴 −ℎ 𝐶)) |
| 24 | | simpl 482 |
. . . . . . . 8
⊢ ((𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ) → 𝐶 ∈
ℋ) |
| 25 | 24 | anim1i 615 |
. . . . . . 7
⊢ (((𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ) ∧ 𝐵 ∈ ℋ) → (𝐶 ∈ ℋ ∧ 𝐵 ∈
ℋ)) |
| 26 | | hvsub4 31056 |
. . . . . . 7
⊢ (((𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐵 ∈ ℋ)) → ((𝐶 +ℎ 𝐷) −ℎ
(𝐶 +ℎ
𝐵)) = ((𝐶 −ℎ 𝐶) +ℎ (𝐷 −ℎ
𝐵))) |
| 27 | 25, 26 | syldan 591 |
. . . . . 6
⊢ (((𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ) ∧ 𝐵 ∈ ℋ) → ((𝐶 +ℎ 𝐷) −ℎ
(𝐶 +ℎ
𝐵)) = ((𝐶 −ℎ 𝐶) +ℎ (𝐷 −ℎ
𝐵))) |
| 28 | | hvsubid 31045 |
. . . . . . . 8
⊢ (𝐶 ∈ ℋ → (𝐶 −ℎ
𝐶) =
0ℎ) |
| 29 | 28 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ) ∧ 𝐵 ∈ ℋ) → (𝐶 −ℎ
𝐶) =
0ℎ) |
| 30 | 29 | oveq1d 7446 |
. . . . . 6
⊢ (((𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ) ∧ 𝐵 ∈ ℋ) → ((𝐶 −ℎ
𝐶) +ℎ
(𝐷
−ℎ 𝐵)) = (0ℎ
+ℎ (𝐷
−ℎ 𝐵))) |
| 31 | | hvsubcl 31036 |
. . . . . . . 8
⊢ ((𝐷 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐷 −ℎ
𝐵) ∈
ℋ) |
| 32 | | hvaddlid 31042 |
. . . . . . . 8
⊢ ((𝐷 −ℎ
𝐵) ∈ ℋ →
(0ℎ +ℎ (𝐷 −ℎ 𝐵)) = (𝐷 −ℎ 𝐵)) |
| 33 | 31, 32 | syl 17 |
. . . . . . 7
⊢ ((𝐷 ∈ ℋ ∧ 𝐵 ∈ ℋ) →
(0ℎ +ℎ (𝐷 −ℎ 𝐵)) = (𝐷 −ℎ 𝐵)) |
| 34 | 33 | adantll 714 |
. . . . . 6
⊢ (((𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ) ∧ 𝐵 ∈ ℋ) →
(0ℎ +ℎ (𝐷 −ℎ 𝐵)) = (𝐷 −ℎ 𝐵)) |
| 35 | 27, 30, 34 | 3eqtrd 2781 |
. . . . 5
⊢ (((𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ) ∧ 𝐵 ∈ ℋ) → ((𝐶 +ℎ 𝐷) −ℎ
(𝐶 +ℎ
𝐵)) = (𝐷 −ℎ 𝐵)) |
| 36 | 35 | ancoms 458 |
. . . 4
⊢ ((𝐵 ∈ ℋ ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐶 +ℎ 𝐷) −ℎ
(𝐶 +ℎ
𝐵)) = (𝐷 −ℎ 𝐵)) |
| 37 | 36 | adantll 714 |
. . 3
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐶 +ℎ 𝐷) −ℎ
(𝐶 +ℎ
𝐵)) = (𝐷 −ℎ 𝐵)) |
| 38 | 23, 37 | eqeq12d 2753 |
. 2
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) →
(((𝐴 +ℎ
𝐵)
−ℎ (𝐶 +ℎ 𝐵)) = ((𝐶 +ℎ 𝐷) −ℎ (𝐶 +ℎ 𝐵)) ↔ (𝐴 −ℎ 𝐶) = (𝐷 −ℎ 𝐵))) |
| 39 | 9, 38 | bitr3d 281 |
1
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 +ℎ 𝐵) = (𝐶 +ℎ 𝐷) ↔ (𝐴 −ℎ 𝐶) = (𝐷 −ℎ 𝐵))) |