Theorem chirred

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, 16-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	chirred	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right)\to \left(A=0_{\mathscr{H}}\vee A=\mathscr{H}\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqeq1	$$⊢A=if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right)\to \left(A=0_{\mathscr{H}}\leftrightarrow if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right)=0_{\mathscr{H}}\right)$$
2		eqeq1	$$⊢A=if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right)\to \left(A=\mathscr{H}\leftrightarrow if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right)=\mathscr{H}\right)$$
3	1 2	orbi12d	$$⊢A=if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right)\to \left(\left(A=0_{\mathscr{H}}\vee A=\mathscr{H}\right)\leftrightarrow \left(if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right)=0_{\mathscr{H}}\vee if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right)=\mathscr{H}\right)\right)$$
4		eleq1	$$⊢A=if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right)\to \left(A\in {\mathbf{C}}_{\mathscr{H}}\leftrightarrow if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right)\in {\mathbf{C}}_{\mathscr{H}}\right)$$
5		nfv	$$⊢ℲxA\in {\mathbf{C}}_{\mathscr{H}}$$
6		nfra1	$$⊢Ⅎx\forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x$$
7	5 6	nfan	$$⊢Ⅎx\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right)$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}x{0}_{\mathscr{H}}$$
10	7 8 9	nfif	$$⊢\underset{\_}{Ⅎ}xif\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right)$$
11	10	nfeq2	$$⊢ℲxA=if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right)$$
12		breq1	$$⊢A=if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right)\to \left(A{𝐶}_{\mathscr{H}}x\leftrightarrow if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right){𝐶}_{\mathscr{H}}x\right)$$
13	11 12	ralbid	$$⊢A=if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right)\to \left(\forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right){𝐶}_{\mathscr{H}}x\right)$$
14	4 13	anbi12d	$$⊢A=if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right)\to \left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right)\leftrightarrow \left(if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right)\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right){𝐶}_{\mathscr{H}}x\right)\right)$$
15		eleq1	$$⊢0_{\mathscr{H}}=if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right)\to \left(0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}\leftrightarrow if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right)\in {\mathbf{C}}_{\mathscr{H}}\right)$$
16	10	nfeq2	$$⊢Ⅎx{0}_{\mathscr{H}}=if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right)$$
17		breq1	$$⊢0_{\mathscr{H}}=if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right)\to \left(0_{\mathscr{H}}{𝐶}_{\mathscr{H}}x\leftrightarrow if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right){𝐶}_{\mathscr{H}}x\right)$$
18	16 17	ralbid	$$⊢0_{\mathscr{H}}=if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right)\to \left(\forall x\in {\mathbf{C}}_{\mathscr{H}}{0}_{\mathscr{H}}{𝐶}_{\mathscr{H}}x\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right){𝐶}_{\mathscr{H}}x\right)$$
19	15 18	anbi12d	$$⊢0_{\mathscr{H}}=if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right)\to \left(\left(0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}{0}_{\mathscr{H}}{𝐶}_{\mathscr{H}}x\right)\leftrightarrow \left(if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right)\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right){𝐶}_{\mathscr{H}}x\right)\right)$$
20		h0elch	$$⊢0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}$$
21		cm0	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to 0_{\mathscr{H}}{𝐶}_{\mathscr{H}}x$$
22	21	rgen	$$⊢\forall x\in {\mathbf{C}}_{\mathscr{H}}{0}_{\mathscr{H}}{𝐶}_{\mathscr{H}}x$$
23	20 22	pm3.2i	$$⊢\left(0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}{0}_{\mathscr{H}}{𝐶}_{\mathscr{H}}x\right)$$
24	14 19 23	elimhyp	$$⊢\left(if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right)\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right){𝐶}_{\mathscr{H}}x\right)$$
25	24	simpli	$$⊢if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
26	24	simpri	$$⊢\forall x\in {\mathbf{C}}_{\mathscr{H}}if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right){𝐶}_{\mathscr{H}}x$$
27		nfcv	$$⊢\underset{\_}{Ⅎ}x{𝐶}_{\mathscr{H}}$$
28		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
29	10 27 28	nfbr	$$⊢Ⅎxif\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right){𝐶}_{\mathscr{H}}y$$
30		breq2	$$⊢x=y\to \left(if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right){𝐶}_{\mathscr{H}}x\leftrightarrow if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right){𝐶}_{\mathscr{H}}y\right)$$
31	29 30	rspc	$$⊢y\in {\mathbf{C}}_{\mathscr{H}}\to \left(\forall x\in {\mathbf{C}}_{\mathscr{H}}if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right){𝐶}_{\mathscr{H}}x\to if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right){𝐶}_{\mathscr{H}}y\right)$$
32	26 31	mpi	$$⊢y\in {\mathbf{C}}_{\mathscr{H}}\to if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right){𝐶}_{\mathscr{H}}y$$
33	25 32	chirredi	$$⊢\left(if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right)=0_{\mathscr{H}}\vee if\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right),A,0_{\mathscr{H}}\right)=\mathscr{H}\right)$$
34	3 33	dedth	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝐶}_{\mathscr{H}}x\right)\to \left(A=0_{\mathscr{H}}\vee A=\mathscr{H}\right)$$