Theorem lnophmlem1

Description: Lemma for lnophmi . (Contributed by NM, 24-Jan-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lnophmlem.1	|- A e. ~H
	lnophmlem.2	|- B e. ~H
	lnophmlem.3	|- T e. LinOp
	lnophmlem.4	|- A. x e. ~H ( x .ih ( T ` x ) ) e. RR
Assertion	lnophmlem1	|- ( A .ih ( T ` A ) ) e. RR

Proof

Step	Hyp	Ref	Expression
1		lnophmlem.1	|- A e. ~H
2		lnophmlem.2	|- B e. ~H
3		lnophmlem.3	|- T e. LinOp
4		lnophmlem.4	|- A. x e. ~H ( x .ih ( T ` x ) ) e. RR
5		id	|- ( x = A -> x = A )
6		fveq2	|- ( x = A -> ( T ` x ) = ( T ` A ) )
7	5 6	oveq12d	|- ( x = A -> ( x .ih ( T ` x ) ) = ( A .ih ( T ` A ) ) )
8	7	eleq1d	|- ( x = A -> ( ( x .ih ( T ` x ) ) e. RR <-> ( A .ih ( T ` A ) ) e. RR ) )
9	8	rspcv	|- ( A e. ~H -> ( A. x e. ~H ( x .ih ( T ` x ) ) e. RR -> ( A .ih ( T ` A ) ) e. RR ) )
10	1 4 9	mp2	|- ( A .ih ( T ` A ) ) e. RR