dihglbcpreN - Mathbox for Norm Megill

	Mathbox for Norm Megill	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dihglbcpreN		Structured version Unicode version

Theorem dihglbcpreN 34837

Description: Isomorphism H of a lattice glb when the glb is not under the fiducial hyperplane

. (Contributed by NM, 20-Mar-2014.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
dihglbc.b
dihglbc.g
dihglbc.h
dihglbc.i
dihglbc.l
dihglbcpre.j	$.\/$
dihglbcpre.m	$./\$
dihglbcpre.a
dihglbcpre.p
dihglbcpre.t
dihglbcpre.r
dihglbcpre.e
dihglbcpre.f

**Assertion**
Ref	Expression
dihglbcpreN	$/\$ $/\$ $/\$ $/\$

Distinct variable groups:

, $./\$

, $.\/$

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

) $.\/$ (

) $./\$ (

)

Proof of Theorem dihglbcpreN Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dihglbc.h	. . . 4
2		dihglbc.i	. . . 4
3	1, 2	dihvalrel 34816	. . 3 $/\$
4	3	3ad2ant1 1026	. 2 $/\$ $/\$ $/\$ $/\$
5		simp2r 1032	. . . . . 6 $/\$ $/\$ $/\$ $/\$
6		n0 3771	. . . . . 6
7	5, 6	sylib 199	. . . . 5 $/\$ $/\$ $/\$ $/\$
8		simpr 462	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
9		simpl1 1008	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
10	1, 2	dihvalrel 34816	. . . . . . . . 9 $/\$
11	9, 10	syl 17	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
12	8, 11	jca 534	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
13	12	ex 435	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
14	13	eximdv 1758	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
15	7, 14	mpd 15	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
16		df-rex 2777	. . . 4 $/\$
17	15, 16	sylibr 215	. . 3 $/\$ $/\$ $/\$ $/\$
18		reliin 4974	. . 3
19	17, 18	syl 17	. 2 $/\$ $/\$ $/\$ $/\$
20		id 22	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
21		simp1 1005	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
22		simp1l 1029	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
23		hlclat 32893	. . . . . . 7
24	22, 23	syl 17	. . . . . 6 $/\$ $/\$ $/\$ $/\$
25		simp2l 1031	. . . . . 6 $/\$ $/\$ $/\$ $/\$
26		dihglbc.b	. . . . . . 7
27		dihglbc.g	. . . . . . 7
28	26, 27	clatglbcl 16359	. . . . . 6 $/\$
29	24, 25, 28	syl2anc 665	. . . . 5 $/\$ $/\$ $/\$ $/\$
30		simp3 1007	. . . . 5 $/\$ $/\$ $/\$ $/\$
31		dihglbc.l	. . . . . 6
32		dihglbcpre.j	. . . . . 6 $.\/$
33		dihglbcpre.m	. . . . . 6 $./\$
34		dihglbcpre.a	. . . . . 6
35	26, 31, 32, 33, 34, 1	lhpmcvr2 33558	. . . . 5 $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
36	21, 29, 30, 35	syl12anc 1262	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
37		simpl1 1008	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
38	29	adantr 466	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
39		simpl3 1010	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
40		simpr 462	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$
41		dihglbcpre.p	. . . . . . . . . 10
42		dihglbcpre.t	. . . . . . . . . 10
43		dihglbcpre.r	. . . . . . . . . 10
44		dihglbcpre.e	. . . . . . . . . 10
45		dihglbcpre.f	. . . . . . . . . 10
46		vex 3083	. . . . . . . . . 10
47		vex 3083	. . . . . . . . . 10
48	26, 31, 32, 33, 34, 1, 41, 42, 43, 44, 2, 45, 46, 47	dihopelvalc 34786	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
49	37, 38, 39, 40, 48	syl121anc 1269	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
50		simpl2r 1059	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
51		r19.28zv 3894	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
52	50, 51	syl 17	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
53		simp11 1035	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
54		simp12l 1118	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
55		simp3 1007	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
56	54, 55	sseldd 3465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
57		simp13 1037	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
58		simp11l 1116	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
59	58, 23	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
60	26, 31, 27	clatglble 16370	. . . . . . . . . . . . . . . 16 $/\$ $/\$
61	59, 54, 55, 60	syl3anc 1264	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
62		hllat 32898	. . . . . . . . . . . . . . . . 17
63	58, 62	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
64	29	3ad2ant1 1026	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
65		simp11r 1117	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
66	26, 1	lhpbase 33532	. . . . . . . . . . . . . . . . 17
67	65, 66	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
68	26, 31	lattr 16301	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
69	63, 64, 56, 67, 68	syl13anc 1266	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
70	61, 69	mpand 679	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
71	57, 70	mtod 180	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
72		simp2l 1031	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
73		simp2ll 1072	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
74	26, 34	atbase 32824	. . . . . . . . . . . . . . . . 17
75	73, 74	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
76	26, 33	latmcl 16297	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $./\$
77	63, 64, 67, 76	syl3anc 1264	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$
78	26, 31, 32	latlej1 16305	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $./\$ $.\/$ $./\$
79	63, 75, 77, 78	syl3anc 1264	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
80		simp2r 1032	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
81	79, 80	breqtrd 4448	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
82	26, 31, 63, 75, 64, 56, 81, 61	lattrd 16303	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
83	26, 31, 32, 33, 34	atmod3i1 33398	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $./\$ $.\/$
84	58, 73, 56, 67, 82, 83	syl131anc 1277	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $./\$ $.\/$
85		eqid 2422	. . . . . . . . . . . . . . . . 17
86	31, 32, 85, 34, 1	lhpjat2 33555	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $.\/$
87	53, 72, 86	syl2anc 665	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$
88	87	oveq2d 6321	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$ $.\/$ $./\$
89		hlol 32896	. . . . . . . . . . . . . . . 16
90	58, 89	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
91	26, 33, 85	olm11 32762	. . . . . . . . . . . . . . 15 $/\$ $./\$
92	90, 56, 91	syl2anc 665	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$
93	84, 88, 92	3eqtrd 2467	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
94	26, 31, 32, 33, 34, 1, 41, 42, 43, 44, 2, 45, 46, 47	dihopelvalc 34786	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
95	53, 56, 71, 72, 93, 94	syl122anc 1273	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$
96	95	3expa 1205	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$
97	96	ralbidva 2858	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
98		simp11l 1116	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
99	98, 23	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
100		simp11 1035	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$
101		simp3l 1033	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
102		simp3r 1034	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
103	31, 34, 1, 41	lhpocnel2 33553	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
104	100, 103	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$
105		simp2l 1031	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$
106	31, 34, 1, 42, 45	ltrniotacl 34115	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
107	100, 104, 105, 106	syl3anc 1264	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
108	1, 42, 44	tendocl 34303	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
109	100, 102, 107, 108	syl3anc 1264	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
110	1, 42	ltrncnv 33680	. . . . . . . . . . . . . . . 16 $/\$ $/\$
111	100, 109, 110	syl2anc 665	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
112	1, 42	ltrnco 34255	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
113	100, 101, 111, 112	syl3anc 1264	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
114	26, 1, 42, 43	trlcl 33699	. . . . . . . . . . . . . 14 $/\$ $/\$
115	100, 113, 114	syl2anc 665	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
116		simp12l 1118	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
117	26, 31, 27	clatleglb 16371	. . . . . . . . . . . . 13 $/\$ $/\$
118	99, 115, 116, 117	syl3anc 1264	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
119	118	3expa 1205	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
120	119	pm5.32da 645	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
121	52, 97, 120	3bitr4rd 289	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
122		opex 4685	. . . . . . . . . 10
123		eliin 4305	. . . . . . . . . 10
124	122, 123	ax-mp 5	. . . . . . . . 9
125	121, 124	syl6bbr 266	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
126	49, 125	bitrd 256	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
127	126	exp44 616	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
128	127	imp4a 592	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
129	128	rexlimdv 2912	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
130	36, 129	mpd 15	. . 3 $/\$ $/\$ $/\$ $/\$
131	130	eqrelrdv2 4953	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
132	4, 19, 20, 131	syl21anc 1263	1 $/\$ $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $/\$ wa 370 $/\$ w3a 982

wceq 1437

wex 1657

wcel 1872

wne 2614

wral 2771

wrex 2772

cvv 3080

wss 3436

c0 3761

cop 4004

ciin 4300 class class class wbr 4423

ccnv 4852

ccom 4857

wrel 4858

cfv 5601

crio 6266 (class class class)co 6305

cbs 15120

cple 15196

coc 15197

cglb 16187

cjn 16188

cmee 16189

cp1 16283

clat 16290

ccla 16352

col 32709

catm 32798

chlt 32885

clh 33518

cltrn 33635

ctrl 33693

ctendo 34288

cdih 34765

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1663 ax-4 1676 ax-5 1752 ax-6 1798 ax-7 1843 ax-8 1874 ax-9 1876 ax-10 1891 ax-11 1896 ax-12 1909 ax-13 2057 ax-ext 2401 ax-rep 4536 ax-sep 4546 ax-nul 4555 ax-pow 4602 ax-pr 4660 ax-un 6597 ax-cnex 9602 ax-resscn 9603 ax-1cn 9604 ax-icn 9605 ax-addcl 9606 ax-addrcl 9607 ax-mulcl 9608 ax-mulrcl 9609 ax-mulcom 9610 ax-addass 9611 ax-mulass 9612 ax-distr 9613 ax-i2m1 9614 ax-1ne0 9615 ax-1rid 9616 ax-rnegex 9617 ax-rrecex 9618 ax-cnre 9619 ax-pre-lttri 9620 ax-pre-lttrn 9621 ax-pre-ltadd 9622 ax-pre-mulgt0 9623 ax-riotaBAD 32494

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-fal 1443 df-ex 1658 df-nf 1662 df-sb 1791 df-eu 2273 df-mo 2274 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2568 df-ne 2616 df-nel 2617 df-ral 2776 df-rex 2777 df-reu 2778 df-rmo 2779 df-rab 2780 df-v 3082 df-sbc 3300 df-csb 3396 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-pss 3452 df-nul 3762 df-if 3912 df-pw 3983 df-sn 3999 df-pr 4001 df-tp 4003 df-op 4005 df-uni 4220 df-int 4256 df-iun 4301 df-iin 4302 df-br 4424 df-opab 4483 df-mpt 4484 df-tr 4519 df-eprel 4764 df-id 4768 df-po 4774 df-so 4775 df-fr 4812 df-we 4814 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-res 4865 df-ima 4866 df-pred 5399 df-ord 5445 df-on 5446 df-lim 5447 df-suc 5448 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-riota 6267 df-ov 6308 df-oprab 6309 df-mpt2 6310 df-om 6707 df-1st 6807 df-2nd 6808 df-tpos 6984 df-undef 7031 df-wrecs 7039 df-recs 7101 df-rdg 7139 df-1o 7193 df-oadd 7197 df-er 7374 df-map 7485 df-en 7581 df-dom 7582 df-sdom 7583 df-fin 7584 df-pnf 9684 df-mnf 9685 df-xr 9686 df-ltxr 9687 df-le 9688 df-sub 9869 df-neg 9870 df-nn 10617 df-2 10675 df-3 10676 df-4 10677 df-5 10678 df-6 10679 df-n0 10877 df-z 10945 df-uz 11167 df-fz 11792 df-struct 15122 df-ndx 15123 df-slot 15124 df-base 15125 df-sets 15126 df-ress 15127 df-plusg 15202 df-mulr 15203 df-sca 15205 df-vsca 15206 df-0g 15339 df-preset 16172 df-poset 16190 df-plt 16203 df-lub 16219 df-glb 16220 df-join 16221 df-meet 16222 df-p0 16284 df-p1 16285 df-lat 16291 df-clat 16353 df-mgm 16487 df-sgrp 16526 df-mnd 16536 df-submnd 16582 df-grp 16672 df-minusg 16673 df-sbg 16674 df-subg 16813 df-cntz 16970 df-lsm 17287 df-cmn 17431 df-abl 17432 df-mgp 17723 df-ur 17735 df-ring 17781 df-oppr 17850 df-dvdsr 17868 df-unit 17869 df-invr 17899 df-dvr 17910 df-drng 17976 df-lmod 18092 df-lss 18155 df-lsp 18194 df-lvec 18325 df-oposet 32711 df-ol 32713 df-oml 32714 df-covers 32801 df-ats 32802 df-atl 32833 df-cvlat 32857 df-hlat 32886 df-llines 33032 df-lplanes 33033 df-lvols 33034 df-lines 33035 df-psubsp 33037 df-pmap 33038 df-padd 33330 df-lhyp 33522 df-laut 33523 df-ldil 33638 df-ltrn 33639 df-trl 33694 df-tendo 34291 df-edring 34293 df-disoa 34566 df-dvech 34616 df-dib 34676 df-dic 34710 df-dih 34766

This theorem is referenced by: dihglbcN 34838

W3C validator