This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pjidmi

Description: A projection is idempotent. Property (ii) of Beran p. 109. (Contributed by NM, 28-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses pjidm.1 ⊢ H ∈ C ℋ
pjidm.2 ⊢ A ∈ ℋ
Assertion pjidmi ⊢ proj ℎ ⁡ H ⁡ proj ℎ ⁡ H ⁡ A = proj ℎ ⁡ H ⁡ A

Proof

Step Hyp Ref Expression
1 pjidm.1 ⊢ H ∈ C ℋ
2 pjidm.2 ⊢ A ∈ ℋ
3 1 2 pjclii ⊢ proj ℎ ⁡ H ⁡ A ∈ H
4 1 2 pjhclii ⊢ proj ℎ ⁡ H ⁡ A ∈ ℋ
5 1 4 pjchi ⊢ proj ℎ ⁡ H ⁡ A ∈ H ↔ proj ℎ ⁡ H ⁡ proj ℎ ⁡ H ⁡ A = proj ℎ ⁡ H ⁡ A
6 3 5 mpbi ⊢ proj ℎ ⁡ H ⁡ proj ℎ ⁡ H ⁡ A = proj ℎ ⁡ H ⁡ A