# Metamath Proof Explorer

## Theorem pjrni

Description: The range of a projection. Part of Theorem 26.2 of Halmos p. 44. (Contributed by NM, 30-Oct-1999) (Revised by Mario Carneiro, 10-Sep-2015) (New usage is discouraged.)

Ref Expression
Hypothesis pjfn.1 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
Assertion pjrni ${⊢}\mathrm{ran}{\mathrm{proj}}_{ℎ}\left({H}\right)={H}$

### Proof

Step Hyp Ref Expression
1 pjfn.1 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
2 1 pjfni ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right)Fnℋ$
3 1 pjcli ${⊢}{x}\in ℋ\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)\in {H}$
4 3 rgen ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)\in {H}$
5 ffnfv ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right):ℋ⟶{H}↔\left({\mathrm{proj}}_{ℎ}\left({H}\right)Fnℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)\in {H}\right)$
6 2 4 5 mpbir2an ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right):ℋ⟶{H}$
7 frn ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right):ℋ⟶{H}\to \mathrm{ran}{\mathrm{proj}}_{ℎ}\left({H}\right)\subseteq {H}$
8 6 7 ax-mp ${⊢}\mathrm{ran}{\mathrm{proj}}_{ℎ}\left({H}\right)\subseteq {H}$
9 pjid ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {y}\in {H}\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)={y}$
10 1 9 mpan ${⊢}{y}\in {H}\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)={y}$
11 1 cheli ${⊢}{y}\in {H}\to {y}\in ℋ$
12 fnfvelrn ${⊢}\left({\mathrm{proj}}_{ℎ}\left({H}\right)Fnℋ\wedge {y}\in ℋ\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\left({H}\right)$
13 2 11 12 sylancr ${⊢}{y}\in {H}\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\left({H}\right)$
14 10 13 eqeltrrd ${⊢}{y}\in {H}\to {y}\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\left({H}\right)$
15 14 ssriv ${⊢}{H}\subseteq \mathrm{ran}{\mathrm{proj}}_{ℎ}\left({H}\right)$
16 8 15 eqssi ${⊢}\mathrm{ran}{\mathrm{proj}}_{ℎ}\left({H}\right)={H}$