This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
cvrexch.j ⊢ ∨ = ( join ‘ 𝐾 )
cvrexch.m ⊢ ∧ = ( meet ‘ 𝐾 )
cvrexch.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
Assertion cvrexch ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 ↔ 𝑋 𝐶 ( 𝑋 ∨ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 cvrexch.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cvrexch.j ⊢ ∨ = ( join ‘ 𝐾 )
3 cvrexch.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 cvrexch.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
5 1 2 3 4 cvrexchlem ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 → 𝑋 𝐶 ( 𝑋 ∨ 𝑌 ) ) )
6 simp1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ HL )
7 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
8 7 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ OP )
9 simp3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
10 eqid ⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
11 1 10 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 )
12 8 9 11 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 )
13 simp2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
14 1 10 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 )
15 8 13 14 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 )
16 1 2 3 4 cvrexchlem ⊢ ( ( 𝐾 ∈ HL ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ) → ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) )
17 6 12 15 16 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) )
18 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
19 1 2 3 10 oldmj1 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
20 18 19 syl3an1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
21 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
22 21 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ Lat )
23 1 3 latmcom ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
24 22 15 12 23 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
25 20 24 eqtrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
26 25 breq1d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∨ 𝑌 ) ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ↔ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
27 1 2 3 10 oldmm1 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
28 18 27 syl3an1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
29 1 2 latjcom ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
30 22 15 12 29 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
31 28 30 eqtrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
32 31 breq2d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∧ 𝑌 ) ) ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) )
33 17 26 32 3imtr4d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∨ 𝑌 ) ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∧ 𝑌 ) ) ) )
34 1 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
35 21 34 syl3an1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
36 1 10 4 cvrcon3b ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ) → ( 𝑋 𝐶 ( 𝑋 ∨ 𝑌 ) ↔ ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∨ 𝑌 ) ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
37 8 13 35 36 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 ( 𝑋 ∨ 𝑌 ) ↔ ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∨ 𝑌 ) ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
38 1 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
39 21 38 syl3an1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
40 1 10 4 cvrcon3b ⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∧ 𝑌 ) ) ) )
41 8 39 9 40 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∧ 𝑌 ) ) ) )
42 33 37 41 3imtr4d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 ( 𝑋 ∨ 𝑌 ) → ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 ) )
43 5 42 impbid ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 ↔ 𝑋 𝐶 ( 𝑋 ∨ 𝑌 ) ) )