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