This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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