| Step |
Hyp |
Ref |
Expression |
| 1 |
|
hvsubval |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 −ℎ 𝐵 ) = ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) |
| 2 |
1
|
oveq1d |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) = ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ·ih 𝐶 ) ) |
| 3 |
2
|
3adant3 |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) = ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ·ih 𝐶 ) ) |
| 4 |
|
neg1cn |
⊢ - 1 ∈ ℂ |
| 5 |
|
hvmulcl |
⊢ ( ( - 1 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( - 1 ·ℎ 𝐵 ) ∈ ℋ ) |
| 6 |
4 5
|
mpan |
⊢ ( 𝐵 ∈ ℋ → ( - 1 ·ℎ 𝐵 ) ∈ ℋ ) |
| 7 |
|
ax-his2 |
⊢ ( ( 𝐴 ∈ ℋ ∧ ( - 1 ·ℎ 𝐵 ) ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ·ih 𝐶 ) = ( ( 𝐴 ·ih 𝐶 ) + ( ( - 1 ·ℎ 𝐵 ) ·ih 𝐶 ) ) ) |
| 8 |
6 7
|
syl3an2 |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ·ih 𝐶 ) = ( ( 𝐴 ·ih 𝐶 ) + ( ( - 1 ·ℎ 𝐵 ) ·ih 𝐶 ) ) ) |
| 9 |
|
ax-his3 |
⊢ ( ( - 1 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( - 1 ·ℎ 𝐵 ) ·ih 𝐶 ) = ( - 1 · ( 𝐵 ·ih 𝐶 ) ) ) |
| 10 |
4 9
|
mp3an1 |
⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( - 1 ·ℎ 𝐵 ) ·ih 𝐶 ) = ( - 1 · ( 𝐵 ·ih 𝐶 ) ) ) |
| 11 |
|
hicl |
⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐵 ·ih 𝐶 ) ∈ ℂ ) |
| 12 |
11
|
mulm1d |
⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( - 1 · ( 𝐵 ·ih 𝐶 ) ) = - ( 𝐵 ·ih 𝐶 ) ) |
| 13 |
10 12
|
eqtrd |
⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( - 1 ·ℎ 𝐵 ) ·ih 𝐶 ) = - ( 𝐵 ·ih 𝐶 ) ) |
| 14 |
13
|
oveq2d |
⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 ·ih 𝐶 ) + ( ( - 1 ·ℎ 𝐵 ) ·ih 𝐶 ) ) = ( ( 𝐴 ·ih 𝐶 ) + - ( 𝐵 ·ih 𝐶 ) ) ) |
| 15 |
14
|
3adant1 |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 ·ih 𝐶 ) + ( ( - 1 ·ℎ 𝐵 ) ·ih 𝐶 ) ) = ( ( 𝐴 ·ih 𝐶 ) + - ( 𝐵 ·ih 𝐶 ) ) ) |
| 16 |
8 15
|
eqtrd |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ·ih 𝐶 ) = ( ( 𝐴 ·ih 𝐶 ) + - ( 𝐵 ·ih 𝐶 ) ) ) |
| 17 |
|
hicl |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐴 ·ih 𝐶 ) ∈ ℂ ) |
| 18 |
17
|
3adant2 |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐴 ·ih 𝐶 ) ∈ ℂ ) |
| 19 |
11
|
3adant1 |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐵 ·ih 𝐶 ) ∈ ℂ ) |
| 20 |
18 19
|
negsubd |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 ·ih 𝐶 ) + - ( 𝐵 ·ih 𝐶 ) ) = ( ( 𝐴 ·ih 𝐶 ) − ( 𝐵 ·ih 𝐶 ) ) ) |
| 21 |
3 16 20
|
3eqtrd |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) = ( ( 𝐴 ·ih 𝐶 ) − ( 𝐵 ·ih 𝐶 ) ) ) |