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	⊢ 𝑆 : ℋ ⟶ ℋ
	pjinvar.2	⊢ 𝐻 ∈ Cℋ
	pjinvar.3	⊢ 𝑇 = ( projℎ ‘ 𝐻 )
Assertion	pjinvari	⊢ ( ( 𝑆 ∘ 𝑇 ) : ℋ ⟶ 𝐻 ↔ ( 𝑆 ∘ 𝑇 ) = ( 𝑇 ∘ ( 𝑆 ∘ 𝑇 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pjinvar.1	⊢ 𝑆 : ℋ ⟶ ℋ
2		pjinvar.2	⊢ 𝐻 ∈ Cℋ
3		pjinvar.3	⊢ 𝑇 = ( projℎ ‘ 𝐻 )
4	3	fveq1i	⊢ ( 𝑇 ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) = ( ( projℎ ‘ 𝐻 ) ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) )
5		ffvelrn	⊢ ( ( ( 𝑆 ∘ 𝑇 ) : ℋ ⟶ 𝐻 ∧ 𝑥 ∈ ℋ ) → ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ∈ 𝐻 )
6		pjid	⊢ ( ( 𝐻 ∈ Cℋ ∧ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ∈ 𝐻 ) → ( ( projℎ ‘ 𝐻 ) ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) = ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) )
7	2 5 6	sylancr	⊢ ( ( ( 𝑆 ∘ 𝑇 ) : ℋ ⟶ 𝐻 ∧ 𝑥 ∈ ℋ ) → ( ( projℎ ‘ 𝐻 ) ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) = ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) )
8	4 7	eqtr2id	⊢ ( ( ( 𝑆 ∘ 𝑇 ) : ℋ ⟶ 𝐻 ∧ 𝑥 ∈ ℋ ) → ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) = ( 𝑇 ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) )
9		fvco3	⊢ ( ( ( 𝑆 ∘ 𝑇 ) : ℋ ⟶ 𝐻 ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ∘ ( 𝑆 ∘ 𝑇 ) ) ‘ 𝑥 ) = ( 𝑇 ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) )
10	8 9	eqtr4d	⊢ ( ( ( 𝑆 ∘ 𝑇 ) : ℋ ⟶ 𝐻 ∧ 𝑥 ∈ ℋ ) → ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) = ( ( 𝑇 ∘ ( 𝑆 ∘ 𝑇 ) ) ‘ 𝑥 ) )
11	10	ralrimiva	⊢ ( ( 𝑆 ∘ 𝑇 ) : ℋ ⟶ 𝐻 → ∀ 𝑥 ∈ ℋ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) = ( ( 𝑇 ∘ ( 𝑆 ∘ 𝑇 ) ) ‘ 𝑥 ) )
12	2	pjfoi	⊢ ( projℎ ‘ 𝐻 ) : ℋ –onto→ 𝐻
13		fof	⊢ ( ( projℎ ‘ 𝐻 ) : ℋ –onto→ 𝐻 → ( projℎ ‘ 𝐻 ) : ℋ ⟶ 𝐻 )
14	12 13	ax-mp	⊢ ( projℎ ‘ 𝐻 ) : ℋ ⟶ 𝐻
15	3	feq1i	⊢ ( 𝑇 : ℋ ⟶ 𝐻 ↔ ( projℎ ‘ 𝐻 ) : ℋ ⟶ 𝐻 )
16	14 15	mpbir	⊢ 𝑇 : ℋ ⟶ 𝐻
17	2	chssii	⊢ 𝐻 ⊆ ℋ
18		fss	⊢ ( ( 𝑇 : ℋ ⟶ 𝐻 ∧ 𝐻 ⊆ ℋ ) → 𝑇 : ℋ ⟶ ℋ )
19	16 17 18	mp2an	⊢ 𝑇 : ℋ ⟶ ℋ
20	1 19	hocofni	⊢ ( 𝑆 ∘ 𝑇 ) Fn ℋ
21	1 19	hocofi	⊢ ( 𝑆 ∘ 𝑇 ) : ℋ ⟶ ℋ
22	19 21	hocofni	⊢ ( 𝑇 ∘ ( 𝑆 ∘ 𝑇 ) ) Fn ℋ
23		eqfnfv	⊢ ( ( ( 𝑆 ∘ 𝑇 ) Fn ℋ ∧ ( 𝑇 ∘ ( 𝑆 ∘ 𝑇 ) ) Fn ℋ ) → ( ( 𝑆 ∘ 𝑇 ) = ( 𝑇 ∘ ( 𝑆 ∘ 𝑇 ) ) ↔ ∀ 𝑥 ∈ ℋ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) = ( ( 𝑇 ∘ ( 𝑆 ∘ 𝑇 ) ) ‘ 𝑥 ) ) )
24	20 22 23	mp2an	⊢ ( ( 𝑆 ∘ 𝑇 ) = ( 𝑇 ∘ ( 𝑆 ∘ 𝑇 ) ) ↔ ∀ 𝑥 ∈ ℋ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) = ( ( 𝑇 ∘ ( 𝑆 ∘ 𝑇 ) ) ‘ 𝑥 ) )
25	11 24	sylibr	⊢ ( ( 𝑆 ∘ 𝑇 ) : ℋ ⟶ 𝐻 → ( 𝑆 ∘ 𝑇 ) = ( 𝑇 ∘ ( 𝑆 ∘ 𝑇 ) ) )
26		fco	⊢ ( ( 𝑇 : ℋ ⟶ 𝐻 ∧ ( 𝑆 ∘ 𝑇 ) : ℋ ⟶ ℋ ) → ( 𝑇 ∘ ( 𝑆 ∘ 𝑇 ) ) : ℋ ⟶ 𝐻 )
27	16 21 26	mp2an	⊢ ( 𝑇 ∘ ( 𝑆 ∘ 𝑇 ) ) : ℋ ⟶ 𝐻
28		feq1	⊢ ( ( 𝑆 ∘ 𝑇 ) = ( 𝑇 ∘ ( 𝑆 ∘ 𝑇 ) ) → ( ( 𝑆 ∘ 𝑇 ) : ℋ ⟶ 𝐻 ↔ ( 𝑇 ∘ ( 𝑆 ∘ 𝑇 ) ) : ℋ ⟶ 𝐻 ) )
29	27 28	mpbiri	⊢ ( ( 𝑆 ∘ 𝑇 ) = ( 𝑇 ∘ ( 𝑆 ∘ 𝑇 ) ) → ( 𝑆 ∘ 𝑇 ) : ℋ ⟶ 𝐻 )
30	25 29	impbii	⊢ ( ( 𝑆 ∘ 𝑇 ) : ℋ ⟶ 𝐻 ↔ ( 𝑆 ∘ 𝑇 ) = ( 𝑇 ∘ ( 𝑆 ∘ 𝑇 ) ) )