Metamath Proof Explorer

Theorem elpjrn

Description: Reconstruction of the subspace of a projection operator. (Contributed by NM, 24-Apr-2006) (Revised by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

Ref Expression
Assertion elpjrn 
|- ( T e. ran projh -> ran T = { x e. ~H | ( T ` x ) = x } )

Proof

Step Hyp Ref Expression
1 elpjch 
 |-  ( T e. ran projh -> ( ran T e. CH /\ T = ( projh ` ran T ) ) )
2 1 simpld 
 |-  ( T e. ran projh -> ran T e. CH )
3 chss 
 |-  ( ran T e. CH -> ran T C_ ~H )
4 2 3 syl 
 |-  ( T e. ran projh -> ran T C_ ~H )
5 4 sseld 
 |-  ( T e. ran projh -> ( x e. ran T -> x e. ~H ) )
6 elpjhmop 
 |-  ( T e. ran projh -> T e. HrmOp )
7 hmopf 
 |-  ( T e. HrmOp -> T : ~H --> ~H )
8 6 7 syl 
 |-  ( T e. ran projh -> T : ~H --> ~H )
9 8 ffnd 
 |-  ( T e. ran projh -> T Fn ~H )
10 fvelrnb 
 |-  ( T Fn ~H -> ( x e. ran T <-> E. y e. ~H ( T ` y ) = x ) )
11 9 10 syl 
 |-  ( T e. ran projh -> ( x e. ran T <-> E. y e. ~H ( T ` y ) = x ) )
12 fvco3 
 |-  ( ( T : ~H --> ~H /\ y e. ~H ) -> ( ( T o. T ) ` y ) = ( T ` ( T ` y ) ) )
13 8 12 sylan 
 |-  ( ( T e. ran projh /\ y e. ~H ) -> ( ( T o. T ) ` y ) = ( T ` ( T ` y ) ) )
14 elpjidm 
 |-  ( T e. ran projh -> ( T o. T ) = T )
15 14 adantr 
 |-  ( ( T e. ran projh /\ y e. ~H ) -> ( T o. T ) = T )
16 15 fveq1d 
 |-  ( ( T e. ran projh /\ y e. ~H ) -> ( ( T o. T ) ` y ) = ( T ` y ) )
17 13 16 eqtr3d 
 |-  ( ( T e. ran projh /\ y e. ~H ) -> ( T ` ( T ` y ) ) = ( T ` y ) )
18 fveq2 
 |-  ( ( T ` y ) = x -> ( T ` ( T ` y ) ) = ( T ` x ) )
19 id 
 |-  ( ( T ` y ) = x -> ( T ` y ) = x )
20 18 19 eqeq12d 
 |-  ( ( T ` y ) = x -> ( ( T ` ( T ` y ) ) = ( T ` y ) <-> ( T ` x ) = x ) )
21 17 20 syl5ibcom 
 |-  ( ( T e. ran projh /\ y e. ~H ) -> ( ( T ` y ) = x -> ( T ` x ) = x ) )
22 21 rexlimdva 
 |-  ( T e. ran projh -> ( E. y e. ~H ( T ` y ) = x -> ( T ` x ) = x ) )
23 11 22 sylbid 
 |-  ( T e. ran projh -> ( x e. ran T -> ( T ` x ) = x ) )
24 5 23 jcad 
 |-  ( T e. ran projh -> ( x e. ran T -> ( x e. ~H /\ ( T ` x ) = x ) ) )
25 fnfvelrn 
 |-  ( ( T Fn ~H /\ x e. ~H ) -> ( T ` x ) e. ran T )
26 9 25 sylan 
 |-  ( ( T e. ran projh /\ x e. ~H ) -> ( T ` x ) e. ran T )
27 eleq1 
 |-  ( ( T ` x ) = x -> ( ( T ` x ) e. ran T <-> x e. ran T ) )
28 26 27 syl5ibcom 
 |-  ( ( T e. ran projh /\ x e. ~H ) -> ( ( T ` x ) = x -> x e. ran T ) )
29 28 expimpd 
 |-  ( T e. ran projh -> ( ( x e. ~H /\ ( T ` x ) = x ) -> x e. ran T ) )
30 24 29 impbid 
 |-  ( T e. ran projh -> ( x e. ran T <-> ( x e. ~H /\ ( T ` x ) = x ) ) )
31 30 abbi2dv 
 |-  ( T e. ran projh -> ran T = { x | ( x e. ~H /\ ( T ` x ) = x ) } )
32 df-rab 
 |-  { x e. ~H | ( T ` x ) = x } = { x | ( x e. ~H /\ ( T ` x ) = x ) }
33 31 32 eqtr4di 
 |-  ( T e. ran projh -> ran T = { x e. ~H | ( T ` x ) = x } )