This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cvexchi

Description: The Hilbert lattice satisfies the exchange axiom. Proposition 1(iii) of Kalmbach p. 140 and its converse. Originally proved by Garrett Birkhoff in 1933. (Contributed by NM, 12-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypotheses chpssat.1 
|- A e. CH
chpssat.2 
|- B e. CH
Assertion cvexchi 
|- ( ( A i^i B )  A

Proof

Step Hyp Ref Expression
1 chpssat.1 
 |-  A e. CH
2 chpssat.2 
 |-  B e. CH
3 1 2 cvexchlem 
 |-  ( ( A i^i B )  A
4 2 choccli 
 |-  ( _|_ ` B ) e. CH
5 1 choccli 
 |-  ( _|_ ` A ) e. CH
6 4 5 cvexchlem 
 |-  ( ( ( _|_ ` B ) i^i ( _|_ ` A ) )  ( _|_ ` B )
7 1 2 chdmj1i 
 |-  ( _|_ ` ( A vH B ) ) = ( ( _|_ ` A ) i^i ( _|_ ` B ) )
8 incom 
 |-  ( ( _|_ ` A ) i^i ( _|_ ` B ) ) = ( ( _|_ ` B ) i^i ( _|_ ` A ) )
9 7 8 eqtri 
 |-  ( _|_ ` ( A vH B ) ) = ( ( _|_ ` B ) i^i ( _|_ ` A ) )
10 9 breq1i 
 |-  ( ( _|_ ` ( A vH B ) )  ( ( _|_ ` B ) i^i ( _|_ ` A ) )
11 1 2 chdmm1i 
 |-  ( _|_ ` ( A i^i B ) ) = ( ( _|_ ` A ) vH ( _|_ ` B ) )
12 5 4 chjcomi 
 |-  ( ( _|_ ` A ) vH ( _|_ ` B ) ) = ( ( _|_ ` B ) vH ( _|_ ` A ) )
13 11 12 eqtri 
 |-  ( _|_ ` ( A i^i B ) ) = ( ( _|_ ` B ) vH ( _|_ ` A ) )
14 13 breq2i 
 |-  ( ( _|_ ` B )  ( _|_ ` B )
15 6 10 14 3imtr4i 
 |-  ( ( _|_ ` ( A vH B ) )  ( _|_ ` B )
16 1 2 chjcli 
 |-  ( A vH B ) e. CH
17 cvcon3 
 |-  ( ( A e. CH /\ ( A vH B ) e. CH ) -> ( A  ( _|_ ` ( A vH B ) )
18 1 16 17 mp2an 
 |-  ( A  ( _|_ ` ( A vH B ) )
19 1 2 chincli 
 |-  ( A i^i B ) e. CH
20 cvcon3 
 |-  ( ( ( A i^i B ) e. CH /\ B e. CH ) -> ( ( A i^i B )  ( _|_ ` B )
21 19 2 20 mp2an 
 |-  ( ( A i^i B )  ( _|_ ` B )
22 15 18 21 3imtr4i 
 |-  ( A  ( A i^i B )
23 3 22 impbii 
 |-  ( ( A i^i B )  A