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 ⊢ 𝐴 ∈ Cℋ
chpssat.2 ⊢ 𝐵 ∈ Cℋ
Assertion cvexchi ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 ↔ 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) )

Proof

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