atom1d

Description: The 1-dimensional subspaces of Hilbert space are its atoms. Part of Remark 10.3.5 of BeltramettiCassinelli p. 107. (Contributed by NM, 4-Jun-2004) (New usage is discouraged.)

		Ref	Expression
	Assertion	atom1d	$⊢ A \in HAtoms \leftrightarrow \exists x \in ℋ (x \neq 0_{ℎ} \land A = span (\{x\}))$

Proof

Step	Hyp	Ref	Expression
1		elat2	$⊢ A \in HAtoms \leftrightarrow (A \in C_{ℋ} \land (A \neq 0_{ℋ} \land \forall y \in C_{ℋ} (y \subseteq A \to (y = A \lor y = 0_{ℋ}))))$
2		chne0	$⊢ A \in C_{ℋ} \to (A \neq 0_{ℋ} \leftrightarrow \exists x \in A x \neq 0_{ℎ})$
3		nfv	$⊢ Ⅎ x A \in C_{ℋ}$
4		nfv	$⊢ Ⅎ x \forall y \in C_{ℋ} (y \subseteq A \to (y = A \lor y = 0_{ℋ}))$
5		nfre1	$⊢ Ⅎ x \exists x \in ℋ (x \neq 0_{ℎ} \land A = ⊥ (⊥ (\{x\})))$
6	4 5	nfim	$⊢ Ⅎ x (\forall y \in C_{ℋ} (y \subseteq A \to (y = A \lor y = 0_{ℋ})) \to \exists x \in ℋ (x \neq 0_{ℎ} \land A = ⊥ (⊥ (\{x\}))))$
7		chel	$⊢ (A \in C_{ℋ} \land x \in A) \to x \in ℋ$
8	7	adantrr	$⊢ (A \in C_{ℋ} \land (x \in A \land x \neq 0_{ℎ})) \to x \in ℋ$
9	8	adantrr	$⊢ (A \in C_{ℋ} \land ((x \in A \land x \neq 0_{ℎ}) \land \forall y \in C_{ℋ} (y \subseteq A \to (y = A \lor y = 0_{ℋ})))) \to x \in ℋ$
10		simprlr	$⊢ (A \in C_{ℋ} \land ((x \in A \land x \neq 0_{ℎ}) \land \forall y \in C_{ℋ} (y \subseteq A \to (y = A \lor y = 0_{ℋ})))) \to x \neq 0_{ℎ}$
11		h1dn0	$⊢ (x \in ℋ \land x \neq 0_{ℎ}) \to ⊥ (⊥ (\{x\})) \neq 0_{ℋ}$
12	7 11	sylan	$⊢ ((A \in C_{ℋ} \land x \in A) \land x \neq 0_{ℎ}) \to ⊥ (⊥ (\{x\})) \neq 0_{ℋ}$
13	12	anasss	$⊢ (A \in C_{ℋ} \land (x \in A \land x \neq 0_{ℎ})) \to ⊥ (⊥ (\{x\})) \neq 0_{ℋ}$
14	13	adantrr	$⊢ (A \in C_{ℋ} \land ((x \in A \land x \neq 0_{ℎ}) \land \forall y \in C_{ℋ} (y \subseteq A \to (y = A \lor y = 0_{ℋ})))) \to ⊥ (⊥ (\{x\})) \neq 0_{ℋ}$
15		ch1dle	$⊢ (A \in C_{ℋ} \land x \in A) \to ⊥ (⊥ (\{x\})) \subseteq A$
16		snssi	$⊢ x \in ℋ \to \{x\} \subseteq ℋ$
17		occl	$⊢ \{x\} \subseteq ℋ \to ⊥ (\{x\}) \in C_{ℋ}$
18	7 16 17	3syl	$⊢ (A \in C_{ℋ} \land x \in A) \to ⊥ (\{x\}) \in C_{ℋ}$
19		choccl	$⊢ ⊥ (\{x\}) \in C_{ℋ} \to ⊥ (⊥ (\{x\})) \in C_{ℋ}$
20		sseq1	$⊢ y = ⊥ (⊥ (\{x\})) \to (y \subseteq A \leftrightarrow ⊥ (⊥ (\{x\})) \subseteq A)$
21		eqeq1	$⊢ y = ⊥ (⊥ (\{x\})) \to (y = A \leftrightarrow ⊥ (⊥ (\{x\})) = A)$
22		eqeq1	$⊢ y = ⊥ (⊥ (\{x\})) \to (y = 0_{ℋ} \leftrightarrow ⊥ (⊥ (\{x\})) = 0_{ℋ})$
23	21 22	orbi12d	$⊢ y = ⊥ (⊥ (\{x\})) \to ((y = A \lor y = 0_{ℋ}) \leftrightarrow (⊥ (⊥ (\{x\})) = A \lor ⊥ (⊥ (\{x\})) = 0_{ℋ}))$
24	20 23	imbi12d	$⊢ y = ⊥ (⊥ (\{x\})) \to ((y \subseteq A \to (y = A \lor y = 0_{ℋ})) \leftrightarrow (⊥ (⊥ (\{x\})) \subseteq A \to (⊥ (⊥ (\{x\})) = A \lor ⊥ (⊥ (\{x\})) = 0_{ℋ})))$
25	24	rspcv	$⊢ ⊥ (⊥ (\{x\})) \in C_{ℋ} \to (\forall y \in C_{ℋ} (y \subseteq A \to (y = A \lor y = 0_{ℋ})) \to (⊥ (⊥ (\{x\})) \subseteq A \to (⊥ (⊥ (\{x\})) = A \lor ⊥ (⊥ (\{x\})) = 0_{ℋ})))$
26	18 19 25	3syl	$⊢ (A \in C_{ℋ} \land x \in A) \to (\forall y \in C_{ℋ} (y \subseteq A \to (y = A \lor y = 0_{ℋ})) \to (⊥ (⊥ (\{x\})) \subseteq A \to (⊥ (⊥ (\{x\})) = A \lor ⊥ (⊥ (\{x\})) = 0_{ℋ})))$
27	15 26	mpid	$⊢ (A \in C_{ℋ} \land x \in A) \to (\forall y \in C_{ℋ} (y \subseteq A \to (y = A \lor y = 0_{ℋ})) \to (⊥ (⊥ (\{x\})) = A \lor ⊥ (⊥ (\{x\})) = 0_{ℋ}))$
28	27	impr	$⊢ (A \in C_{ℋ} \land (x \in A \land \forall y \in C_{ℋ} (y \subseteq A \to (y = A \lor y = 0_{ℋ})))) \to (⊥ (⊥ (\{x\})) = A \lor ⊥ (⊥ (\{x\})) = 0_{ℋ})$
29	28	adantrlr	$⊢ (A \in C_{ℋ} \land ((x \in A \land x \neq 0_{ℎ}) \land \forall y \in C_{ℋ} (y \subseteq A \to (y = A \lor y = 0_{ℋ})))) \to (⊥ (⊥ (\{x\})) = A \lor ⊥ (⊥ (\{x\})) = 0_{ℋ})$
30	29	ord	$⊢ (A \in C_{ℋ} \land ((x \in A \land x \neq 0_{ℎ}) \land \forall y \in C_{ℋ} (y \subseteq A \to (y = A \lor y = 0_{ℋ})))) \to (\neg ⊥ (⊥ (\{x\})) = A \to ⊥ (⊥ (\{x\})) = 0_{ℋ})$
31		nne	$⊢ \neg ⊥ (⊥ (\{x\})) \neq 0_{ℋ} \leftrightarrow ⊥ (⊥ (\{x\})) = 0_{ℋ}$
32	30 31	syl6ibr	$⊢ (A \in C_{ℋ} \land ((x \in A \land x \neq 0_{ℎ}) \land \forall y \in C_{ℋ} (y \subseteq A \to (y = A \lor y = 0_{ℋ})))) \to (\neg ⊥ (⊥ (\{x\})) = A \to \neg ⊥ (⊥ (\{x\})) \neq 0_{ℋ})$
33	14 32	mt4d	$⊢ (A \in C_{ℋ} \land ((x \in A \land x \neq 0_{ℎ}) \land \forall y \in C_{ℋ} (y \subseteq A \to (y = A \lor y = 0_{ℋ})))) \to ⊥ (⊥ (\{x\})) = A$
34	33	eqcomd	$⊢ (A \in C_{ℋ} \land ((x \in A \land x \neq 0_{ℎ}) \land \forall y \in C_{ℋ} (y \subseteq A \to (y = A \lor y = 0_{ℋ})))) \to A = ⊥ (⊥ (\{x\}))$
35		rspe	$⊢ (x \in ℋ \land (x \neq 0_{ℎ} \land A = ⊥ (⊥ (\{x\})))) \to \exists x \in ℋ (x \neq 0_{ℎ} \land A = ⊥ (⊥ (\{x\})))$
36	9 10 34 35	syl12anc	$⊢ (A \in C_{ℋ} \land ((x \in A \land x \neq 0_{ℎ}) \land \forall y \in C_{ℋ} (y \subseteq A \to (y = A \lor y = 0_{ℋ})))) \to \exists x \in ℋ (x \neq 0_{ℎ} \land A = ⊥ (⊥ (\{x\})))$
37	36	exp44	$⊢ A \in C_{ℋ} \to (x \in A \to (x \neq 0_{ℎ} \to (\forall y \in C_{ℋ} (y \subseteq A \to (y = A \lor y = 0_{ℋ})) \to \exists x \in ℋ (x \neq 0_{ℎ} \land A = ⊥ (⊥ (\{x\}))))))$
38	3 6 37	rexlimd	$⊢ A \in C_{ℋ} \to (\exists x \in A x \neq 0_{ℎ} \to (\forall y \in C_{ℋ} (y \subseteq A \to (y = A \lor y = 0_{ℋ})) \to \exists x \in ℋ (x \neq 0_{ℎ} \land A = ⊥ (⊥ (\{x\})))))$
39	2 38	sylbid	$⊢ A \in C_{ℋ} \to (A \neq 0_{ℋ} \to (\forall y \in C_{ℋ} (y \subseteq A \to (y = A \lor y = 0_{ℋ})) \to \exists x \in ℋ (x \neq 0_{ℎ} \land A = ⊥ (⊥ (\{x\})))))$
40	39	imp32	$⊢ (A \in C_{ℋ} \land (A \neq 0_{ℋ} \land \forall y \in C_{ℋ} (y \subseteq A \to (y = A \lor y = 0_{ℋ})))) \to \exists x \in ℋ (x \neq 0_{ℎ} \land A = ⊥ (⊥ (\{x\})))$
41	1 40	sylbi	$⊢ A \in HAtoms \to \exists x \in ℋ (x \neq 0_{ℎ} \land A = ⊥ (⊥ (\{x\})))$
42		h1da	$⊢ (x \in ℋ \land x \neq 0_{ℎ}) \to ⊥ (⊥ (\{x\})) \in HAtoms$
43		eleq1	$⊢ A = ⊥ (⊥ (\{x\})) \to (A \in HAtoms \leftrightarrow ⊥ (⊥ (\{x\})) \in HAtoms)$
44	42 43	syl5ibr	$⊢ A = ⊥ (⊥ (\{x\})) \to ((x \in ℋ \land x \neq 0_{ℎ}) \to A \in HAtoms)$
45	44	expdcom	$⊢ x \in ℋ \to (x \neq 0_{ℎ} \to (A = ⊥ (⊥ (\{x\})) \to A \in HAtoms))$
46	45	impd	$⊢ x \in ℋ \to ((x \neq 0_{ℎ} \land A = ⊥ (⊥ (\{x\}))) \to A \in HAtoms)$
47	46	rexlimiv	$⊢ \exists x \in ℋ (x \neq 0_{ℎ} \land A = ⊥ (⊥ (\{x\}))) \to A \in HAtoms$
48	41 47	impbii	$⊢ A \in HAtoms \leftrightarrow \exists x \in ℋ (x \neq 0_{ℎ} \land A = ⊥ (⊥ (\{x\})))$
49		spansn	$⊢ x \in ℋ \to span (\{x\}) = ⊥ (⊥ (\{x\}))$
50	49	eqeq2d	$⊢ x \in ℋ \to (A = span (\{x\}) \leftrightarrow A = ⊥ (⊥ (\{x\})))$
51	50	anbi2d	$⊢ x \in ℋ \to ((x \neq 0_{ℎ} \land A = span (\{x\})) \leftrightarrow (x \neq 0_{ℎ} \land A = ⊥ (⊥ (\{x\}))))$
52	51	rexbiia	$⊢ \exists x \in ℋ (x \neq 0_{ℎ} \land A = span (\{x\})) \leftrightarrow \exists x \in ℋ (x \neq 0_{ℎ} \land A = ⊥ (⊥ (\{x\})))$
53	48 52	bitr4i	$⊢ A \in HAtoms \leftrightarrow \exists x \in ℋ (x \neq 0_{ℎ} \land A = span (\{x\}))$

Metamath Proof Explorer

Theorem atom1d

Proof