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	$⊢ \underset{˙}{\lor} = join (K)$
	cvrexch.m	$⊢ \underset{˙}{\land} = meet (K)$
	cvrexch.c	$⊢ C = ⋖_{K}$
Assertion	cvrexch	$⊢ (K \in HL \land X \in B \land Y \in B) \to ((X \underset{˙}{\land} Y) C Y \leftrightarrow X C (X \underset{˙}{\lor} Y))$

Proof

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

Metamath Proof Explorer

Theorem cvrexch

Proof