Theorem axpjcl

Description: Closure of a projection in its subspace. If we consider this together with axpjpj to be axioms, the need for the ax-hcompl can often be avoided for the kinds of theorems we are interested in here. An interesting project is to see how far we can go by using them in place of it. In particular, we can prove the orthomodular law pjomli .) (Contributed by NM, 23-Oct-1999) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	axpjcl	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ 𝐻 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) = ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 )
2		pjeq	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) = ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ↔ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ 𝐻 ∧ ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ 𝑥 ) ) ) )
3	1 2	mpbii	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ 𝐻 ∧ ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ 𝑥 ) ) )
4	3	simpld	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ 𝐻 )