Theorem pjsubi

Description: Projection of vector difference is difference of projections. (Contributed by NM, 14-Nov-2000) (New usage is discouraged.)

	Ref	Expression
Hypothesis	pjadjt.1	⊢ 𝐻 ∈ Cℋ
Assertion	pjsubi	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 −ℎ 𝐵 ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pjadjt.1	⊢ 𝐻 ∈ Cℋ
2		fvoveq1	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 −ℎ 𝐵 ) ) = ( ( projℎ ‘ 𝐻 ) ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐵 ) ) )
3		fveq2	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) = ( ( projℎ ‘ 𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) )
4	3	oveq1d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) )
5	2 4	eqeq12d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 −ℎ 𝐵 ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) ↔ ( ( projℎ ‘ 𝐻 ) ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐵 ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) ) )
6		oveq2	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐵 ) = ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) )
7	6	fveq2d	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( ( projℎ ‘ 𝐻 ) ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐵 ) ) = ( ( projℎ ‘ 𝐻 ) ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) )
8		fveq2	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) = ( ( projℎ ‘ 𝐻 ) ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) )
9	8	oveq2d	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( ( ( projℎ ‘ 𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) )
10	7 9	eqeq12d	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( ( ( projℎ ‘ 𝐻 ) ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐵 ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) ↔ ( ( projℎ ‘ 𝐻 ) ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) ) )
11		ifhvhv0	⊢ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ∈ ℋ
12		ifhvhv0	⊢ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ∈ ℋ
13	1 11 12	pjsubii	⊢ ( ( projℎ ‘ 𝐻 ) ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) )
14	5 10 13	dedth2h	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 −ℎ 𝐵 ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) )