# 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 syl6bb
` |-  ( 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 ) ) )`