Step |
Hyp |
Ref |
Expression |
1 |
|
pjadjt.1 |
|- H e. CH |
2 |
1
|
pjhcli |
|- ( A e. ~H -> ( ( projh ` H ) ` A ) e. ~H ) |
3 |
|
normcl |
|- ( ( ( projh ` H ) ` A ) e. ~H -> ( normh ` ( ( projh ` H ) ` A ) ) e. RR ) |
4 |
2 3
|
syl |
|- ( A e. ~H -> ( normh ` ( ( projh ` H ) ` A ) ) e. RR ) |
5 |
4
|
sqge0d |
|- ( A e. ~H -> 0 <_ ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) ) |
6 |
1
|
pjinormi |
|- ( A e. ~H -> ( ( ( projh ` H ) ` A ) .ih A ) = ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) ) |
7 |
5 6
|
breqtrrd |
|- ( A e. ~H -> 0 <_ ( ( ( projh ` H ) ` A ) .ih A ) ) |