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 ∈ C ℋ
chpssat.2 ⊢ B ∈ C ℋ
Assertion cvexchi ⊢ A ∩ B ⋖ ℋ B ↔ A ⋖ ℋ A ∨ ℋ B

Proof

Step Hyp Ref Expression
1 chpssat.1 ⊢ A ∈ C ℋ
2 chpssat.2 ⊢ B ∈ C ℋ
3 1 2 cvexchlem ⊢ A ∩ B ⋖ ℋ B → A ⋖ ℋ A ∨ ℋ B
4 2 choccli ⊢ ⊥ ⁡ B ∈ C ℋ
5 1 choccli ⊢ ⊥ ⁡ A ∈ C ℋ
6 4 5 cvexchlem ⊢ ⊥ ⁡ B ∩ ⊥ ⁡ A ⋖ ℋ ⊥ ⁡ A → ⊥ ⁡ B ⋖ ℋ ⊥ ⁡ B ∨ ℋ ⊥ ⁡ A
7 1 2 chdmj1i ⊢ ⊥ ⁡ A ∨ ℋ B = ⊥ ⁡ A ∩ ⊥ ⁡ B
8 incom ⊢ ⊥ ⁡ A ∩ ⊥ ⁡ B = ⊥ ⁡ B ∩ ⊥ ⁡ A
9 7 8 eqtri ⊢ ⊥ ⁡ A ∨ ℋ B = ⊥ ⁡ B ∩ ⊥ ⁡ A
10 9 breq1i ⊢ ⊥ ⁡ A ∨ ℋ B ⋖ ℋ ⊥ ⁡ A ↔ ⊥ ⁡ B ∩ ⊥ ⁡ A ⋖ ℋ ⊥ ⁡ A
11 1 2 chdmm1i ⊢ ⊥ ⁡ A ∩ B = ⊥ ⁡ A ∨ ℋ ⊥ ⁡ B
12 5 4 chjcomi ⊢ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ B = ⊥ ⁡ B ∨ ℋ ⊥ ⁡ A
13 11 12 eqtri ⊢ ⊥ ⁡ A ∩ B = ⊥ ⁡ B ∨ ℋ ⊥ ⁡ A
14 13 breq2i ⊢ ⊥ ⁡ B ⋖ ℋ ⊥ ⁡ A ∩ B ↔ ⊥ ⁡ B ⋖ ℋ ⊥ ⁡ B ∨ ℋ ⊥ ⁡ A
15 6 10 14 3imtr4i ⊢ ⊥ ⁡ A ∨ ℋ B ⋖ ℋ ⊥ ⁡ A → ⊥ ⁡ B ⋖ ℋ ⊥ ⁡ A ∩ B
16 1 2 chjcli ⊢ A ∨ ℋ B ∈ C ℋ
17 cvcon3 ⊢ A ∈ C ℋ ∧ A ∨ ℋ B ∈ C ℋ → A ⋖ ℋ A ∨ ℋ B ↔ ⊥ ⁡ A ∨ ℋ B ⋖ ℋ ⊥ ⁡ A
18 1 16 17 mp2an ⊢ A ⋖ ℋ A ∨ ℋ B ↔ ⊥ ⁡ A ∨ ℋ B ⋖ ℋ ⊥ ⁡ A
19 1 2 chincli ⊢ A ∩ B ∈ C ℋ
20 cvcon3 ⊢ A ∩ B ∈ C ℋ ∧ B ∈ C ℋ → A ∩ B ⋖ ℋ B ↔ ⊥ ⁡ B ⋖ ℋ ⊥ ⁡ A ∩ B
21 19 2 20 mp2an ⊢ A ∩ B ⋖ ℋ B ↔ ⊥ ⁡ B ⋖ ℋ ⊥ ⁡ A ∩ B
22 15 18 21 3imtr4i ⊢ A ⋖ ℋ A ∨ ℋ B → A ∩ B ⋖ ℋ B
23 3 22 impbii ⊢ A ∩ B ⋖ ℋ B ↔ A ⋖ ℋ A ∨ ℋ B