spansncvi

Description: Hilbert space has the covering property (using spans of singletons to represent atoms). Exercise 5 of Kalmbach p. 153. (Contributed by NM, 7-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	spansncv.1	$⊢ A \in C_{ℋ}$
	spansncv.2	$⊢ B \in C_{ℋ}$
	spansncv.3	$⊢ C \in ℋ$
Assertion	spansncvi	$⊢ (A \subset B \land B \subseteq A \lor_{ℋ} span (\{C\})) \to B = A \lor_{ℋ} span (\{C\})$

Proof

Step	Hyp	Ref	Expression
1		spansncv.1	$⊢ A \in C_{ℋ}$
2		spansncv.2	$⊢ B \in C_{ℋ}$
3		spansncv.3	$⊢ C \in ℋ$
4		simpr	$⊢ (A \subset B \land B \subseteq A \lor_{ℋ} span (\{C\})) \to B \subseteq A \lor_{ℋ} span (\{C\})$
5		pssss	$⊢ A \subset B \to A \subseteq B$
6	5	adantr	$⊢ (A \subset B \land B \subseteq A \lor_{ℋ} span (\{C\})) \to A \subseteq B$
7		pssnel	$⊢ A \subset B \to \exists x (x \in B \land \neg x \in A)$
8		ssel2	$⊢ (B \subseteq A \lor_{ℋ} span (\{C\}) \land x \in B) \to x \in (A \lor_{ℋ} span (\{C\}))$
9	1 3	spansnji	$⊢ A +_{ℋ} span (\{C\}) = A \lor_{ℋ} span (\{C\})$
10	9	eleq2i	$⊢ x \in (A +_{ℋ} span (\{C\})) \leftrightarrow x \in (A \lor_{ℋ} span (\{C\}))$
11	3	spansnchi	$⊢ span (\{C\}) \in C_{ℋ}$
12	1 11	chseli	$⊢ x \in (A +_{ℋ} span (\{C\})) \leftrightarrow \exists y \in A \exists z \in span (\{C\}) x = y +_{ℎ} z$
13	10 12	bitr3i	$⊢ x \in (A \lor_{ℋ} span (\{C\})) \leftrightarrow \exists y \in A \exists z \in span (\{C\}) x = y +_{ℎ} z$
14		eleq1	$⊢ x = y +_{ℎ} z \to (x \in B \leftrightarrow y +_{ℎ} z \in B)$
15	14	biimpac	$⊢ (x \in B \land x = y +_{ℎ} z) \to y +_{ℎ} z \in B$
16	5	sselda	$⊢ (A \subset B \land y \in A) \to y \in B$
17	2	chshii	$⊢ B \in S_{ℋ}$
18		shsubcl	$⊢ (B \in S_{ℋ} \land y +_{ℎ} z \in B \land y \in B) \to (y +_{ℎ} z) -_{ℎ} y \in B$
19	17 18	mp3an1	$⊢ (y +_{ℎ} z \in B \land y \in B) \to (y +_{ℎ} z) -_{ℎ} y \in B$
20	15 16 19	syl2an	$⊢ ((x \in B \land x = y +_{ℎ} z) \land (A \subset B \land y \in A)) \to (y +_{ℎ} z) -_{ℎ} y \in B$
21	20	exp43	$⊢ x \in B \to (x = y +_{ℎ} z \to (A \subset B \to (y \in A \to (y +_{ℎ} z) -_{ℎ} y \in B)))$
22	21	com14	$⊢ y \in A \to (x = y +_{ℎ} z \to (A \subset B \to (x \in B \to (y +_{ℎ} z) -_{ℎ} y \in B)))$
23	22	imp45	$⊢ (y \in A \land (x = y +_{ℎ} z \land (A \subset B \land x \in B))) \to (y +_{ℎ} z) -_{ℎ} y \in B$
24	1	cheli	$⊢ y \in A \to y \in ℋ$
25	11	cheli	$⊢ z \in span (\{C\}) \to z \in ℋ$
26		hvpncan2	$⊢ (y \in ℋ \land z \in ℋ) \to (y +_{ℎ} z) -_{ℎ} y = z$
27	24 25 26	syl2an	$⊢ (y \in A \land z \in span (\{C\})) \to (y +_{ℎ} z) -_{ℎ} y = z$
28	27	eleq1d	$⊢ (y \in A \land z \in span (\{C\})) \to ((y +_{ℎ} z) -_{ℎ} y \in B \leftrightarrow z \in B)$
29	23 28	syl5ib	$⊢ (y \in A \land z \in span (\{C\})) \to ((y \in A \land (x = y +_{ℎ} z \land (A \subset B \land x \in B))) \to z \in B)$
30	29	imp	$⊢ ((y \in A \land z \in span (\{C\})) \land (y \in A \land (x = y +_{ℎ} z \land (A \subset B \land x \in B)))) \to z \in B$
31	30	anandis	$⊢ (y \in A \land (z \in span (\{C\}) \land (x = y +_{ℎ} z \land (A \subset B \land x \in B)))) \to z \in B$
32	31	exp45	$⊢ y \in A \to (z \in span (\{C\}) \to (x = y +_{ℎ} z \to ((A \subset B \land x \in B) \to z \in B)))$
33	32	imp41	$⊢ (((y \in A \land z \in span (\{C\})) \land x = y +_{ℎ} z) \land (A \subset B \land x \in B)) \to z \in B$
34	33	adantrr	$⊢ (((y \in A \land z \in span (\{C\})) \land x = y +_{ℎ} z) \land ((A \subset B \land x \in B) \land \neg x \in A)) \to z \in B$
35		oveq2	$⊢ z = 0_{ℎ} \to y +_{ℎ} z = y +_{ℎ} 0_{ℎ}$
36		ax-hvaddid	$⊢ y \in ℋ \to y +_{ℎ} 0_{ℎ} = y$
37	24 36	syl	$⊢ y \in A \to y +_{ℎ} 0_{ℎ} = y$
38	35 37	sylan9eqr	$⊢ (y \in A \land z = 0_{ℎ}) \to y +_{ℎ} z = y$
39	38	eqeq2d	$⊢ (y \in A \land z = 0_{ℎ}) \to (x = y +_{ℎ} z \leftrightarrow x = y)$
40		eleq1a	$⊢ y \in A \to (x = y \to x \in A)$
41	40	adantr	$⊢ (y \in A \land z = 0_{ℎ}) \to (x = y \to x \in A)$
42	39 41	sylbid	$⊢ (y \in A \land z = 0_{ℎ}) \to (x = y +_{ℎ} z \to x \in A)$
43	42	impancom	$⊢ (y \in A \land x = y +_{ℎ} z) \to (z = 0_{ℎ} \to x \in A)$
44	43	necon3bd	$⊢ (y \in A \land x = y +_{ℎ} z) \to (\neg x \in A \to z \neq 0_{ℎ})$
45	44	imp	$⊢ ((y \in A \land x = y +_{ℎ} z) \land \neg x \in A) \to z \neq 0_{ℎ}$
46		spansnss	$⊢ (B \in S_{ℋ} \land z \in B) \to span (\{z\}) \subseteq B$
47	17 46	mpan	$⊢ z \in B \to span (\{z\}) \subseteq B$
48		spansneleq	$⊢ (C \in ℋ \land z \neq 0_{ℎ}) \to (z \in span (\{C\}) \to span (\{z\}) = span (\{C\}))$
49	3 48	mpan	$⊢ z \neq 0_{ℎ} \to (z \in span (\{C\}) \to span (\{z\}) = span (\{C\}))$
50	49	imp	$⊢ (z \neq 0_{ℎ} \land z \in span (\{C\})) \to span (\{z\}) = span (\{C\})$
51	50	sseq1d	$⊢ (z \neq 0_{ℎ} \land z \in span (\{C\})) \to (span (\{z\}) \subseteq B \leftrightarrow span (\{C\}) \subseteq B)$
52	47 51	syl5ib	$⊢ (z \neq 0_{ℎ} \land z \in span (\{C\})) \to (z \in B \to span (\{C\}) \subseteq B)$
53	52	ancoms	$⊢ (z \in span (\{C\}) \land z \neq 0_{ℎ}) \to (z \in B \to span (\{C\}) \subseteq B)$
54	45 53	sylan2	$⊢ (z \in span (\{C\}) \land ((y \in A \land x = y +_{ℎ} z) \land \neg x \in A)) \to (z \in B \to span (\{C\}) \subseteq B)$
55	54	exp44	$⊢ z \in span (\{C\}) \to (y \in A \to (x = y +_{ℎ} z \to (\neg x \in A \to (z \in B \to span (\{C\}) \subseteq B))))$
56	55	com12	$⊢ y \in A \to (z \in span (\{C\}) \to (x = y +_{ℎ} z \to (\neg x \in A \to (z \in B \to span (\{C\}) \subseteq B))))$
57	56	imp41	$⊢ (((y \in A \land z \in span (\{C\})) \land x = y +_{ℎ} z) \land \neg x \in A) \to (z \in B \to span (\{C\}) \subseteq B)$
58	57	adantrl	$⊢ (((y \in A \land z \in span (\{C\})) \land x = y +_{ℎ} z) \land ((A \subset B \land x \in B) \land \neg x \in A)) \to (z \in B \to span (\{C\}) \subseteq B)$
59	34 58	mpd	$⊢ (((y \in A \land z \in span (\{C\})) \land x = y +_{ℎ} z) \land ((A \subset B \land x \in B) \land \neg x \in A)) \to span (\{C\}) \subseteq B$
60	59	exp43	$⊢ (y \in A \land z \in span (\{C\})) \to (x = y +_{ℎ} z \to ((A \subset B \land x \in B) \to (\neg x \in A \to span (\{C\}) \subseteq B)))$
61	60	rexlimivv	$⊢ \exists y \in A \exists z \in span (\{C\}) x = y +_{ℎ} z \to ((A \subset B \land x \in B) \to (\neg x \in A \to span (\{C\}) \subseteq B))$
62	13 61	sylbi	$⊢ x \in (A \lor_{ℋ} span (\{C\})) \to ((A \subset B \land x \in B) \to (\neg x \in A \to span (\{C\}) \subseteq B))$
63	8 62	syl	$⊢ (B \subseteq A \lor_{ℋ} span (\{C\}) \land x \in B) \to ((A \subset B \land x \in B) \to (\neg x \in A \to span (\{C\}) \subseteq B))$
64	63	imp	$⊢ ((B \subseteq A \lor_{ℋ} span (\{C\}) \land x \in B) \land (A \subset B \land x \in B)) \to (\neg x \in A \to span (\{C\}) \subseteq B)$
65	64	anandirs	$⊢ ((B \subseteq A \lor_{ℋ} span (\{C\}) \land A \subset B) \land x \in B) \to (\neg x \in A \to span (\{C\}) \subseteq B)$
66	65	expimpd	$⊢ (B \subseteq A \lor_{ℋ} span (\{C\}) \land A \subset B) \to ((x \in B \land \neg x \in A) \to span (\{C\}) \subseteq B)$
67	66	exlimdv	$⊢ (B \subseteq A \lor_{ℋ} span (\{C\}) \land A \subset B) \to (\exists x (x \in B \land \neg x \in A) \to span (\{C\}) \subseteq B)$
68	7 67	syl5	$⊢ (B \subseteq A \lor_{ℋ} span (\{C\}) \land A \subset B) \to (A \subset B \to span (\{C\}) \subseteq B)$
69	68	ex	$⊢ B \subseteq A \lor_{ℋ} span (\{C\}) \to (A \subset B \to (A \subset B \to span (\{C\}) \subseteq B))$
70	69	pm2.43d	$⊢ B \subseteq A \lor_{ℋ} span (\{C\}) \to (A \subset B \to span (\{C\}) \subseteq B)$
71	70	impcom	$⊢ (A \subset B \land B \subseteq A \lor_{ℋ} span (\{C\})) \to span (\{C\}) \subseteq B$
72	1 11 2	chlubii	$⊢ (A \subseteq B \land span (\{C\}) \subseteq B) \to A \lor_{ℋ} span (\{C\}) \subseteq B$
73	6 71 72	syl2anc	$⊢ (A \subset B \land B \subseteq A \lor_{ℋ} span (\{C\})) \to A \lor_{ℋ} span (\{C\}) \subseteq B$
74	4 73	eqssd	$⊢ (A \subset B \land B \subseteq A \lor_{ℋ} span (\{C\})) \to B = A \lor_{ℋ} span (\{C\})$

Metamath Proof Explorer

Theorem spansncvi

Proof