Step |
Hyp |
Ref |
Expression |
1 |
|
ax-his4 |
|- ( ( A e. ~H /\ A =/= 0h ) -> 0 < ( A .ih A ) ) |
2 |
1
|
gt0ne0d |
|- ( ( A e. ~H /\ A =/= 0h ) -> ( A .ih A ) =/= 0 ) |
3 |
2
|
ex |
|- ( A e. ~H -> ( A =/= 0h -> ( A .ih A ) =/= 0 ) ) |
4 |
3
|
necon4d |
|- ( A e. ~H -> ( ( A .ih A ) = 0 -> A = 0h ) ) |
5 |
|
hi01 |
|- ( A e. ~H -> ( 0h .ih A ) = 0 ) |
6 |
|
oveq1 |
|- ( A = 0h -> ( A .ih A ) = ( 0h .ih A ) ) |
7 |
6
|
eqeq1d |
|- ( A = 0h -> ( ( A .ih A ) = 0 <-> ( 0h .ih A ) = 0 ) ) |
8 |
5 7
|
syl5ibrcom |
|- ( A e. ~H -> ( A = 0h -> ( A .ih A ) = 0 ) ) |
9 |
4 8
|
impbid |
|- ( A e. ~H -> ( ( A .ih A ) = 0 <-> A = 0h ) ) |