Proof of Theorem hvsub4
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | hvaddcl 31031 | . . 3
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) ∈
ℋ) | 
| 2 |  | hvaddcl 31031 | . . 3
⊢ ((𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ) → (𝐶 +ℎ 𝐷) ∈
ℋ) | 
| 3 |  | hvsubval 31035 | . . 3
⊢ (((𝐴 +ℎ 𝐵) ∈ ℋ ∧ (𝐶 +ℎ 𝐷) ∈ ℋ) → ((𝐴 +ℎ 𝐵) −ℎ
(𝐶 +ℎ
𝐷)) = ((𝐴 +ℎ 𝐵) +ℎ (-1
·ℎ (𝐶 +ℎ 𝐷)))) | 
| 4 | 1, 2, 3 | syl2an 596 | . 2
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 +ℎ 𝐵) −ℎ
(𝐶 +ℎ
𝐷)) = ((𝐴 +ℎ 𝐵) +ℎ (-1
·ℎ (𝐶 +ℎ 𝐷)))) | 
| 5 |  | hvsubval 31035 | . . . . 5
⊢ ((𝐴 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 −ℎ
𝐶) = (𝐴 +ℎ (-1
·ℎ 𝐶))) | 
| 6 | 5 | ad2ant2r 747 | . . . 4
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → (𝐴 −ℎ
𝐶) = (𝐴 +ℎ (-1
·ℎ 𝐶))) | 
| 7 |  | hvsubval 31035 | . . . . 5
⊢ ((𝐵 ∈ ℋ ∧ 𝐷 ∈ ℋ) → (𝐵 −ℎ
𝐷) = (𝐵 +ℎ (-1
·ℎ 𝐷))) | 
| 8 | 7 | ad2ant2l 746 | . . . 4
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → (𝐵 −ℎ
𝐷) = (𝐵 +ℎ (-1
·ℎ 𝐷))) | 
| 9 | 6, 8 | oveq12d 7449 | . . 3
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 −ℎ
𝐶) +ℎ
(𝐵
−ℎ 𝐷)) = ((𝐴 +ℎ (-1
·ℎ 𝐶)) +ℎ (𝐵 +ℎ (-1
·ℎ 𝐷)))) | 
| 10 |  | neg1cn 12380 | . . . . . . 7
⊢ -1 ∈
ℂ | 
| 11 |  | ax-hvdistr1 31027 | . . . . . . 7
⊢ ((-1
∈ ℂ ∧ 𝐶
∈ ℋ ∧ 𝐷
∈ ℋ) → (-1 ·ℎ (𝐶 +ℎ 𝐷)) = ((-1
·ℎ 𝐶) +ℎ (-1
·ℎ 𝐷))) | 
| 12 | 10, 11 | mp3an1 1450 | . . . . . 6
⊢ ((𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ) → (-1
·ℎ (𝐶 +ℎ 𝐷)) = ((-1 ·ℎ
𝐶) +ℎ (-1
·ℎ 𝐷))) | 
| 13 | 12 | adantl 481 | . . . . 5
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → (-1
·ℎ (𝐶 +ℎ 𝐷)) = ((-1 ·ℎ
𝐶) +ℎ (-1
·ℎ 𝐷))) | 
| 14 | 13 | oveq2d 7447 | . . . 4
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 +ℎ 𝐵) +ℎ (-1
·ℎ (𝐶 +ℎ 𝐷))) = ((𝐴 +ℎ 𝐵) +ℎ ((-1
·ℎ 𝐶) +ℎ (-1
·ℎ 𝐷)))) | 
| 15 |  | hvmulcl 31032 | . . . . . . . . 9
⊢ ((-1
∈ ℂ ∧ 𝐶
∈ ℋ) → (-1 ·ℎ 𝐶) ∈ ℋ) | 
| 16 | 10, 15 | mpan 690 | . . . . . . . 8
⊢ (𝐶 ∈ ℋ → (-1
·ℎ 𝐶) ∈ ℋ) | 
| 17 | 16 | anim2i 617 | . . . . . . 7
⊢ ((𝐴 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ∈ ℋ ∧ (-1
·ℎ 𝐶) ∈ ℋ)) | 
| 18 |  | hvmulcl 31032 | . . . . . . . . 9
⊢ ((-1
∈ ℂ ∧ 𝐷
∈ ℋ) → (-1 ·ℎ 𝐷) ∈ ℋ) | 
| 19 | 10, 18 | mpan 690 | . . . . . . . 8
⊢ (𝐷 ∈ ℋ → (-1
·ℎ 𝐷) ∈ ℋ) | 
| 20 | 19 | anim2i 617 | . . . . . . 7
⊢ ((𝐵 ∈ ℋ ∧ 𝐷 ∈ ℋ) → (𝐵 ∈ ℋ ∧ (-1
·ℎ 𝐷) ∈ ℋ)) | 
| 21 | 17, 20 | anim12i 613 | . . . . . 6
⊢ (((𝐴 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ (𝐵 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 ∈ ℋ ∧ (-1
·ℎ 𝐶) ∈ ℋ) ∧ (𝐵 ∈ ℋ ∧ (-1
·ℎ 𝐷) ∈ ℋ))) | 
| 22 | 21 | an4s 660 | . . . . 5
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 ∈ ℋ ∧ (-1
·ℎ 𝐶) ∈ ℋ) ∧ (𝐵 ∈ ℋ ∧ (-1
·ℎ 𝐷) ∈ ℋ))) | 
| 23 |  | hvadd4 31055 | . . . . 5
⊢ (((𝐴 ∈ ℋ ∧ (-1
·ℎ 𝐶) ∈ ℋ) ∧ (𝐵 ∈ ℋ ∧ (-1
·ℎ 𝐷) ∈ ℋ)) → ((𝐴 +ℎ (-1
·ℎ 𝐶)) +ℎ (𝐵 +ℎ (-1
·ℎ 𝐷))) = ((𝐴 +ℎ 𝐵) +ℎ ((-1
·ℎ 𝐶) +ℎ (-1
·ℎ 𝐷)))) | 
| 24 | 22, 23 | syl 17 | . . . 4
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 +ℎ (-1
·ℎ 𝐶)) +ℎ (𝐵 +ℎ (-1
·ℎ 𝐷))) = ((𝐴 +ℎ 𝐵) +ℎ ((-1
·ℎ 𝐶) +ℎ (-1
·ℎ 𝐷)))) | 
| 25 | 14, 24 | eqtr4d 2780 | . . 3
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 +ℎ 𝐵) +ℎ (-1
·ℎ (𝐶 +ℎ 𝐷))) = ((𝐴 +ℎ (-1
·ℎ 𝐶)) +ℎ (𝐵 +ℎ (-1
·ℎ 𝐷)))) | 
| 26 | 9, 25 | eqtr4d 2780 | . 2
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 −ℎ
𝐶) +ℎ
(𝐵
−ℎ 𝐷)) = ((𝐴 +ℎ 𝐵) +ℎ (-1
·ℎ (𝐶 +ℎ 𝐷)))) | 
| 27 | 4, 26 | eqtr4d 2780 | 1
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 +ℎ 𝐵) −ℎ
(𝐶 +ℎ
𝐷)) = ((𝐴 −ℎ 𝐶) +ℎ (𝐵 −ℎ
𝐷))) |