Theorem pjssge0ii

Description: Theorem 4.5(iv)->(v) of Beran p. 112. (Contributed by NM, 13-Aug-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjidm.1	|- H e. CH
	pjidm.2	|- A e. ~H
	pjsslem.1	|- G e. CH
Assertion	pjssge0ii	|- ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) = ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) -> 0 <_ ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) .ih A ) )

Proof

Step	Hyp	Ref	Expression
1		pjidm.1	|- H e. CH
2		pjidm.2	|- A e. ~H
3		pjsslem.1	|- G e. CH
4	1	choccli	|- ( _|_ ` H ) e. CH
5	3 4	chincli	|- ( G i^i ( _|_ ` H ) ) e. CH
6	5 2	pjhclii	|- ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) e. ~H
7	6	normcli	|- ( normh ` ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) ) e. RR
8	7	sqge0i	|- 0 <_ ( ( normh ` ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) ) ^ 2 )
9		oveq1	|- ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) = ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) -> ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) .ih A ) = ( ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) .ih A ) )
10	5 2	pjinormii	|- ( ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) .ih A ) = ( ( normh ` ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) ) ^ 2 )
11	9 10	eqtrdi	|- ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) = ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) -> ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) .ih A ) = ( ( normh ` ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) ) ^ 2 ) )
12	8 11	breqtrrid	|- ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) = ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) -> 0 <_ ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) .ih A ) )