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 S_{ℋ}$
	cdjreu.2	$⊢ B \in S_{ℋ}$
Assertion	cdjreui	$⊢ (C \in (A +_{ℋ} B) \land A \cap B = 0_{ℋ}) \to \exists! x \in A \exists y \in B C = x +_{ℎ} y$

Proof

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

Metamath Proof Explorer

Theorem cdjreui

Proof