latjass

Description: Lattice join is associative. Lemma 2.2 in MegPav2002 p. 362. ( chjass analog.) (Contributed by NM, 17-Sep-2011)

	Ref	Expression
Hypotheses	latjass.b	$⊢ B = {Base}_{K}$
	latjass.j	$⊢ \underset{˙}{\lor} = join (K)$
Assertion	latjass	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z = X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z)$

Proof

Step	Hyp	Ref	Expression
1		latjass.b	$⊢ B = {Base}_{K}$
2		latjass.j	$⊢ \underset{˙}{\lor} = join (K)$
3		eqid	$⊢ \leq_{K} = \leq_{K}$
4		simpl	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to K \in Lat$
5	1 2	latjcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\lor} Y \in B$
6	5	3adant3r3	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\lor} Y \in B$
7		simpr3	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Z \in B$
8	1 2	latjcl	$⊢ (K \in Lat \land X \underset{˙}{\lor} Y \in B \land Z \in B) \to (X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z \in B$
9	4 6 7 8	syl3anc	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z \in B$
10		simpr1	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to X \in B$
11	1 2	latjcl	$⊢ (K \in Lat \land Y \in B \land Z \in B) \to Y \underset{˙}{\lor} Z \in B$
12	11	3adant3r1	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Y \underset{˙}{\lor} Z \in B$
13	1 2	latjcl	$⊢ (K \in Lat \land X \in B \land Y \underset{˙}{\lor} Z \in B) \to X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z) \in B$
14	4 10 12 13	syl3anc	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z) \in B$
15	1 3 2	latlej1	$⊢ (K \in Lat \land X \in B \land Y \underset{˙}{\lor} Z \in B) \to X \leq_{K} (X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z))$
16	4 10 12 15	syl3anc	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to X \leq_{K} (X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z))$
17		simpr2	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Y \in B$
18	1 3 2	latlej1	$⊢ (K \in Lat \land Y \in B \land Z \in B) \to Y \leq_{K} (Y \underset{˙}{\lor} Z)$
19	18	3adant3r1	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Y \leq_{K} (Y \underset{˙}{\lor} Z)$
20	1 3 2	latlej2	$⊢ (K \in Lat \land X \in B \land Y \underset{˙}{\lor} Z \in B) \to (Y \underset{˙}{\lor} Z) \leq_{K} (X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z))$
21	4 10 12 20	syl3anc	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (Y \underset{˙}{\lor} Z) \leq_{K} (X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z))$
22	1 3 4 17 12 14 19 21	lattrd	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Y \leq_{K} (X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z))$
23	1 3 2	latjle12	$⊢ (K \in Lat \land (X \in B \land Y \in B \land X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z) \in B)) \to ((X \leq_{K} (X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z)) \land Y \leq_{K} (X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z))) \leftrightarrow (X \underset{˙}{\lor} Y) \leq_{K} (X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z)))$
24	4 10 17 14 23	syl13anc	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to ((X \leq_{K} (X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z)) \land Y \leq_{K} (X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z))) \leftrightarrow (X \underset{˙}{\lor} Y) \leq_{K} (X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z)))$
25	16 22 24	mpbi2and	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\lor} Y) \leq_{K} (X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z))$
26	1 3 2	latlej2	$⊢ (K \in Lat \land Y \in B \land Z \in B) \to Z \leq_{K} (Y \underset{˙}{\lor} Z)$
27	26	3adant3r1	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Z \leq_{K} (Y \underset{˙}{\lor} Z)$
28	1 3 4 7 12 14 27 21	lattrd	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Z \leq_{K} (X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z))$
29	1 3 2	latjle12	$⊢ (K \in Lat \land (X \underset{˙}{\lor} Y \in B \land Z \in B \land X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z) \in B)) \to (((X \underset{˙}{\lor} Y) \leq_{K} (X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z)) \land Z \leq_{K} (X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z))) \leftrightarrow ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z) \leq_{K} (X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z)))$
30	4 6 7 14 29	syl13anc	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (((X \underset{˙}{\lor} Y) \leq_{K} (X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z)) \land Z \leq_{K} (X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z))) \leftrightarrow ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z) \leq_{K} (X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z)))$
31	25 28 30	mpbi2and	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z) \leq_{K} (X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z))$
32	1 3 2	latlej1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \leq_{K} (X \underset{˙}{\lor} Y)$
33	32	3adant3r3	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to X \leq_{K} (X \underset{˙}{\lor} Y)$
34	1 3 2	latlej1	$⊢ (K \in Lat \land X \underset{˙}{\lor} Y \in B \land Z \in B) \to (X \underset{˙}{\lor} Y) \leq_{K} ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z)$
35	4 6 7 34	syl3anc	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\lor} Y) \leq_{K} ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z)$
36	1 3 4 10 6 9 33 35	lattrd	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to X \leq_{K} ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z)$
37	1 3 2	latlej2	$⊢ (K \in Lat \land X \in B \land Y \in B) \to Y \leq_{K} (X \underset{˙}{\lor} Y)$
38	37	3adant3r3	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Y \leq_{K} (X \underset{˙}{\lor} Y)$
39	1 3 4 17 6 9 38 35	lattrd	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Y \leq_{K} ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z)$
40	1 3 2	latlej2	$⊢ (K \in Lat \land X \underset{˙}{\lor} Y \in B \land Z \in B) \to Z \leq_{K} ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z)$
41	4 6 7 40	syl3anc	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Z \leq_{K} ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z)$
42	1 3 2	latjle12	$⊢ (K \in Lat \land (Y \in B \land Z \in B \land (X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z \in B)) \to ((Y \leq_{K} ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z) \land Z \leq_{K} ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z)) \leftrightarrow (Y \underset{˙}{\lor} Z) \leq_{K} ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z))$
43	4 17 7 9 42	syl13anc	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to ((Y \leq_{K} ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z) \land Z \leq_{K} ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z)) \leftrightarrow (Y \underset{˙}{\lor} Z) \leq_{K} ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z))$
44	39 41 43	mpbi2and	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (Y \underset{˙}{\lor} Z) \leq_{K} ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z)$
45	1 3 2	latjle12	$⊢ (K \in Lat \land (X \in B \land Y \underset{˙}{\lor} Z \in B \land (X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z \in B)) \to ((X \leq_{K} ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z) \land (Y \underset{˙}{\lor} Z) \leq_{K} ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z)) \leftrightarrow (X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z)) \leq_{K} ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z))$
46	4 10 12 9 45	syl13anc	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to ((X \leq_{K} ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z) \land (Y \underset{˙}{\lor} Z) \leq_{K} ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z)) \leftrightarrow (X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z)) \leq_{K} ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z))$
47	36 44 46	mpbi2and	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z)) \leq_{K} ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z)$
48	1 3 4 9 14 31 47	latasymd	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z = X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z)$

Metamath Proof Explorer

Theorem latjass

Proof