Step |
Hyp |
Ref |
Expression |
1 |
|
ax-hv0cl |
⊢ 0ℎ ∈ ℋ |
2 |
|
ax-hvmul0 |
⊢ ( 0ℎ ∈ ℋ → ( 0 ·ℎ 0ℎ ) = 0ℎ ) |
3 |
1 2
|
ax-mp |
⊢ ( 0 ·ℎ 0ℎ ) = 0ℎ |
4 |
3
|
oveq1i |
⊢ ( ( 0 ·ℎ 0ℎ ) ·ih 𝐴 ) = ( 0ℎ ·ih 𝐴 ) |
5 |
|
0cn |
⊢ 0 ∈ ℂ |
6 |
|
ax-his3 |
⊢ ( ( 0 ∈ ℂ ∧ 0ℎ ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( 0 ·ℎ 0ℎ ) ·ih 𝐴 ) = ( 0 · ( 0ℎ ·ih 𝐴 ) ) ) |
7 |
5 1 6
|
mp3an12 |
⊢ ( 𝐴 ∈ ℋ → ( ( 0 ·ℎ 0ℎ ) ·ih 𝐴 ) = ( 0 · ( 0ℎ ·ih 𝐴 ) ) ) |
8 |
4 7
|
syl5eqr |
⊢ ( 𝐴 ∈ ℋ → ( 0ℎ ·ih 𝐴 ) = ( 0 · ( 0ℎ ·ih 𝐴 ) ) ) |
9 |
|
hicl |
⊢ ( ( 0ℎ ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( 0ℎ ·ih 𝐴 ) ∈ ℂ ) |
10 |
1 9
|
mpan |
⊢ ( 𝐴 ∈ ℋ → ( 0ℎ ·ih 𝐴 ) ∈ ℂ ) |
11 |
10
|
mul02d |
⊢ ( 𝐴 ∈ ℋ → ( 0 · ( 0ℎ ·ih 𝐴 ) ) = 0 ) |
12 |
8 11
|
eqtrd |
⊢ ( 𝐴 ∈ ℋ → ( 0ℎ ·ih 𝐴 ) = 0 ) |