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 ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) )