Metamath Proof Explorer

Theorem hmopidmch

Description: An idempotent Hermitian operator generates a closed subspace. Part of proof of Theorem of AkhiezerGlazman p. 64. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion hmopidmch 
|- ( ( T e. HrmOp /\ ( T o. T ) = T ) -> ran T e. CH )

Proof

Step Hyp Ref Expression
1 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 ) )
2 1 eleq1d 
 |-  ( T = if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) -> ( ran T e. CH <-> ran if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) e. CH ) )
3 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 ) )
4 id 
 |-  ( T = if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) -> T = if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) )
5 4 4 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 ) ) )
6 5 4 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 ) ) )
7 3 6 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 ) ) ) )
8 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 ) )
9 id 
 |-  ( Iop = if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) -> Iop = if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) )
10 9 9 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 ) ) )
11 10 9 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 ) ) )
12 8 11 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 ) ) ) )
13 idhmop 
 |-  Iop e. HrmOp
14 hoif 
 |-  Iop : ~H -1-1-onto-> ~H
15 f1of 
 |-  ( Iop : ~H -1-1-onto-> ~H -> Iop : ~H --> ~H )
16 14 15 ax-mp 
 |-  Iop : ~H --> ~H
17 16 hoid1i 
 |-  ( Iop o. Iop ) = Iop
18 13 17 pm3.2i 
 |-  ( Iop e. HrmOp /\ ( Iop o. Iop ) = Iop )
19 7 12 18 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 ) )
20 19 simpli 
 |-  if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) e. HrmOp
21 19 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 )
22 20 21 hmopidmchi 
 |-  ran if ( ( T e. HrmOp /\ ( T o. T ) = T ) , T , Iop ) e. CH
23 2 22 dedth 
 |-  ( ( T e. HrmOp /\ ( T o. T ) = T ) -> ran T e. CH )