Theorem latjass 16886

Description: Lattice join is associative. Lemma 2.2 in [MegPav2002] p. 362. (Th. chjass 11089 analog.)

Hypotheses

Ref	Expression
latjass.b	|- B = (base` K)
latjass.j	|- J = (join` K)

Assertion

Ref	Expression
latjass	|- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> ((XJY)JZ) = (XJ(YJZ)))

Proof of Theorem latjass

Step	Hyp	Ref	Expression
1		latpos 16851	. . . 4 |- (K e. LatNEW -> K e. PosetNEW)
2	1	adantr 425	. . 3 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> K e. PosetNEW)
3		simpl 346	. . . 4 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> K e. LatNEW)
4		latjass.b	. . . . . 6 |- B = (base` K)
5		latjass.j	. . . . . 6 |- J = (join` K)
6	4, 5	latjcl 16852	. . . . 5 |- ((K e. LatNEW /\ X e. B /\ Y e. B) -> (XJY) e. B)
7	6	3adant3r3 1079	. . . 4 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> (XJY) e. B)
8		simpr3 884	. . . 4 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> Z e. B)
9	4, 5	latjcl 16852	. . . 4 |- ((K e. LatNEW /\ (XJY) e. B /\ Z e. B) -> ((XJY)JZ) e. B)
10	3, 7, 8, 9	syl111anc 1100	. . 3 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> ((XJY)JZ) e. B)
11		simpr1 882	. . . 4 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> X e. B)
12	4, 5	latjcl 16852	. . . . 5 |- ((K e. LatNEW /\ Y e. B /\ Z e. B) -> (YJZ) e. B)
13	12	3adant3r1 1077	. . . 4 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> (YJZ) e. B)
14	4, 5	latjcl 16852	. . . 4 |- ((K e. LatNEW /\ X e. B /\ (YJZ) e. B) -> (XJ(YJZ)) e. B)
15	3, 11, 13, 14	syl111anc 1100	. . 3 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> (XJ(YJZ)) e. B)
16		eqid 1884	. . . 4 |- (le` K) = (le` K)
17	4, 16	posasymb 16776	. . 3 |- ((K e. PosetNEW /\ ((XJY)JZ) e. B /\ (XJ(YJZ)) e. B) -> ((((XJY)JZ)(le` K)(XJ(YJZ)) /\ (XJ(YJZ))(le` K)((XJY)JZ)) <-> ((XJY)JZ) = (XJ(YJZ))))
18	2, 10, 15, 17	syl111anc 1100	. 2 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> ((((XJY)JZ)(le` K)(XJ(YJZ)) /\ (XJ(YJZ))(le` K)((XJY)JZ)) <-> ((XJY)JZ) = (XJ(YJZ))))
19	4, 16, 5	latjle12 16863	. . . 4 |- ((K e. LatNEW /\ ((XJY) e. B /\ Z e. B /\ (XJ(YJZ)) e. B)) -> (((XJY)(le` K)(XJ(YJZ)) /\ Z(le` K)(XJ(YJZ))) <-> ((XJY)JZ)(le` K)(XJ(YJZ))))
20	3, 7, 8, 15, 19	syl13anc 1102	. . 3 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> (((XJY)(le` K)(XJ(YJZ)) /\ Z(le` K)(XJ(YJZ))) <-> ((XJY)JZ)(le` K)(XJ(YJZ))))
21		simpr2 883	. . . . 5 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> Y e. B)
22	4, 16, 5	latjle12 16863	. . . . 5 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ (XJ(YJZ)) e. B)) -> ((X(le` K)(XJ(YJZ)) /\ Y(le` K)(XJ(YJZ))) <-> (XJY)(le` K)(XJ(YJZ))))
23	3, 11, 21, 15, 22	syl13anc 1102	. . . 4 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> ((X(le` K)(XJ(YJZ)) /\ Y(le` K)(XJ(YJZ))) <-> (XJY)(le` K)(XJ(YJZ))))
24	4, 16, 5	latlej1 16861	. . . . 5 |- ((K e. LatNEW /\ X e. B /\ (YJZ) e. B) -> X(le` K)(XJ(YJZ)))
25	3, 11, 13, 24	syl111anc 1100	. . . 4 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> X(le` K)(XJ(YJZ)))
26	21, 13, 15	3jca 1050	. . . . . 6 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> (Y e. B /\ (YJZ) e. B /\ (XJ(YJZ)) e. B))
27	3, 26	jca 310	. . . . 5 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> (K e. LatNEW /\ (Y e. B /\ (YJZ) e. B /\ (XJ(YJZ)) e. B)))
28	4, 16, 5	latlej1 16861	. . . . . . 7 |- ((K e. LatNEW /\ Y e. B /\ Z e. B) -> Y(le` K)(YJZ))
29	28	3adant3r1 1077	. . . . . 6 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> Y(le` K)(YJZ))
30	4, 16, 5	latlej2 16862	. . . . . . 7 |- ((K e. LatNEW /\ X e. B /\ (YJZ) e. B) -> (YJZ)(le` K)(XJ(YJZ)))
31	3, 11, 13, 30	syl111anc 1100	. . . . . 6 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> (YJZ)(le` K)(XJ(YJZ)))
32	29, 31	jca 310	. . . . 5 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> (Y(le` K)(YJZ) /\ (YJZ)(le` K)(XJ(YJZ))))
33	4, 16	lattr 16858	. . . . 5 |- ((K e. LatNEW /\ (Y e. B /\ (YJZ) e. B /\ (XJ(YJZ)) e. B)) -> ((Y(le` K)(YJZ) /\ (YJZ)(le` K)(XJ(YJZ))) -> Y(le` K)(XJ(YJZ))))
34	27, 32, 33	sylc 83	. . . 4 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> Y(le` K)(XJ(YJZ)))
35	23, 25, 34	mpbi2and 801	. . 3 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> (XJY)(le` K)(XJ(YJZ)))
36	8, 13, 15	3jca 1050	. . . . 5 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> (Z e. B /\ (YJZ) e. B /\ (XJ(YJZ)) e. B))
37	3, 36	jca 310	. . . 4 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> (K e. LatNEW /\ (Z e. B /\ (YJZ) e. B /\ (XJ(YJZ)) e. B)))
38	4, 16, 5	latlej2 16862	. . . . . 6 |- ((K e. LatNEW /\ Y e. B /\ Z e. B) -> Z(le` K)(YJZ))
39	38	3adant3r1 1077	. . . . 5 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> Z(le` K)(YJZ))
40	39, 31	jca 310	. . . 4 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> (Z(le` K)(YJZ) /\ (YJZ)(le` K)(XJ(YJZ))))
41	4, 16	lattr 16858	. . . 4 |- ((K e. LatNEW /\ (Z e. B /\ (YJZ) e. B /\ (XJ(YJZ)) e. B)) -> ((Z(le` K)(YJZ) /\ (YJZ)(le` K)(XJ(YJZ))) -> Z(le` K)(XJ(YJZ))))
42	37, 40, 41	sylc 83	. . 3 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> Z(le` K)(XJ(YJZ)))
43	20, 35, 42	mpbi2and 801	. 2 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> ((XJY)JZ)(le` K)(XJ(YJZ)))
44	4, 16, 5	latjle12 16863	. . . 4 |- ((K e. LatNEW /\ (X e. B /\ (YJZ) e. B /\ ((XJY)JZ) e. B)) -> ((X(le` K)((XJY)JZ) /\ (YJZ)(le` K)((XJY)JZ)) <-> (XJ(YJZ))(le` K)((XJY)JZ)))
45	3, 11, 13, 10, 44	syl13anc 1102	. . 3 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> ((X(le` K)((XJY)JZ) /\ (YJZ)(le` K)((XJY)JZ)) <-> (XJ(YJZ))(le` K)((XJY)JZ)))
46	11, 7, 10	3jca 1050	. . . . 5 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> (X e. B /\ (XJY) e. B /\ ((XJY)JZ) e. B))
47	3, 46	jca 310	. . . 4 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> (K e. LatNEW /\ (X e. B /\ (XJY) e. B /\ ((XJY)JZ) e. B)))
48	4, 16, 5	latlej1 16861	. . . . . 6 |- ((K e. LatNEW /\ X e. B /\ Y e. B) -> X(le` K)(XJY))
49	48	3adant3r3 1079	. . . . 5 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> X(le` K)(XJY))
50	4, 16, 5	latlej1 16861	. . . . . 6 |- ((K e. LatNEW /\ (XJY) e. B /\ Z e. B) -> (XJY)(le` K)((XJY)JZ))
51	3, 7, 8, 50	syl111anc 1100	. . . . 5 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> (XJY)(le` K)((XJY)JZ))
52	49, 51	jca 310	. . . 4 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> (X(le` K)(XJY) /\ (XJY)(le` K)((XJY)JZ)))
53	4, 16	lattr 16858	. . . 4 |- ((K e. LatNEW /\ (X e. B /\ (XJY) e. B /\ ((XJY)JZ) e. B)) -> ((X(le` K)(XJY) /\ (XJY)(le` K)((XJY)JZ)) -> X(le` K)((XJY)JZ)))
54	47, 52, 53	sylc 83	. . 3 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> X(le` K)((XJY)JZ))
55	4, 16, 5	latjle12 16863	. . . . 5 |- ((K e. LatNEW /\ (Y e. B /\ Z e. B /\ ((XJY)JZ) e. B)) -> ((Y(le` K)((XJY)JZ) /\ Z(le` K)((XJY)JZ)) <-> (YJZ)(le` K)((XJY)JZ)))
56	3, 21, 8, 10, 55	syl13anc 1102	. . . 4 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> ((Y(le` K)((XJY)JZ) /\ Z(le` K)((XJY)JZ)) <-> (YJZ)(le` K)((XJY)JZ)))
57	21, 7, 10	3jca 1050	. . . . . 6 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> (Y e. B /\ (XJY) e. B /\ ((XJY)JZ) e. B))
58	3, 57	jca 310	. . . . 5 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> (K e. LatNEW /\ (Y e. B /\ (XJY) e. B /\ ((XJY)JZ) e. B)))
59	4, 16, 5	latlej2 16862	. . . . . . 7 |- ((K e. LatNEW /\ X e. B /\ Y e. B) -> Y(le` K)(XJY))
60	59	3adant3r3 1079	. . . . . 6 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> Y(le` K)(XJY))
61	60, 51	jca 310	. . . . 5 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> (Y(le` K)(XJY) /\ (XJY)(le` K)((XJY)JZ)))
62	4, 16	lattr 16858	. . . . 5 |- ((K e. LatNEW /\ (Y e. B /\ (XJY) e. B /\ ((XJY)JZ) e. B)) -> ((Y(le` K)(XJY) /\ (XJY)(le` K)((XJY)JZ)) -> Y(le` K)((XJY)JZ)))
63	58, 61, 62	sylc 83	. . . 4 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> Y(le` K)((XJY)JZ))
64	4, 16, 5	latlej2 16862	. . . . 5 |- ((K e. LatNEW /\ (XJY) e. B /\ Z e. B) -> Z(le` K)((XJY)JZ))
65	3, 7, 8, 64	syl111anc 1100	. . . 4 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> Z(le` K)((XJY)JZ))
66	56, 63, 65	mpbi2and 801	. . 3 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> (YJZ)(le` K)((XJY)JZ))
67	45, 54, 66	mpbi2and 801	. 2 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> (XJ(YJZ))(le` K)((XJY)JZ))
68	18, 43, 67	mpbi2and 801	1 |- ((K e. LatNEW /\ (X e. B /\ Y e. B /\ Z e. B)) -> ((XJY)JZ) = (XJ(YJZ)))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300   class class class wbr 3338  ` cfv 3998  (class class class)co 4884  basecbs 16758  lecple 16759  PosetNEWcpo 16760  joincjn 16766  LatNEWclat 16834

This theorem is referenced by:  latj23 16887  olmass 16954  cvrexchlem 17059  cvrat3 17075

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-tru 1262  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-mpt2 5007  df-iota 5089  df-er 5318  df-en 5427  df-dom 5428  df-sdom 5429  df-undef 5556  df-riota 5560  df-struct 16708  df-poset 16772  df-lub 16799  df-join 16801  df-lat 16847

Copyright terms: Public domain