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:\mathscr{H}⟶\mathscr{H}$$
	pjinvar.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
	pjinvar.3	$$⊢T={\mathrm{proj}}_{ℎ}\left(H\right)$$
Assertion	pjinvari	$$⊢\left(S\circ T\right):\mathscr{H}⟶H\leftrightarrow S\circ T=T\circ \left(S\circ T\right)$$

Proof

Step	Hyp	Ref	Expression
1		pjinvar.1	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
2		pjinvar.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
3		pjinvar.3	$$⊢T={\mathrm{proj}}_{ℎ}\left(H\right)$$
4	3	fveq1i	$$⊢T\left(\left(S\circ T\right)\left(x\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(\left(S\circ T\right)\left(x\right)\right)$$
5		ffvelcdm	$$⊢\left(\left(S\circ T\right):\mathscr{H}⟶H\wedge x\in \mathscr{H}\right)\to \left(S\circ T\right)\left(x\right)\in H$$
6		pjid	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge \left(S\circ T\right)\left(x\right)\in H\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(\left(S\circ T\right)\left(x\right)\right)=\left(S\circ T\right)\left(x\right)$$
7	2 5 6	sylancr	$$⊢\left(\left(S\circ T\right):\mathscr{H}⟶H\wedge x\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(\left(S\circ T\right)\left(x\right)\right)=\left(S\circ T\right)\left(x\right)$$
8	4 7	eqtr2id	$$⊢\left(\left(S\circ T\right):\mathscr{H}⟶H\wedge x\in \mathscr{H}\right)\to \left(S\circ T\right)\left(x\right)=T\left(\left(S\circ T\right)\left(x\right)\right)$$
9		fvco3	$$⊢\left(\left(S\circ T\right):\mathscr{H}⟶H\wedge x\in \mathscr{H}\right)\to \left(T\circ \left(S\circ T\right)\right)\left(x\right)=T\left(\left(S\circ T\right)\left(x\right)\right)$$
10	8 9	eqtr4d	$$⊢\left(\left(S\circ T\right):\mathscr{H}⟶H\wedge x\in \mathscr{H}\right)\to \left(S\circ T\right)\left(x\right)=\left(T\circ \left(S\circ T\right)\right)\left(x\right)$$
11	10	ralrimiva	$$⊢\left(S\circ T\right):\mathscr{H}⟶H\to \forall x\in \mathscr{H}\left(S\circ T\right)\left(x\right)=\left(T\circ \left(S\circ T\right)\right)\left(x\right)$$
12	2	pjfoi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}\underset{onto}{⟶}H$$
13		fof	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}\underset{onto}{⟶}H\to {\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶H$$
14	12 13	ax-mp	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶H$$
15	3	feq1i	$$⊢T:\mathscr{H}⟶H\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶H$$
16	14 15	mpbir	$$⊢T:\mathscr{H}⟶H$$
17	2	chssii	$$⊢H\subseteq \mathscr{H}$$
18		fss	$$⊢\left(T:\mathscr{H}⟶H\wedge H\subseteq \mathscr{H}\right)\to T:\mathscr{H}⟶\mathscr{H}$$
19	16 17 18	mp2an	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
20	1 19	hocofni	$$⊢\left(S\circ T\right)Fn\mathscr{H}$$
21	1 19	hocofi	$$⊢\left(S\circ T\right):\mathscr{H}⟶\mathscr{H}$$
22	19 21	hocofni	$$⊢\left(T\circ \left(S\circ T\right)\right)Fn\mathscr{H}$$
23		eqfnfv	$$⊢\left(\left(S\circ T\right)Fn\mathscr{H}\wedge \left(T\circ \left(S\circ T\right)\right)Fn\mathscr{H}\right)\to \left(S\circ T=T\circ \left(S\circ T\right)\leftrightarrow \forall x\in \mathscr{H}\left(S\circ T\right)\left(x\right)=\left(T\circ \left(S\circ T\right)\right)\left(x\right)\right)$$
24	20 22 23	mp2an	$$⊢S\circ T=T\circ \left(S\circ T\right)\leftrightarrow \forall x\in \mathscr{H}\left(S\circ T\right)\left(x\right)=\left(T\circ \left(S\circ T\right)\right)\left(x\right)$$
25	11 24	sylibr	$$⊢\left(S\circ T\right):\mathscr{H}⟶H\to S\circ T=T\circ \left(S\circ T\right)$$
26		fco	$$⊢\left(T:\mathscr{H}⟶H\wedge \left(S\circ T\right):\mathscr{H}⟶\mathscr{H}\right)\to \left(T\circ \left(S\circ T\right)\right):\mathscr{H}⟶H$$
27	16 21 26	mp2an	$$⊢\left(T\circ \left(S\circ T\right)\right):\mathscr{H}⟶H$$
28		feq1	$$⊢S\circ T=T\circ \left(S\circ T\right)\to \left(\left(S\circ T\right):\mathscr{H}⟶H\leftrightarrow \left(T\circ \left(S\circ T\right)\right):\mathscr{H}⟶H\right)$$
29	27 28	mpbiri	$$⊢S\circ T=T\circ \left(S\circ T\right)\to \left(S\circ T\right):\mathscr{H}⟶H$$
30	25 29	impbii	$$⊢\left(S\circ T\right):\mathscr{H}⟶H\leftrightarrow S\circ T=T\circ \left(S\circ T\right)$$