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

Metamath Proof Explorer

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ℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ) )