Step |
Hyp |
Ref |
Expression |
1 |
|
his5 |
⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) → ( 𝐶 ·ih ( 𝐵 ·ℎ 𝐷 ) ) = ( ( ∗ ‘ 𝐵 ) · ( 𝐶 ·ih 𝐷 ) ) ) |
2 |
1
|
3expb |
⊢ ( ( 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( 𝐶 ·ih ( 𝐵 ·ℎ 𝐷 ) ) = ( ( ∗ ‘ 𝐵 ) · ( 𝐶 ·ih 𝐷 ) ) ) |
3 |
2
|
adantll |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( 𝐶 ·ih ( 𝐵 ·ℎ 𝐷 ) ) = ( ( ∗ ‘ 𝐵 ) · ( 𝐶 ·ih 𝐷 ) ) ) |
4 |
3
|
oveq2d |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( 𝐴 · ( 𝐶 ·ih ( 𝐵 ·ℎ 𝐷 ) ) ) = ( 𝐴 · ( ( ∗ ‘ 𝐵 ) · ( 𝐶 ·ih 𝐷 ) ) ) ) |
5 |
|
simpll |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → 𝐴 ∈ ℂ ) |
6 |
|
simprl |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → 𝐶 ∈ ℋ ) |
7 |
|
hvmulcl |
⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℋ ) → ( 𝐵 ·ℎ 𝐷 ) ∈ ℋ ) |
8 |
7
|
ad2ant2l |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( 𝐵 ·ℎ 𝐷 ) ∈ ℋ ) |
9 |
|
ax-his3 |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℋ ∧ ( 𝐵 ·ℎ 𝐷 ) ∈ ℋ ) → ( ( 𝐴 ·ℎ 𝐶 ) ·ih ( 𝐵 ·ℎ 𝐷 ) ) = ( 𝐴 · ( 𝐶 ·ih ( 𝐵 ·ℎ 𝐷 ) ) ) ) |
10 |
5 6 8 9
|
syl3anc |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 ·ℎ 𝐶 ) ·ih ( 𝐵 ·ℎ 𝐷 ) ) = ( 𝐴 · ( 𝐶 ·ih ( 𝐵 ·ℎ 𝐷 ) ) ) ) |
11 |
|
cjcl |
⊢ ( 𝐵 ∈ ℂ → ( ∗ ‘ 𝐵 ) ∈ ℂ ) |
12 |
11
|
ad2antlr |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ∗ ‘ 𝐵 ) ∈ ℂ ) |
13 |
|
hicl |
⊢ ( ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) → ( 𝐶 ·ih 𝐷 ) ∈ ℂ ) |
14 |
13
|
adantl |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( 𝐶 ·ih 𝐷 ) ∈ ℂ ) |
15 |
5 12 14
|
mulassd |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 · ( ∗ ‘ 𝐵 ) ) · ( 𝐶 ·ih 𝐷 ) ) = ( 𝐴 · ( ( ∗ ‘ 𝐵 ) · ( 𝐶 ·ih 𝐷 ) ) ) ) |
16 |
4 10 15
|
3eqtr4d |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 ·ℎ 𝐶 ) ·ih ( 𝐵 ·ℎ 𝐷 ) ) = ( ( 𝐴 · ( ∗ ‘ 𝐵 ) ) · ( 𝐶 ·ih 𝐷 ) ) ) |