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 |
|
df-h0v |
⊢ 0ℎ = ( 0vec ‘ 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 ) |
8 |
1
|
fveq2i |
⊢ ( 0vec ‘ 𝑈 ) = ( 0vec ‘ 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 ) |
9 |
7 8
|
eqtr4i |
⊢ 0ℎ = ( 0vec ‘ 𝑈 ) |
10 |
6 9 3
|
hlipgt0 |
⊢ ( ( 𝑈 ∈ CHilOLD ∧ 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → 0 < ( 𝐴 ·ih 𝐴 ) ) |
11 |
2 10
|
mp3an1 |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → 0 < ( 𝐴 ·ih 𝐴 ) ) |