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=BaseK
cvrexch.j ˙=joinK
cvrexch.m ˙=meetK
cvrexch.c C=K
Assertion cvrexch KHLXBYBX˙YCYXCX˙Y

Proof

Step Hyp Ref Expression
1 cvrexch.b B=BaseK
2 cvrexch.j ˙=joinK
3 cvrexch.m ˙=meetK
4 cvrexch.c C=K
5 1 2 3 4 cvrexchlem KHLXBYBX˙YCYXCX˙Y
6 simp1 KHLXBYBKHL
7 hlop KHLKOP
8 7 3ad2ant1 KHLXBYBKOP
9 simp3 KHLXBYBYB
10 eqid ocK=ocK
11 1 10 opoccl KOPYBocKYB
12 8 9 11 syl2anc KHLXBYBocKYB
13 simp2 KHLXBYBXB
14 1 10 opoccl KOPXBocKXB
15 8 13 14 syl2anc KHLXBYBocKXB
16 1 2 3 4 cvrexchlem KHLocKYBocKXBocKY˙ocKXCocKXocKYCocKY˙ocKX
17 6 12 15 16 syl3anc KHLXBYBocKY˙ocKXCocKXocKYCocKY˙ocKX
18 hlol KHLKOL
19 1 2 3 10 oldmj1 KOLXBYBocKX˙Y=ocKX˙ocKY
20 18 19 syl3an1 KHLXBYBocKX˙Y=ocKX˙ocKY
21 hllat KHLKLat
22 21 3ad2ant1 KHLXBYBKLat
23 1 3 latmcom KLatocKXBocKYBocKX˙ocKY=ocKY˙ocKX
24 22 15 12 23 syl3anc KHLXBYBocKX˙ocKY=ocKY˙ocKX
25 20 24 eqtrd KHLXBYBocKX˙Y=ocKY˙ocKX
26 25 breq1d KHLXBYBocKX˙YCocKXocKY˙ocKXCocKX
27 1 2 3 10 oldmm1 KOLXBYBocKX˙Y=ocKX˙ocKY
28 18 27 syl3an1 KHLXBYBocKX˙Y=ocKX˙ocKY
29 1 2 latjcom KLatocKXBocKYBocKX˙ocKY=ocKY˙ocKX
30 22 15 12 29 syl3anc KHLXBYBocKX˙ocKY=ocKY˙ocKX
31 28 30 eqtrd KHLXBYBocKX˙Y=ocKY˙ocKX
32 31 breq2d KHLXBYBocKYCocKX˙YocKYCocKY˙ocKX
33 17 26 32 3imtr4d KHLXBYBocKX˙YCocKXocKYCocKX˙Y
34 1 2 latjcl KLatXBYBX˙YB
35 21 34 syl3an1 KHLXBYBX˙YB
36 1 10 4 cvrcon3b KOPXBX˙YBXCX˙YocKX˙YCocKX
37 8 13 35 36 syl3anc KHLXBYBXCX˙YocKX˙YCocKX
38 1 3 latmcl KLatXBYBX˙YB
39 21 38 syl3an1 KHLXBYBX˙YB
40 1 10 4 cvrcon3b KOPX˙YBYBX˙YCYocKYCocKX˙Y
41 8 39 9 40 syl3anc KHLXBYBX˙YCYocKYCocKX˙Y
42 33 37 41 3imtr4d KHLXBYBXCX˙YX˙YCY
43 5 42 impbid KHLXBYBX˙YCYXCX˙Y