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

Metamath Proof Explorer

Theorem pjeq

Description: Equality with a projection. (Contributed by NM, 20-Jan-2007) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Assertion pjeq ⊢ H ∈ C ℋ ∧ A ∈ ℋ → proj ℎ ⁡ H ⁡ A = B ↔ B ∈ H ∧ ∃ x ∈ ⊥ ⁡ H A = B + ℎ x

Proof

Step Hyp Ref Expression
1 pjhth ⊢ H ∈ C ℋ → H + ℋ ⊥ ⁡ H = ℋ
2 1 eleq2d ⊢ H ∈ C ℋ → A ∈ H + ℋ ⊥ ⁡ H ↔ A ∈ ℋ
3 2 biimpar ⊢ H ∈ C ℋ ∧ A ∈ ℋ → A ∈ H + ℋ ⊥ ⁡ H
4 pjpreeq ⊢ H ∈ C ℋ ∧ A ∈ H + ℋ ⊥ ⁡ H → proj ℎ ⁡ H ⁡ A = B ↔ B ∈ H ∧ ∃ x ∈ ⊥ ⁡ H A = B + ℎ x
5 3 4 syldan ⊢ H ∈ C ℋ ∧ A ∈ ℋ → proj ℎ ⁡ H ⁡ A = B ↔ B ∈ H ∧ ∃ x ∈ ⊥ ⁡ H A = B + ℎ x