Metamath Proof Explorer

Theorem hmopidmpji

Description: An idempotent Hermitian operator is a projection operator. Theorem 26.4 of Halmos p. 44. (Halmos seems to omit the proof that H is a closed subspace, which is not trivial as hmopidmchi shows.) (Contributed by NM, 22-Apr-2006) (Revised by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses hmopidmch.1 
|- T e. HrmOp
hmopidmch.2 
|- ( T o. T ) = T
Assertion hmopidmpji 
|- T = ( projh ` ran T )

Proof

Step Hyp Ref Expression
1 hmopidmch.1 
 |-  T e. HrmOp
2 hmopidmch.2 
 |-  ( T o. T ) = T
3 hmoplin 
 |-  ( T e. HrmOp -> T e. LinOp )
4 1 3 ax-mp 
 |-  T e. LinOp
5 4 lnopfi 
 |-  T : ~H --> ~H
6 ffn 
 |-  ( T : ~H --> ~H -> T Fn ~H )
7 5 6 ax-mp 
 |-  T Fn ~H
8 1 2 hmopidmchi 
 |-  ran T e. CH
9 8 pjfni 
 |-  ( projh ` ran T ) Fn ~H
10 eqfnfv 
 |-  ( ( T Fn ~H /\ ( projh ` ran T ) Fn ~H ) -> ( T = ( projh ` ran T ) <-> A. x e. ~H ( T ` x ) = ( ( projh ` ran T ) ` x ) ) )
11 7 9 10 mp2an 
 |-  ( T = ( projh ` ran T ) <-> A. x e. ~H ( T ` x ) = ( ( projh ` ran T ) ` x ) )
12 fnfvelrn 
 |-  ( ( T Fn ~H /\ x e. ~H ) -> ( T ` x ) e. ran T )
13 7 12 mpan 
 |-  ( x e. ~H -> ( T ` x ) e. ran T )
14 id 
 |-  ( x e. ~H -> x e. ~H )
15 5 ffvelrni 
 |-  ( x e. ~H -> ( T ` x ) e. ~H )
16 hvsubcl 
 |-  ( ( x e. ~H /\ ( T ` x ) e. ~H ) -> ( x -h ( T ` x ) ) e. ~H )
17 14 15 16 syl2anc 
 |-  ( x e. ~H -> ( x -h ( T ` x ) ) e. ~H )
18 simpl 
 |-  ( ( x e. ~H /\ y e. ~H ) -> x e. ~H )
19 15 adantr 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( T ` x ) e. ~H )
20 5 ffvelrni 
 |-  ( y e. ~H -> ( T ` y ) e. ~H )
21 20 adantl 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( T ` y ) e. ~H )
22 his2sub 
 |-  ( ( x e. ~H /\ ( T ` x ) e. ~H /\ ( T ` y ) e. ~H ) -> ( ( x -h ( T ` x ) ) .ih ( T ` y ) ) = ( ( x .ih ( T ` y ) ) - ( ( T ` x ) .ih ( T ` y ) ) ) )
23 18 19 21 22 syl3anc 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( x -h ( T ` x ) ) .ih ( T ` y ) ) = ( ( x .ih ( T ` y ) ) - ( ( T ` x ) .ih ( T ` y ) ) ) )
24 hmop 
 |-  ( ( T e. HrmOp /\ x e. ~H /\ ( T ` y ) e. ~H ) -> ( x .ih ( T ` ( T ` y ) ) ) = ( ( T ` x ) .ih ( T ` y ) ) )
25 1 24 mp3an1 
 |-  ( ( x e. ~H /\ ( T ` y ) e. ~H ) -> ( x .ih ( T ` ( T ` y ) ) ) = ( ( T ` x ) .ih ( T ` y ) ) )
26 20 25 sylan2 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( x .ih ( T ` ( T ` y ) ) ) = ( ( T ` x ) .ih ( T ` y ) ) )
27 5 5 hocoi 
 |-  ( y e. ~H -> ( ( T o. T ) ` y ) = ( T ` ( T ` y ) ) )
28 2 fveq1i 
 |-  ( ( T o. T ) ` y ) = ( T ` y )
29 27 28 eqtr3di 
 |-  ( y e. ~H -> ( T ` ( T ` y ) ) = ( T ` y ) )
30 29 adantl 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( T ` ( T ` y ) ) = ( T ` y ) )
31 30 oveq2d 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( x .ih ( T ` ( T ` y ) ) ) = ( x .ih ( T ` y ) ) )
32 26 31 eqtr3d 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( T ` x ) .ih ( T ` y ) ) = ( x .ih ( T ` y ) ) )
33 32 oveq2d 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( x .ih ( T ` y ) ) - ( ( T ` x ) .ih ( T ` y ) ) ) = ( ( x .ih ( T ` y ) ) - ( x .ih ( T ` y ) ) ) )
34 hicl 
 |-  ( ( x e. ~H /\ ( T ` y ) e. ~H ) -> ( x .ih ( T ` y ) ) e. CC )
35 20 34 sylan2 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( x .ih ( T ` y ) ) e. CC )
36 35 subidd 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( x .ih ( T ` y ) ) - ( x .ih ( T ` y ) ) ) = 0 )
37 23 33 36 3eqtrd 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( x -h ( T ` x ) ) .ih ( T ` y ) ) = 0 )
38 37 ralrimiva 
 |-  ( x e. ~H -> A. y e. ~H ( ( x -h ( T ` x ) ) .ih ( T ` y ) ) = 0 )
39 oveq2 
 |-  ( z = ( T ` y ) -> ( ( x -h ( T ` x ) ) .ih z ) = ( ( x -h ( T ` x ) ) .ih ( T ` y ) ) )
40 39 eqeq1d 
 |-  ( z = ( T ` y ) -> ( ( ( x -h ( T ` x ) ) .ih z ) = 0 <-> ( ( x -h ( T ` x ) ) .ih ( T ` y ) ) = 0 ) )
41 40 ralrn 
 |-  ( T Fn ~H -> ( A. z e. ran T ( ( x -h ( T ` x ) ) .ih z ) = 0 <-> A. y e. ~H ( ( x -h ( T ` x ) ) .ih ( T ` y ) ) = 0 ) )
42 7 41 ax-mp 
 |-  ( A. z e. ran T ( ( x -h ( T ` x ) ) .ih z ) = 0 <-> A. y e. ~H ( ( x -h ( T ` x ) ) .ih ( T ` y ) ) = 0 )
43 38 42 sylibr 
 |-  ( x e. ~H -> A. z e. ran T ( ( x -h ( T ` x ) ) .ih z ) = 0 )
44 8 chssii 
 |-  ran T C_ ~H
45 ocel 
 |-  ( ran T C_ ~H -> ( ( x -h ( T ` x ) ) e. ( _|_ ` ran T ) <-> ( ( x -h ( T ` x ) ) e. ~H /\ A. z e. ran T ( ( x -h ( T ` x ) ) .ih z ) = 0 ) ) )
46 44 45 ax-mp 
 |-  ( ( x -h ( T ` x ) ) e. ( _|_ ` ran T ) <-> ( ( x -h ( T ` x ) ) e. ~H /\ A. z e. ran T ( ( x -h ( T ` x ) ) .ih z ) = 0 ) )
47 17 43 46 sylanbrc 
 |-  ( x e. ~H -> ( x -h ( T ` x ) ) e. ( _|_ ` ran T ) )
48 8 pjcompi 
 |-  ( ( ( T ` x ) e. ran T /\ ( x -h ( T ` x ) ) e. ( _|_ ` ran T ) ) -> ( ( projh ` ran T ) ` ( ( T ` x ) +h ( x -h ( T ` x ) ) ) ) = ( T ` x ) )
49 13 47 48 syl2anc 
 |-  ( x e. ~H -> ( ( projh ` ran T ) ` ( ( T ` x ) +h ( x -h ( T ` x ) ) ) ) = ( T ` x ) )
50 hvpncan3 
 |-  ( ( ( T ` x ) e. ~H /\ x e. ~H ) -> ( ( T ` x ) +h ( x -h ( T ` x ) ) ) = x )
51 15 14 50 syl2anc 
 |-  ( x e. ~H -> ( ( T ` x ) +h ( x -h ( T ` x ) ) ) = x )
52 51 fveq2d 
 |-  ( x e. ~H -> ( ( projh ` ran T ) ` ( ( T ` x ) +h ( x -h ( T ` x ) ) ) ) = ( ( projh ` ran T ) ` x ) )
53 49 52 eqtr3d 
 |-  ( x e. ~H -> ( T ` x ) = ( ( projh ` ran T ) ` x ) )
54 11 53 mprgbir 
 |-  T = ( projh ` ran T )