Theorem elpjrn

Description: Reconstruction of the subspace of a projection operator. (Contributed by NM, 24-Apr-2006) (Revised by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	elpjrn	⊢ ( 𝑇 ∈ ran projℎ → ran 𝑇 = { 𝑥 ∈ ℋ ∣ ( 𝑇 ‘ 𝑥 ) = 𝑥 } )

Proof

Step	Hyp	Ref	Expression
1		elpjch	⊢ ( 𝑇 ∈ ran projℎ → ( ran 𝑇 ∈ Cℋ ∧ 𝑇 = ( projℎ ‘ ran 𝑇 ) ) )
2	1	simpld	⊢ ( 𝑇 ∈ ran projℎ → ran 𝑇 ∈ Cℋ )
3		chss	⊢ ( ran 𝑇 ∈ Cℋ → ran 𝑇 ⊆ ℋ )
4	2 3	syl	⊢ ( 𝑇 ∈ ran projℎ → ran 𝑇 ⊆ ℋ )
5	4	sseld	⊢ ( 𝑇 ∈ ran projℎ → ( 𝑥 ∈ ran 𝑇 → 𝑥 ∈ ℋ ) )
6		elpjhmop	⊢ ( 𝑇 ∈ ran projℎ → 𝑇 ∈ HrmOp )
7		hmopf	⊢ ( 𝑇 ∈ HrmOp → 𝑇 : ℋ ⟶ ℋ )
8	6 7	syl	⊢ ( 𝑇 ∈ ran projℎ → 𝑇 : ℋ ⟶ ℋ )
9	8	ffnd	⊢ ( 𝑇 ∈ ran projℎ → 𝑇 Fn ℋ )
10		fvelrnb	⊢ ( 𝑇 Fn ℋ → ( 𝑥 ∈ ran 𝑇 ↔ ∃ 𝑦 ∈ ℋ ( 𝑇 ‘ 𝑦 ) = 𝑥 ) )
11	9 10	syl	⊢ ( 𝑇 ∈ ran projℎ → ( 𝑥 ∈ ran 𝑇 ↔ ∃ 𝑦 ∈ ℋ ( 𝑇 ‘ 𝑦 ) = 𝑥 ) )
12		fvco3	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑇 ∘ 𝑇 ) ‘ 𝑦 ) = ( 𝑇 ‘ ( 𝑇 ‘ 𝑦 ) ) )
13	8 12	sylan	⊢ ( ( 𝑇 ∈ ran projℎ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑇 ∘ 𝑇 ) ‘ 𝑦 ) = ( 𝑇 ‘ ( 𝑇 ‘ 𝑦 ) ) )
14		elpjidm	⊢ ( 𝑇 ∈ ran projℎ → ( 𝑇 ∘ 𝑇 ) = 𝑇 )
15	14	adantr	⊢ ( ( 𝑇 ∈ ran projℎ ∧ 𝑦 ∈ ℋ ) → ( 𝑇 ∘ 𝑇 ) = 𝑇 )
16	15	fveq1d	⊢ ( ( 𝑇 ∈ ran projℎ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑇 ∘ 𝑇 ) ‘ 𝑦 ) = ( 𝑇 ‘ 𝑦 ) )
17	13 16	eqtr3d	⊢ ( ( 𝑇 ∈ ran projℎ ∧ 𝑦 ∈ ℋ ) → ( 𝑇 ‘ ( 𝑇 ‘ 𝑦 ) ) = ( 𝑇 ‘ 𝑦 ) )
18		fveq2	⊢ ( ( 𝑇 ‘ 𝑦 ) = 𝑥 → ( 𝑇 ‘ ( 𝑇 ‘ 𝑦 ) ) = ( 𝑇 ‘ 𝑥 ) )
19		id	⊢ ( ( 𝑇 ‘ 𝑦 ) = 𝑥 → ( 𝑇 ‘ 𝑦 ) = 𝑥 )
20	18 19	eqeq12d	⊢ ( ( 𝑇 ‘ 𝑦 ) = 𝑥 → ( ( 𝑇 ‘ ( 𝑇 ‘ 𝑦 ) ) = ( 𝑇 ‘ 𝑦 ) ↔ ( 𝑇 ‘ 𝑥 ) = 𝑥 ) )
21	17 20	syl5ibcom	⊢ ( ( 𝑇 ∈ ran projℎ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑦 ) = 𝑥 → ( 𝑇 ‘ 𝑥 ) = 𝑥 ) )
22	21	rexlimdva	⊢ ( 𝑇 ∈ ran projℎ → ( ∃ 𝑦 ∈ ℋ ( 𝑇 ‘ 𝑦 ) = 𝑥 → ( 𝑇 ‘ 𝑥 ) = 𝑥 ) )
23	11 22	sylbid	⊢ ( 𝑇 ∈ ran projℎ → ( 𝑥 ∈ ran 𝑇 → ( 𝑇 ‘ 𝑥 ) = 𝑥 ) )
24	5 23	jcad	⊢ ( 𝑇 ∈ ran projℎ → ( 𝑥 ∈ ran 𝑇 → ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) = 𝑥 ) ) )
25		fnfvelrn	⊢ ( ( 𝑇 Fn ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ 𝑥 ) ∈ ran 𝑇 )
26	9 25	sylan	⊢ ( ( 𝑇 ∈ ran projℎ ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ 𝑥 ) ∈ ran 𝑇 )
27		eleq1	⊢ ( ( 𝑇 ‘ 𝑥 ) = 𝑥 → ( ( 𝑇 ‘ 𝑥 ) ∈ ran 𝑇 ↔ 𝑥 ∈ ran 𝑇 ) )
28	26 27	syl5ibcom	⊢ ( ( 𝑇 ∈ ran projℎ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) = 𝑥 → 𝑥 ∈ ran 𝑇 ) )
29	28	expimpd	⊢ ( 𝑇 ∈ ran projℎ → ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) = 𝑥 ) → 𝑥 ∈ ran 𝑇 ) )
30	24 29	impbid	⊢ ( 𝑇 ∈ ran projℎ → ( 𝑥 ∈ ran 𝑇 ↔ ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) = 𝑥 ) ) )
31	30	abbi2dv	⊢ ( 𝑇 ∈ ran projℎ → ran 𝑇 = { 𝑥 ∣ ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) = 𝑥 ) } )
32		df-rab	⊢ { 𝑥 ∈ ℋ ∣ ( 𝑇 ‘ 𝑥 ) = 𝑥 } = { 𝑥 ∣ ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) = 𝑥 ) }
33	31 32	eqtr4di	⊢ ( 𝑇 ∈ ran projℎ → ran 𝑇 = { 𝑥 ∈ ℋ ∣ ( 𝑇 ‘ 𝑥 ) = 𝑥 } )