Step |
Hyp |
Ref |
Expression |
1 |
|
hvaddcl |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 +ℎ 𝐵 ) ∈ ℋ ) |
2 |
|
hvsubval |
⊢ ( ( ( 𝐴 +ℎ 𝐵 ) ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 +ℎ 𝐵 ) −ℎ 𝐵 ) = ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( - 1 ·ℎ 𝐵 ) ) ) |
3 |
1 2
|
sylancom |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 +ℎ 𝐵 ) −ℎ 𝐵 ) = ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( - 1 ·ℎ 𝐵 ) ) ) |
4 |
|
neg1cn |
⊢ - 1 ∈ ℂ |
5 |
|
hvmulcl |
⊢ ( ( - 1 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( - 1 ·ℎ 𝐵 ) ∈ ℋ ) |
6 |
4 5
|
mpan |
⊢ ( 𝐵 ∈ ℋ → ( - 1 ·ℎ 𝐵 ) ∈ ℋ ) |
7 |
6
|
ancli |
⊢ ( 𝐵 ∈ ℋ → ( 𝐵 ∈ ℋ ∧ ( - 1 ·ℎ 𝐵 ) ∈ ℋ ) ) |
8 |
|
ax-hvass |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ ( - 1 ·ℎ 𝐵 ) ∈ ℋ ) → ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( - 1 ·ℎ 𝐵 ) ) = ( 𝐴 +ℎ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) ) |
9 |
8
|
3expb |
⊢ ( ( 𝐴 ∈ ℋ ∧ ( 𝐵 ∈ ℋ ∧ ( - 1 ·ℎ 𝐵 ) ∈ ℋ ) ) → ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( - 1 ·ℎ 𝐵 ) ) = ( 𝐴 +ℎ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) ) |
10 |
7 9
|
sylan2 |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( - 1 ·ℎ 𝐵 ) ) = ( 𝐴 +ℎ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) ) |
11 |
|
hvnegid |
⊢ ( 𝐵 ∈ ℋ → ( 𝐵 +ℎ ( - 1 ·ℎ 𝐵 ) ) = 0ℎ ) |
12 |
11
|
oveq2d |
⊢ ( 𝐵 ∈ ℋ → ( 𝐴 +ℎ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( 𝐴 +ℎ 0ℎ ) ) |
13 |
|
ax-hvaddid |
⊢ ( 𝐴 ∈ ℋ → ( 𝐴 +ℎ 0ℎ ) = 𝐴 ) |
14 |
12 13
|
sylan9eqr |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 +ℎ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = 𝐴 ) |
15 |
3 10 14
|
3eqtrd |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 +ℎ 𝐵 ) −ℎ 𝐵 ) = 𝐴 ) |