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 ⊢ 𝐴 ∈ Cℋ
chirred.2 ⊢ ( 𝑥 ∈ Cℋ → 𝐴 𝐶ℋ 𝑥 )
Assertion chirredi ( 𝐴 = 0ℋ ∨ 𝐴 = ℋ )

Proof

Step Hyp Ref Expression
1 chirred.1 ⊢ 𝐴 ∈ Cℋ
2 chirred.2 ⊢ ( 𝑥 ∈ Cℋ → 𝐴 𝐶ℋ 𝑥 )
3 eqid ⊢ 0ℋ = 0ℋ
4 ioran ⊢ ( ¬ ( 𝐴 = 0ℋ ∨ ( ⊥ ‘ 𝐴 ) = 0ℋ ) ↔ ( ¬ 𝐴 = 0ℋ ∧ ¬ ( ⊥ ‘ 𝐴 ) = 0ℋ ) )
5 df-ne ⊢ ( 𝐴 ≠ 0ℋ ↔ ¬ 𝐴 = 0ℋ )
6 df-ne ⊢ ( ( ⊥ ‘ 𝐴 ) ≠ 0ℋ ↔ ¬ ( ⊥ ‘ 𝐴 ) = 0ℋ )
7 5 6 anbi12i ⊢ ( ( 𝐴 ≠ 0ℋ ∧ ( ⊥ ‘ 𝐴 ) ≠ 0ℋ ) ↔ ( ¬ 𝐴 = 0ℋ ∧ ¬ ( ⊥ ‘ 𝐴 ) = 0ℋ ) )
8 4 7 bitr4i ⊢ ( ¬ ( 𝐴 = 0ℋ ∨ ( ⊥ ‘ 𝐴 ) = 0ℋ ) ↔ ( 𝐴 ≠ 0ℋ ∧ ( ⊥ ‘ 𝐴 ) ≠ 0ℋ ) )
9 1 hatomici ⊢ ( 𝐴 ≠ 0ℋ → ∃ 𝑝 ∈ HAtoms 𝑝 ⊆ 𝐴 )
10 1 choccli ⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
11 10 hatomici ⊢ ( ( ⊥ ‘ 𝐴 ) ≠ 0ℋ → ∃ 𝑞 ∈ HAtoms 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) )
12 9 11 anim12i ⊢ ( ( 𝐴 ≠ 0ℋ ∧ ( ⊥ ‘ 𝐴 ) ≠ 0ℋ ) → ( ∃ 𝑝 ∈ HAtoms 𝑝 ⊆ 𝐴 ∧ ∃ 𝑞 ∈ HAtoms 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) )
13 reeanv ⊢ ( ∃ 𝑝 ∈ HAtoms ∃ 𝑞 ∈ HAtoms ( 𝑝 ⊆ 𝐴 ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ↔ ( ∃ 𝑝 ∈ HAtoms 𝑝 ⊆ 𝐴 ∧ ∃ 𝑞 ∈ HAtoms 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) )
14 12 13 sylibr ⊢ ( ( 𝐴 ≠ 0ℋ ∧ ( ⊥ ‘ 𝐴 ) ≠ 0ℋ ) → ∃ 𝑝 ∈ HAtoms ∃ 𝑞 ∈ HAtoms ( 𝑝 ⊆ 𝐴 ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) )
15 simpll ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) → 𝑝 ∈ HAtoms )
16 simprl ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) → 𝑞 ∈ HAtoms )
17 atelch ⊢ ( 𝑝 ∈ HAtoms → 𝑝 ∈ Cℋ )
18 chsscon3 ⊢ ( ( 𝑝 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( 𝑝 ⊆ 𝐴 ↔ ( ⊥ ‘ 𝐴 ) ⊆ ( ⊥ ‘ 𝑝 ) ) )
19 17 1 18 sylancl ⊢ ( 𝑝 ∈ HAtoms → ( 𝑝 ⊆ 𝐴 ↔ ( ⊥ ‘ 𝐴 ) ⊆ ( ⊥ ‘ 𝑝 ) ) )
20 19 biimpa ⊢ ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) → ( ⊥ ‘ 𝐴 ) ⊆ ( ⊥ ‘ 𝑝 ) )
21 sstr ⊢ ( ( 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ∧ ( ⊥ ‘ 𝐴 ) ⊆ ( ⊥ ‘ 𝑝 ) ) → 𝑞 ⊆ ( ⊥ ‘ 𝑝 ) )
22 20 21 sylan2 ⊢ ( ( 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ∧ ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ) → 𝑞 ⊆ ( ⊥ ‘ 𝑝 ) )
23 22 ancoms ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) → 𝑞 ⊆ ( ⊥ ‘ 𝑝 ) )
24 atne0 ⊢ ( 𝑝 ∈ HAtoms → 𝑝 ≠ 0ℋ )
25 24 adantr ⊢ ( ( 𝑝 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝑝 ) ) → 𝑝 ≠ 0ℋ )
26 sseq1 ⊢ ( 𝑝 = 𝑞 → ( 𝑝 ⊆ ( ⊥ ‘ 𝑝 ) ↔ 𝑞 ⊆ ( ⊥ ‘ 𝑝 ) ) )
27 26 bicomd ⊢ ( 𝑝 = 𝑞 → ( 𝑞 ⊆ ( ⊥ ‘ 𝑝 ) ↔ 𝑝 ⊆ ( ⊥ ‘ 𝑝 ) ) )
28 chssoc ⊢ ( 𝑝 ∈ Cℋ → ( 𝑝 ⊆ ( ⊥ ‘ 𝑝 ) ↔ 𝑝 = 0ℋ ) )
29 17 28 syl ⊢ ( 𝑝 ∈ HAtoms → ( 𝑝 ⊆ ( ⊥ ‘ 𝑝 ) ↔ 𝑝 = 0ℋ ) )
30 27 29 sylan9bbr ⊢ ( ( 𝑝 ∈ HAtoms ∧ 𝑝 = 𝑞 ) → ( 𝑞 ⊆ ( ⊥ ‘ 𝑝 ) ↔ 𝑝 = 0ℋ ) )
31 30 biimpa ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 = 𝑞 ) ∧ 𝑞 ⊆ ( ⊥ ‘ 𝑝 ) ) → 𝑝 = 0ℋ )
32 31 an32s ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝑝 ) ) ∧ 𝑝 = 𝑞 ) → 𝑝 = 0ℋ )
33 32 ex ⊢ ( ( 𝑝 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝑝 ) ) → ( 𝑝 = 𝑞 → 𝑝 = 0ℋ ) )
34 33 necon3d ⊢ ( ( 𝑝 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝑝 ) ) → ( 𝑝 ≠ 0ℋ → 𝑝 ≠ 𝑞 ) )
35 25 34 mpd ⊢ ( ( 𝑝 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝑝 ) ) → 𝑝 ≠ 𝑞 )
36 35 adantlr ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ 𝑞 ⊆ ( ⊥ ‘ 𝑝 ) ) → 𝑝 ≠ 𝑞 )
37 23 36 syldan ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) → 𝑝 ≠ 𝑞 )
38 37 adantrl ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) → 𝑝 ≠ 𝑞 )
39 superpos ⊢ ( ( 𝑝 ∈ HAtoms ∧ 𝑞 ∈ HAtoms ∧ 𝑝 ≠ 𝑞 ) → ∃ 𝑟 ∈ HAtoms ( 𝑟 ≠ 𝑝 ∧ 𝑟 ≠ 𝑞 ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) )
40 15 16 38 39 syl3anc ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) → ∃ 𝑟 ∈ HAtoms ( 𝑟 ≠ 𝑝 ∧ 𝑟 ≠ 𝑞 ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) )
41 df-3an ⊢ ( ( 𝑟 ≠ 𝑝 ∧ 𝑟 ≠ 𝑞 ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ↔ ( ( 𝑟 ≠ 𝑝 ∧ 𝑟 ≠ 𝑞 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) )
42 neanior ⊢ ( ( 𝑟 ≠ 𝑝 ∧ 𝑟 ≠ 𝑞 ) ↔ ¬ ( 𝑟 = 𝑝 ∨ 𝑟 = 𝑞 ) )
43 42 anbi1i ⊢ ( ( ( 𝑟 ≠ 𝑝 ∧ 𝑟 ≠ 𝑞 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ↔ ( ¬ ( 𝑟 = 𝑝 ∨ 𝑟 = 𝑞 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) )
44 41 43 bitri ⊢ ( ( 𝑟 ≠ 𝑝 ∧ 𝑟 ≠ 𝑞 ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ↔ ( ¬ ( 𝑟 = 𝑝 ∨ 𝑟 = 𝑞 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) )
45 1 2 chirredlem4 ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( 𝑟 = 𝑝 ∨ 𝑟 = 𝑞 ) )
46 45 anassrs ⊢ ( ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ 𝑟 ∈ HAtoms ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) → ( 𝑟 = 𝑝 ∨ 𝑟 = 𝑞 ) )
47 46 pm2.24d ⊢ ( ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ 𝑟 ∈ HAtoms ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) → ( ¬ ( 𝑟 = 𝑝 ∨ 𝑟 = 𝑞 ) → ¬ 0ℋ = 0ℋ ) )
48 47 ex ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ 𝑟 ∈ HAtoms ) → ( 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) → ( ¬ ( 𝑟 = 𝑝 ∨ 𝑟 = 𝑞 ) → ¬ 0ℋ = 0ℋ ) ) )
49 48 com23 ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ 𝑟 ∈ HAtoms ) → ( ¬ ( 𝑟 = 𝑝 ∨ 𝑟 = 𝑞 ) → ( 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) → ¬ 0ℋ = 0ℋ ) ) )
50 49 impd ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ 𝑟 ∈ HAtoms ) → ( ( ¬ ( 𝑟 = 𝑝 ∨ 𝑟 = 𝑞 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) → ¬ 0ℋ = 0ℋ ) )
51 44 50 syl5bi ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ 𝑟 ∈ HAtoms ) → ( ( 𝑟 ≠ 𝑝 ∧ 𝑟 ≠ 𝑞 ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) → ¬ 0ℋ = 0ℋ ) )
52 51 rexlimdva ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) → ( ∃ 𝑟 ∈ HAtoms ( 𝑟 ≠ 𝑝 ∧ 𝑟 ≠ 𝑞 ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) → ¬ 0ℋ = 0ℋ ) )
53 40 52 mpd ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) → ¬ 0ℋ = 0ℋ )
54 53 an4s ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ 𝑞 ∈ HAtoms ) ∧ ( 𝑝 ⊆ 𝐴 ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) → ¬ 0ℋ = 0ℋ )
55 54 ex ⊢ ( ( 𝑝 ∈ HAtoms ∧ 𝑞 ∈ HAtoms ) → ( ( 𝑝 ⊆ 𝐴 ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) → ¬ 0ℋ = 0ℋ ) )
56 55 rexlimivv ⊢ ( ∃ 𝑝 ∈ HAtoms ∃ 𝑞 ∈ HAtoms ( 𝑝 ⊆ 𝐴 ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) → ¬ 0ℋ = 0ℋ )
57 14 56 syl ⊢ ( ( 𝐴 ≠ 0ℋ ∧ ( ⊥ ‘ 𝐴 ) ≠ 0ℋ ) → ¬ 0ℋ = 0ℋ )
58 8 57 sylbi ⊢ ( ¬ ( 𝐴 = 0ℋ ∨ ( ⊥ ‘ 𝐴 ) = 0ℋ ) → ¬ 0ℋ = 0ℋ )
59 3 58 mt4 ⊢ ( 𝐴 = 0ℋ ∨ ( ⊥ ‘ 𝐴 ) = 0ℋ )
60 fveq2 ⊢ ( ( ⊥ ‘ 𝐴 ) = 0ℋ → ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) = ( ⊥ ‘ 0ℋ ) )
61 1 ococi ⊢ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) = 𝐴
62 choc0 ⊢ ( ⊥ ‘ 0ℋ ) = ℋ
63 60 61 62 3eqtr3g ⊢ ( ( ⊥ ‘ 𝐴 ) = 0ℋ → 𝐴 = ℋ )
64 63 orim2i ⊢ ( ( 𝐴 = 0ℋ ∨ ( ⊥ ‘ 𝐴 ) = 0ℋ ) → ( 𝐴 = 0ℋ ∨ 𝐴 = ℋ ) )
65 59 64 ax-mp ⊢ ( 𝐴 = 0ℋ ∨ 𝐴 = ℋ )