# Metamath Proof Explorer

## Theorem pjeq

Description: Equality with a projection. (Contributed by NM, 20-Jan-2007) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Assertion pjeq ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {A}\in ℋ\right)\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={B}↔\left({B}\in {H}\wedge \exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={B}{+}_{ℎ}{x}\right)\right)$

### Proof

Step Hyp Ref Expression
1 pjhth ${⊢}{H}\in {\mathbf{C}}_{ℋ}\to {H}{+}_{ℋ}\perp \left({H}\right)=ℋ$
2 1 eleq2d ${⊢}{H}\in {\mathbf{C}}_{ℋ}\to \left({A}\in \left({H}{+}_{ℋ}\perp \left({H}\right)\right)↔{A}\in ℋ\right)$
3 2 biimpar ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {A}\in ℋ\right)\to {A}\in \left({H}{+}_{ℋ}\perp \left({H}\right)\right)$
4 pjpreeq ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {A}\in \left({H}{+}_{ℋ}\perp \left({H}\right)\right)\right)\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={B}↔\left({B}\in {H}\wedge \exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={B}{+}_{ℎ}{x}\right)\right)$
5 3 4 syldan ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {A}\in ℋ\right)\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={B}↔\left({B}\in {H}\wedge \exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={B}{+}_{ℎ}{x}\right)\right)$