Theorem pj11i

Description: One-to-one correspondence of projection and subspace. (Contributed by NM, 26-Nov-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjsumt.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
	pjsumt.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pj11i	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(H\right)\leftrightarrow G=H$$

Proof

Step	Hyp	Ref	Expression
1		pjsumt.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjsumt.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
3		rneq	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(H\right)\to \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(G\right)=\mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)$$
4	1	pjrni	$$⊢\mathrm{ran}{\mathrm{proj}}_{ℎ}\left(G\right)=G$$
5	2	pjrni	$$⊢\mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)=H$$
6	3 4 5	3eqtr3g	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(H\right)\to G=H$$
7		fveq2	$$⊢G=H\to {\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(H\right)$$
8	6 7	impbii	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(H\right)\leftrightarrow G=H$$