Theorem atom1d 10280

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 =/= 0h /\ A = (span` {x})))

Distinct variable group:   x,A

Proof of Theorem atom1d

Step	Hyp	Ref	Expression
1		elat2 10267	. . . 4 |- (A e. Atoms <-> (A e. CH /\ (A =/= 0H /\ A.y e. CH (y (_ A -> (y = A \/ y = 0H)))))
2		chne0t 9417	. . . . . 6 |- (A e. CH -> (A =/= 0H <-> E.x e. A x =/= 0h))
3		ax-17 971	. . . . . . 7 |- (A e. CH -> A.x A e. CH)
4		ax-17 971	. . . . . . . 8 |- (A.y e. CH (y (_ A -> (y = A \/ y = 0H)) -> A.xA.y e. CH (y (_ A -> (y = A \/ y = 0H)))
5		hbre1 1689	. . . . . . . 8 |- (E.x e. H~ (x =/= 0h /\ A = (_|_` (_|_` {x}))) -> A.xE.x e. H~ (x =/= 0h /\ A = (_|_` (_|_` {x}))))
6	4, 5	hbim 1007	. . . . . . 7 |- ((A.y e. CH (y (_ A -> (y = A \/ y = 0H)) -> E.x e. H~ (x =/= 0h /\ A = (_|_` (_|_` {x})))) -> A.x(A.y e. CH (y (_ A -> (y = A \/ y = 0H)) -> E.x e. H~ (x =/= 0h /\ A = (_|_` (_|_` {x})))))
7		ra4e 1695	. . . . . . . . 9 |- ((x e. H~ /\ (x =/= 0h /\ A = (_|_` (_|_` {x})))) -> E.x e. H~ (x =/= 0h /\ A = (_|_` (_|_` {x}))))
8		chelt 9100	. . . . . . . . . . 11 |- ((A e. CH /\ x e. A) -> x e. H~)
9	8	adantrr 395	. . . . . . . . . 10 |- ((A e. CH /\ (x e. A /\ x =/= 0h)) -> x e. H~)
10	9	adantrr 395	. . . . . . . . 9 |- ((A e. CH /\ ((x e. A /\ x =/= 0h) /\ A.y e. CH (y (_ A -> (y = A \/ y = 0H)))) -> x e. H~)
11		pm3.27 323	. . . . . . . . . . 11 |- ((x e. A /\ x =/= 0h) -> x =/= 0h)
12	11	ad2antrl 406	. . . . . . . . . 10 |- ((A e. CH /\ ((x e. A /\ x =/= 0h) /\ A.y e. CH (y (_ A -> (y = A \/ y = 0H)))) -> x =/= 0h)
13		h1dn0 9475	. . . . . . . . . . . . . . 15 |- ((x e. H~ /\ x =/= 0h) -> (_|_` (_|_` {x})) =/= 0H)
14	13, 8	sylan 448	. . . . . . . . . . . . . 14 |- (((A e. CH /\ x e. A) /\ x =/= 0h) -> (_|_` (_|_` {x})) =/= 0H)
15	14	anasss 440	. . . . . . . . . . . . 13 |- ((A e. CH /\ (x e. A /\ x =/= 0h)) -> (_|_` (_|_` {x})) =/= 0H)
16	15	adantrr 395	. . . . . . . . . . . 12 |- ((A e. CH /\ ((x e. A /\ x =/= 0h) /\ A.y e. CH (y (_ A -> (y = A \/ y = 0H)))) -> (_|_` (_|_` {x})) =/= 0H)
17		ch1dle 10279	. . . . . . . . . . . . . . . . . 18 |- ((A e. CH /\ x e. A) -> (_|_` (_|_` {x})) (_ A)
18		snssi 2466	. . . . . . . . . . . . . . . . . . . 20 |- (x e. H~ -> {x} (_ H~)
19		occlt 9182	. . . . . . . . . . . . . . . . . . . 20 |- ({x} (_ H~ -> (_|_` {x}) e. CH)
20	8, 18, 19	3syl 20	. . . . . . . . . . . . . . . . . . 19 |- ((A e. CH /\ x e. A) -> (_|_` {x}) e. CH)
21		chocclt 9184	. . . . . . . . . . . . . . . . . . 19 |- ((_|_` {x}) e. CH -> (_|_` (_|_` {x})) e. CH)
22		sseq1 2082	. . . . . . . . . . . . . . . . . . . . 21 |- (y = (_|_` (_|_` {x})) -> (y (_ A <-> (_|_` (_|_` {x})) (_ A))
23		eqeq1 1481	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = (_|_` (_|_` {x})) -> (y = A <-> (_|_` (_|_` {x})) = A))
24		eqeq1 1481	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = (_|_` (_|_` {x})) -> (y = 0H <-> (_|_` (_|_` {x})) = 0H))
25	23, 24	orbi12d 627	. . . . . . . . . . . . . . . . . . . . 21 |- (y = (_|_` (_|_` {x})) -> ((y = A \/ y = 0H) <-> ((_|_` (_|_` {x})) = A \/ (_|_` (_|_` {x})) = 0H)))
26	22, 25	imbi12d 626	. . . . . . . . . . . . . . . . . . . 20 |- (y = (_|_` (_|_` {x})) -> ((y (_ A -> (y = A \/ y = 0H)) <-> ((_|_` (_|_` {x})) (_ A -> ((_|_` (_|_` {x})) = A \/ (_|_` (_|_` {x})) = 0H))))
27	26	rcla4v 1873	. . . . . . . . . . . . . . . . . . 19 |- ((_|_` (_|_` {x})) e. CH -> (A.y e. CH (y (_ A -> (y = A \/ y = 0H)) -> ((_|_` (_|_` {x})) (_ A -> ((_|_` (_|_` {x})) = A \/ (_|_` (_|_` {x})) = 0H))))
28	20, 21, 27	3syl 20	. . . . . . . . . . . . . . . . . 18 |- ((A e. CH /\ x e. A) -> (A.y e. CH (y (_ A -> (y = A \/ y = 0H)) -> ((_|_` (_|_` {x})) (_ A -> ((_|_` (_|_` {x})) = A \/ (_|_` (_|_` {x})) = 0H))))
29	17, 28	mpid 47	. . . . . . . . . . . . . . . . 17 |- ((A e. CH /\ x e. A) -> (A.y e. CH (y (_ A -> (y = A \/ y = 0H)) -> ((_|_` (_|_` {x})) = A \/ (_|_` (_|_` {x})) = 0H)))
30	29	ex 373	. . . . . . . . . . . . . . . 16 |- (A e. CH -> (x e. A -> (A.y e. CH (y (_ A -> (y = A \/ y = 0H)) -> ((_|_` (_|_` {x})) = A \/ (_|_` (_|_` {x})) = 0H))))
31	30	imp32 363	. . . . . . . . . . . . . . 15 |- ((A e. CH /\ (x e. A /\ A.y e. CH (y (_ A -> (y = A \/ y = 0H)))) -> ((_|_` (_|_` {x})) = A \/ (_|_` (_|_` {x})) = 0H))
32	31	adantrlr 401	. . . . . . . . . . . . . 14 |- ((A e. CH /\ ((x e. A /\ x =/= 0h) /\ A.y e. CH (y (_ A -> (y = A \/ y = 0H)))) -> ((_|_` (_|_` {x})) = A \/ (_|_` (_|_` {x})) = 0H))
33	32	ord 232	. . . . . . . . . . . . 13 |- ((A e. CH /\ ((x e. A /\ x =/= 0h) /\ A.y e. CH (y (_ A -> (y = A \/ y = 0H)))) -> (-. (_|_` (_|_` {x})) = A -> (_|_` (_|_` {x})) = 0H))
34		nne 1589	. . . . . . . . . . . . 13 |- (-. (_|_` (_|_` {x})) =/= 0H <-> (_|_` (_|_` {x})) = 0H)
35	33, 34	syl6ibr 213	. . . . . . . . . . . 12 |- ((A e. CH /\ ((x e. A /\ x =/= 0h) /\ A.y e. CH (y (_ A -> (y = A \/ y = 0H)))) -> (-. (_|_` (_|_` {x})) = A -> -. (_|_` (_|_` {x})) =/= 0H))
36	16, 35	mt4d 115	. . . . . . . . . . 11 |- ((A e. CH /\ ((x e. A /\ x =/= 0h) /\ A.y e. CH (y (_ A -> (y = A \/ y = 0H)))) -> (_|_` (_|_` {x})) = A)
37	36	eqcomd 1480	. . . . . . . . . 10 |- ((A e. CH /\ ((x e. A /\ x =/= 0h) /\ A.y e. CH (y (_ A -> (y = A \/ y = 0H)))) -> A = (_|_` (_|_` {x})))
38	12, 37	jca 288	. . . . . . . . 9 |- ((A e. CH /\ ((x e. A /\ x =/= 0h) /\ A.y e. CH (y (_ A -> (y = A \/ y = 0H)))) -> (x =/= 0h /\ A = (_|_` (_|_` {x}))))
39	7, 10, 38	sylanc 471	. . . . . . . 8 |- ((A e. CH /\ ((x e. A /\ x =/= 0h) /\ A.y e. CH (y (_ A -> (y = A \/ y = 0H)))) -> E.x e. H~ (x =/= 0h /\ A = (_|_` (_|_` {x}))))
40	39	exp44 385	. . . . . . 7 |- (A e. CH -> (x e. A -> (x =/= 0h -> (A.y e. CH (y (_ A -> (y = A \/ y = 0H)) -> E.x e. H~ (x =/= 0h /\ A = (_|_` (_|_` {x})))))))
41	3, 6, 40	r19.23ad 1745	. . . . . 6 |- (A e. CH -> (E.x e. A x =/= 0h -> (A.y e. CH (y (_ A -> (y = A \/ y = 0H)) -> E.x e. H~ (x =/= 0h /\ A = (_|_` (_|_` {x}))))))
42	2, 41	sylbid 203	. . . . 5 |- (A e. CH -> (A =/= 0H -> (A.y e. CH (y (_ A -> (y = A \/ y = 0H)) -> E.x e. H~ (x =/= 0h /\ A = (_|_` (_|_` {x}))))))
43	42	imp32 363	. . . 4 |- ((A e. CH /\ (A =/= 0H /\ A.y e. CH (y (_ A -> (y = A \/ y = 0H)))) -> E.x e. H~ (x =/= 0h /\ A = (_|_` (_|_` {x}))))
44	1, 43	sylbi 199	. . 3 |- (