# 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}\in {\mathbf{S}}_{ℋ}$
cdjreu.2 ${⊢}{B}\in {\mathbf{S}}_{ℋ}$
Assertion cdjreui ${⊢}\left({C}\in \left({A}{+}_{ℋ}{B}\right)\wedge {A}\cap {B}={0}_{ℋ}\right)\to \exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{C}={x}{+}_{ℎ}{y}$

### Proof

Step Hyp Ref Expression
1 cdjreu.1 ${⊢}{A}\in {\mathbf{S}}_{ℋ}$
2 cdjreu.2 ${⊢}{B}\in {\mathbf{S}}_{ℋ}$
3 1 2 shseli ${⊢}{C}\in \left({A}{+}_{ℋ}{B}\right)↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{C}={x}{+}_{ℎ}{y}$
4 3 biimpi ${⊢}{C}\in \left({A}{+}_{ℋ}{B}\right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{C}={x}{+}_{ℎ}{y}$
5 reeanv ${⊢}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({C}={x}{+}_{ℎ}{y}\wedge {C}={z}{+}_{ℎ}{w}\right)↔\left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{C}={x}{+}_{ℎ}{y}\wedge \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{C}={z}{+}_{ℎ}{w}\right)$
6 eqtr2 ${⊢}\left({C}={x}{+}_{ℎ}{y}\wedge {C}={z}{+}_{ℎ}{w}\right)\to {x}{+}_{ℎ}{y}={z}{+}_{ℎ}{w}$
7 1 sheli ${⊢}{x}\in {A}\to {x}\in ℋ$
8 2 sheli ${⊢}{y}\in {B}\to {y}\in ℋ$
9 7 8 anim12i ${⊢}\left({x}\in {A}\wedge {y}\in {B}\right)\to \left({x}\in ℋ\wedge {y}\in ℋ\right)$
10 1 sheli ${⊢}{z}\in {A}\to {z}\in ℋ$
11 2 sheli ${⊢}{w}\in {B}\to {w}\in ℋ$
12 10 11 anim12i ${⊢}\left({z}\in {A}\wedge {w}\in {B}\right)\to \left({z}\in ℋ\wedge {w}\in ℋ\right)$
13 hvaddsub4 ${⊢}\left(\left({x}\in ℋ\wedge {y}\in ℋ\right)\wedge \left({z}\in ℋ\wedge {w}\in ℋ\right)\right)\to \left({x}{+}_{ℎ}{y}={z}{+}_{ℎ}{w}↔{x}{-}_{ℎ}{z}={w}{-}_{ℎ}{y}\right)$
14 9 12 13 syl2an ${⊢}\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge \left({z}\in {A}\wedge {w}\in {B}\right)\right)\to \left({x}{+}_{ℎ}{y}={z}{+}_{ℎ}{w}↔{x}{-}_{ℎ}{z}={w}{-}_{ℎ}{y}\right)$
15 14 an4s ${⊢}\left(\left({x}\in {A}\wedge {z}\in {A}\right)\wedge \left({y}\in {B}\wedge {w}\in {B}\right)\right)\to \left({x}{+}_{ℎ}{y}={z}{+}_{ℎ}{w}↔{x}{-}_{ℎ}{z}={w}{-}_{ℎ}{y}\right)$
16 15 adantll ${⊢}\left(\left({A}\cap {B}={0}_{ℋ}\wedge \left({x}\in {A}\wedge {z}\in {A}\right)\right)\wedge \left({y}\in {B}\wedge {w}\in {B}\right)\right)\to \left({x}{+}_{ℎ}{y}={z}{+}_{ℎ}{w}↔{x}{-}_{ℎ}{z}={w}{-}_{ℎ}{y}\right)$
17 shsubcl ${⊢}\left({B}\in {\mathbf{S}}_{ℋ}\wedge {w}\in {B}\wedge {y}\in {B}\right)\to {w}{-}_{ℎ}{y}\in {B}$
18 2 17 mp3an1 ${⊢}\left({w}\in {B}\wedge {y}\in {B}\right)\to {w}{-}_{ℎ}{y}\in {B}$
19 18 ancoms ${⊢}\left({y}\in {B}\wedge {w}\in {B}\right)\to {w}{-}_{ℎ}{y}\in {B}$
20 eleq1 ${⊢}{x}{-}_{ℎ}{z}={w}{-}_{ℎ}{y}\to \left({x}{-}_{ℎ}{z}\in {B}↔{w}{-}_{ℎ}{y}\in {B}\right)$
21 19 20 syl5ibrcom ${⊢}\left({y}\in {B}\wedge {w}\in {B}\right)\to \left({x}{-}_{ℎ}{z}={w}{-}_{ℎ}{y}\to {x}{-}_{ℎ}{z}\in {B}\right)$
22 21 adantl ${⊢}\left(\left({x}\in {A}\wedge {z}\in {A}\right)\wedge \left({y}\in {B}\wedge {w}\in {B}\right)\right)\to \left({x}{-}_{ℎ}{z}={w}{-}_{ℎ}{y}\to {x}{-}_{ℎ}{z}\in {B}\right)$
23 shsubcl ${⊢}\left({A}\in {\mathbf{S}}_{ℋ}\wedge {x}\in {A}\wedge {z}\in {A}\right)\to {x}{-}_{ℎ}{z}\in {A}$
24 1 23 mp3an1 ${⊢}\left({x}\in {A}\wedge {z}\in {A}\right)\to {x}{-}_{ℎ}{z}\in {A}$
25 24 adantr ${⊢}\left(\left({x}\in {A}\wedge {z}\in {A}\right)\wedge \left({y}\in {B}\wedge {w}\in {B}\right)\right)\to {x}{-}_{ℎ}{z}\in {A}$
26 22 25 jctild ${⊢}\left(\left({x}\in {A}\wedge {z}\in {A}\right)\wedge \left({y}\in {B}\wedge {w}\in {B}\right)\right)\to \left({x}{-}_{ℎ}{z}={w}{-}_{ℎ}{y}\to \left({x}{-}_{ℎ}{z}\in {A}\wedge {x}{-}_{ℎ}{z}\in {B}\right)\right)$
27 26 adantll ${⊢}\left(\left({A}\cap {B}={0}_{ℋ}\wedge \left({x}\in {A}\wedge {z}\in {A}\right)\right)\wedge \left({y}\in {B}\wedge {w}\in {B}\right)\right)\to \left({x}{-}_{ℎ}{z}={w}{-}_{ℎ}{y}\to \left({x}{-}_{ℎ}{z}\in {A}\wedge {x}{-}_{ℎ}{z}\in {B}\right)\right)$
28 elin ${⊢}{x}{-}_{ℎ}{z}\in \left({A}\cap {B}\right)↔\left({x}{-}_{ℎ}{z}\in {A}\wedge {x}{-}_{ℎ}{z}\in {B}\right)$
29 eleq2 ${⊢}{A}\cap {B}={0}_{ℋ}\to \left({x}{-}_{ℎ}{z}\in \left({A}\cap {B}\right)↔{x}{-}_{ℎ}{z}\in {0}_{ℋ}\right)$
30 28 29 syl5bbr ${⊢}{A}\cap {B}={0}_{ℋ}\to \left(\left({x}{-}_{ℎ}{z}\in {A}\wedge {x}{-}_{ℎ}{z}\in {B}\right)↔{x}{-}_{ℎ}{z}\in {0}_{ℋ}\right)$
31 30 ad2antrr ${⊢}\left(\left({A}\cap {B}={0}_{ℋ}\wedge \left({x}\in {A}\wedge {z}\in {A}\right)\right)\wedge \left({y}\in {B}\wedge {w}\in {B}\right)\right)\to \left(\left({x}{-}_{ℎ}{z}\in {A}\wedge {x}{-}_{ℎ}{z}\in {B}\right)↔{x}{-}_{ℎ}{z}\in {0}_{ℋ}\right)$
32 27 31 sylibd ${⊢}\left(\left({A}\cap {B}={0}_{ℋ}\wedge \left({x}\in {A}\wedge {z}\in {A}\right)\right)\wedge \left({y}\in {B}\wedge {w}\in {B}\right)\right)\to \left({x}{-}_{ℎ}{z}={w}{-}_{ℎ}{y}\to {x}{-}_{ℎ}{z}\in {0}_{ℋ}\right)$
33 elch0 ${⊢}{x}{-}_{ℎ}{z}\in {0}_{ℋ}↔{x}{-}_{ℎ}{z}={0}_{ℎ}$
34 hvsubeq0 ${⊢}\left({x}\in ℋ\wedge {z}\in ℋ\right)\to \left({x}{-}_{ℎ}{z}={0}_{ℎ}↔{x}={z}\right)$
35 33 34 syl5bb ${⊢}\left({x}\in ℋ\wedge {z}\in ℋ\right)\to \left({x}{-}_{ℎ}{z}\in {0}_{ℋ}↔{x}={z}\right)$
36 7 10 35 syl2an ${⊢}\left({x}\in {A}\wedge {z}\in {A}\right)\to \left({x}{-}_{ℎ}{z}\in {0}_{ℋ}↔{x}={z}\right)$
37 36 ad2antlr ${⊢}\left(\left({A}\cap {B}={0}_{ℋ}\wedge \left({x}\in {A}\wedge {z}\in {A}\right)\right)\wedge \left({y}\in {B}\wedge {w}\in {B}\right)\right)\to \left({x}{-}_{ℎ}{z}\in {0}_{ℋ}↔{x}={z}\right)$
38 32 37 sylibd ${⊢}\left(\left({A}\cap {B}={0}_{ℋ}\wedge \left({x}\in {A}\wedge {z}\in {A}\right)\right)\wedge \left({y}\in {B}\wedge {w}\in {B}\right)\right)\to \left({x}{-}_{ℎ}{z}={w}{-}_{ℎ}{y}\to {x}={z}\right)$
39 16 38 sylbid ${⊢}\left(\left({A}\cap {B}={0}_{ℋ}\wedge \left({x}\in {A}\wedge {z}\in {A}\right)\right)\wedge \left({y}\in {B}\wedge {w}\in {B}\right)\right)\to \left({x}{+}_{ℎ}{y}={z}{+}_{ℎ}{w}\to {x}={z}\right)$
40 6 39 syl5 ${⊢}\left(\left({A}\cap {B}={0}_{ℋ}\wedge \left({x}\in {A}\wedge {z}\in {A}\right)\right)\wedge \left({y}\in {B}\wedge {w}\in {B}\right)\right)\to \left(\left({C}={x}{+}_{ℎ}{y}\wedge {C}={z}{+}_{ℎ}{w}\right)\to {x}={z}\right)$
41 40 rexlimdvva ${⊢}\left({A}\cap {B}={0}_{ℋ}\wedge \left({x}\in {A}\wedge {z}\in {A}\right)\right)\to \left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({C}={x}{+}_{ℎ}{y}\wedge {C}={z}{+}_{ℎ}{w}\right)\to {x}={z}\right)$
42 5 41 syl5bir ${⊢}\left({A}\cap {B}={0}_{ℋ}\wedge \left({x}\in {A}\wedge {z}\in {A}\right)\right)\to \left(\left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{C}={x}{+}_{ℎ}{y}\wedge \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{C}={z}{+}_{ℎ}{w}\right)\to {x}={z}\right)$
43 42 ralrimivva ${⊢}{A}\cap {B}={0}_{ℋ}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{C}={x}{+}_{ℎ}{y}\wedge \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{C}={z}{+}_{ℎ}{w}\right)\to {x}={z}\right)$
44 4 43 anim12i ${⊢}\left({C}\in \left({A}{+}_{ℋ}{B}\right)\wedge {A}\cap {B}={0}_{ℋ}\right)\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{C}={x}{+}_{ℎ}{y}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{C}={x}{+}_{ℎ}{y}\wedge \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{C}={z}{+}_{ℎ}{w}\right)\to {x}={z}\right)\right)$
45 oveq1 ${⊢}{x}={z}\to {x}{+}_{ℎ}{y}={z}{+}_{ℎ}{y}$
46 45 eqeq2d ${⊢}{x}={z}\to \left({C}={x}{+}_{ℎ}{y}↔{C}={z}{+}_{ℎ}{y}\right)$
47 46 rexbidv ${⊢}{x}={z}\to \left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{C}={x}{+}_{ℎ}{y}↔\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{C}={z}{+}_{ℎ}{y}\right)$
48 oveq2 ${⊢}{y}={w}\to {z}{+}_{ℎ}{y}={z}{+}_{ℎ}{w}$
49 48 eqeq2d ${⊢}{y}={w}\to \left({C}={z}{+}_{ℎ}{y}↔{C}={z}{+}_{ℎ}{w}\right)$
50 49 cbvrexvw ${⊢}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{C}={z}{+}_{ℎ}{y}↔\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{C}={z}{+}_{ℎ}{w}$
51 47 50 syl6bb ${⊢}{x}={z}\to \left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{C}={x}{+}_{ℎ}{y}↔\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{C}={z}{+}_{ℎ}{w}\right)$
52 51 reu4 ${⊢}\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{C}={x}{+}_{ℎ}{y}↔\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{C}={x}{+}_{ℎ}{y}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{C}={x}{+}_{ℎ}{y}\wedge \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{C}={z}{+}_{ℎ}{w}\right)\to {x}={z}\right)\right)$
53 44 52 sylibr ${⊢}\left({C}\in \left({A}{+}_{ℋ}{B}\right)\wedge {A}\cap {B}={0}_{ℋ}\right)\to \exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{C}={x}{+}_{ℎ}{y}$