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 | |
|
cvrexch.j | |
||
cvrexch.m | |
||
cvrexch.c | |
||
Assertion | cvrexch | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cvrexch.b | |
|
2 | cvrexch.j | |
|
3 | cvrexch.m | |
|
4 | cvrexch.c | |
|
5 | 1 2 3 4 | cvrexchlem | |
6 | simp1 | |
|
7 | hlop | |
|
8 | 7 | 3ad2ant1 | |
9 | simp3 | |
|
10 | eqid | |
|
11 | 1 10 | opoccl | |
12 | 8 9 11 | syl2anc | |
13 | simp2 | |
|
14 | 1 10 | opoccl | |
15 | 8 13 14 | syl2anc | |
16 | 1 2 3 4 | cvrexchlem | |
17 | 6 12 15 16 | syl3anc | |
18 | hlol | |
|
19 | 1 2 3 10 | oldmj1 | |
20 | 18 19 | syl3an1 | |
21 | hllat | |
|
22 | 21 | 3ad2ant1 | |
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 | |