Theorem pjscji

Description: The projection of orthogonal subspaces is the sum of the projections. (Contributed by NM, 11-Nov-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjco.1	⊢ 𝐺 ∈ Cℋ
	pjco.2	⊢ 𝐻 ∈ Cℋ
Assertion	pjscji	⊢ ( 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) → ( projℎ ‘ ( 𝐺 ∨ℋ 𝐻 ) ) = ( ( projℎ ‘ 𝐺 ) +op ( projℎ ‘ 𝐻 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pjco.1	⊢ 𝐺 ∈ Cℋ
2		pjco.2	⊢ 𝐻 ∈ Cℋ
3		pjcjt2	⊢ ( ( 𝐺 ∈ Cℋ ∧ 𝐻 ∈ Cℋ ∧ 𝑥 ∈ ℋ ) → ( 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) → ( ( projℎ ‘ ( 𝐺 ∨ℋ 𝐻 ) ) ‘ 𝑥 ) = ( ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) ) )
4	1 2 3	mp3an12	⊢ ( 𝑥 ∈ ℋ → ( 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) → ( ( projℎ ‘ ( 𝐺 ∨ℋ 𝐻 ) ) ‘ 𝑥 ) = ( ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) ) )
5	4	impcom	⊢ ( ( 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) ∧ 𝑥 ∈ ℋ ) → ( ( projℎ ‘ ( 𝐺 ∨ℋ 𝐻 ) ) ‘ 𝑥 ) = ( ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) )
6	1	pjfi	⊢ ( projℎ ‘ 𝐺 ) : ℋ ⟶ ℋ
7	2	pjfi	⊢ ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ
8		hosval	⊢ ( ( ( projℎ ‘ 𝐺 ) : ℋ ⟶ ℋ ∧ ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( ( projℎ ‘ 𝐺 ) +op ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) = ( ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) )
9	6 7 8	mp3an12	⊢ ( 𝑥 ∈ ℋ → ( ( ( projℎ ‘ 𝐺 ) +op ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) = ( ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) )
10	9	adantl	⊢ ( ( 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) ∧ 𝑥 ∈ ℋ ) → ( ( ( projℎ ‘ 𝐺 ) +op ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) = ( ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) )
11	5 10	eqtr4d	⊢ ( ( 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) ∧ 𝑥 ∈ ℋ ) → ( ( projℎ ‘ ( 𝐺 ∨ℋ 𝐻 ) ) ‘ 𝑥 ) = ( ( ( projℎ ‘ 𝐺 ) +op ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) )
12	11	ralrimiva	⊢ ( 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) → ∀ 𝑥 ∈ ℋ ( ( projℎ ‘ ( 𝐺 ∨ℋ 𝐻 ) ) ‘ 𝑥 ) = ( ( ( projℎ ‘ 𝐺 ) +op ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) )
13	1 2	chjcli	⊢ ( 𝐺 ∨ℋ 𝐻 ) ∈ Cℋ
14	13	pjfi	⊢ ( projℎ ‘ ( 𝐺 ∨ℋ 𝐻 ) ) : ℋ ⟶ ℋ
15	6 7	hoaddcli	⊢ ( ( projℎ ‘ 𝐺 ) +op ( projℎ ‘ 𝐻 ) ) : ℋ ⟶ ℋ
16	14 15	hoeqi	⊢ ( ∀ 𝑥 ∈ ℋ ( ( projℎ ‘ ( 𝐺 ∨ℋ 𝐻 ) ) ‘ 𝑥 ) = ( ( ( projℎ ‘ 𝐺 ) +op ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ↔ ( projℎ ‘ ( 𝐺 ∨ℋ 𝐻 ) ) = ( ( projℎ ‘ 𝐺 ) +op ( projℎ ‘ 𝐻 ) ) )
17	12 16	sylib	⊢ ( 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) → ( projℎ ‘ ( 𝐺 ∨ℋ 𝐻 ) ) = ( ( projℎ ‘ 𝐺 ) +op ( projℎ ‘ 𝐻 ) ) )