Metamath Proof Explorer


Theorem cdjreui

Description: A member of the sum of disjoint subspaces has a unique decomposition. Part of Lemma 5 of Holland p. 1520. (Contributed by NM, 20-May-2005) (New usage is discouraged.)

Ref Expression
Hypotheses cdjreu.1 A S
cdjreu.2 B S
Assertion cdjreui C A + B A B = 0 ∃! x A y B C = x + y

Proof

Step Hyp Ref Expression
1 cdjreu.1 A S
2 cdjreu.2 B S
3 1 2 shseli C A + B x A y B C = x + y
4 3 biimpi C A + B x A y B C = x + y
5 reeanv y B w B C = x + y C = z + w y B C = x + y w B C = z + w
6 eqtr2 C = x + y C = z + w x + y = z + w
7 1 sheli x A x
8 2 sheli y B y
9 7 8 anim12i x A y B x y
10 1 sheli z A z
11 2 sheli w B w
12 10 11 anim12i z A w B z w
13 hvaddsub4 x y z w x + y = z + w x - z = w - y
14 9 12 13 syl2an x A y B z A w B x + y = z + w x - z = w - y
15 14 an4s x A z A y B w B x + y = z + w x - z = w - y
16 15 adantll A B = 0 x A z A y B w B x + y = z + w x - z = w - y
17 shsubcl B S w B y B w - y B
18 2 17 mp3an1 w B y B w - y B
19 18 ancoms y B w B w - y B
20 eleq1 x - z = w - y x - z B w - y B
21 19 20 syl5ibrcom y B w B x - z = w - y x - z B
22 21 adantl x A z A y B w B x - z = w - y x - z B
23 shsubcl A S x A z A x - z A
24 1 23 mp3an1 x A z A x - z A
25 24 adantr x A z A y B w B x - z A
26 22 25 jctild x A z A y B w B x - z = w - y x - z A x - z B
27 26 adantll A B = 0 x A z A y B w B x - z = w - y x - z A x - z B
28 elin x - z A B x - z A x - z B
29 eleq2 A B = 0 x - z A B x - z 0
30 28 29 bitr3id A B = 0 x - z A x - z B x - z 0
31 30 ad2antrr A B = 0 x A z A y B w B x - z A x - z B x - z 0
32 27 31 sylibd A B = 0 x A z A y B w B x - z = w - y x - z 0
33 elch0 x - z 0 x - z = 0
34 hvsubeq0 x z x - z = 0 x = z
35 33 34 syl5bb x z x - z 0 x = z
36 7 10 35 syl2an x A z A x - z 0 x = z
37 36 ad2antlr A B = 0 x A z A y B w B x - z 0 x = z
38 32 37 sylibd A B = 0 x A z A y B w B x - z = w - y x = z
39 16 38 sylbid A B = 0 x A z A y B w B x + y = z + w x = z
40 6 39 syl5 A B = 0 x A z A y B w B C = x + y C = z + w x = z
41 40 rexlimdvva A B = 0 x A z A y B w B C = x + y C = z + w x = z
42 5 41 syl5bir A B = 0 x A z A y B C = x + y w B C = z + w x = z
43 42 ralrimivva A B = 0 x A z A y B C = x + y w B C = z + w x = z
44 4 43 anim12i C A + B A B = 0 x A y B C = x + y x A z A y B C = x + y w B C = z + w x = z
45 oveq1 x = z x + y = z + y
46 45 eqeq2d x = z C = x + y C = z + y
47 46 rexbidv x = z y B C = x + y y B C = z + y
48 oveq2 y = w z + y = z + w
49 48 eqeq2d y = w C = z + y C = z + w
50 49 cbvrexvw y B C = z + y w B C = z + w
51 47 50 bitrdi x = z y B C = x + y w B C = z + w
52 51 reu4 ∃! x A y B C = x + y x A y B C = x + y x A z A y B C = x + y w B C = z + w x = z
53 44 52 sylibr C A + B A B = 0 ∃! x A y B C = x + y