Metamath Proof Explorer

Theorem 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 e. CH
chirred.2 
|- ( x e. CH -> A C_H x )
Assertion chirredi 
|- ( A = 0H \/ A = ~H )

Proof

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