Theorem pjtoi

Description: Subspace sum of projection and projection of orthocomplement. (Contributed by NM, 16-Nov-2000) (New usage is discouraged.)

	Ref	Expression
Hypothesis	pjidmco.1	⊢ 𝐻 ∈ Cℋ
Assertion	pjtoi	⊢ ( ( projℎ ‘ 𝐻 ) +op ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ) = ( projℎ ‘ ℋ )

Proof

Step	Hyp	Ref	Expression
1		pjidmco.1	⊢ 𝐻 ∈ Cℋ
2		axpjpj	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝑥 ∈ ℋ ) → 𝑥 = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝑥 ) ) )
3	1 2	mpan	⊢ ( 𝑥 ∈ ℋ → 𝑥 = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝑥 ) ) )
4		pjch1	⊢ ( 𝑥 ∈ ℋ → ( ( projℎ ‘ ℋ ) ‘ 𝑥 ) = 𝑥 )
5	1	pjfi	⊢ ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ
6	1	choccli	⊢ ( ⊥ ‘ 𝐻 ) ∈ Cℋ
7	6	pjfi	⊢ ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) : ℋ ⟶ ℋ
8		hosval	⊢ ( ( ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ ∧ ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( ( projℎ ‘ 𝐻 ) +op ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝑥 ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝑥 ) ) )
9	5 7 8	mp3an12	⊢ ( 𝑥 ∈ ℋ → ( ( ( projℎ ‘ 𝐻 ) +op ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝑥 ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝑥 ) ) )
10	3 4 9	3eqtr4rd	⊢ ( 𝑥 ∈ ℋ → ( ( ( projℎ ‘ 𝐻 ) +op ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝑥 ) = ( ( projℎ ‘ ℋ ) ‘ 𝑥 ) )
11	10	rgen	⊢ ∀ 𝑥 ∈ ℋ ( ( ( projℎ ‘ 𝐻 ) +op ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝑥 ) = ( ( projℎ ‘ ℋ ) ‘ 𝑥 )
12	5 7	hoaddcli	⊢ ( ( projℎ ‘ 𝐻 ) +op ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ) : ℋ ⟶ ℋ
13		helch	⊢ ℋ ∈ Cℋ
14	13	pjfi	⊢ ( projℎ ‘ ℋ ) : ℋ ⟶ ℋ
15	12 14	hoeqi	⊢ ( ∀ 𝑥 ∈ ℋ ( ( ( projℎ ‘ 𝐻 ) +op ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝑥 ) = ( ( projℎ ‘ ℋ ) ‘ 𝑥 ) ↔ ( ( projℎ ‘ 𝐻 ) +op ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ) = ( projℎ ‘ ℋ ) )
16	11 15	mpbi	⊢ ( ( projℎ ‘ 𝐻 ) +op ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ) = ( projℎ ‘ ℋ )