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