Metamath Proof Explorer

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 ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) → ( 𝐴 = 0ℋ ∨ 𝐴 = ℋ ) )

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢ ( 𝐴 = if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) → ( 𝐴 = 0ℋ ↔ if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) = 0ℋ ) )
2 eqeq1 ⊢ ( 𝐴 = if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) → ( 𝐴 = ℋ ↔ if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) = ℋ ) )
3 1 2 orbi12d ⊢ ( 𝐴 = if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) → ( ( 𝐴 = 0ℋ ∨ 𝐴 = ℋ ) ↔ ( if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) = 0ℋ ∨ if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) = ℋ ) ) )
4 eleq1 ⊢ ( 𝐴 = if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) → ( 𝐴 ∈ Cℋ ↔ if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) ∈ Cℋ ) )
5 nfv ⊢ Ⅎ 𝑥 𝐴 ∈ Cℋ
6 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥
7 5 6 nfan ⊢ Ⅎ 𝑥 ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 )
8 nfcv ⊢ Ⅎ 𝑥 𝐴
9 nfcv ⊢ Ⅎ 𝑥 0ℋ
10 7 8 9 nfif ⊢ Ⅎ 𝑥 if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ )
11 10 nfeq2 ⊢ Ⅎ 𝑥 𝐴 = if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ )
12 breq1 ⊢ ( 𝐴 = if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) → ( 𝐴 𝐶ℋ 𝑥 ↔ if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) 𝐶ℋ 𝑥 ) )
13 11 12 ralbid ⊢ ( 𝐴 = if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) → ( ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ↔ ∀ 𝑥 ∈ Cℋ if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) 𝐶ℋ 𝑥 ) )
14 4 13 anbi12d ⊢ ( 𝐴 = if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) → ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) ↔ ( if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) 𝐶ℋ 𝑥 ) ) )
15 eleq1 ⊢ ( 0ℋ = if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) → ( 0ℋ ∈ Cℋ ↔ if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) ∈ Cℋ ) )
16 10 nfeq2 ⊢ Ⅎ 𝑥 0ℋ = if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ )
17 breq1 ⊢ ( 0ℋ = if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) → ( 0ℋ 𝐶ℋ 𝑥 ↔ if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) 𝐶ℋ 𝑥 ) )
18 16 17 ralbid ⊢ ( 0ℋ = if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) → ( ∀ 𝑥 ∈ Cℋ 0ℋ 𝐶ℋ 𝑥 ↔ ∀ 𝑥 ∈ Cℋ if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) 𝐶ℋ 𝑥 ) )
19 15 18 anbi12d ⊢ ( 0ℋ = if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) → ( ( 0ℋ ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 0ℋ 𝐶ℋ 𝑥 ) ↔ ( if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) 𝐶ℋ 𝑥 ) ) )
20 h0elch ⊢ 0ℋ ∈ Cℋ
21 cm0 ⊢ ( 𝑥 ∈ Cℋ → 0ℋ 𝐶ℋ 𝑥 )
22 21 rgen ⊢ ∀ 𝑥 ∈ Cℋ 0ℋ 𝐶ℋ 𝑥
23 20 22 pm3.2i ⊢ ( 0ℋ ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 0ℋ 𝐶ℋ 𝑥 )
24 14 19 23 elimhyp ⊢ ( if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) 𝐶ℋ 𝑥 )
25 24 simpli ⊢ if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) ∈ Cℋ
26 24 simpri ⊢ ∀ 𝑥 ∈ Cℋ if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) 𝐶ℋ 𝑥
27 nfcv ⊢ Ⅎ 𝑥 𝐶ℋ
28 nfcv ⊢ Ⅎ 𝑥 𝑦
29 10 27 28 nfbr ⊢ Ⅎ 𝑥 if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) 𝐶ℋ 𝑦
30 breq2 ⊢ ( 𝑥 = 𝑦 → ( if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) 𝐶ℋ 𝑥 ↔ if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) 𝐶ℋ 𝑦 ) )
31 29 30 rspc ⊢ ( 𝑦 ∈ Cℋ → ( ∀ 𝑥 ∈ Cℋ if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) 𝐶ℋ 𝑥 → if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) 𝐶ℋ 𝑦 ) )
32 26 31 mpi ⊢ ( 𝑦 ∈ Cℋ → if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) 𝐶ℋ 𝑦 )
33 25 32 chirredi ⊢ ( if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) = 0ℋ ∨ if ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) , 𝐴 , 0ℋ ) = ℋ )
34 3 33 dedth ⊢ ( ( 𝐴 ∈ Cℋ ∧ ∀ 𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥 ) → ( 𝐴 = 0ℋ ∨ 𝐴 = ℋ ) )