Theorem pjinormii

Description: The inner product of a projection and its argument is the square of the norm of the projection. Remark in Halmos p. 44. (Contributed by NM, 13-Aug-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjidm.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
	pjidm.2	$$⊢A\in \mathscr{H}$$
Assertion	pjinormii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}A={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2$$

Proof

Step	Hyp	Ref	Expression
1		pjidm.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjidm.2	$$⊢A\in \mathscr{H}$$
3	1 2	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}$$
4	3	normsqi	$$⊢{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)$$
5	1 3 2	pjadjii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right){\cdot }_{\mathrm{ih}}A={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)$$
6	1 2	pjidmi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)$$
7	6	oveq1i	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right){\cdot }_{\mathrm{ih}}A={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}A$$
8	4 5 7	3eqtr2ri	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}A={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2$$