Theorem pjcjt2

Description: The projection on a subspace join is the sum of the projections. (Contributed by NM, 1-Nov-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	pjcjt2	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐺 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( 𝐻 ⊆ ( ⊥ ‘ 𝐺 ) → ( ( projℎ ‘ ( 𝐻 ∨ℋ 𝐺 ) ) ‘ 𝐴 ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		sseq1	⊢ ( 𝐻 = if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) → ( 𝐻 ⊆ ( ⊥ ‘ 𝐺 ) ↔ if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ⊆ ( ⊥ ‘ 𝐺 ) ) )
2		fvoveq1	⊢ ( 𝐻 = if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) → ( projℎ ‘ ( 𝐻 ∨ℋ 𝐺 ) ) = ( projℎ ‘ ( if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ∨ℋ 𝐺 ) ) )
3	2	fveq1d	⊢ ( 𝐻 = if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) → ( ( projℎ ‘ ( 𝐻 ∨ℋ 𝐺 ) ) ‘ 𝐴 ) = ( ( projℎ ‘ ( if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ∨ℋ 𝐺 ) ) ‘ 𝐴 ) )
4		fveq2	⊢ ( 𝐻 = if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) → ( projℎ ‘ 𝐻 ) = ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ) )
5	4	fveq1d	⊢ ( 𝐻 = if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) → ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) = ( ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ) ‘ 𝐴 ) )
6	5	oveq1d	⊢ ( 𝐻 = if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) = ( ( ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) )
7	3 6	eqeq12d	⊢ ( 𝐻 = if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) → ( ( ( projℎ ‘ ( 𝐻 ∨ℋ 𝐺 ) ) ‘ 𝐴 ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ↔ ( ( projℎ ‘ ( if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ∨ℋ 𝐺 ) ) ‘ 𝐴 ) = ( ( ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ) )
8	1 7	imbi12d	⊢ ( 𝐻 = if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) → ( ( 𝐻 ⊆ ( ⊥ ‘ 𝐺 ) → ( ( projℎ ‘ ( 𝐻 ∨ℋ 𝐺 ) ) ‘ 𝐴 ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ) ↔ ( if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ⊆ ( ⊥ ‘ 𝐺 ) → ( ( projℎ ‘ ( if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ∨ℋ 𝐺 ) ) ‘ 𝐴 ) = ( ( ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ) ) )
9		fveq2	⊢ ( 𝐺 = if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) → ( ⊥ ‘ 𝐺 ) = ( ⊥ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) )
10	9	sseq2d	⊢ ( 𝐺 = if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) → ( if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ⊆ ( ⊥ ‘ 𝐺 ) ↔ if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ⊆ ( ⊥ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) ) )
11		oveq2	⊢ ( 𝐺 = if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) → ( if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ∨ℋ 𝐺 ) = ( if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ∨ℋ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) )
12	11	fveq2d	⊢ ( 𝐺 = if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) → ( projℎ ‘ ( if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ∨ℋ 𝐺 ) ) = ( projℎ ‘ ( if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ∨ℋ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) ) )
13	12	fveq1d	⊢ ( 𝐺 = if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) → ( ( projℎ ‘ ( if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ∨ℋ 𝐺 ) ) ‘ 𝐴 ) = ( ( projℎ ‘ ( if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ∨ℋ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) ) ‘ 𝐴 ) )
14		fveq2	⊢ ( 𝐺 = if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) → ( projℎ ‘ 𝐺 ) = ( projℎ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) )
15	14	fveq1d	⊢ ( 𝐺 = if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) → ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) = ( ( projℎ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) ‘ 𝐴 ) )
16	15	oveq2d	⊢ ( 𝐺 = if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) → ( ( ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) = ( ( ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) ‘ 𝐴 ) ) )
17	13 16	eqeq12d	⊢ ( 𝐺 = if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) → ( ( ( projℎ ‘ ( if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ∨ℋ 𝐺 ) ) ‘ 𝐴 ) = ( ( ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ↔ ( ( projℎ ‘ ( if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ∨ℋ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) ) ‘ 𝐴 ) = ( ( ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) ‘ 𝐴 ) ) ) )
18	10 17	imbi12d	⊢ ( 𝐺 = if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) → ( ( if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ⊆ ( ⊥ ‘ 𝐺 ) → ( ( projℎ ‘ ( if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ∨ℋ 𝐺 ) ) ‘ 𝐴 ) = ( ( ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ) ↔ ( if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ⊆ ( ⊥ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) → ( ( projℎ ‘ ( if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ∨ℋ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) ) ‘ 𝐴 ) = ( ( ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) ‘ 𝐴 ) ) ) ) )
19		fveq2	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( projℎ ‘ ( if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ∨ℋ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) ) ‘ 𝐴 ) = ( ( projℎ ‘ ( if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ∨ℋ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) )
20		fveq2	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ) ‘ 𝐴 ) = ( ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) )
21		fveq2	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( projℎ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) ‘ 𝐴 ) = ( ( projℎ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) )
22	20 21	oveq12d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) ‘ 𝐴 ) ) = ( ( ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) +ℎ ( ( projℎ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ) )
23	19 22	eqeq12d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( ( projℎ ‘ ( if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ∨ℋ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) ) ‘ 𝐴 ) = ( ( ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) ‘ 𝐴 ) ) ↔ ( ( projℎ ‘ ( if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ∨ℋ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = ( ( ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) +ℎ ( ( projℎ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ) ) )
24	23	imbi2d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ⊆ ( ⊥ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) → ( ( projℎ ‘ ( if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ∨ℋ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) ) ‘ 𝐴 ) = ( ( ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) ‘ 𝐴 ) ) ) ↔ ( if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ⊆ ( ⊥ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) → ( ( projℎ ‘ ( if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ∨ℋ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = ( ( ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) +ℎ ( ( projℎ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ) ) ) )
25		ifchhv	⊢ if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ∈ Cℋ
26		ifhvhv0	⊢ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ∈ ℋ
27		ifchhv	⊢ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ∈ Cℋ
28	25 26 27	pjcji	⊢ ( if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ⊆ ( ⊥ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) → ( ( projℎ ‘ ( if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ∨ℋ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = ( ( ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) +ℎ ( ( projℎ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) ) )
29	8 18 24 28	dedth3h	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐺 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( 𝐻 ⊆ ( ⊥ ‘ 𝐺 ) → ( ( projℎ ‘ ( 𝐻 ∨ℋ 𝐺 ) ) ‘ 𝐴 ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ) )