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	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) = 𝐵 ↔ ( 𝐵 ∈ 𝐻 ∧ ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝐵 +ℎ 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		pjhth	⊢ ( 𝐻 ∈ Cℋ → ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) = ℋ )
2	1	eleq2d	⊢ ( 𝐻 ∈ Cℋ → ( 𝐴 ∈ ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) ↔ 𝐴 ∈ ℋ ) )
3	2	biimpar	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → 𝐴 ∈ ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) )
4		pjpreeq	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) ) → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) = 𝐵 ↔ ( 𝐵 ∈ 𝐻 ∧ ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝐵 +ℎ 𝑥 ) ) ) )
5	3 4	syldan	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) = 𝐵 ↔ ( 𝐵 ∈ 𝐻 ∧ ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝐵 +ℎ 𝑥 ) ) ) )