Step |
Hyp |
Ref |
Expression |
1 |
|
hvmulcl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ·ℎ 𝐵 ) ∈ ℋ ) |
2 |
|
ax-his2 |
⊢ ( ( ( 𝐴 ·ℎ 𝐵 ) ∈ ℋ ∧ 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) → ( ( ( 𝐴 ·ℎ 𝐵 ) +ℎ 𝐶 ) ·ih 𝐷 ) = ( ( ( 𝐴 ·ℎ 𝐵 ) ·ih 𝐷 ) + ( 𝐶 ·ih 𝐷 ) ) ) |
3 |
2
|
3expb |
⊢ ( ( ( 𝐴 ·ℎ 𝐵 ) ∈ ℋ ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( ( 𝐴 ·ℎ 𝐵 ) +ℎ 𝐶 ) ·ih 𝐷 ) = ( ( ( 𝐴 ·ℎ 𝐵 ) ·ih 𝐷 ) + ( 𝐶 ·ih 𝐷 ) ) ) |
4 |
1 3
|
sylan |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( ( 𝐴 ·ℎ 𝐵 ) +ℎ 𝐶 ) ·ih 𝐷 ) = ( ( ( 𝐴 ·ℎ 𝐵 ) ·ih 𝐷 ) + ( 𝐶 ·ih 𝐷 ) ) ) |
5 |
|
ax-his3 |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐷 ∈ ℋ ) → ( ( 𝐴 ·ℎ 𝐵 ) ·ih 𝐷 ) = ( 𝐴 · ( 𝐵 ·ih 𝐷 ) ) ) |
6 |
5
|
3expa |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) ∧ 𝐷 ∈ ℋ ) → ( ( 𝐴 ·ℎ 𝐵 ) ·ih 𝐷 ) = ( 𝐴 · ( 𝐵 ·ih 𝐷 ) ) ) |
7 |
6
|
adantrl |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 ·ℎ 𝐵 ) ·ih 𝐷 ) = ( 𝐴 · ( 𝐵 ·ih 𝐷 ) ) ) |
8 |
7
|
oveq1d |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( ( 𝐴 ·ℎ 𝐵 ) ·ih 𝐷 ) + ( 𝐶 ·ih 𝐷 ) ) = ( ( 𝐴 · ( 𝐵 ·ih 𝐷 ) ) + ( 𝐶 ·ih 𝐷 ) ) ) |
9 |
4 8
|
eqtrd |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( ( 𝐴 ·ℎ 𝐵 ) +ℎ 𝐶 ) ·ih 𝐷 ) = ( ( 𝐴 · ( 𝐵 ·ih 𝐷 ) ) + ( 𝐶 ·ih 𝐷 ) ) ) |