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	⊢ 𝐴 ∈ Sℋ
	cdjreu.2	⊢ 𝐵 ∈ Sℋ
Assertion	cdjreui	⊢ ( ( 𝐶 ∈ ( 𝐴 +ℋ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		cdjreu.1	⊢ 𝐴 ∈ Sℋ
2		cdjreu.2	⊢ 𝐵 ∈ Sℋ
3	1 2	shseli	⊢ ( 𝐶 ∈ ( 𝐴 +ℋ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) )
4	3	biimpi	⊢ ( 𝐶 ∈ ( 𝐴 +ℋ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) )
5		reeanv	⊢ ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑤 ∈ 𝐵 ( 𝐶 = ( 𝑥 +ℎ 𝑦 ) ∧ 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) ↔ ( ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝐵 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) )
6		eqtr2	⊢ ( ( 𝐶 = ( 𝑥 +ℎ 𝑦 ) ∧ 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) → ( 𝑥 +ℎ 𝑦 ) = ( 𝑧 +ℎ 𝑤 ) )
7	1	sheli	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ℋ )
8	2	sheli	⊢ ( 𝑦 ∈ 𝐵 → 𝑦 ∈ ℋ )
9	7 8	anim12i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) )
10	1	sheli	⊢ ( 𝑧 ∈ 𝐴 → 𝑧 ∈ ℋ )
11	2	sheli	⊢ ( 𝑤 ∈ 𝐵 → 𝑤 ∈ ℋ )
12	10 11	anim12i	⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) → ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) )
13		hvaddsub4	⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) → ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑧 +ℎ 𝑤 ) ↔ ( 𝑥 −ℎ 𝑧 ) = ( 𝑤 −ℎ 𝑦 ) ) )
14	9 12 13	syl2an	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑧 +ℎ 𝑤 ) ↔ ( 𝑥 −ℎ 𝑧 ) = ( 𝑤 −ℎ 𝑦 ) ) )
15	14	an4s	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑧 +ℎ 𝑤 ) ↔ ( 𝑥 −ℎ 𝑧 ) = ( 𝑤 −ℎ 𝑦 ) ) )
16	15	adantll	⊢ ( ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑧 +ℎ 𝑤 ) ↔ ( 𝑥 −ℎ 𝑧 ) = ( 𝑤 −ℎ 𝑦 ) ) )
17		shsubcl	⊢ ( ( 𝐵 ∈ Sℋ ∧ 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑤 −ℎ 𝑦 ) ∈ 𝐵 )
18	2 17	mp3an1	⊢ ( ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑤 −ℎ 𝑦 ) ∈ 𝐵 )
19	18	ancoms	⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) → ( 𝑤 −ℎ 𝑦 ) ∈ 𝐵 )
20		eleq1	⊢ ( ( 𝑥 −ℎ 𝑧 ) = ( 𝑤 −ℎ 𝑦 ) → ( ( 𝑥 −ℎ 𝑧 ) ∈ 𝐵 ↔ ( 𝑤 −ℎ 𝑦 ) ∈ 𝐵 ) )
21	19 20	syl5ibrcom	⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) → ( ( 𝑥 −ℎ 𝑧 ) = ( 𝑤 −ℎ 𝑦 ) → ( 𝑥 −ℎ 𝑧 ) ∈ 𝐵 ) )
22	21	adantl	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑥 −ℎ 𝑧 ) = ( 𝑤 −ℎ 𝑦 ) → ( 𝑥 −ℎ 𝑧 ) ∈ 𝐵 ) )
23		shsubcl	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 −ℎ 𝑧 ) ∈ 𝐴 )
24	1 23	mp3an1	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 −ℎ 𝑧 ) ∈ 𝐴 )
25	24	adantr	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑥 −ℎ 𝑧 ) ∈ 𝐴 )
26	22 25	jctild	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑥 −ℎ 𝑧 ) = ( 𝑤 −ℎ 𝑦 ) → ( ( 𝑥 −ℎ 𝑧 ) ∈ 𝐴 ∧ ( 𝑥 −ℎ 𝑧 ) ∈ 𝐵 ) ) )
27	26	adantll	⊢ ( ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑥 −ℎ 𝑧 ) = ( 𝑤 −ℎ 𝑦 ) → ( ( 𝑥 −ℎ 𝑧 ) ∈ 𝐴 ∧ ( 𝑥 −ℎ 𝑧 ) ∈ 𝐵 ) ) )
28		elin	⊢ ( ( 𝑥 −ℎ 𝑧 ) ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( ( 𝑥 −ℎ 𝑧 ) ∈ 𝐴 ∧ ( 𝑥 −ℎ 𝑧 ) ∈ 𝐵 ) )
29		eleq2	⊢ ( ( 𝐴 ∩ 𝐵 ) = 0ℋ → ( ( 𝑥 −ℎ 𝑧 ) ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑥 −ℎ 𝑧 ) ∈ 0ℋ ) )
30	28 29	bitr3id	⊢ ( ( 𝐴 ∩ 𝐵 ) = 0ℋ → ( ( ( 𝑥 −ℎ 𝑧 ) ∈ 𝐴 ∧ ( 𝑥 −ℎ 𝑧 ) ∈ 𝐵 ) ↔ ( 𝑥 −ℎ 𝑧 ) ∈ 0ℋ ) )
31	30	ad2antrr	⊢ ( ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( ( 𝑥 −ℎ 𝑧 ) ∈ 𝐴 ∧ ( 𝑥 −ℎ 𝑧 ) ∈ 𝐵 ) ↔ ( 𝑥 −ℎ 𝑧 ) ∈ 0ℋ ) )
32	27 31	sylibd	⊢ ( ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑥 −ℎ 𝑧 ) = ( 𝑤 −ℎ 𝑦 ) → ( 𝑥 −ℎ 𝑧 ) ∈ 0ℋ ) )
33		elch0	⊢ ( ( 𝑥 −ℎ 𝑧 ) ∈ 0ℋ ↔ ( 𝑥 −ℎ 𝑧 ) = 0ℎ )
34		hvsubeq0	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 −ℎ 𝑧 ) = 0ℎ ↔ 𝑥 = 𝑧 ) )
35	33 34	bitrid	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 −ℎ 𝑧 ) ∈ 0ℋ ↔ 𝑥 = 𝑧 ) )
36	7 10 35	syl2an	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑥 −ℎ 𝑧 ) ∈ 0ℋ ↔ 𝑥 = 𝑧 ) )
37	36	ad2antlr	⊢ ( ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑥 −ℎ 𝑧 ) ∈ 0ℋ ↔ 𝑥 = 𝑧 ) )
38	32 37	sylibd	⊢ ( ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑥 −ℎ 𝑧 ) = ( 𝑤 −ℎ 𝑦 ) → 𝑥 = 𝑧 ) )
39	16 38	sylbid	⊢ ( ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑧 +ℎ 𝑤 ) → 𝑥 = 𝑧 ) )
40	6 39	syl5	⊢ ( ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝐶 = ( 𝑥 +ℎ 𝑦 ) ∧ 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) → 𝑥 = 𝑧 ) )
41	40	rexlimdvva	⊢ ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑤 ∈ 𝐵 ( 𝐶 = ( 𝑥 +ℎ 𝑦 ) ∧ 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) → 𝑥 = 𝑧 ) )
42	5 41	biimtrrid	⊢ ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝐵 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) → 𝑥 = 𝑧 ) )
43	42	ralrimivva	⊢ ( ( 𝐴 ∩ 𝐵 ) = 0ℋ → ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝐵 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) → 𝑥 = 𝑧 ) )
44	4 43	anim12i	⊢ ( ( 𝐶 ∈ ( 𝐴 +ℋ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝐵 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) → 𝑥 = 𝑧 ) ) )
45		oveq1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 +ℎ 𝑦 ) = ( 𝑧 +ℎ 𝑦 ) )
46	45	eqeq2d	⊢ ( 𝑥 = 𝑧 → ( 𝐶 = ( 𝑥 +ℎ 𝑦 ) ↔ 𝐶 = ( 𝑧 +ℎ 𝑦 ) ) )
47	46	rexbidv	⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) ↔ ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑧 +ℎ 𝑦 ) ) )
48		oveq2	⊢ ( 𝑦 = 𝑤 → ( 𝑧 +ℎ 𝑦 ) = ( 𝑧 +ℎ 𝑤 ) )
49	48	eqeq2d	⊢ ( 𝑦 = 𝑤 → ( 𝐶 = ( 𝑧 +ℎ 𝑦 ) ↔ 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) )
50	49	cbvrexvw	⊢ ( ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑧 +ℎ 𝑦 ) ↔ ∃ 𝑤 ∈ 𝐵 𝐶 = ( 𝑧 +ℎ 𝑤 ) )
51	47 50	bitrdi	⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) ↔ ∃ 𝑤 ∈ 𝐵 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) )
52	51	reu4	⊢ ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) ↔ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝐵 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) → 𝑥 = 𝑧 ) ) )
53	44 52	sylibr	⊢ ( ( 𝐶 ∈ ( 𝐴 +ℋ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) )