# Metamath Proof Explorer

## Theorem dfpjop

Description: Definition of projection operator in Hughes p. 47, except that we do not need linearity to be explicit by virtue of hmoplin . (Contributed by NM, 24-Apr-2006) (Revised by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

Ref Expression
Assertion dfpjop ( 𝑇 ∈ ran proj ↔ ( 𝑇 ∈ HrmOp ∧ ( 𝑇𝑇 ) = 𝑇 ) )

### Proof

Step Hyp Ref Expression
1 pjmfn proj Fn C
2 fvelrnb ( proj Fn C → ( 𝑇 ∈ ran proj ↔ ∃ 𝑥C ( proj𝑥 ) = 𝑇 ) )
3 1 2 ax-mp ( 𝑇 ∈ ran proj ↔ ∃ 𝑥C ( proj𝑥 ) = 𝑇 )
4 pjhmop ( 𝑥C → ( proj𝑥 ) ∈ HrmOp )
5 pjidmco ( 𝑥C → ( ( proj𝑥 ) ∘ ( proj𝑥 ) ) = ( proj𝑥 ) )
6 4 5 jca ( 𝑥C → ( ( proj𝑥 ) ∈ HrmOp ∧ ( ( proj𝑥 ) ∘ ( proj𝑥 ) ) = ( proj𝑥 ) ) )
7 eleq1 ( ( proj𝑥 ) = 𝑇 → ( ( proj𝑥 ) ∈ HrmOp ↔ 𝑇 ∈ HrmOp ) )
8 id ( ( proj𝑥 ) = 𝑇 → ( proj𝑥 ) = 𝑇 )
9 8 8 coeq12d ( ( proj𝑥 ) = 𝑇 → ( ( proj𝑥 ) ∘ ( proj𝑥 ) ) = ( 𝑇𝑇 ) )
10 9 8 eqeq12d ( ( proj𝑥 ) = 𝑇 → ( ( ( proj𝑥 ) ∘ ( proj𝑥 ) ) = ( proj𝑥 ) ↔ ( 𝑇𝑇 ) = 𝑇 ) )
11 7 10 anbi12d ( ( proj𝑥 ) = 𝑇 → ( ( ( proj𝑥 ) ∈ HrmOp ∧ ( ( proj𝑥 ) ∘ ( proj𝑥 ) ) = ( proj𝑥 ) ) ↔ ( 𝑇 ∈ HrmOp ∧ ( 𝑇𝑇 ) = 𝑇 ) ) )
12 6 11 syl5ibcom ( 𝑥C → ( ( proj𝑥 ) = 𝑇 → ( 𝑇 ∈ HrmOp ∧ ( 𝑇𝑇 ) = 𝑇 ) ) )
13 12 rexlimiv ( ∃ 𝑥C ( proj𝑥 ) = 𝑇 → ( 𝑇 ∈ HrmOp ∧ ( 𝑇𝑇 ) = 𝑇 ) )
14 3 13 sylbi ( 𝑇 ∈ ran proj → ( 𝑇 ∈ HrmOp ∧ ( 𝑇𝑇 ) = 𝑇 ) )
15 hmopidmpj ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇𝑇 ) = 𝑇 ) → 𝑇 = ( proj ‘ ran 𝑇 ) )
16 hmopidmch ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇𝑇 ) = 𝑇 ) → ran 𝑇C )
17 fnfvelrn ( ( proj Fn C ∧ ran 𝑇C ) → ( proj ‘ ran 𝑇 ) ∈ ran proj )
18 1 16 17 sylancr ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇𝑇 ) = 𝑇 ) → ( proj ‘ ran 𝑇 ) ∈ ran proj )
19 15 18 eqeltrd ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇𝑇 ) = 𝑇 ) → 𝑇 ∈ ran proj )
20 14 19 impbii ( 𝑇 ∈ ran proj ↔ ( 𝑇 ∈ HrmOp ∧ ( 𝑇𝑇 ) = 𝑇 ) )