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 
|- ( ( H e. CH /\ G e. CH /\ A e. ~H ) -> ( H C_ ( _|_ ` G ) -> ( ( projh ` ( H vH G ) ) ` A ) = ( ( ( projh ` H ) ` A ) +h ( ( projh ` G ) ` A ) ) ) )

Proof

Step Hyp Ref Expression
1 sseq1 
 |-  ( H = if ( H e. CH , H , ~H ) -> ( H C_ ( _|_ ` G ) <-> if ( H e. CH , H , ~H ) C_ ( _|_ ` G ) ) )
2 fvoveq1 
 |-  ( H = if ( H e. CH , H , ~H ) -> ( projh ` ( H vH G ) ) = ( projh ` ( if ( H e. CH , H , ~H ) vH G ) ) )
3 2 fveq1d 
 |-  ( H = if ( H e. CH , H , ~H ) -> ( ( projh ` ( H vH G ) ) ` A ) = ( ( projh ` ( if ( H e. CH , H , ~H ) vH G ) ) ` A ) )
4 fveq2 
 |-  ( H = if ( H e. CH , H , ~H ) -> ( projh ` H ) = ( projh ` if ( H e. CH , H , ~H ) ) )
5 4 fveq1d 
 |-  ( H = if ( H e. CH , H , ~H ) -> ( ( projh ` H ) ` A ) = ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) )
6 5 oveq1d 
 |-  ( H = if ( H e. CH , H , ~H ) -> ( ( ( projh ` H ) ` A ) +h ( ( projh ` G ) ` A ) ) = ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` G ) ` A ) ) )
7 3 6 eqeq12d 
 |-  ( H = if ( H e. CH , H , ~H ) -> ( ( ( projh ` ( H vH G ) ) ` A ) = ( ( ( projh ` H ) ` A ) +h ( ( projh ` G ) ` A ) ) <-> ( ( projh ` ( if ( H e. CH , H , ~H ) vH G ) ) ` A ) = ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` G ) ` A ) ) ) )
8 1 7 imbi12d 
 |-  ( H = if ( H e. CH , H , ~H ) -> ( ( H C_ ( _|_ ` G ) -> ( ( projh ` ( H vH G ) ) ` A ) = ( ( ( projh ` H ) ` A ) +h ( ( projh ` G ) ` A ) ) ) <-> ( if ( H e. CH , H , ~H ) C_ ( _|_ ` G ) -> ( ( projh ` ( if ( H e. CH , H , ~H ) vH G ) ) ` A ) = ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` G ) ` A ) ) ) ) )
9 fveq2 
 |-  ( G = if ( G e. CH , G , ~H ) -> ( _|_ ` G ) = ( _|_ ` if ( G e. CH , G , ~H ) ) )
10 9 sseq2d 
 |-  ( G = if ( G e. CH , G , ~H ) -> ( if ( H e. CH , H , ~H ) C_ ( _|_ ` G ) <-> if ( H e. CH , H , ~H ) C_ ( _|_ ` if ( G e. CH , G , ~H ) ) ) )
11 oveq2 
 |-  ( G = if ( G e. CH , G , ~H ) -> ( if ( H e. CH , H , ~H ) vH G ) = ( if ( H e. CH , H , ~H ) vH if ( G e. CH , G , ~H ) ) )
12 11 fveq2d 
 |-  ( G = if ( G e. CH , G , ~H ) -> ( projh ` ( if ( H e. CH , H , ~H ) vH G ) ) = ( projh ` ( if ( H e. CH , H , ~H ) vH if ( G e. CH , G , ~H ) ) ) )
13 12 fveq1d 
 |-  ( G = if ( G e. CH , G , ~H ) -> ( ( projh ` ( if ( H e. CH , H , ~H ) vH G ) ) ` A ) = ( ( projh ` ( if ( H e. CH , H , ~H ) vH if ( G e. CH , G , ~H ) ) ) ` A ) )
14 fveq2 
 |-  ( G = if ( G e. CH , G , ~H ) -> ( projh ` G ) = ( projh ` if ( G e. CH , G , ~H ) ) )
15 14 fveq1d 
 |-  ( G = if ( G e. CH , G , ~H ) -> ( ( projh ` G ) ` A ) = ( ( projh ` if ( G e. CH , G , ~H ) ) ` A ) )
16 15 oveq2d 
 |-  ( G = if ( G e. CH , G , ~H ) -> ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` G ) ` A ) ) = ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` if ( G e. CH , G , ~H ) ) ` A ) ) )
17 13 16 eqeq12d 
 |-  ( G = if ( G e. CH , G , ~H ) -> ( ( ( projh ` ( if ( H e. CH , H , ~H ) vH G ) ) ` A ) = ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` G ) ` A ) ) <-> ( ( projh ` ( if ( H e. CH , H , ~H ) vH if ( G e. CH , G , ~H ) ) ) ` A ) = ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` if ( G e. CH , G , ~H ) ) ` A ) ) ) )
18 10 17 imbi12d 
 |-  ( G = if ( G e. CH , G , ~H ) -> ( ( if ( H e. CH , H , ~H ) C_ ( _|_ ` G ) -> ( ( projh ` ( if ( H e. CH , H , ~H ) vH G ) ) ` A ) = ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` G ) ` A ) ) ) <-> ( if ( H e. CH , H , ~H ) C_ ( _|_ ` if ( G e. CH , G , ~H ) ) -> ( ( projh ` ( if ( H e. CH , H , ~H ) vH if ( G e. CH , G , ~H ) ) ) ` A ) = ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` if ( G e. CH , G , ~H ) ) ` A ) ) ) ) )
19 fveq2 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( projh ` ( if ( H e. CH , H , ~H ) vH if ( G e. CH , G , ~H ) ) ) ` A ) = ( ( projh ` ( if ( H e. CH , H , ~H ) vH if ( G e. CH , G , ~H ) ) ) ` if ( A e. ~H , A , 0h ) ) )
20 fveq2 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) = ( ( projh ` if ( H e. CH , H , ~H ) ) ` if ( A e. ~H , A , 0h ) ) )
21 fveq2 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( projh ` if ( G e. CH , G , ~H ) ) ` A ) = ( ( projh ` if ( G e. CH , G , ~H ) ) ` if ( A e. ~H , A , 0h ) ) )
22 20 21 oveq12d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` if ( G e. CH , G , ~H ) ) ` A ) ) = ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` if ( A e. ~H , A , 0h ) ) +h ( ( projh ` if ( G e. CH , G , ~H ) ) ` if ( A e. ~H , A , 0h ) ) ) )
23 19 22 eqeq12d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( ( projh ` ( if ( H e. CH , H , ~H ) vH if ( G e. CH , G , ~H ) ) ) ` A ) = ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` if ( G e. CH , G , ~H ) ) ` A ) ) <-> ( ( projh ` ( if ( H e. CH , H , ~H ) vH if ( G e. CH , G , ~H ) ) ) ` if ( A e. ~H , A , 0h ) ) = ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` if ( A e. ~H , A , 0h ) ) +h ( ( projh ` if ( G e. CH , G , ~H ) ) ` if ( A e. ~H , A , 0h ) ) ) ) )
24 23 imbi2d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( if ( H e. CH , H , ~H ) C_ ( _|_ ` if ( G e. CH , G , ~H ) ) -> ( ( projh ` ( if ( H e. CH , H , ~H ) vH if ( G e. CH , G , ~H ) ) ) ` A ) = ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` if ( G e. CH , G , ~H ) ) ` A ) ) ) <-> ( if ( H e. CH , H , ~H ) C_ ( _|_ ` if ( G e. CH , G , ~H ) ) -> ( ( projh ` ( if ( H e. CH , H , ~H ) vH if ( G e. CH , G , ~H ) ) ) ` if ( A e. ~H , A , 0h ) ) = ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` if ( A e. ~H , A , 0h ) ) +h ( ( projh ` if ( G e. CH , G , ~H ) ) ` if ( A e. ~H , A , 0h ) ) ) ) ) )
25 ifchhv 
 |-  if ( H e. CH , H , ~H ) e. CH
26 ifhvhv0 
 |-  if ( A e. ~H , A , 0h ) e. ~H
27 ifchhv 
 |-  if ( G e. CH , G , ~H ) e. CH
28 25 26 27 pjcji 
 |-  ( if ( H e. CH , H , ~H ) C_ ( _|_ ` if ( G e. CH , G , ~H ) ) -> ( ( projh ` ( if ( H e. CH , H , ~H ) vH if ( G e. CH , G , ~H ) ) ) ` if ( A e. ~H , A , 0h ) ) = ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` if ( A e. ~H , A , 0h ) ) +h ( ( projh ` if ( G e. CH , G , ~H ) ) ` if ( A e. ~H , A , 0h ) ) ) )
29 8 18 24 28 dedth3h 
 |-  ( ( H e. CH /\ G e. CH /\ A e. ~H ) -> ( H C_ ( _|_ ` G ) -> ( ( projh ` ( H vH G ) ) ` A ) = ( ( ( projh ` H ) ` A ) +h ( ( projh ` G ) ` A ) ) ) )