Theorem irred 10321

Description: The Hilbert lattice is irreducible: any element that commutes with all elements must be zero or one. Theorem 14.8.4 of [BeltramettiCassinelli] p. 166.

Hypotheses

Ref	Expression
irred.1	|- A e. CH
irred.2	|- (x e. CH -> A C_H x)

Assertion

Ref	Expression
irred	|- (A = 0H \/ A = H~)

Distinct variable group:   x,A

Proof of Theorem irred

Step	Hyp	Ref	Expression
1		eqid 1475	. . 3 |- 0H = 0H
2		ioran 306	. . . . . 6 |- (-. (A = 0H \/ (_|_` A) = 0H) <-> (-. A = 0H /\ -. (_|_` A) = 0H))
3		df-ne 1587	. . . . . . 7 |- (A =/= 0H <-> -. A = 0H)
4		df-ne 1587	. . . . . . 7 |- ((_|_` A) =/= 0H <-> -. (_|_` A) = 0H)
5	3, 4	anbi12i 482	. . . . . 6 |- ((A =/= 0H /\ (_|_` A) =/= 0H) <-> (-. A = 0H /\ -. (_|_` A) = 0H))
6	2, 5	bitr4 176	. . . . 5 |- (-. (A = 0H \/ (_|_` A) = 0H) <-> (A =/= 0H /\ (_|_` A) =/= 0H))
7		irred.1	. . . . . . . . 9 |- A e. CH
8	7	hatomic 10286	. . . . . . . 8 |- (A =/= 0H -> E.p e. Atoms p (_ A)
9	7	choccl 9185	. . . . . . . . 9 |- (_|_` A) e. CH
10	9	hatomic 10286	. . . . . . . 8 |- ((_|_` A) =/= 0H -> E.q e. Atoms q (_ (_|_` A))
11	8, 10	anim12i 333	. . . . . . 7 |- ((A =/= 0H /\ (_|_` A) =/= 0H) -> (E.p e. Atoms p (_ A /\ E.q e. Atoms q (_ (_|_` A)))
12		reeanv 1778	. . . . . . 7 |- (E.p e. Atoms E.q e. Atoms (p (_ A /\ q (_ (_|_` A)) <-> (E.p e. Atoms p (_ A /\ E.q e. Atoms q (_ (_|_` A)))
13	11, 12	sylibr 200	. . . . . 6 |- ((A =/= 0H /\ (_|_` A) =/= 0H) -> E.p e. Atoms E.q e. Atoms (p (_ A /\ q (_ (_|_` A)))
14		superpos 10281	. . . . . . . . . . 11 |- ((p e. Atoms /\ q e. Atoms /\ p =/= q) -> E.r e. Atoms (r =/= p /\ r =/= q /\ r (_ (p vH q)))
15		simpll 412	. . . . . . . . . . 11 |- (((p e. Atoms /\ p (_ A) /\ (q e. Atoms /\ q (_ (_|_` A))) -> p e. Atoms)
16		simprl 414	. . . . . . . . . . 11 |- (((p e. Atoms /\ p (_ A) /\ (q e. Atoms /\ q (_ (_|_` A))) -> q e. Atoms)
17		sstr 2072	. . . . . . . . . . . . . . 15 |- ((q (_ (_|_` A) /\ (_|_` A) (_ (_|_` p)) -> q (_ (_|_` p))
18		atelch 10271	. . . . . . . . . . . . . . . . 17 |- (p e. Atoms -> p e. CH)
19		chsscon3t 9423	. . . . . . . . . . . . . . . . . 18 |- ((p e. CH /\ A e. CH) -> (p (_ A <-> (_|_` A) (_ (_|_` p)))
20	7, 19	mpan2 696	. . . . . . . . . . . . . . . . 17 |- (p e. CH -> (p (_ A <-> (_|_` A) (_ (_|_` p)))
21	18, 20	syl 10	. . . . . . . . . . . . . . . 16 |- (p e. Atoms -> (p (_ A <-> (_|_` A) (_ (_|_` p)))
22	21	biimpa 416	. . . . . . . . . . . . . . 15 |- ((p e. Atoms /\ p (_ A) -> (_|_` A) (_ (_|_` p))
23	17, 22	sylan2 451	. . . . . . . . . . . . . 14 |- ((q (_ (_|_` A) /\ (p e. Atoms /\ p (_ A)) -> q (_ (_|_` p))
24	23	ancoms 436	. . . . . . . . . . . . 13 |- (((p e. Atoms /\ p (_ A) /\ q (_ (_|_` A)) -> q (_ (_|_` p))
25		atn0 10272	. . . . . . . . . . . . . . . 16 |- (p e. Atoms -> p =/= 0H)
26	25	adantr 389	. . . . . . . . . . . . . . 15 |- ((p e. Atoms /\ q (_ (_|_` p)) -> p =/= 0H)
27		sseq1 2082	. . . . . . . . . . . . . . . . . . . . 21 |- (p = q -> (p (_ (_|_` p) <-> q (_ (_|_` p)))
28	27	bicomd 521	. . . . . . . . . . . . . . . . . . . 20 |- (p = q -> (q (_ (_|_` p) <-> p (_ (_|_` p)))
29		chssoct 9419	. . . . . . . . . . . . . . . . . . . . 21 |- (p e. CH -> (p (_ (_|_` p) <-> p = 0H))
30	18, 29	syl 10	. . . . . . . . . . . . . . . . . . . 20 |- (p e. Atoms -> (p (_ (_|_` p) <-> p = 0H))
31	28, 30	sylan9bbr 541	. . . . . . . . . . . . . . . . . . 19 |- ((p e. Atoms /\ p = q) -> (q (_ (_|_` p) <-> p = 0H))
32	31	biimpa 416	. . . . . . . . . . . . . . . . . 18 |- (((p e. Atoms /\ p = q) /\ q (_ (_|_` p)) -> p = 0H)
33	32	an1rs 489	. . . . . . . . . . . . . . . . 17 |- (((p e. Atoms /\ q (_ (_|_` p)) /\ p = q) -> p = 0H)
34	33	ex 373	. . . . . . . . . . . . . . . 16 |- ((p e. Atoms /\ q (_ (_|_` p)) -> (p = q -> p = 0H))
35	34	necon3d 1604	. . . . . . . . . . . . . . 15 |- ((p e. Atoms /\ q (_ (_|_` p)) -> (p =/= 0H -> p =/= q))
36	26, 35	mpd 26	. . . . . . . . . . . . . 14 |- ((p e. Atoms /\ q (_ (_|_` p)) -> p =/= q)
37	36	adantlr 393	. . . . . . . . . . . . 13 |- (((p e. Atoms /\ p (_ A) /\ q (_ (_|_` p)) -> p =/= q)
38	24, 37	syldan 467	. . . . . . . . . . . 12 |- (((p e. Atoms /\ p (_ A) /\ q (_ (_|_` A)) -> p =/= q)
39	38	adantrl 394	. . . . . . . . . . 11 |- (((p e. Atoms /\ p (_ A) /\ (q e. Atoms /\ q (_ (_|_` A))) -> p =/= q)
40	14, 15, 16, 39	syl3anc 858	. . . . . . . . . 10 |- (((p e. Atoms /\ p (_ A) /\ (q e. Atoms /\ q (_ (_|_` A))) -> E.r e. Atoms (r =/= p /\ r =/= q /\ r (_ (p vH q)))
41		irred.2	. . . . . . . . . . . . . . . . . 18 |- (x e. CH -> A C_H x)
42	7, 41	irredlem4 10320	. . . . . . . . . . . . . . . . 17 |- ((((p e. Atoms /\ p (_ A) /\ (q e. Atoms /\ q (_ (_|_` A))) /\ (r e. Atoms /\ r (_ (p vH q))) -> (r = p \/ r = q))
43	42	anassrs 441	. . . . . . . . . . . . . . . 16 |- (((((p e. Atoms /\ p (_ A) /\ (q e. Atoms /\ q (_ (_|_` A))) /\ r e. Atoms) /\ r (_ (p vH q)) -> (r = p \/ r = q))
44	43	pm2.24d 105	. . . . . . . . . . . . . . 15 |- (((((p e. Atoms /\ p (_ A) /\ (q e. Atoms /\ q (_ (_|_` A))) /\ r e. Atoms) /\ r (_ (p vH q)) -> (-. (r = p \/ r = q) -> -. 0H = 0H))
45	44	ex 373	. . . . . . . . . . . . . 14 |- ((((p e. Atoms /\ p (_ A) /\ (q e. Atoms /\ q (_ (_|_` A))) /\ r e. Atoms) -> (r (_ (p vH q) -> (-. (r = p \/ r = q) -> -. 0H = 0H)))
46	45	com23 32	. . . . . . . . . . . . 13 |- ((((p e. Atoms /\ p (_ A) /\ (q e. Atoms /\ q (_ (_|_` A))) /\ r e. Atoms) -> (-. (r = p \/ r = q) -> (r (_ (p vH q) -> -. 0H = 0H)))
47	46	imp3a 361	. . . . . . . . . . . 12 |- ((((p e. Atoms /\ p (_ A) /\ (q e. Atoms /\ q (_ (_|_` A))) /\ r e. Atoms) -> ((-. (r = p \/ r = q) /\ r (_ (p vH q)) -> -. 0H = 0H))
48		df-3an 777	. . . . . . . . . . . . 13 |- ((r =/= p /\ r =/= q /\ r (_ (p vH q)) <-> ((r =/= p /\ r =/= q) /\ r (_ (p vH q)))
49		neanior 1639	. . . . . . . . . . . . . 14 |- ((r =/= p /\ r =/= q) <-> -. (r = p \/ r = q))
50	49	anbi1i 481	. . . . . . . . . . . . 13 |- (((r =/= p /\ r =/= q) /\ r (_ (p vH q)) <-> (-. (r = p \/ r = q) /\ r (_ (p vH q)))
51	48, 50	bitr 173	. . . . . . . . . . . 12 |- ((r =/= p /\ r =/= q /\ r (_ (p vH q)) <-> (-. (r = p \/ r = q) /\ r (_ (p vH q)))
52	47, 51	syl5ib 206	. . . . . . . . . . 11 |- ((((p e. Atoms /\ p (_ A) /\ (q e. Atoms /\ q (_ (_|_` A))) /\ r e. Atoms) -> ((r =/= p /\ r =/= q /\ r (_ (p vH q)) -> -. 0H = 0H))
53	52	r19.23adva 1747	. . . . . . . . . 10 |- (((p e. Atoms /\ p (_ A) /\ (q e. Atoms /\ q (_ (_|_` A))) -> (E.r e. Atoms (r =/= p /\ r =/= q /\ r (_ (p vH q)) -> -. 0H = 0H))
54	40, 53	mpd 26	. . . . . . . . 9 |- (((p e. Atoms /\ p (_ A) /\ (q e. Atoms /\ q (_ (_|_` A))) -> -. 0H = 0H)
55	54	an4s 508	. . . . . . . 8 |- (((p e. Atoms /\ q e. Atoms) /\ (p (_ A /\ q (_ (_|_` A))) -> -. 0H = 0H)
56	55	ex 373	. . . . . . 7 |- ((p e. Atoms /\ q e. Atoms) -> ((p (_ A /\ q (_ (_|_` A)) -> -. 0H = 0H))
57	56	r19.23aivv 1748	. . . . . 6 |- (E.p e. Atoms E.q e. Atoms (p (_ A /\ q (_ (_|_` A)) -> -. 0H = 0H)
58	13, 57	syl 10	. . . . 5 |- ((A =/= 0H /\ (_|_` A) =/= 0H) -> -. 0H = 0H)
59	6, 58	sylbi 199	. . . 4 |- (-. (A = 0H \/ (_|_` A) = 0H) -> -. 0H = 0H)
60	59	a3i 74	. . 3 |- (0H = 0H -> (A = 0H \/ (_|_` A) = 0H))
61	1, 60	ax-mp 7	. 2 |- (A = 0H \/ (_|_` A) = 0H)
62		fveq2 3724	. . . 4 |- ((_|_` A) = 0H -> (_|_` (_|_` A)) = (_|_` 0H))
63	7	ococ 9247	. . . 4 |- (_|_` (_|_` A)) = A
64		choc0 9290	. . . 4 |- (_|_` 0H) = H~
65	62, 63, 64	3eqtr3g 1530	. . 3 |- ((_|_` A) = 0H -> A = H~)
66	65	orim2i 338	. 2 |- ((A = 0H \/ (_|_` A) = 0H) -> (A =