This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pjaddi

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

		Ref	Expression
	Hypothesis	pjadjt.1	⊢ 𝐻 ∈ C_ℋ
	Assertion	pjaddi	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 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	pjaddii	⊢ ( ( proj_ℎ ‘ 𝐻 ) ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) +_ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ) ) = ( ( ( proj_ℎ ‘ 𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ) +_ℎ ( ( proj_ℎ ‘ 𝐻 ) ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ) )
14	5 10 13	dedth2h	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( proj_ℎ ‘ 𝐻 ) ‘ ( 𝐴 +_ℎ 𝐵 ) ) = ( ( ( proj_ℎ ‘ 𝐻 ) ‘ 𝐴 ) +_ℎ ( ( proj_ℎ ‘ 𝐻 ) ‘ 𝐵 ) ) )