Theorem dibintclN 31650

Description: The intersection of partial isomorphism B closed subspaces is a closed subspace. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.)

Hypotheses

Ref	Expression
dibintcl.h	|- H = ( LHyp ` K )
dibintcl.i	|- I = ( ( DIsoB ` K ) ` W )

Assertion

Ref	Expression
dibintclN	|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> |^| S e. ran I )

Proof of Theorem dibintclN

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dibintcl.h	. . . . . . . 8 |- H = ( LHyp ` K )
2		dibintcl.i	. . . . . . . 8 |- I = ( ( DIsoB ` K ) ` W )
3	1, 2	dibf11N 31644	. . . . . . 7 |- ( ( K e. HL /\ W e. H ) -> I : dom I -1-1-onto-> ran I )
4	3	adantr 452	. . . . . 6 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> I : dom I -1-1-onto-> ran I )
5		f1ofn 5634	. . . . . 6 |- ( I : dom I -1-1-onto-> ran I -> I Fn dom I )
6	4, 5	syl 16	. . . . 5 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> I Fn dom I )
7		cnvimass 5183	. . . . 5 |- ( `' I " S ) C_ dom I
8		fnssres 5517	. . . . 5 |- ( ( I Fn dom I /\ ( `' I " S ) C_ dom I ) -> ( I |` ( `' I " S ) ) Fn ( `' I " S ) )
9	6, 7, 8	sylancl 644	. . . 4 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ( I |` ( `' I " S ) ) Fn ( `' I " S ) )
10		fniinfv 5744	. . . 4 |- ( ( I |` ( `' I " S ) ) Fn ( `' I " S ) -> |^|_ y e. ( `' I " S ) ( ( I |` ( `' I " S ) ) ` y ) = |^| ran ( I |` ( `' I " S ) ) )
11	9, 10	syl 16	. . 3 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> |^|_ y e. ( `' I " S ) ( ( I |` ( `' I " S ) ) ` y ) = |^| ran ( I |` ( `' I " S ) ) )
12		df-ima 4850	. . . . 5 |- ( I " ( `' I " S ) ) = ran ( I |` ( `' I " S ) )
13		f1ofo 5640	. . . . . . . 8 |- ( I : dom I -1-1-onto-> ran I -> I : dom I -onto-> ran I )
14	3, 13	syl 16	. . . . . . 7 |- ( ( K e. HL /\ W e. H ) -> I : dom I -onto-> ran I )
15	14	adantr 452	. . . . . 6 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> I : dom I -onto-> ran I )
16		simprl 733	. . . . . 6 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> S C_ ran I )
17		foimacnv 5651	. . . . . 6 |- ( ( I : dom I -onto-> ran I /\ S C_ ran I ) -> ( I " ( `' I " S ) ) = S )
18	15, 16, 17	syl2anc 643	. . . . 5 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ( I " ( `' I " S ) ) = S )
19	12, 18	syl5eqr 2450	. . . 4 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ran ( I |` ( `' I " S ) ) = S )
20	19	inteqd 4015	. . 3 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> |^| ran ( I |` ( `' I " S ) ) = |^| S )
21	11, 20	eqtrd 2436	. 2 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> |^|_ y e. ( `' I " S ) ( ( I |` ( `' I " S ) ) ` y ) = |^| S )
22		simpl 444	. . . . 5 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ( K e. HL /\ W e. H ) )
23	7	a1i 11	. . . . 5 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ( `' I " S ) C_ dom I )
24		simprr 734	. . . . . . 7 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> S =/= (/) )
25		n0 3597	. . . . . . 7 |- ( S =/= (/) <-> E. y y e. S )
26	24, 25	sylib 189	. . . . . 6 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> E. y y e. S )
27	16	sselda 3308	. . . . . . . 8 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) /\ y e. S ) -> y e. ran I )
28	3	ad2antrr 707	. . . . . . . . . 10 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) /\ y e. S ) -> I : dom I -1-1-onto-> ran I )
29	28, 5	syl 16	. . . . . . . . 9 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) /\ y e. S ) -> I Fn dom I )
30		fvelrnb 5733	. . . . . . . . 9 |- ( I Fn dom I -> ( y e. ran I <-> E. x e. dom I ( I ` x ) = y ) )
31	29, 30	syl 16	. . . . . . . 8 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) /\ y e. S ) -> ( y e. ran I <-> E. x e. dom I ( I ` x ) = y ) )
32	27, 31	mpbid 202	. . . . . . 7 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) /\ y e. S ) -> E. x e. dom I ( I ` x ) = y )
33		f1ofun 5635	. . . . . . . . . . . . . . . 16 |- ( I : dom I -1-1-onto-> ran I -> Fun I )
34	3, 33	syl 16	. . . . . . . . . . . . . . 15 |- ( ( K e. HL /\ W e. H ) -> Fun I )
35	34	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> Fun I )
36		fvimacnv 5804	. . . . . . . . . . . . . 14 |- ( ( Fun I /\ x e. dom I ) -> ( ( I ` x ) e. S <-> x e. ( `' I " S ) ) )
37	35, 36	sylan 458	. . . . . . . . . . . . 13 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) /\ x e. dom I ) -> ( ( I ` x ) e. S <-> x e. ( `' I " S ) ) )
38		ne0i 3594	. . . . . . . . . . . . 13 |- ( x e. ( `' I " S ) -> ( `' I " S ) =/= (/) )
39	37, 38	syl6bi 220	. . . . . . . . . . . 12 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) /\ x e. dom I ) -> ( ( I ` x ) e. S -> ( `' I " S ) =/= (/) ) )
40	39	ex 424	. . . . . . . . . . 11 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ( x e. dom I -> ( ( I ` x ) e. S -> ( `' I " S ) =/= (/) ) ) )
41		eleq1 2464	. . . . . . . . . . . . 13 |- ( ( I ` x ) = y -> ( ( I ` x ) e. S <-> y e. S ) )
42	41	biimprd 215	. . . . . . . . . . . 12 |- ( ( I ` x ) = y -> ( y e. S -> ( I ` x ) e. S ) )
43	42	imim1d 71	. . . . . . . . . . 11 |- ( ( I ` x ) = y -> ( ( ( I ` x ) e. S -> ( `' I " S ) =/= (/) ) -> ( y e. S -> ( `' I " S ) =/= (/) ) ) )
44	40, 43	syl9 68	. . . . . . . . . 10 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ( ( I ` x ) = y -> ( x e. dom I -> ( y e. S -> ( `' I " S ) =/= (/) ) ) ) )
45	44	com24 83	. . . . . . . . 9 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ( y e. S -> ( x e. dom I -> ( ( I ` x ) = y -> ( `' I " S ) =/= (/) ) ) ) )
46	45	imp 419	. . . . . . . 8 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) /\ y e. S ) -> ( x e. dom I -> ( ( I ` x ) = y -> ( `' I " S ) =/= (/) ) ) )
47	46	rexlimdv 2789	. . . . . . 7 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) /\ y e. S ) -> ( E. x e. dom I ( I ` x ) = y -> ( `' I " S ) =/= (/) ) )
48	32, 47	mpd 15	. . . . . 6 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) /\ y e. S ) -> ( `' I " S ) =/= (/) )
49	26, 48	exlimddv 1645	. . . . 5 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ( `' I " S ) =/= (/) )
50		eqid 2404	. . . . . 6 |- ( glb ` K ) = ( glb ` K )
51	50, 1, 2	dibglbN 31649	. . . . 5 |- ( ( ( K e. HL /\ W e. H ) /\ ( ( `' I " S ) C_ dom I /\ ( `' I " S ) =/= (/) ) ) -> ( I ` ( ( glb ` K ) ` ( `' I " S ) ) ) = |^|_ y e. ( `' I " S ) ( I ` y ) )
52	22, 23, 49, 51	syl12anc 1182	. . . 4 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ( I ` ( ( glb ` K ) ` ( `' I " S ) ) ) = |^|_ y e. ( `' I " S ) ( I ` y ) )
53		fvres 5704	. . . . 5 |- ( y e. ( `' I " S ) -> ( ( I |` ( `' I " S ) ) ` y ) = ( I ` y ) )
54	53	iineq2i 4072	. . . 4 |- |^|_ y e. ( `' I " S ) ( ( I |` ( `' I " S ) ) ` y ) = |^|_ y e. ( `' I " S ) ( I ` y )
55	52, 54	syl6eqr 2454	. . 3 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ( I ` ( ( glb ` K ) ` ( `' I " S ) ) ) = |^|_ y e. ( `' I " S ) ( ( I |` ( `' I " S ) ) ` y ) )
56		hlclat 29841	. . . . . . 7 |- ( K e. HL -> K e. CLat )
57	56	ad2antrr 707	. . . . . 6 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> K e. CLat )
58		eqid 2404	. . . . . . . . . 10 |- ( Base ` K ) = ( Base ` K )
59		eqid 2404	. . . . . . . . . 10 |- ( le ` K ) = ( le ` K )
60	58, 59, 1, 2	dibdmN 31640	. . . . . . . . 9 |- ( ( K e. HL /\ W e. H ) -> dom I = { x e. ( Base ` K ) | x ( le ` K ) W } )
61		ssrab2 3388	. . . . . . . . 9 |- { x e. ( Base ` K ) | x ( le ` K ) W } C_ ( Base ` K )
62	60, 61	syl6eqss 3358	. . . . . . . 8 |- ( ( K e. HL /\ W e. H ) -> dom I C_ ( Base ` K ) )
63	62	adantr 452	. . . . . . 7 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> dom I C_ ( Base ` K ) )
64	7, 63	syl5ss 3319	. . . . . 6 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ( `' I " S ) C_ ( Base ` K ) )
65	58, 50	clatglbcl 14496	. . . . . 6 |- ( ( K e. CLat /\ ( `' I " S ) C_ ( Base ` K ) ) -> ( ( glb ` K ) ` ( `' I " S ) ) e. ( Base ` K ) )
66	57, 64, 65	syl2anc 643	. . . . 5 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ( ( glb ` K ) ` ( `' I " S ) ) e. ( Base ` K ) )
67		n0 3597	. . . . . . 7 |- ( ( `' I " S ) =/= (/) <-> E. y y e. ( `' I " S ) )
68	49, 67	sylib 189	. . . . . 6 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> E. y y e. ( `' I " S ) )
69		hllat 29846	. . . . . . . 8 |- ( K e. HL -> K e. Lat )
70	69	ad3antrrr 711	. . . . . . 7 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) /\ y e. ( `' I " S ) ) -> K e. Lat )
71	66	adantr 452	. . . . . . 7 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) /\ y e. ( `' I " S ) ) -> ( ( glb ` K ) ` ( `' I " S ) ) e. ( Base ` K ) )
72	64	sselda 3308	. . . . . . 7 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) /\ y e. ( `' I " S ) ) -> y e. ( Base ` K ) )
73	58, 1	lhpbase 30480	. . . . . . . 8 |- ( W e. H -> W e. ( Base ` K ) )
74	73	ad3antlr 712	. . . . . . 7 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) /\ y e. ( `' I " S ) ) -> W e. ( Base ` K ) )
75	56	ad3antrrr 711	. . . . . . . 8 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) /\ y e. ( `' I " S ) ) -> K e. CLat )
76	60	adantr 452	. . . . . . . . . . 11 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> dom I = { x e. ( Base ` K ) | x ( le ` K ) W } )
77	7, 76	syl5sseq 3356	. . . . . . . . . 10 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ( `' I " S ) C_ { x e. ( Base ` K ) | x ( le ` K ) W } )
78	77, 61	syl6ss 3320	. . . . . . . . 9 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ( `' I " S ) C_ ( Base ` K ) )
79	78	adantr 452	. . . . . . . 8 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) /\ y e. ( `' I " S ) ) -> ( `' I " S ) C_ ( Base ` K ) )
80		simpr 448	. . . . . . . 8 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) /\ y e. ( `' I " S ) ) -> y e. ( `' I " S ) )
81	58, 59, 50	clatglble 14507	. . . . . . . 8 |- ( ( K e. CLat /\ ( `' I " S ) C_ ( Base ` K ) /\ y e. ( `' I " S ) ) -> ( ( glb ` K ) ` ( `' I " S ) ) ( le ` K ) y )
82	75, 79, 80, 81	syl3anc 1184	. . . . . . 7 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) /\ y e. ( `' I " S ) ) -> ( ( glb ` K ) ` ( `' I " S ) ) ( le ` K ) y )
83	7	sseli 3304	. . . . . . . . . 10 |- ( y e. ( `' I " S ) -> y e. dom I )
84	83	adantl 453	. . . . . . . . 9 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) /\ y e. ( `' I " S ) ) -> y e. dom I )
85	58, 59, 1, 2	dibeldmN 31641	. . . . . . . . . 10 |- ( ( K e. HL /\ W e. H ) -> ( y e. dom I <-> ( y e. ( Base ` K ) /\ y ( le ` K ) W ) ) )
86	85	ad2antrr 707	. . . . . . . . 9 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) /\ y e. ( `' I " S ) ) -> ( y e. dom I <-> ( y e. ( Base ` K ) /\ y ( le ` K ) W ) ) )
87	84, 86	mpbid 202	. . . . . . . 8 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) /\ y e. ( `' I " S ) ) -> ( y e. ( Base ` K ) /\ y ( le ` K ) W ) )
88	87	simprd 450	. . . . . . 7 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) /\ y e. ( `' I " S ) ) -> y ( le ` K ) W )
89	58, 59, 70, 71, 72, 74, 82, 88	lattrd 14442	. . . . . 6 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) /\ y e. ( `' I " S ) ) -> ( ( glb ` K ) ` ( `' I " S ) ) ( le ` K ) W )
90	68, 89	exlimddv 1645	. . . . 5 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ( ( glb ` K ) ` ( `' I " S ) ) ( le ` K ) W )
91	58, 59, 1, 2	dibeldmN 31641	. . . . . 6 |- ( ( K e. HL /\ W e. H ) -> ( ( ( glb ` K ) ` ( `' I " S ) ) e. dom I <-> ( ( ( glb ` K ) ` ( `' I " S ) ) e. ( Base ` K ) /\ ( ( glb ` K ) ` ( `' I " S ) ) ( le ` K ) W ) ) )
92	91	adantr 452	. . . . 5 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ( ( ( glb ` K ) ` ( `' I " S ) ) e. dom I <-> ( ( ( glb ` K ) ` ( `' I " S ) ) e. ( Base ` K ) /\ ( ( glb ` K ) ` ( `' I " S ) ) ( le ` K ) W ) ) )
93	66, 90, 92	mpbir2and 889	. . . 4 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ( ( glb ` K ) ` ( `' I " S ) ) e. dom I )
94	1, 2	dibclN 31645	. . . 4 |- ( ( ( K e. HL /\ W e. H ) /\ ( ( glb ` K ) ` ( `' I " S ) ) e. dom I ) -> ( I ` ( ( glb ` K ) ` ( `' I " S ) ) ) e. ran I )
95	93, 94	syldan 457	. . 3 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> ( I ` ( ( glb ` K ) ` ( `' I " S ) ) ) e. ran I )
96	55, 95	eqeltrrd 2479	. 2 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> |^|_ y e. ( `' I " S ) ( ( I |` ( `' I " S ) ) ` y ) e. ran I )
97	21, 96	eqeltrrd 2479	1 |- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ ran I /\ S =/= (/) ) ) -> |^| S e. ran I )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   E.wex 1547   = wceq 1649   e. wcel 1721   =/= wne 2567   E.wrex 2667   {crab 2670   C_ wss 3280   (/)c0 3588   |^|cint 4010   |^|_ciin 4054   class class class wbr 4172   `'ccnv 4836   dom cdm 4837   ran crn 4838   |` cres 4839   "cima 4840   Fun wfun 5407   Fn wfn 5408   -onto->wfo 5411   -1-1-onto->wf1o 5412   ` cfv 5413   Basecbs 13424   lecple 13491   glbcglb 14355   Latclat 14429   CLatccla 14491   HLchlt 29833   LHypclh 30466   DIsoBcdib 31621

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-iin 4056  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-undef 6502  df-riota 6508  df-map 6979  df-poset 14358  df-plt 14370  df-lub 14386  df-glb 14387  df-join 14388  df-meet 14389  df-p0 14423  df-p1 14424  df-lat 14430  df-clat 14492  df-oposet 29659  df-ol 29661  df-oml 29662  df-covers 29749  df-ats 29750  df-atl 29781  df-cvlat 29805  df-hlat 29834  df-llines 29980  df-lplanes 29981  df-lvols 29982  df-lines 29983  df-psubsp 29985  df-pmap 29986  df-padd 30278  df-lhyp 30470  df-laut 30471  df-ldil 30586  df-ltrn 30587  df-trl 30641  df-disoa 31512  df-dib 31622