Step |
Hyp |
Ref |
Expression |
1 |
|
axhil.1 |
⊢ 𝑈 = 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 |
2 |
|
axhil.2 |
⊢ 𝑈 ∈ CHilOLD |
3 |
|
df-hba |
⊢ ℋ = ( BaseSet ‘ 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 ) |
4 |
1
|
fveq2i |
⊢ ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 ) |
5 |
3 4
|
eqtr4i |
⊢ ℋ = ( BaseSet ‘ 𝑈 ) |
6 |
2
|
hlnvi |
⊢ 𝑈 ∈ NrmCVec |
7 |
1 6
|
h2hva |
⊢ +ℎ = ( +𝑣 ‘ 𝑈 ) |
8 |
1 6
|
h2hsm |
⊢ ·ℎ = ( ·𝑠OLD ‘ 𝑈 ) |
9 |
5 7 8
|
hldi |
⊢ ( ( 𝑈 ∈ CHilOLD ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ) → ( 𝐴 ·ℎ ( 𝐵 +ℎ 𝐶 ) ) = ( ( 𝐴 ·ℎ 𝐵 ) +ℎ ( 𝐴 ·ℎ 𝐶 ) ) ) |
10 |
2 9
|
mpan |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐴 ·ℎ ( 𝐵 +ℎ 𝐶 ) ) = ( ( 𝐴 ·ℎ 𝐵 ) +ℎ ( 𝐴 ·ℎ 𝐶 ) ) ) |