Step |
Hyp |
Ref |
Expression |
1 |
|
hiidrcl |
|- ( A e. ~H -> ( A .ih A ) e. RR ) |
2 |
1
|
adantr |
|- ( ( A e. ~H /\ A =/= 0h ) -> ( A .ih A ) e. RR ) |
3 |
|
ax-his4 |
|- ( ( A e. ~H /\ A =/= 0h ) -> 0 < ( A .ih A ) ) |
4 |
|
sqrtgt0 |
|- ( ( ( A .ih A ) e. RR /\ 0 < ( A .ih A ) ) -> 0 < ( sqrt ` ( A .ih A ) ) ) |
5 |
2 3 4
|
syl2anc |
|- ( ( A e. ~H /\ A =/= 0h ) -> 0 < ( sqrt ` ( A .ih A ) ) ) |
6 |
5
|
ex |
|- ( A e. ~H -> ( A =/= 0h -> 0 < ( sqrt ` ( A .ih A ) ) ) ) |
7 |
|
oveq1 |
|- ( A = 0h -> ( A .ih A ) = ( 0h .ih A ) ) |
8 |
|
hi01 |
|- ( A e. ~H -> ( 0h .ih A ) = 0 ) |
9 |
7 8
|
sylan9eqr |
|- ( ( A e. ~H /\ A = 0h ) -> ( A .ih A ) = 0 ) |
10 |
9
|
fveq2d |
|- ( ( A e. ~H /\ A = 0h ) -> ( sqrt ` ( A .ih A ) ) = ( sqrt ` 0 ) ) |
11 |
|
sqrt0 |
|- ( sqrt ` 0 ) = 0 |
12 |
10 11
|
eqtrdi |
|- ( ( A e. ~H /\ A = 0h ) -> ( sqrt ` ( A .ih A ) ) = 0 ) |
13 |
12
|
ex |
|- ( A e. ~H -> ( A = 0h -> ( sqrt ` ( A .ih A ) ) = 0 ) ) |
14 |
|
hiidge0 |
|- ( A e. ~H -> 0 <_ ( A .ih A ) ) |
15 |
1 14
|
resqrtcld |
|- ( A e. ~H -> ( sqrt ` ( A .ih A ) ) e. RR ) |
16 |
|
0re |
|- 0 e. RR |
17 |
|
lttri3 |
|- ( ( ( sqrt ` ( A .ih A ) ) e. RR /\ 0 e. RR ) -> ( ( sqrt ` ( A .ih A ) ) = 0 <-> ( -. ( sqrt ` ( A .ih A ) ) < 0 /\ -. 0 < ( sqrt ` ( A .ih A ) ) ) ) ) |
18 |
15 16 17
|
sylancl |
|- ( A e. ~H -> ( ( sqrt ` ( A .ih A ) ) = 0 <-> ( -. ( sqrt ` ( A .ih A ) ) < 0 /\ -. 0 < ( sqrt ` ( A .ih A ) ) ) ) ) |
19 |
|
simpr |
|- ( ( -. ( sqrt ` ( A .ih A ) ) < 0 /\ -. 0 < ( sqrt ` ( A .ih A ) ) ) -> -. 0 < ( sqrt ` ( A .ih A ) ) ) |
20 |
18 19
|
syl6bi |
|- ( A e. ~H -> ( ( sqrt ` ( A .ih A ) ) = 0 -> -. 0 < ( sqrt ` ( A .ih A ) ) ) ) |
21 |
13 20
|
syld |
|- ( A e. ~H -> ( A = 0h -> -. 0 < ( sqrt ` ( A .ih A ) ) ) ) |
22 |
21
|
necon2ad |
|- ( A e. ~H -> ( 0 < ( sqrt ` ( A .ih A ) ) -> A =/= 0h ) ) |
23 |
6 22
|
impbid |
|- ( A e. ~H -> ( A =/= 0h <-> 0 < ( sqrt ` ( A .ih A ) ) ) ) |
24 |
|
normval |
|- ( A e. ~H -> ( normh ` A ) = ( sqrt ` ( A .ih A ) ) ) |
25 |
24
|
breq2d |
|- ( A e. ~H -> ( 0 < ( normh ` A ) <-> 0 < ( sqrt ` ( A .ih A ) ) ) ) |
26 |
23 25
|
bitr4d |
|- ( A e. ~H -> ( A =/= 0h <-> 0 < ( normh ` A ) ) ) |