Description: Reconstruction of the subspace of a projection operator. Part of Theorem 26.2 of Halmos p. 44. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | elpjch | |- ( T e. ran projh -> ( ran T e. CH /\ T = ( projh ` ran T ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfpjop | |- ( T e. ran projh <-> ( T e. HrmOp /\ ( T o. T ) = T ) ) |
|
| 2 | hmopidmch | |- ( ( T e. HrmOp /\ ( T o. T ) = T ) -> ran T e. CH ) |
|
| 3 | hmopidmpj | |- ( ( T e. HrmOp /\ ( T o. T ) = T ) -> T = ( projh ` ran T ) ) |
|
| 4 | 2 3 | jca | |- ( ( T e. HrmOp /\ ( T o. T ) = T ) -> ( ran T e. CH /\ T = ( projh ` ran T ) ) ) |
| 5 | 1 4 | sylbi | |- ( T e. ran projh -> ( ran T e. CH /\ T = ( projh ` ran T ) ) ) |