Theorem atom1d 5750

Description: The 1-dimensional subspaces of Hilbert space are its atoms. Part of Remark 10.3.5 of [BeltramettiCassinelli] p. 107.

Assertion

Ref	Expression
atom1d	|- (A e. Atoms <-> E.x e. H~ (-. x = 0v /\ A = (span` {x})))

Distinct variable group(s):   x,A

Proof of Theorem atom1d

Step	Hyp	Ref	Expression
1		elat2 5739	. . . 4 |- (A e. Atoms <-> (A e. CH /\ (-. A = 0H /\ A.y e. CH (y (_ A -> (y = A \/ y = 0H)))))
2		chne0t 5452	. . . . . 6 |- (A e. CH -> (-. A = 0H <-> E.x e. A -. x = 0v))
3		ax-17 925	. . . . . . 7 |- (A e. CH -> A.x A e. CH)
4		ax-17 925	. . . . . . . 8 |- (A.y e. CH (y (_ A -> (y = A \/ y = 0H)) -> A.xA.y e. CH (y (_ A -> (y = A \/ y = 0H)))
5		hbre1 1239	. . . . . . . 8 |- (E.x e. H~ (-. x = 0v /\ A = (_|_` (_|_` {x}))) -> A.xE.x e. H~ (-. x = 0v /\ A = (_|_` (_|_` {x}))))
6	4, 5	hbim 702	. . . . . . 7 |- ((A.y e. CH (y (_ A -> (y = A \/ y = 0H)) -> E.x e. H~ (-. x = 0v /\ A = (_|_` (_|_` {x})))) -> A.x(A.y e. CH (y (_ A -> (y = A \/ y = 0H)) -> E.x e. H~ (-. x = 0v /\ A = (_|_` (_|_` {x})))))
7		ra4e 1244	. . . . . . . . 9 |- ((x e. H~ /\ (-. x = 0v /\ A = (_|_` (_|_` {x})))) -> E.x e. H~ (-. x = 0v /\ A = (_|_` (_|_` {x}))))
8		chelt 5135	. . . . . . . . . . 11 |- ((A e. CH /\ x e. A) -> x e. H~)
9	8	adantrr 312	. . . . . . . . . 10 |- ((A e. CH /\ (x e. A /\ -. x = 0v)) -> x e. H~)
10	9	adantrr 312	. . . . . . . . 9 |- ((A e. CH /\ ((x e. A /\ -. x = 0v) /\ A.y e. CH (y (_ A -> (y = A \/ y = 0H)))) -> x e. H~)
11		pm3.27 260	. . . . . . . . . . 11 |- ((x e. A /\ -. x = 0v) -> -. x = 0v)
12	11	ad2antrl 322	. . . . . . . . . 10 |- ((A e. CH /\ ((x e. A /\ -. x = 0v) /\ A.y e. CH (y (_ A -> (y = A \/ y = 0H)))) -> -. x = 0v)
13		h1dn0 5457	. . . . . . . . . . . . . . 15 |- ((x e. H~ /\ -. x = 0v) -> -. (_|_` (_|_` {x})) = 0H)
14	13, 8	sylan 343	. . . . . . . . . . . . . 14 |- (((A e. CH /\ x e. A) /\ -. x = 0v) -> -. (_|_` (_|_` {x})) = 0H)
15	14	anasss 337	. . . . . . . . . . . . 13 |- ((A e. CH /\ (x e. A /\ -. x = 0v)) -> -. (_|_` (_|_` {x})) = 0H)
16	15	adantrr 312	. . . . . . . . . . . 12 |- ((A e. CH /\ ((x e. A /\ -. x = 0v) /\ A.y e. CH (y (_ A -> (y = A \/ y = 0H)))) -> -. (_|_` (_|_` {x})) = 0H)
17		sseq1 1521	. . . . . . . . . . . . . . . . . . . . 21 |- (y = (_|_` (_|_` {x})) -> (y (_ A <-> (_|_` (_|_` {x})) (_ A))
18		cleq1 1107	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = (_|_` (_|_` {x})) -> (y = A <-> (_|_` (_|_` {x})) = A))
19		cleq1 1107	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = (_|_` (_|_` {x})) -> (y = 0H <-> (_|_` (_|_` {x})) = 0H))
20	18, 19	orbi12d 475	. . . . . . . . . . . . . . . . . . . . 21 |- (y = (_|_` (_|_` {x})) -> ((y = A \/ y = 0H) <-> ((_|_` (_|_` {x})) = A \/ (_|_` (_|_` {x})) = 0H)))
21	17, 20	imbi12d 474	. . . . . . . . . . . . . . . . . . . 20 |- (y = (_|_` (_|_` {x})) -> ((y (_ A -> (y = A \/ y = 0H)) <-> ((_|_` (_|_` {x})) (_ A -> ((_|_` (_|_` {x})) = A \/ (_|_` (_|_` {x})) = 0H))))
22	21	rcla4v 1402	. . . . . . . . . . . . . . . . . . 19 |- (A.y e. CH (y (_ A -> (y = A \/ y = 0H)) -> ((_|_` (_|_` {x})) e. CH -> ((_|_` (_|_` {x})) (_ A -> ((_|_` (_|_` {x})) = A \/ (_|_` (_|_` {x})) = 0H))))
23	22	imp3a 279	. . . . . . . . . . . . . . . . . 18 |- (A.y e. CH (y (_ A -> (y = A \/ y = 0H)) -> (((_|_` (_|_` {x})) e. CH /\ (_|_` (_|_` {x})) (_ A) -> ((_|_` (_|_` {x})) = A \/ (_|_` (_|_` {x})) = 0H)))
24		snssi 1851	. . . . . . . . . . . . . . . . . . . . 21 |- (x e. H~ -> {x} (_ H~)
25		occlt 5189	. . . . . . . . . . . . . . . . . . . . 21 |- ({x} (_ H~ -> (_|_` {x}) e. CH)
26	24, 25	syl 12	. . . . . . . . . . . . . . . . . . . 20 |- (x e. H~ -> (_|_` {x}) e. CH)
27		choclt 5191	. . . . . . . . . . . . . . . . . . . 20 |- ((_|_` {x}) e. CH -> (_|_` (_|_` {x})) e. CH)
28	8, 26, 27	3syl 21	. . . . . . . . . . . . . . . . . . 19 |- ((A e. CH /\ x e. A) -> (_|_` (_|_` {x})) e. CH)
29		ch1dle 5749	. . . . . . . . . . . . . . . . . . 19 |- ((A e. CH /\ x e. A) -> (_|_` (_|_` {x})) (_ A)
30	28, 29	jca 236	. . . . . . . . . . . . . . . . . 18 |- ((A e. CH /\ x e. A) -> ((_|_` (_|_` {x})) e. CH /\ (_|_` (_|_` {x})) (_ A))
31	23, 30	syl5 22	. . . . . . . . . . . . . . . . 17 |- (A.y e. CH (y (_ A -> (y = A \/ y = 0H)) -> ((A e. CH /\ x e. A) -> ((_|_` (_|_` {x})) = A \/ (_|_` (_|_` {x})) = 0H)))
32	31	exp3a 292	. . . . . . . . . . . . . . . 16 |- (A.y e. CH (y (_ A -> (y = A \/ y = 0H)) -> (A e. CH -> (x e. A -> ((_|_` (_|_` {x})) = A \/ (_|_` (_|_` {x})) = 0H))))
33	32	com3l 34	. . . . . . . . . . . . . . 15 |- (A e. CH -> (x e. A -> (A.y e. CH (y (_ A -> (y = A \/ y = 0H)) -> ((_|_` (_|_` {x})) = A \/ (_|_` (_|_` {x})) = 0H))))
34	33	adantrd 308	. . . . . . . . . . . . . 14 |- (A e. CH -> ((x e. A /\ -. x = 0v) -> (A.y e. CH (y (_ A -> (y = A \/ y = 0H)) -> ((_|_` (_|_` {x})) = A \/ (_|_` (_|_` {x})) = 0H))))
35	34	imp32 281	. . . . . . . . . . . . 13 |- ((A e. CH /\ ((x e. A /\ -. x = 0v) /\ A.y e. CH (y (_ A -> (y = A \/ y = 0H)))) -> ((_|_` (_|_` {x})) = A \/ (_|_` (_|_` {x})) = 0H))
36	35	ord 202	. . . . . . . . . . . 12 |- ((A e. CH /\ ((x e. A /\ -. x = 0v) /\ A.y e. CH (y (_ A -> (y = A \/ y = 0H)))) -> (-. (_|_` (_|_` {x})) = A -> (_|_` (_|_` {x})) = 0H))
37	16, 36	mt3d 101	. . . . . . . . . . 11 |- ((A e. CH /\ ((x e. A /\ -. x = 0v) /\ A.y e. CH (y (_ A -> (y = A \/ y = 0H)))) -> (_|_` (_|_` {x})) = A)
38	37	cleqcomd 1106	. . . . . . . . . 10 |- ((A e. CH /\ ((x e. A /\ -. x = 0v) /\ A.y e. CH (y (_ A -> (y = A \/ y = 0H)))) -> A = (_|_` (_|_` {x})))
39	12, 38	jca 236	. . . . . . . . 9 |- ((A e. CH /\ ((x e. A /\ -. x = 0v) /\ A.y e. CH (y (_ A -> (y = A \/ y = 0H)))) -> (-. x = 0v /\ A = (_|_` (_|_` {x}))))
40	7, 10, 39	sylanc 361	. . . . . . . 8 |- ((A e. CH /\ ((x e. A /\ -. x = 0v) /\ A.y e. CH (y (_ A -> (y = A \/ y = 0H)))) -> E.x e. H~ (-. x = 0v /\ A = (_|_` (_|_` {x}))))
41	40	exp44 302	. . . . . . 7 |- (A e. CH -> (x e. A -> (-. x = 0v -> (A.y e. CH (y (_ A -> (y = A \/ y = 0H)) -> E.x e. H~ (-. x = 0v /\ A = (_|_` (_|_` {x})))))))
42	3, 6, 41	r19.23ad 1285	. . . . . 6 |- (A e. CH -> (E.x e. A -. x = 0v -> (A.y e. CH (y (_ A -> (y = A \/ y = 0H)) -> E.x e. H~ (-. x = 0v /\ A = (_|_` (_|_` {x}))))))
43	2, 42	sylbid 178	. . . . 5 |- (A e. CH -> (-. A = 0H -> (A.y e. CH (y (_ A -> (y = A \/ y = 0H)) -> E.x e. H~ (-. x = 0v /\ A = (_|_` (_|_` {x}))))))
44	43	imp32 281	. . . 4 |- ((A e. CH /\ (-. A = 0H /\ A.y e. CH (y (_ A -> (y = A \/ y = 0H)))) -> E.x e.