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 S B S A B = 0 * x x A y B C = x + y

Proof

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