# Metamath Proof Explorer

## Theorem cvrexch

Description: A Hilbert lattice satisfies the exchange axiom. Proposition 1(iii) of Kalmbach p. 140 and its converse. Originally proved by Garrett Birkhoff in 1933. ( cvexchi analog.) (Contributed by NM, 18-Nov-2011)

Ref Expression
Hypotheses cvrexch.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
cvrexch.j
cvrexch.m
cvrexch.c ${⊢}{C}={⋖}_{{K}}$
Assertion cvrexch

### Proof

Step Hyp Ref Expression
1 cvrexch.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 cvrexch.j
3 cvrexch.m
4 cvrexch.c ${⊢}{C}={⋖}_{{K}}$
5 1 2 3 4 cvrexchlem
6 simp1 ${⊢}\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {K}\in \mathrm{HL}$
7 hlop ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OP}$
8 7 3ad2ant1 ${⊢}\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {K}\in \mathrm{OP}$
9 simp3 ${⊢}\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {Y}\in {B}$
10 eqid ${⊢}\mathrm{oc}\left({K}\right)=\mathrm{oc}\left({K}\right)$
11 1 10 opoccl ${⊢}\left({K}\in \mathrm{OP}\wedge {Y}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({Y}\right)\in {B}$
12 8 9 11 syl2anc ${⊢}\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({Y}\right)\in {B}$
13 simp2 ${⊢}\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {X}\in {B}$
14 1 10 opoccl ${⊢}\left({K}\in \mathrm{OP}\wedge {X}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({X}\right)\in {B}$
15 8 13 14 syl2anc ${⊢}\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({X}\right)\in {B}$
16 1 2 3 4 cvrexchlem
17 6 12 15 16 syl3anc
18 hlol ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OL}$
19 1 2 3 10 oldmj1
20 18 19 syl3an1
21 hllat ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{Lat}$
22 21 3ad2ant1 ${⊢}\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {K}\in \mathrm{Lat}$
23 1 3 latmcom
24 22 15 12 23 syl3anc
25 20 24 eqtrd
26 25 breq1d
27 1 2 3 10 oldmm1
28 18 27 syl3an1
29 1 2 latjcom
30 22 15 12 29 syl3anc
31 28 30 eqtrd
32 31 breq2d
33 17 26 32 3imtr4d
34 1 2 latjcl
35 21 34 syl3an1
36 1 10 4 cvrcon3b
37 8 13 35 36 syl3anc
38 1 3 latmcl
39 21 38 syl3an1
40 1 10 4 cvrcon3b
41 8 39 9 40 syl3anc
42 33 37 41 3imtr4d
43 5 42 impbid