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 ) ) )