Metamath Proof Explorer

Theorem pjinvari

Description: A closed subspace H with projection T is invariant under an operator S iff S T = T S T . Theorem 27.1 of Halmos p. 45. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

Ref Expression
Hypotheses pjinvar.1 
|- S : ~H --> ~H
pjinvar.2 
|- H e. CH
pjinvar.3 
|- T = ( projh ` H )
Assertion pjinvari 
|- ( ( S o. T ) : ~H --> H <-> ( S o. T ) = ( T o. ( S o. T ) ) )

Proof

Step Hyp Ref Expression
1 pjinvar.1 
 |-  S : ~H --> ~H
2 pjinvar.2 
 |-  H e. CH
3 pjinvar.3 
 |-  T = ( projh ` H )
4 3 fveq1i 
 |-  ( T ` ( ( S o. T ) ` x ) ) = ( ( projh ` H ) ` ( ( S o. T ) ` x ) )
5 ffvelrn 
 |-  ( ( ( S o. T ) : ~H --> H /\ x e. ~H ) -> ( ( S o. T ) ` x ) e. H )
6 pjid 
 |-  ( ( H e. CH /\ ( ( S o. T ) ` x ) e. H ) -> ( ( projh ` H ) ` ( ( S o. T ) ` x ) ) = ( ( S o. T ) ` x ) )
7 2 5 6 sylancr 
 |-  ( ( ( S o. T ) : ~H --> H /\ x e. ~H ) -> ( ( projh ` H ) ` ( ( S o. T ) ` x ) ) = ( ( S o. T ) ` x ) )
8 4 7 syl5req 
 |-  ( ( ( S o. T ) : ~H --> H /\ x e. ~H ) -> ( ( S o. T ) ` x ) = ( T ` ( ( S o. T ) ` x ) ) )
9 fvco3 
 |-  ( ( ( S o. T ) : ~H --> H /\ x e. ~H ) -> ( ( T o. ( S o. T ) ) ` x ) = ( T ` ( ( S o. T ) ` x ) ) )
10 8 9 eqtr4d 
 |-  ( ( ( S o. T ) : ~H --> H /\ x e. ~H ) -> ( ( S o. T ) ` x ) = ( ( T o. ( S o. T ) ) ` x ) )
11 10 ralrimiva 
 |-  ( ( S o. T ) : ~H --> H -> A. x e. ~H ( ( S o. T ) ` x ) = ( ( T o. ( S o. T ) ) ` x ) )
12 2 pjfoi 
 |-  ( projh ` H ) : ~H -onto-> H
13 fof 
 |-  ( ( projh ` H ) : ~H -onto-> H -> ( projh ` H ) : ~H --> H )
14 12 13 ax-mp 
 |-  ( projh ` H ) : ~H --> H
15 3 feq1i 
 |-  ( T : ~H --> H <-> ( projh ` H ) : ~H --> H )
16 14 15 mpbir 
 |-  T : ~H --> H
17 2 chssii 
 |-  H C_ ~H
18 fss 
 |-  ( ( T : ~H --> H /\ H C_ ~H ) -> T : ~H --> ~H )
19 16 17 18 mp2an 
 |-  T : ~H --> ~H
20 1 19 hocofni 
 |-  ( S o. T ) Fn ~H
21 1 19 hocofi 
 |-  ( S o. T ) : ~H --> ~H
22 19 21 hocofni 
 |-  ( T o. ( S o. T ) ) Fn ~H
23 eqfnfv 
 |-  ( ( ( S o. T ) Fn ~H /\ ( T o. ( S o. T ) ) Fn ~H ) -> ( ( S o. T ) = ( T o. ( S o. T ) ) <-> A. x e. ~H ( ( S o. T ) ` x ) = ( ( T o. ( S o. T ) ) ` x ) ) )
24 20 22 23 mp2an 
 |-  ( ( S o. T ) = ( T o. ( S o. T ) ) <-> A. x e. ~H ( ( S o. T ) ` x ) = ( ( T o. ( S o. T ) ) ` x ) )
25 11 24 sylibr 
 |-  ( ( S o. T ) : ~H --> H -> ( S o. T ) = ( T o. ( S o. T ) ) )
26 fco 
 |-  ( ( T : ~H --> H /\ ( S o. T ) : ~H --> ~H ) -> ( T o. ( S o. T ) ) : ~H --> H )
27 16 21 26 mp2an 
 |-  ( T o. ( S o. T ) ) : ~H --> H
28 feq1 
 |-  ( ( S o. T ) = ( T o. ( S o. T ) ) -> ( ( S o. T ) : ~H --> H <-> ( T o. ( S o. T ) ) : ~H --> H ) )
29 27 28 mpbiri 
 |-  ( ( S o. T ) = ( T o. ( S o. T ) ) -> ( S o. T ) : ~H --> H )
30 25 29 impbii 
 |-  ( ( S o. T ) : ~H --> H <-> ( S o. T ) = ( T o. ( S o. T ) ) )