Metamath Proof Explorer


Theorem pjhthmo

Description: Projection Theorem, uniqueness part. Any two disjoint subspaces yield a unique decomposition of vectors into each subspace. (Contributed by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Assertion pjhthmo
|- ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) -> E* x ( x e. A /\ E. y e. B C = ( x +h y ) ) )

Proof

Step Hyp Ref Expression
1 an4
 |-  ( ( ( x e. A /\ z e. A ) /\ ( E. y e. B C = ( x +h y ) /\ E. w e. B C = ( z +h w ) ) ) <-> ( ( x e. A /\ E. y e. B C = ( x +h y ) ) /\ ( z e. A /\ E. w e. B C = ( z +h w ) ) ) )
2 reeanv
 |-  ( E. y e. B E. w e. B ( C = ( x +h y ) /\ C = ( z +h w ) ) <-> ( E. y e. B C = ( x +h y ) /\ E. w e. B C = ( z +h w ) ) )
3 simpll1
 |-  ( ( ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) /\ ( x e. A /\ z e. A ) ) /\ ( ( y e. B /\ w e. B ) /\ ( C = ( x +h y ) /\ C = ( z +h w ) ) ) ) -> A e. SH )
4 simpll2
 |-  ( ( ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) /\ ( x e. A /\ z e. A ) ) /\ ( ( y e. B /\ w e. B ) /\ ( C = ( x +h y ) /\ C = ( z +h w ) ) ) ) -> B e. SH )
5 simpll3
 |-  ( ( ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) /\ ( x e. A /\ z e. A ) ) /\ ( ( y e. B /\ w e. B ) /\ ( C = ( x +h y ) /\ C = ( z +h w ) ) ) ) -> ( A i^i B ) = 0H )
6 simplrl
 |-  ( ( ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) /\ ( x e. A /\ z e. A ) ) /\ ( ( y e. B /\ w e. B ) /\ ( C = ( x +h y ) /\ C = ( z +h w ) ) ) ) -> x e. A )
7 simprll
 |-  ( ( ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) /\ ( x e. A /\ z e. A ) ) /\ ( ( y e. B /\ w e. B ) /\ ( C = ( x +h y ) /\ C = ( z +h w ) ) ) ) -> y e. B )
8 simplrr
 |-  ( ( ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) /\ ( x e. A /\ z e. A ) ) /\ ( ( y e. B /\ w e. B ) /\ ( C = ( x +h y ) /\ C = ( z +h w ) ) ) ) -> z e. A )
9 simprlr
 |-  ( ( ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) /\ ( x e. A /\ z e. A ) ) /\ ( ( y e. B /\ w e. B ) /\ ( C = ( x +h y ) /\ C = ( z +h w ) ) ) ) -> w e. B )
10 simprrl
 |-  ( ( ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) /\ ( x e. A /\ z e. A ) ) /\ ( ( y e. B /\ w e. B ) /\ ( C = ( x +h y ) /\ C = ( z +h w ) ) ) ) -> C = ( x +h y ) )
11 simprrr
 |-  ( ( ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) /\ ( x e. A /\ z e. A ) ) /\ ( ( y e. B /\ w e. B ) /\ ( C = ( x +h y ) /\ C = ( z +h w ) ) ) ) -> C = ( z +h w ) )
12 10 11 eqtr3d
 |-  ( ( ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) /\ ( x e. A /\ z e. A ) ) /\ ( ( y e. B /\ w e. B ) /\ ( C = ( x +h y ) /\ C = ( z +h w ) ) ) ) -> ( x +h y ) = ( z +h w ) )
13 3 4 5 6 7 8 9 12 shuni
 |-  ( ( ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) /\ ( x e. A /\ z e. A ) ) /\ ( ( y e. B /\ w e. B ) /\ ( C = ( x +h y ) /\ C = ( z +h w ) ) ) ) -> ( x = z /\ y = w ) )
14 13 simpld
 |-  ( ( ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) /\ ( x e. A /\ z e. A ) ) /\ ( ( y e. B /\ w e. B ) /\ ( C = ( x +h y ) /\ C = ( z +h w ) ) ) ) -> x = z )
15 14 exp32
 |-  ( ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) /\ ( x e. A /\ z e. A ) ) -> ( ( y e. B /\ w e. B ) -> ( ( C = ( x +h y ) /\ C = ( z +h w ) ) -> x = z ) ) )
16 15 rexlimdvv
 |-  ( ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) /\ ( x e. A /\ z e. A ) ) -> ( E. y e. B E. w e. B ( C = ( x +h y ) /\ C = ( z +h w ) ) -> x = z ) )
17 2 16 syl5bir
 |-  ( ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) /\ ( x e. A /\ z e. A ) ) -> ( ( E. y e. B C = ( x +h y ) /\ E. w e. B C = ( z +h w ) ) -> x = z ) )
18 17 expimpd
 |-  ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) -> ( ( ( x e. A /\ z e. A ) /\ ( E. y e. B C = ( x +h y ) /\ E. w e. B C = ( z +h w ) ) ) -> x = z ) )
19 1 18 syl5bir
 |-  ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) -> ( ( ( x e. A /\ E. y e. B C = ( x +h y ) ) /\ ( z e. A /\ E. w e. B C = ( z +h w ) ) ) -> x = z ) )
20 19 alrimivv
 |-  ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) -> A. x A. z ( ( ( x e. A /\ E. y e. B C = ( x +h y ) ) /\ ( z e. A /\ E. w e. B C = ( z +h w ) ) ) -> x = z ) )
21 eleq1w
 |-  ( x = z -> ( x e. A <-> z e. A ) )
22 oveq1
 |-  ( x = z -> ( x +h y ) = ( z +h y ) )
23 22 eqeq2d
 |-  ( x = z -> ( C = ( x +h y ) <-> C = ( z +h y ) ) )
24 23 rexbidv
 |-  ( x = z -> ( E. y e. B C = ( x +h y ) <-> E. y e. B C = ( z +h y ) ) )
25 oveq2
 |-  ( y = w -> ( z +h y ) = ( z +h w ) )
26 25 eqeq2d
 |-  ( y = w -> ( C = ( z +h y ) <-> C = ( z +h w ) ) )
27 26 cbvrexvw
 |-  ( E. y e. B C = ( z +h y ) <-> E. w e. B C = ( z +h w ) )
28 24 27 bitrdi
 |-  ( x = z -> ( E. y e. B C = ( x +h y ) <-> E. w e. B C = ( z +h w ) ) )
29 21 28 anbi12d
 |-  ( x = z -> ( ( x e. A /\ E. y e. B C = ( x +h y ) ) <-> ( z e. A /\ E. w e. B C = ( z +h w ) ) ) )
30 29 mo4
 |-  ( E* x ( x e. A /\ E. y e. B C = ( x +h y ) ) <-> A. x A. z ( ( ( x e. A /\ E. y e. B C = ( x +h y ) ) /\ ( z e. A /\ E. w e. B C = ( z +h w ) ) ) -> x = z ) )
31 20 30 sylibr
 |-  ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) -> E* x ( x e. A /\ E. y e. B C = ( x +h y ) ) )