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 = ( Base ` K )
cvrexch.j 
|- .\/ = ( join ` K )
cvrexch.m 
|- ./\ = ( meet ` K )
cvrexch.c 
|- C = (
Assertion cvrexch 
|- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ( X ./\ Y ) C Y <-> X C ( X .\/ Y ) ) )

Proof

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