Metamath Proof Explorer

Theorem lnopunilem2

Description: Lemma for lnopunii . (Contributed by NM, 12-May-2005) (New usage is discouraged.)

Ref Expression
Hypotheses lnopunilem.1 
|- T e. LinOp
lnopunilem.2 
|- A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x )
lnopunilem.3 
|- A e. ~H
lnopunilem.4 
|- B e. ~H
Assertion lnopunilem2 
|- ( ( T ` A ) .ih ( T ` B ) ) = ( A .ih B )

Proof

Step Hyp Ref Expression
1 lnopunilem.1 
 |-  T e. LinOp
2 lnopunilem.2 
 |-  A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x )
3 lnopunilem.3 
 |-  A e. ~H
4 lnopunilem.4 
 |-  B e. ~H
5 fvoveq1 
 |-  ( y = if ( y e. CC , y , 0 ) -> ( Re ` ( y x. ( ( T ` A ) .ih ( T ` B ) ) ) ) = ( Re ` ( if ( y e. CC , y , 0 ) x. ( ( T ` A ) .ih ( T ` B ) ) ) ) )
6 fvoveq1 
 |-  ( y = if ( y e. CC , y , 0 ) -> ( Re ` ( y x. ( A .ih B ) ) ) = ( Re ` ( if ( y e. CC , y , 0 ) x. ( A .ih B ) ) ) )
7 5 6 eqeq12d 
 |-  ( y = if ( y e. CC , y , 0 ) -> ( ( Re ` ( y x. ( ( T ` A ) .ih ( T ` B ) ) ) ) = ( Re ` ( y x. ( A .ih B ) ) ) <-> ( Re ` ( if ( y e. CC , y , 0 ) x. ( ( T ` A ) .ih ( T ` B ) ) ) ) = ( Re ` ( if ( y e. CC , y , 0 ) x. ( A .ih B ) ) ) ) )
8 0cn 
 |-  0 e. CC
9 8 elimel 
 |-  if ( y e. CC , y , 0 ) e. CC
10 1 2 3 4 9 lnopunilem1 
 |-  ( Re ` ( if ( y e. CC , y , 0 ) x. ( ( T ` A ) .ih ( T ` B ) ) ) ) = ( Re ` ( if ( y e. CC , y , 0 ) x. ( A .ih B ) ) )
11 7 10 dedth 
 |-  ( y e. CC -> ( Re ` ( y x. ( ( T ` A ) .ih ( T ` B ) ) ) ) = ( Re ` ( y x. ( A .ih B ) ) ) )
12 11 rgen 
 |-  A. y e. CC ( Re ` ( y x. ( ( T ` A ) .ih ( T ` B ) ) ) ) = ( Re ` ( y x. ( A .ih B ) ) )
13 1 lnopfi 
 |-  T : ~H --> ~H
14 13 ffvelcdmi 
 |-  ( A e. ~H -> ( T ` A ) e. ~H )
15 3 14 ax-mp 
 |-  ( T ` A ) e. ~H
16 13 ffvelcdmi 
 |-  ( B e. ~H -> ( T ` B ) e. ~H )
17 4 16 ax-mp 
 |-  ( T ` B ) e. ~H
18 15 17 hicli 
 |-  ( ( T ` A ) .ih ( T ` B ) ) e. CC
19 3 4 hicli 
 |-  ( A .ih B ) e. CC
20 recan 
 |-  ( ( ( ( T ` A ) .ih ( T ` B ) ) e. CC /\ ( A .ih B ) e. CC ) -> ( A. y e. CC ( Re ` ( y x. ( ( T ` A ) .ih ( T ` B ) ) ) ) = ( Re ` ( y x. ( A .ih B ) ) ) <-> ( ( T ` A ) .ih ( T ` B ) ) = ( A .ih B ) ) )
21 18 19 20 mp2an 
 |-  ( A. y e. CC ( Re ` ( y x. ( ( T ` A ) .ih ( T ` B ) ) ) ) = ( Re ` ( y x. ( A .ih B ) ) ) <-> ( ( T ` A ) .ih ( T ` B ) ) = ( A .ih B ) )
22 12 21 mpbi 
 |-  ( ( T ` A ) .ih ( T ` B ) ) = ( A .ih B )