Metamath Proof Explorer

Theorem pjpjpre

Description: Decomposition of a vector into projections. This formulation of axpjpj avoids pjhth . (Contributed by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses pjpjpre.1 
|- ( ph -> H e. CH )
pjpjpre.2 
|- ( ph -> A e. ( H +H ( _|_ ` H ) ) )
Assertion pjpjpre 
|- ( ph -> A = ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) )

Proof

Step Hyp Ref Expression
1 pjpjpre.1 
 |-  ( ph -> H e. CH )
2 pjpjpre.2 
 |-  ( ph -> A e. ( H +H ( _|_ ` H ) ) )
3 chsh 
 |-  ( H e. CH -> H e. SH )
4 1 3 syl 
 |-  ( ph -> H e. SH )
5 shocsh 
 |-  ( H e. SH -> ( _|_ ` H ) e. SH )
6 4 5 syl 
 |-  ( ph -> ( _|_ ` H ) e. SH )
7 shsel 
 |-  ( ( H e. SH /\ ( _|_ ` H ) e. SH ) -> ( A e. ( H +H ( _|_ ` H ) ) <-> E. x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) ) )
8 4 6 7 syl2anc 
 |-  ( ph -> ( A e. ( H +H ( _|_ ` H ) ) <-> E. x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) ) )
9 2 8 mpbid 
 |-  ( ph -> E. x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) )
10 simprr 
 |-  ( ( ph /\ ( ( x e. H /\ y e. ( _|_ ` H ) ) /\ A = ( x +h y ) ) ) -> A = ( x +h y ) )
11 simprll 
 |-  ( ( ph /\ ( ( x e. H /\ y e. ( _|_ ` H ) ) /\ A = ( x +h y ) ) ) -> x e. H )
12 simprlr 
 |-  ( ( ph /\ ( ( x e. H /\ y e. ( _|_ ` H ) ) /\ A = ( x +h y ) ) ) -> y e. ( _|_ ` H ) )
13 rspe 
 |-  ( ( y e. ( _|_ ` H ) /\ A = ( x +h y ) ) -> E. y e. ( _|_ ` H ) A = ( x +h y ) )
14 12 10 13 syl2anc 
 |-  ( ( ph /\ ( ( x e. H /\ y e. ( _|_ ` H ) ) /\ A = ( x +h y ) ) ) -> E. y e. ( _|_ ` H ) A = ( x +h y ) )
15 pjpreeq 
 |-  ( ( H e. CH /\ A e. ( H +H ( _|_ ` H ) ) ) -> ( ( ( projh ` H ) ` A ) = x <-> ( x e. H /\ E. y e. ( _|_ ` H ) A = ( x +h y ) ) ) )
16 1 2 15 syl2anc 
 |-  ( ph -> ( ( ( projh ` H ) ` A ) = x <-> ( x e. H /\ E. y e. ( _|_ ` H ) A = ( x +h y ) ) ) )
17 16 adantr 
 |-  ( ( ph /\ ( ( x e. H /\ y e. ( _|_ ` H ) ) /\ A = ( x +h y ) ) ) -> ( ( ( projh ` H ) ` A ) = x <-> ( x e. H /\ E. y e. ( _|_ ` H ) A = ( x +h y ) ) ) )
18 11 14 17 mpbir2and 
 |-  ( ( ph /\ ( ( x e. H /\ y e. ( _|_ ` H ) ) /\ A = ( x +h y ) ) ) -> ( ( projh ` H ) ` A ) = x )
19 shococss 
 |-  ( H e. SH -> H C_ ( _|_ ` ( _|_ ` H ) ) )
20 4 19 syl 
 |-  ( ph -> H C_ ( _|_ ` ( _|_ ` H ) ) )
21 20 adantr 
 |-  ( ( ph /\ ( ( x e. H /\ y e. ( _|_ ` H ) ) /\ A = ( x +h y ) ) ) -> H C_ ( _|_ ` ( _|_ ` H ) ) )
22 21 11 sseldd 
 |-  ( ( ph /\ ( ( x e. H /\ y e. ( _|_ ` H ) ) /\ A = ( x +h y ) ) ) -> x e. ( _|_ ` ( _|_ ` H ) ) )
23 1 adantr 
 |-  ( ( ph /\ ( ( x e. H /\ y e. ( _|_ ` H ) ) /\ A = ( x +h y ) ) ) -> H e. CH )
24 23 3 syl 
 |-  ( ( ph /\ ( ( x e. H /\ y e. ( _|_ ` H ) ) /\ A = ( x +h y ) ) ) -> H e. SH )
25 shel 
 |-  ( ( H e. SH /\ x e. H ) -> x e. ~H )
26 24 11 25 syl2anc 
 |-  ( ( ph /\ ( ( x e. H /\ y e. ( _|_ ` H ) ) /\ A = ( x +h y ) ) ) -> x e. ~H )
27 24 5 syl 
 |-  ( ( ph /\ ( ( x e. H /\ y e. ( _|_ ` H ) ) /\ A = ( x +h y ) ) ) -> ( _|_ ` H ) e. SH )
28 shel 
 |-  ( ( ( _|_ ` H ) e. SH /\ y e. ( _|_ ` H ) ) -> y e. ~H )
29 27 12 28 syl2anc 
 |-  ( ( ph /\ ( ( x e. H /\ y e. ( _|_ ` H ) ) /\ A = ( x +h y ) ) ) -> y e. ~H )
30 ax-hvcom 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( x +h y ) = ( y +h x ) )
31 26 29 30 syl2anc 
 |-  ( ( ph /\ ( ( x e. H /\ y e. ( _|_ ` H ) ) /\ A = ( x +h y ) ) ) -> ( x +h y ) = ( y +h x ) )
32 10 31 eqtrd 
 |-  ( ( ph /\ ( ( x e. H /\ y e. ( _|_ ` H ) ) /\ A = ( x +h y ) ) ) -> A = ( y +h x ) )
33 rspe 
 |-  ( ( x e. ( _|_ ` ( _|_ ` H ) ) /\ A = ( y +h x ) ) -> E. x e. ( _|_ ` ( _|_ ` H ) ) A = ( y +h x ) )
34 22 32 33 syl2anc 
 |-  ( ( ph /\ ( ( x e. H /\ y e. ( _|_ ` H ) ) /\ A = ( x +h y ) ) ) -> E. x e. ( _|_ ` ( _|_ ` H ) ) A = ( y +h x ) )
35 choccl 
 |-  ( H e. CH -> ( _|_ ` H ) e. CH )
36 1 35 syl 
 |-  ( ph -> ( _|_ ` H ) e. CH )
37 shocsh 
 |-  ( ( _|_ ` H ) e. SH -> ( _|_ ` ( _|_ ` H ) ) e. SH )
38 6 37 syl 
 |-  ( ph -> ( _|_ ` ( _|_ ` H ) ) e. SH )
39 shless 
 |-  ( ( ( H e. SH /\ ( _|_ ` ( _|_ ` H ) ) e. SH /\ ( _|_ ` H ) e. SH ) /\ H C_ ( _|_ ` ( _|_ ` H ) ) ) -> ( H +H ( _|_ ` H ) ) C_ ( ( _|_ ` ( _|_ ` H ) ) +H ( _|_ ` H ) ) )
40 4 38 6 20 39 syl31anc 
 |-  ( ph -> ( H +H ( _|_ ` H ) ) C_ ( ( _|_ ` ( _|_ ` H ) ) +H ( _|_ ` H ) ) )
41 shscom 
 |-  ( ( ( _|_ ` H ) e. SH /\ ( _|_ ` ( _|_ ` H ) ) e. SH ) -> ( ( _|_ ` H ) +H ( _|_ ` ( _|_ ` H ) ) ) = ( ( _|_ ` ( _|_ ` H ) ) +H ( _|_ ` H ) ) )
42 6 38 41 syl2anc 
 |-  ( ph -> ( ( _|_ ` H ) +H ( _|_ ` ( _|_ ` H ) ) ) = ( ( _|_ ` ( _|_ ` H ) ) +H ( _|_ ` H ) ) )
43 40 42 sseqtrrd 
 |-  ( ph -> ( H +H ( _|_ ` H ) ) C_ ( ( _|_ ` H ) +H ( _|_ ` ( _|_ ` H ) ) ) )
44 43 2 sseldd 
 |-  ( ph -> A e. ( ( _|_ ` H ) +H ( _|_ ` ( _|_ ` H ) ) ) )
45 pjpreeq 
 |-  ( ( ( _|_ ` H ) e. CH /\ A e. ( ( _|_ ` H ) +H ( _|_ ` ( _|_ ` H ) ) ) ) -> ( ( ( projh ` ( _|_ ` H ) ) ` A ) = y <-> ( y e. ( _|_ ` H ) /\ E. x e. ( _|_ ` ( _|_ ` H ) ) A = ( y +h x ) ) ) )
46 36 44 45 syl2anc 
 |-  ( ph -> ( ( ( projh ` ( _|_ ` H ) ) ` A ) = y <-> ( y e. ( _|_ ` H ) /\ E. x e. ( _|_ ` ( _|_ ` H ) ) A = ( y +h x ) ) ) )
47 46 adantr 
 |-  ( ( ph /\ ( ( x e. H /\ y e. ( _|_ ` H ) ) /\ A = ( x +h y ) ) ) -> ( ( ( projh ` ( _|_ ` H ) ) ` A ) = y <-> ( y e. ( _|_ ` H ) /\ E. x e. ( _|_ ` ( _|_ ` H ) ) A = ( y +h x ) ) ) )
48 12 34 47 mpbir2and 
 |-  ( ( ph /\ ( ( x e. H /\ y e. ( _|_ ` H ) ) /\ A = ( x +h y ) ) ) -> ( ( projh ` ( _|_ ` H ) ) ` A ) = y )
49 18 48 oveq12d 
 |-  ( ( ph /\ ( ( x e. H /\ y e. ( _|_ ` H ) ) /\ A = ( x +h y ) ) ) -> ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) = ( x +h y ) )
50 10 49 eqtr4d 
 |-  ( ( ph /\ ( ( x e. H /\ y e. ( _|_ ` H ) ) /\ A = ( x +h y ) ) ) -> A = ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) )
51 50 exp32 
 |-  ( ph -> ( ( x e. H /\ y e. ( _|_ ` H ) ) -> ( A = ( x +h y ) -> A = ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) ) ) )
52 51 rexlimdvv 
 |-  ( ph -> ( E. x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) -> A = ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) ) )
53 9 52 mpd 
 |-  ( ph -> A = ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) )