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