Theorem ishlat 17018

Description: The predicate "is a Hilbert lattice," which is a complete, atomic lattice satisfying the superposition principle and minimum height.

Hypotheses

Ref	Expression
ishlat.b	|- B = (base` K)
ishlat.l	|- L = (le` K)
ishlat.s	|- S = (lt` K)
ishlat.j	|- J = (join` K)
ishlat.z	|- Z = (0.` K)
ishlat.u	|- U = (1.` K)
ishlat.a	|- A = (AtomsNEW` K)

Assertion

Ref	Expression
ishlat	|- (K e. HL <-> ((K e. OML /\ K e. CLat /\ K e. AtLat) /\ (A.x e. A A.y e. A ((x =/= y -> E.z e. A (z =/= x /\ z =/= y /\ zL(xJy))) /\ A.z e. B ((-. xLz /\ xL(zJy)) -> yL(zJx))) /\ E.x e. B E.y e. B E.z e. B ((ZSx /\ xSy) /\ (ySz /\ zSU)))))

Distinct variable groups:   x,y,z,A   x,B,y,z   x,K,y,z

Proof of Theorem ishlat

Step	Hyp	Ref	Expression
1		fveq2 4681	. . . . . 6 |- (l = K -> (AtomsNEW` l) = (AtomsNEW` K))
2		ishlat.a	. . . . . 6 |- A = (AtomsNEW` K)
3	1, 2	syl6eqr 1946	. . . . 5 |- (l = K -> (AtomsNEW` l) = A)
4		fveq2 4681	. . . . . . . . . . . . 13 |- (l = K -> (le` l) = (le` K))
5		ishlat.l	. . . . . . . . . . . . 13 |- L = (le` K)
6	4, 5	syl6eqr 1946	. . . . . . . . . . . 12 |- (l = K -> (le` l) = L)
7	6	breqd 3349	. . . . . . . . . . 11 |- (l = K -> (z(le` l)(x(join` l)y) <-> zL(x(join` l)y)))
8		fveq2 4681	. . . . . . . . . . . . . 14 |- (l = K -> (join` l) = (join` K))
9		ishlat.j	. . . . . . . . . . . . . 14 |- J = (join` K)
10	8, 9	syl6eqr 1946	. . . . . . . . . . . . 13 |- (l = K -> (join` l) = J)
11	10	opreqd 4899	. . . . . . . . . . . 12 |- (l = K -> (x(join` l)y) = (xJy))
12	11	breq2d 3350	. . . . . . . . . . 11 |- (l = K -> (zL(x(join` l)y) <-> zL(xJy)))
13	7, 12	bitrd 587	. . . . . . . . . 10 |- (l = K -> (z(le` l)(x(join` l)y) <-> zL(xJy)))
14	13	3anbi3d 1174	. . . . . . . . 9 |- (l = K -> ((z =/= x /\ z =/= y /\ z(le` l)(x(join` l)y)) <-> (z =/= x /\ z =/= y /\ zL(xJy))))
15	3, 14	rexeqbidv 2275	. . . . . . . 8 |- (l = K -> (E.z e. (AtomsNEW` l)(z =/= x /\ z =/= y /\ z(le` l)(x(join` l)y)) <-> E.z e. A (z =/= x /\ z =/= y /\ zL(xJy))))
16	15	imbi2d 674	. . . . . . 7 |- (l = K -> ((x =/= y -> E.z e. (AtomsNEW` l)(z =/= x /\ z =/= y /\ z(le` l)(x(join` l)y))) <-> (x =/= y -> E.z e. A (z =/= x /\ z =/= y /\ zL(xJy)))))
17		fveq2 4681	. . . . . . . . 9 |- (l = K -> (base` l) = (base` K))
18		ishlat.b	. . . . . . . . 9 |- B = (base` K)
19	17, 18	syl6eqr 1946	. . . . . . . 8 |- (l = K -> (base` l) = B)
20	6	breqd 3349	. . . . . . . . . . 11 |- (l = K -> (x(le` l)z <-> xLz))
21	20	notbid 673	. . . . . . . . . 10 |- (l = K -> (-. x(le` l)z <-> -. xLz))
22	6	breqd 3349	. . . . . . . . . . 11 |- (l = K -> (x(le` l)(z(join` l)y) <-> xL(z(join` l)y)))
23	10	opreqd 4899	. . . . . . . . . . . 12 |- (l = K -> (z(join` l)y) = (zJy))
24	23	breq2d 3350	. . . . . . . . . . 11 |- (l = K -> (xL(z(join` l)y) <-> xL(zJy)))
25	22, 24	bitrd 587	. . . . . . . . . 10 |- (l = K -> (x(le` l)(z(join` l)y) <-> xL(zJy)))
26	21, 25	anbi12d 690	. . . . . . . . 9 |- (l = K -> ((-. x(le` l)z /\ x(le` l)(z(join` l)y)) <-> (-. xLz /\ xL(zJy))))
27	6	breqd 3349	. . . . . . . . . 10 |- (l = K -> (y(le` l)(z(join` l)x) <-> yL(z(join` l)x)))
28	10	opreqd 4899	. . . . . . . . . . 11 |- (l = K -> (z(join` l)x) = (zJx))
29	28	breq2d 3350	. . . . . . . . . 10 |- (l = K -> (yL(z(join` l)x) <-> yL(zJx)))
30	27, 29	bitrd 587	. . . . . . . . 9 |- (l = K -> (y(le` l)(z(join` l)x) <-> yL(zJx)))
31	26, 30	imbi12d 688	. . . . . . . 8 |- (l = K -> (((-. x(le` l)z /\ x(le` l)(z(join` l)y)) -> y(le` l)(z(join` l)x)) <-> ((-. xLz /\ xL(zJy)) -> yL(zJx))))
32	19, 31	raleqbidv 2274	. . . . . . 7 |- (l = K -> (A.z e. (base` l)((-. x(le` l)z /\ x(le` l)(z(join` l)y)) -> y(le` l)(z(join` l)x)) <-> A.z e. B ((-. xLz /\ xL(zJy)) -> yL(zJx))))
33	16, 32	anbi12d 690	. . . . . 6 |- (l = K -> (((x =/= y -> E.z e. (AtomsNEW` l)(z =/= x /\ z =/= y /\ z(le` l)(x(join` l)y))) /\ A.z e. (base` l)((-. x(le` l)z /\ x(le` l)(z(join` l)y)) -> y(le` l)(z(join` l)x))) <-> ((x =/= y -> E.z e. A (z =/= x /\ z =/= y /\ zL(xJy))) /\ A.z e. B ((-. xLz /\ xL(zJy)) -> yL(zJx)))))
34	3, 33	raleqbidv 2274	. . . . 5 |- (l = K -> (A.y e. (AtomsNEW` l)((x =/= y -> E.z e. (AtomsNEW` l)(z =/= x /\ z =/= y /\ z(le` l)(x(join` l)y))) /\ A.z e. (base` l)((-. x(le` l)z /\ x(le` l)(z(join` l)y)) -> y(le` l)(z(join` l)x))) <-> A.y e. A ((x =/= y -> E.z e. A (z =/= x /\ z =/= y /\ zL(xJy))) /\ A.z e. B ((-. xLz /\ xL(zJy)) -> yL(zJx)))))
35	3, 34	raleqbidv 2274	. . . 4 |- (l = K -> (A.x e. (AtomsNEW` l)A.y e. (AtomsNEW` l)((x =/= y -> E.z e. (AtomsNEW` l)(z =/= x /\ z =/= y /\ z(le` l)(x(join` l)y))) /\ A.z e. (base` l)((-. x(le` l)z /\ x(le` l)(z(join` l)y)) -> y(le` l)(z(join` l)x))) <-> A.x e. A A.y e. A ((x =/= y -> E.z e. A (z =/= x /\ z =/= y /\ zL(xJy))) /\ A.z e. B ((-. xLz /\ xL(zJy)) -> yL(zJx)))))
36		fveq2 4681	. . . . . . . . . . . 12 |- (l = K -> (lt` l) = (lt` K))
37		ishlat.s	. . . . . . . . . . . 12 |- S = (lt` K)
38	36, 37	syl6eqr 1946	. . . . . . . . . . 11 |- (l = K -> (lt` l) = S)
39	38	breqd 3349	. . . . . . . . . 10 |- (l = K -> ((0.` l)(lt` l)x <-> (0.` l)Sx))
40		fveq2 4681	. . . . . . . . . . . 12 |- (l = K -> (0.` l) = (0.` K))
41		ishlat.z	. . . . . . . . . . . 12 |- Z = (0.` K)
42	40, 41	syl6eqr 1946	. . . . . . . . . . 11 |- (l = K -> (0.` l) = Z)
43	42	breq1d 3348	. . . . . . . . . 10 |- (l = K -> ((0.` l)Sx <-> ZSx))
44	39, 43	bitrd 587	. . . . . . . . 9 |- (l = K -> ((0.` l)(lt` l)x <-> ZSx))
45	38	breqd 3349	. . . . . . . . 9 |- (l = K -> (x(lt` l)y <-> xSy))
46	44, 45	anbi12d 690	. . . . . . . 8 |- (l = K -> (((0.` l)(lt` l)x /\ x(lt` l)y) <-> (ZSx /\ xSy)))
47	38	breqd 3349	. . . . . . . . 9 |- (l = K -> (y(lt` l)z <-> ySz))
48	38	breqd 3349	. . . . . . . . . 10 |- (l = K -> (z(lt` l)(1.` l) <-> zS(1.` l)))
49		fveq2 4681	. . . . . . . . . . . 12 |- (l = K -> (1.` l) = (1.` K))
50		ishlat.u	. . . . . . . . . . . 12 |- U = (1.` K)
51	49, 50	syl6eqr 1946	. . . . . . . . . . 11 |- (l = K -> (1.` l) = U)
52	51	breq2d 3350	. . . . . . . . . 10 |- (l = K -> (zS(1.` l) <-> zSU))
53	48, 52	bitrd 587	. . . . . . . . 9 |- (l = K -> (z(lt` l)(1.` l) <-> zSU))
54	47, 53	anbi12d 690	. . . . . . . 8 |- (l = K -> ((y(lt` l)z /\ z(lt` l)(1.` l)) <-> (ySz /\ zSU)))
55	46, 54	anbi12d 690	. . . . . . 7 |- (l = K -> ((((0.` l)(lt` l)x /\ x(lt` l)y) /\ (y(lt` l)z /\ z(lt` l)(1.` l))) <-> ((ZSx /\ xSy) /\ (ySz /\ zSU))))
56	19, 55	rexeqbidv 2275	. . . . . 6 |- (l = K -> (E.z e. (base` l)(((0.` l)(lt` l)x /\ x(lt` l)y) /\ (y(lt` l)z /\ z(lt` l)(1.` l))) <-> E.z e. B ((ZSx /\ xSy) /\ (ySz /\ zSU))))
57	19, 56	rexeqbidv 2275	. . . . 5 |- (l = K -> (E.y e. (base` l)E.z e. (base` l)(((0.` l)(lt` l)x /\ x(lt` l)y) /\ (y(lt` l)z /\ z(lt` l)(1.` l))) <-> E.y e. B E.z e. B ((ZSx /\ xSy) /\ (ySz /\ zSU))))
58	19, 57	rexeqbidv 2275	. . . 4 |- (l = K -> (E.x e. (base` l)E.y e. (base` l)E.z e. (base` l)(((0.` l)(lt` l)x /\ x(lt` l)y) /\ (y(lt` l)z /\ z(lt` l)(1.` l))) <-> E.x e. B E.y e. B E.z e. B ((ZSx /\ xSy) /\ (ySz /\ zSU))))
59	35, 58	anbi12d 690	. . 3 |- (l = K -> ((A.x e. (AtomsNEW` l)A.y e. (AtomsNEW` l)((x =/= y -> E.z e. (AtomsNEW` l)(z =/= x /\ z =/= y /\ z(le` l)(x(join` l)y))) /\ A.z e. (base` l)((-. x(le` l)z /\ x(le` l)(z(join` l)y)) -> y(le` l)(z(join` l)x))) /\ E.x e. (base` l)E.y e. (base` l)E.z e. (base` l)(((0.` l)(lt` l)x /\ x(lt` l)y) /\ (y(lt` l)z /\ z(lt` l)(1.` l)))) <-> (A.x e. A A.y e. A ((x =/= y -> E.z e. A (z =/= x /\ z =/= y /\ zL(xJy))) /\ A.z e. B ((-. xLz /\ xL(zJy)) -> yL(zJx))) /\ E.x e. B E.y e. B E.z e. B ((ZSx /\ xSy) /\ (ySz /\ zSU)))))
60		df-hlat 17017	. . 3 |- HL = {l e. ((OML i^i CLat) i^i AtLat) | (A.x e. (AtomsNEW` l)A.y e. (AtomsNEW` l)((x =/= y -> E.z e. (AtomsNEW` l)(z =/= x /\ z =/= y /\ z(le` l)(x(join` l)y))) /\ A.z e. (base` l)((-. x(le` l)z /\ x(le` l)(z(join` l)y)) -> y(le` l)(z(join` l)x))) /\ E.x e. (base` l)E.y e. (base` l)E.z e. (base` l)(((0.` l)(lt` l)x /\ x(lt` l)y) /\ (y(lt` l)z /\ z(lt` l)(1.` l))))}
61	59, 60	elrab2 2416	. 2 |- (K e. HL <-> (K e. ((OML i^i CLat) i^i AtLat) /\ (A.x e. A A.y e. A ((x =/= y -> E.z e. A (z =/= x /\ z =/= y /\ zL(xJy))) /\ A.z e. B ((-. xLz /\ xL(zJy)) -> yL(zJx))) /\ E.x e. B E.y e. B E.z e. B ((ZSx /\ xSy) /\ (ySz /\ zSU)))))
62		elin 2786	. . . . 5 |- (K e. (OML i^i CLat) <-> (K e. OML /\ K e. CLat))
63	62	anbi1i 539	. . . 4 |- ((K e. (OML i^i CLat) /\ K e. AtLat) <-> ((K e. OML /\ K e. CLat) /\ K e. AtLat))
64		elin 2786	. . . 4 |- (K e. ((OML i^i CLat) i^i AtLat) <-> (K e. (OML i^i CLat) /\ K e. AtLat))
65		df-3an 860	. . . 4 |- ((K e. OML /\ K e. CLat /\ K e. AtLat) <-> ((K e. OML /\ K e. CLat) /\ K e. AtLat))
66	63, 64, 65	3bitr4ri 201	. . 3 |- ((K e. OML /\ K e. CLat /\ K e. AtLat) <-> K e. ((OML i^i CLat) i^i AtLat))
67	66	anbi1i 539	. 2 |- (((K e. OML /\ K e. CLat /\ K e. AtLat) /\ (A.x e. A A.y e. A ((x =/= y -> E.z e. A (z =/= x /\ z =/= y /\ zL(xJy))) /\ A.z e. B ((-. xLz /\ xL(zJy)) -> yL(zJx))) /\ E.x e. B E.y e. B E.z e. B ((ZSx /\ xSy) /\ (ySz /\ zSU)))) <-> (K e. ((OML i^i CLat) i^i AtLat) /\ (A.x e. A A.y e. A ((x =/= y -> E.z e. A (z =/= x /\ z =/= y /\ zL(xJy))) /\ A.z e. B ((-. xLz /\ xL(zJy)) -> yL(zJx))) /\ E.x e. B E.y e. B E.z e. B ((ZSx /\ xSy) /\ (ySz /\ zSU)))))
68	61, 67	bitr4i 193	1 |- (K e. HL <-> ((K e. OML /\ K e. CLat /\ K e. AtLat) /\ (A.x e. A A.y e. A ((x =/= y -> E.z e. A (z =/= x /\ z =/= y /\ zL(xJy))) /\ A.z e. B ((-. xLz /\ xL(zJy)) -> yL(zJx))) /\ E.x e. B E.y e. B E.z e. B ((ZSx /\ xSy) /\ (ySz /\ zSU)))))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300   =/= wne 2017  A.wral 2105  E.wrex 2106   i^i cin 2592   class class class wbr 3338  ` cfv 3998  (class class class)co 4884  basecbs 16758  lecple 16759  ltcplt 16761  joincjn 16766  0.cp0 16832  1.cp1 16833  CLatccla 16835  OMLcoml 16840  AtomsNEWcatm 16981  AtLatcal 16982  HLchlt 16983

This theorem is referenced by:  ishlati 17019  hllem1 17020  hlsuprexch 17033  hlhght4 17037

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-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-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  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-rab 2112  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-xp 4000  df-cnv 4002  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fv 4014  df-opr 4886  df-hlat 17017

Copyright terms: Public domain