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

Proof

Step Hyp Ref Expression
1 eqeq1 
 |-  ( A = if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) -> ( A = 0H <-> if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) = 0H ) )
2 eqeq1 
 |-  ( A = if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) -> ( A = ~H <-> if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) = ~H ) )
3 1 2 orbi12d 
 |-  ( A = if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) -> ( ( A = 0H \/ A = ~H ) <-> ( if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) = 0H \/ if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) = ~H ) ) )
4 eleq1 
 |-  ( A = if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) -> ( A e. CH <-> if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) e. CH ) )
5 nfv 
 |-  F/ x A e. CH
6 nfra1 
 |-  F/ x A. x e. CH A C_H x
7 5 6 nfan 
 |-  F/ x ( A e. CH /\ A. x e. CH A C_H x )
8 nfcv 
 |-  F/_ x A
9 nfcv 
 |-  F/_ x 0H
10 7 8 9 nfif 
 |-  F/_ x if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H )
11 10 nfeq2 
 |-  F/ x A = if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H )
12 breq1 
 |-  ( A = if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) -> ( A C_H x <-> if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) C_H x ) )
13 11 12 ralbid 
 |-  ( A = if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) -> ( A. x e. CH A C_H x <-> A. x e. CH if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) C_H x ) )
14 4 13 anbi12d 
 |-  ( A = if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) -> ( ( A e. CH /\ A. x e. CH A C_H x ) <-> ( if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) e. CH /\ A. x e. CH if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) C_H x ) ) )
15 eleq1 
 |-  ( 0H = if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) -> ( 0H e. CH <-> if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) e. CH ) )
16 10 nfeq2 
 |-  F/ x 0H = if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H )
17 breq1 
 |-  ( 0H = if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) -> ( 0H C_H x <-> if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) C_H x ) )
18 16 17 ralbid 
 |-  ( 0H = if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) -> ( A. x e. CH 0H C_H x <-> A. x e. CH if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) C_H x ) )
19 15 18 anbi12d 
 |-  ( 0H = if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) -> ( ( 0H e. CH /\ A. x e. CH 0H C_H x ) <-> ( if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) e. CH /\ A. x e. CH if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) C_H x ) ) )
20 h0elch 
 |-  0H e. CH
21 cm0 
 |-  ( x e. CH -> 0H C_H x )
22 21 rgen 
 |-  A. x e. CH 0H C_H x
23 20 22 pm3.2i 
 |-  ( 0H e. CH /\ A. x e. CH 0H C_H x )
24 14 19 23 elimhyp 
 |-  ( if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) e. CH /\ A. x e. CH if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) C_H x )
25 24 simpli 
 |-  if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) e. CH
26 24 simpri 
 |-  A. x e. CH if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) C_H x
27 nfcv 
 |-  F/_ x C_H
28 nfcv 
 |-  F/_ x y
29 10 27 28 nfbr 
 |-  F/ x if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) C_H y
30 breq2 
 |-  ( x = y -> ( if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) C_H x <-> if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) C_H y ) )
31 29 30 rspc 
 |-  ( y e. CH -> ( A. x e. CH if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) C_H x -> if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) C_H y ) )
32 26 31 mpi 
 |-  ( y e. CH -> if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) C_H y )
33 25 32 chirredi 
 |-  ( if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) = 0H \/ if ( ( A e. CH /\ A. x e. CH A C_H x ) , A , 0H ) = ~H )
34 3 33 dedth 
 |-  ( ( A e. CH /\ A. x e. CH A C_H x ) -> ( A = 0H \/ A = ~H ) )