# Metamath Proof Explorer

## Theorem axpjcl

Description: Closure of a projection in its subspace. If we consider this together with axpjpj to be axioms, the need for the ax-hcompl can often be avoided for the kinds of theorems we are interested in here. An interesting project is to see how far we can go by using them in place of it. In particular, we can prove the orthomodular law pjomli .) (Contributed by NM, 23-Oct-1999) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Assertion axpjcl ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {A}\in ℋ\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in {H}$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)$
2 pjeq ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {A}\in ℋ\right)\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)↔\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in {H}\wedge \exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right){+}_{ℎ}{x}\right)\right)$
3 1 2 mpbii ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {A}\in ℋ\right)\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in {H}\wedge \exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right){+}_{ℎ}{x}\right)$
4 3 simpld ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {A}\in ℋ\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in {H}$