Theorem pj11

Description: One-to-one correspondence of projection and subspace. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	pj11	$$⊢\left(G\in {\mathbf{C}}_{\mathscr{H}}\wedge H\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left({\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(H\right)\leftrightarrow G=H\right)$$

Proof

Step	Hyp	Ref	Expression
1		fveqeq2	$$⊢G=if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,0_{\mathscr{H}}\right)\to \left({\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(H\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,0_{\mathscr{H}}\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)\right)$$
2		eqeq1	$$⊢G=if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,0_{\mathscr{H}}\right)\to \left(G=H\leftrightarrow if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,0_{\mathscr{H}}\right)=H\right)$$
3	1 2	bibi12d	$$⊢G=if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,0_{\mathscr{H}}\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(H\right)\leftrightarrow G=H\right)\leftrightarrow \left({\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,0_{\mathscr{H}}\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)\leftrightarrow if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,0_{\mathscr{H}}\right)=H\right)\right)$$
4		fveq2	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)$$
5	4	eqeq2d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to \left({\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,0_{\mathscr{H}}\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,0_{\mathscr{H}}\right)\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)\right)$$
6		eqeq2	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to \left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,0_{\mathscr{H}}\right)=H\leftrightarrow if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,0_{\mathscr{H}}\right)=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)$$
7	5 6	bibi12d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,0_{\mathscr{H}}\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)\leftrightarrow if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,0_{\mathscr{H}}\right)=H\right)\leftrightarrow \left({\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,0_{\mathscr{H}}\right)\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)\leftrightarrow if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,0_{\mathscr{H}}\right)=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)\right)$$
8		h0elch	$$⊢0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}$$
9	8	elimel	$$⊢if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,0_{\mathscr{H}}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
10	8	elimel	$$⊢if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
11	9 10	pj11i	$$⊢{\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,0_{\mathscr{H}}\right)\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)\leftrightarrow if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,0_{\mathscr{H}}\right)=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)$$
12	3 7 11	dedth2h	$$⊢\left(G\in {\mathbf{C}}_{\mathscr{H}}\wedge H\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left({\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(H\right)\leftrightarrow G=H\right)$$