Metamath Proof Explorer

Theorem hmopidmpj

Description: An idempotent Hermitian operator is a projection operator. Theorem 26.4 of Halmos p. 44. (Contributed by NM, 22-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion hmopidmpj 
|- ( ( T e. HrmOp /\ ( T o. T ) = T ) -> T = ( projh ` ran T ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( T = if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) -> T = if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) )
2 rneq 
 |-  ( T = if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) -> ran T = ran if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) )
3 2 fveq2d 
 |-  ( T = if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) -> ( projh ` ran T ) = ( projh ` ran if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) ) )
4 1 3 eqeq12d 
 |-  ( T = if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) -> ( T = ( projh ` ran T ) <-> if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) = ( projh ` ran if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) ) ) )
5 eleq1 
 |-  ( T = if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) -> ( T e. HrmOp <-> if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) e. HrmOp ) )
6 1 1 coeq12d 
 |-  ( T = if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) -> ( T o. T ) = ( if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) o. if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) ) )
7 6 1 eqeq12d 
 |-  ( T = if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) -> ( ( T o. T ) = T <-> ( if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) o. if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) ) = if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) ) )
8 5 7 anbi12d 
 |-  ( T = if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) -> ( ( T e. HrmOp /\ ( T o. T ) = T ) <-> ( if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) e. HrmOp /\ ( if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) o. if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) ) = if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) ) ) )
9 eleq1 
 |-  ( Iop = if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) -> ( Iop e. HrmOp <-> if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) e. HrmOp ) )
10 id 
 |-  ( Iop = if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) -> Iop = if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) )
11 10 10 coeq12d 
 |-  ( Iop = if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) -> ( Iop o. Iop ) = ( if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) o. if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) ) )
12 11 10 eqeq12d 
 |-  ( Iop = if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) -> ( ( Iop o. Iop ) = Iop <-> ( if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) o. if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) ) = if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) ) )
13 9 12 anbi12d 
 |-  ( Iop = if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) -> ( ( Iop e. HrmOp /\ ( Iop o. Iop ) = Iop ) <-> ( if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) e. HrmOp /\ ( if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) o. if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) ) = if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) ) ) )
14 idhmop 
 |-  Iop e. HrmOp
15 hoif 
 |-  Iop : ~H -1-1-onto-> ~H
16 f1of 
 |-  ( Iop : ~H -1-1-onto-> ~H -> Iop : ~H --> ~H )
17 15 16 ax-mp 
 |-  Iop : ~H --> ~H
18 17 hoid1i 
 |-  ( Iop o. Iop ) = Iop
19 14 18 pm3.2i 
 |-  ( Iop e. HrmOp /\ ( Iop o. Iop ) = Iop )
20 8 13 19 elimhyp 
 |-  ( if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) e. HrmOp /\ ( if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) o. if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) ) = if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) )
21 20 simpli 
 |-  if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) e. HrmOp
22 20 simpri 
 |-  ( if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) o. if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) ) = if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop )
23 21 22 hmopidmpji 
 |-  if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) = ( projh ` ran if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) )
24 4 23 dedth 
 |-  ( ( T e. HrmOp /\ ( T o. T ) = T ) -> T = ( projh ` ran T ) )