Metamath Proof Explorer

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 ⊢T∈ran⁡projℎ→ran⁡T=x∈ℋ|T⁡x=x

Proof

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