chirredi

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. (Contributed by NM, 15-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	chirred.1	$⊢ A \in C_{ℋ}$
	chirred.2	$⊢ x \in C_{ℋ} \to A 𝐶_{ℋ} x$
Assertion	chirredi	$⊢ (A = 0_{ℋ} \lor A = ℋ)$

Proof

Step	Hyp	Ref	Expression
1		chirred.1	$⊢ A \in C_{ℋ}$
2		chirred.2	$⊢ x \in C_{ℋ} \to A 𝐶_{ℋ} x$
3		eqid	$⊢ 0_{ℋ} = 0_{ℋ}$
4		ioran	$⊢ \neg (A = 0_{ℋ} \lor ⊥ (A) = 0_{ℋ}) \leftrightarrow (\neg A = 0_{ℋ} \land \neg ⊥ (A) = 0_{ℋ})$
5		df-ne	$⊢ A \neq 0_{ℋ} \leftrightarrow \neg A = 0_{ℋ}$
6		df-ne	$⊢ ⊥ (A) \neq 0_{ℋ} \leftrightarrow \neg ⊥ (A) = 0_{ℋ}$
7	5 6	anbi12i	$⊢ (A \neq 0_{ℋ} \land ⊥ (A) \neq 0_{ℋ}) \leftrightarrow (\neg A = 0_{ℋ} \land \neg ⊥ (A) = 0_{ℋ})$
8	4 7	bitr4i	$⊢ \neg (A = 0_{ℋ} \lor ⊥ (A) = 0_{ℋ}) \leftrightarrow (A \neq 0_{ℋ} \land ⊥ (A) \neq 0_{ℋ})$
9	1	hatomici	$⊢ A \neq 0_{ℋ} \to \exists p \in HAtoms p \subseteq A$
10	1	choccli	$⊢ ⊥ (A) \in C_{ℋ}$
11	10	hatomici	$⊢ ⊥ (A) \neq 0_{ℋ} \to \exists q \in HAtoms q \subseteq ⊥ (A)$
12	9 11	anim12i	$⊢ (A \neq 0_{ℋ} \land ⊥ (A) \neq 0_{ℋ}) \to (\exists p \in HAtoms p \subseteq A \land \exists q \in HAtoms q \subseteq ⊥ (A))$
13		reeanv	$⊢ \exists p \in HAtoms \exists q \in HAtoms (p \subseteq A \land q \subseteq ⊥ (A)) \leftrightarrow (\exists p \in HAtoms p \subseteq A \land \exists q \in HAtoms q \subseteq ⊥ (A))$
14	12 13	sylibr	$⊢ (A \neq 0_{ℋ} \land ⊥ (A) \neq 0_{ℋ}) \to \exists p \in HAtoms \exists q \in HAtoms (p \subseteq A \land q \subseteq ⊥ (A))$
15		simpll	$⊢ ((p \in HAtoms \land p \subseteq A) \land (q \in HAtoms \land q \subseteq ⊥ (A))) \to p \in HAtoms$
16		simprl	$⊢ ((p \in HAtoms \land p \subseteq A) \land (q \in HAtoms \land q \subseteq ⊥ (A))) \to q \in HAtoms$
17		atelch	$⊢ p \in HAtoms \to p \in C_{ℋ}$
18		chsscon3	$⊢ (p \in C_{ℋ} \land A \in C_{ℋ}) \to (p \subseteq A \leftrightarrow ⊥ (A) \subseteq ⊥ (p))$
19	17 1 18	sylancl	$⊢ p \in HAtoms \to (p \subseteq A \leftrightarrow ⊥ (A) \subseteq ⊥ (p))$
20	19	biimpa	$⊢ (p \in HAtoms \land p \subseteq A) \to ⊥ (A) \subseteq ⊥ (p)$
21		sstr	$⊢ (q \subseteq ⊥ (A) \land ⊥ (A) \subseteq ⊥ (p)) \to q \subseteq ⊥ (p)$
22	20 21	sylan2	$⊢ (q \subseteq ⊥ (A) \land (p \in HAtoms \land p \subseteq A)) \to q \subseteq ⊥ (p)$
23	22	ancoms	$⊢ ((p \in HAtoms \land p \subseteq A) \land q \subseteq ⊥ (A)) \to q \subseteq ⊥ (p)$
24		atne0	$⊢ p \in HAtoms \to p \neq 0_{ℋ}$
25	24	adantr	$⊢ (p \in HAtoms \land q \subseteq ⊥ (p)) \to p \neq 0_{ℋ}$
26		sseq1	$⊢ p = q \to (p \subseteq ⊥ (p) \leftrightarrow q \subseteq ⊥ (p))$
27	26	bicomd	$⊢ p = q \to (q \subseteq ⊥ (p) \leftrightarrow p \subseteq ⊥ (p))$
28		chssoc	$⊢ p \in C_{ℋ} \to (p \subseteq ⊥ (p) \leftrightarrow p = 0_{ℋ})$
29	17 28	syl	$⊢ p \in HAtoms \to (p \subseteq ⊥ (p) \leftrightarrow p = 0_{ℋ})$
30	27 29	sylan9bbr	$⊢ (p \in HAtoms \land p = q) \to (q \subseteq ⊥ (p) \leftrightarrow p = 0_{ℋ})$
31	30	biimpa	$⊢ ((p \in HAtoms \land p = q) \land q \subseteq ⊥ (p)) \to p = 0_{ℋ}$
32	31	an32s	$⊢ ((p \in HAtoms \land q \subseteq ⊥ (p)) \land p = q) \to p = 0_{ℋ}$
33	32	ex	$⊢ (p \in HAtoms \land q \subseteq ⊥ (p)) \to (p = q \to p = 0_{ℋ})$
34	33	necon3d	$⊢ (p \in HAtoms \land q \subseteq ⊥ (p)) \to (p \neq 0_{ℋ} \to p \neq q)$
35	25 34	mpd	$⊢ (p \in HAtoms \land q \subseteq ⊥ (p)) \to p \neq q$
36	35	adantlr	$⊢ ((p \in HAtoms \land p \subseteq A) \land q \subseteq ⊥ (p)) \to p \neq q$
37	23 36	syldan	$⊢ ((p \in HAtoms \land p \subseteq A) \land q \subseteq ⊥ (A)) \to p \neq q$
38	37	adantrl	$⊢ ((p \in HAtoms \land p \subseteq A) \land (q \in HAtoms \land q \subseteq ⊥ (A))) \to p \neq q$
39		superpos	$⊢ (p \in HAtoms \land q \in HAtoms \land p \neq q) \to \exists r \in HAtoms (r \neq p \land r \neq q \land r \subseteq p \lor_{ℋ} q)$
40	15 16 38 39	syl3anc	$⊢ ((p \in HAtoms \land p \subseteq A) \land (q \in HAtoms \land q \subseteq ⊥ (A))) \to \exists r \in HAtoms (r \neq p \land r \neq q \land r \subseteq p \lor_{ℋ} q)$
41		df-3an	$⊢ (r \neq p \land r \neq q \land r \subseteq p \lor_{ℋ} q) \leftrightarrow ((r \neq p \land r \neq q) \land r \subseteq p \lor_{ℋ} q)$
42		neanior	$⊢ (r \neq p \land r \neq q) \leftrightarrow \neg (r = p \lor r = q)$
43	42	anbi1i	$⊢ ((r \neq p \land r \neq q) \land r \subseteq p \lor_{ℋ} q) \leftrightarrow (\neg (r = p \lor r = q) \land r \subseteq p \lor_{ℋ} q)$
44	41 43	bitri	$⊢ (r \neq p \land r \neq q \land r \subseteq p \lor_{ℋ} q) \leftrightarrow (\neg (r = p \lor r = q) \land r \subseteq p \lor_{ℋ} q)$
45	1 2	chirredlem4	$⊢ (((p \in HAtoms \land p \subseteq A) \land (q \in HAtoms \land q \subseteq ⊥ (A))) \land (r \in HAtoms \land r \subseteq p \lor_{ℋ} q)) \to (r = p \lor r = q)$
46	45	anassrs	$⊢ ((((p \in HAtoms \land p \subseteq A) \land (q \in HAtoms \land q \subseteq ⊥ (A))) \land r \in HAtoms) \land r \subseteq p \lor_{ℋ} q) \to (r = p \lor r = q)$
47	46	pm2.24d	$⊢ ((((p \in HAtoms \land p \subseteq A) \land (q \in HAtoms \land q \subseteq ⊥ (A))) \land r \in HAtoms) \land r \subseteq p \lor_{ℋ} q) \to (\neg (r = p \lor r = q) \to \neg 0_{ℋ} = 0_{ℋ})$
48	47	ex	$⊢ (((p \in HAtoms \land p \subseteq A) \land (q \in HAtoms \land q \subseteq ⊥ (A))) \land r \in HAtoms) \to (r \subseteq p \lor_{ℋ} q \to (\neg (r = p \lor r = q) \to \neg 0_{ℋ} = 0_{ℋ}))$
49	48	com23	$⊢ (((p \in HAtoms \land p \subseteq A) \land (q \in HAtoms \land q \subseteq ⊥ (A))) \land r \in HAtoms) \to (\neg (r = p \lor r = q) \to (r \subseteq p \lor_{ℋ} q \to \neg 0_{ℋ} = 0_{ℋ}))$
50	49	impd	$⊢ (((p \in HAtoms \land p \subseteq A) \land (q \in HAtoms \land q \subseteq ⊥ (A))) \land r \in HAtoms) \to ((\neg (r = p \lor r = q) \land r \subseteq p \lor_{ℋ} q) \to \neg 0_{ℋ} = 0_{ℋ})$
51	44 50	syl5bi	$⊢ (((p \in HAtoms \land p \subseteq A) \land (q \in HAtoms \land q \subseteq ⊥ (A))) \land r \in HAtoms) \to ((r \neq p \land r \neq q \land r \subseteq p \lor_{ℋ} q) \to \neg 0_{ℋ} = 0_{ℋ})$
52	51	rexlimdva	$⊢ ((p \in HAtoms \land p \subseteq A) \land (q \in HAtoms \land q \subseteq ⊥ (A))) \to (\exists r \in HAtoms (r \neq p \land r \neq q \land r \subseteq p \lor_{ℋ} q) \to \neg 0_{ℋ} = 0_{ℋ})$
53	40 52	mpd	$⊢ ((p \in HAtoms \land p \subseteq A) \land (q \in HAtoms \land q \subseteq ⊥ (A))) \to \neg 0_{ℋ} = 0_{ℋ}$
54	53	an4s	$⊢ ((p \in HAtoms \land q \in HAtoms) \land (p \subseteq A \land q \subseteq ⊥ (A))) \to \neg 0_{ℋ} = 0_{ℋ}$
55	54	ex	$⊢ (p \in HAtoms \land q \in HAtoms) \to ((p \subseteq A \land q \subseteq ⊥ (A)) \to \neg 0_{ℋ} = 0_{ℋ})$
56	55	rexlimivv	$⊢ \exists p \in HAtoms \exists q \in HAtoms (p \subseteq A \land q \subseteq ⊥ (A)) \to \neg 0_{ℋ} = 0_{ℋ}$
57	14 56	syl	$⊢ (A \neq 0_{ℋ} \land ⊥ (A) \neq 0_{ℋ}) \to \neg 0_{ℋ} = 0_{ℋ}$
58	8 57	sylbi	$⊢ \neg (A = 0_{ℋ} \lor ⊥ (A) = 0_{ℋ}) \to \neg 0_{ℋ} = 0_{ℋ}$
59	3 58	mt4	$⊢ (A = 0_{ℋ} \lor ⊥ (A) = 0_{ℋ})$
60		fveq2	$⊢ ⊥ (A) = 0_{ℋ} \to ⊥ (⊥ (A)) = ⊥ (0_{ℋ})$
61	1	ococi	$⊢ ⊥ (⊥ (A)) = A$
62		choc0	$⊢ ⊥ (0_{ℋ}) = ℋ$
63	60 61 62	3eqtr3g	$⊢ ⊥ (A) = 0_{ℋ} \to A = ℋ$
64	63	orim2i	$⊢ (A = 0_{ℋ} \lor ⊥ (A) = 0_{ℋ}) \to (A = 0_{ℋ} \lor A = ℋ)$
65	59 64	ax-mp	$⊢ (A = 0_{ℋ} \lor A = ℋ)$

Metamath Proof Explorer

Theorem chirredi

Proof