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 T Fn
10 fvelrnb T Fn 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 T Fn 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 abbi2dv 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 syl6eqr T ran proj ran T = x | T x = x