# Metamath Proof Explorer

## Theorem pjhfval

Description: The value of the projection map. (Contributed by NM, 23-Oct-1999) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion pjhfval ${⊢}{H}\in {\mathbf{C}}_{ℋ}\to {\mathrm{proj}}_{ℎ}\left({H}\right)=\left({x}\in ℋ⟼\left(\iota {z}\in {H}|\exists {y}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{x}={z}{+}_{ℎ}{y}\right)\right)$

### Proof

Step Hyp Ref Expression
1 id ${⊢}{h}={H}\to {h}={H}$
2 fveq2 ${⊢}{h}={H}\to \perp \left({h}\right)=\perp \left({H}\right)$
3 2 rexeqdv ${⊢}{h}={H}\to \left(\exists {y}\in \perp \left({h}\right)\phantom{\rule{.4em}{0ex}}{x}={z}{+}_{ℎ}{y}↔\exists {y}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{x}={z}{+}_{ℎ}{y}\right)$
4 1 3 riotaeqbidv ${⊢}{h}={H}\to \left(\iota {z}\in {h}|\exists {y}\in \perp \left({h}\right)\phantom{\rule{.4em}{0ex}}{x}={z}{+}_{ℎ}{y}\right)=\left(\iota {z}\in {H}|\exists {y}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{x}={z}{+}_{ℎ}{y}\right)$
5 4 mpteq2dv ${⊢}{h}={H}\to \left({x}\in ℋ⟼\left(\iota {z}\in {h}|\exists {y}\in \perp \left({h}\right)\phantom{\rule{.4em}{0ex}}{x}={z}{+}_{ℎ}{y}\right)\right)=\left({x}\in ℋ⟼\left(\iota {z}\in {H}|\exists {y}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{x}={z}{+}_{ℎ}{y}\right)\right)$
6 df-pjh ${⊢}{\mathrm{proj}}_{ℎ}=\left({h}\in {\mathbf{C}}_{ℋ}⟼\left({x}\in ℋ⟼\left(\iota {z}\in {h}|\exists {y}\in \perp \left({h}\right)\phantom{\rule{.4em}{0ex}}{x}={z}{+}_{ℎ}{y}\right)\right)\right)$
7 ax-hilex ${⊢}ℋ\in \mathrm{V}$
8 7 mptex ${⊢}\left({x}\in ℋ⟼\left(\iota {z}\in {H}|\exists {y}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{x}={z}{+}_{ℎ}{y}\right)\right)\in \mathrm{V}$
9 5 6 8 fvmpt ${⊢}{H}\in {\mathbf{C}}_{ℋ}\to {\mathrm{proj}}_{ℎ}\left({H}\right)=\left({x}\in ℋ⟼\left(\iota {z}\in {H}|\exists {y}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{x}={z}{+}_{ℎ}{y}\right)\right)$