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 34300

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 34279	. . 3 $/\$
4	3	3ad2ant1 1018	. 2 $/\$ $/\$ $/\$ $/\$
5		simp2r 1024	. . . . . 6 $/\$ $/\$ $/\$ $/\$
6		n0 3747	. . . . . 6
7	5, 6	sylib 196	. . . . 5 $/\$ $/\$ $/\$ $/\$
8		simpr 459	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
9		simpl1 1000	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
10	1, 2	dihvalrel 34279	. . . . . . . . 9 $/\$
11	9, 10	syl 17	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
12	8, 11	jca 530	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
13	12	ex 432	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
14	13	eximdv 1731	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
15	7, 14	mpd 15	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
16		df-rex 2759	. . . 4 $/\$
17	15, 16	sylibr 212	. . 3 $/\$ $/\$ $/\$ $/\$
18		reliin 4943	. . 3
19	17, 18	syl 17	. 2 $/\$ $/\$ $/\$ $/\$
20		id 22	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
21		simp1 997	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
22		simp1l 1021	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
23		hlclat 32356	. . . . . . 7
24	22, 23	syl 17	. . . . . 6 $/\$ $/\$ $/\$ $/\$
25		simp2l 1023	. . . . . 6 $/\$ $/\$ $/\$ $/\$
26		dihglbc.b	. . . . . . 7
27		dihglbc.g	. . . . . . 7
28	26, 27	clatglbcl 16066	. . . . . 6 $/\$
29	24, 25, 28	syl2anc 659	. . . . 5 $/\$ $/\$ $/\$ $/\$
30		simp3 999	. . . . 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 33021	. . . . 5 $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
36	21, 29, 30, 35	syl12anc 1228	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
37		simpl1 1000	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
38	29	adantr 463	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
39		simpl3 1002	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
40		simpr 459	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$
41		dihglbcpre.p	. . . . . . . . . 10
42		dihglbcpre.t	. . . . . . . . . 10
43		dihglbcpre.r	. . . . . . . . . 10
44		dihglbcpre.e	. . . . . . . . . 10
45		dihglbcpre.f	. . . . . . . . . 10
46		vex 3061	. . . . . . . . . 10
47		vex 3061	. . . . . . . . . 10
48	26, 31, 32, 33, 34, 1, 41, 42, 43, 44, 2, 45, 46, 47	dihopelvalc 34249	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
49	37, 38, 39, 40, 48	syl121anc 1235	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
50		simpl2r 1051	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
51		r19.28zv 3867	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
52	50, 51	syl 17	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
53		simp11 1027	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
54		simp12l 1110	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
55		simp3 999	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
56	54, 55	sseldd 3442	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
57		simp13 1029	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
58		simp11l 1108	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
59	58, 23	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
60	26, 31, 27	clatglble 16077	. . . . . . . . . . . . . . . 16 $/\$ $/\$
61	59, 54, 55, 60	syl3anc 1230	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
62		hllat 32361	. . . . . . . . . . . . . . . . 17
63	58, 62	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
64	29	3ad2ant1 1018	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
65		simp11r 1109	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
66	26, 1	lhpbase 32995	. . . . . . . . . . . . . . . . 17
67	65, 66	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
68	26, 31	lattr 16008	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
69	63, 64, 56, 67, 68	syl13anc 1232	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
70	61, 69	mpand 673	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
71	57, 70	mtod 177	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
72		simp2l 1023	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
73		simp2ll 1064	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
74	26, 34	atbase 32287	. . . . . . . . . . . . . . . . 17
75	73, 74	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
76	26, 33	latmcl 16004	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $./\$
77	63, 64, 67, 76	syl3anc 1230	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$
78	26, 31, 32	latlej1 16012	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $./\$ $.\/$ $./\$
79	63, 75, 77, 78	syl3anc 1230	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
80		simp2r 1024	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
81	79, 80	breqtrd 4418	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
82	26, 31, 63, 75, 64, 56, 81, 61	lattrd 16010	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
83	26, 31, 32, 33, 34	atmod3i1 32861	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $./\$ $.\/$
84	58, 73, 56, 67, 82, 83	syl131anc 1243	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $./\$ $.\/$
85		eqid 2402	. . . . . . . . . . . . . . . . 17
86	31, 32, 85, 34, 1	lhpjat2 33018	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $.\/$
87	53, 72, 86	syl2anc 659	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$
88	87	oveq2d 6293	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$ $.\/$ $./\$
89		hlol 32359	. . . . . . . . . . . . . . . 16
90	58, 89	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
91	26, 33, 85	olm11 32225	. . . . . . . . . . . . . . 15 $/\$ $./\$
92	90, 56, 91	syl2anc 659	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$
93	84, 88, 92	3eqtrd 2447	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
94	26, 31, 32, 33, 34, 1, 41, 42, 43, 44, 2, 45, 46, 47	dihopelvalc 34249	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
95	53, 56, 71, 72, 93, 94	syl122anc 1239	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$
96	95	3expa 1197	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$
97	96	ralbidva 2839	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
98		simp11l 1108	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
99	98, 23	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
100		simp11 1027	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$
101		simp3l 1025	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
102		simp3r 1026	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
103	31, 34, 1, 41	lhpocnel2 33016	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
104	100, 103	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$
105		simp2l 1023	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$
106	31, 34, 1, 42, 45	ltrniotacl 33578	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
107	100, 104, 105, 106	syl3anc 1230	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
108	1, 42, 44	tendocl 33766	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
109	100, 102, 107, 108	syl3anc 1230	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
110	1, 42	ltrncnv 33143	. . . . . . . . . . . . . . . 16 $/\$ $/\$
111	100, 109, 110	syl2anc 659	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
112	1, 42	ltrnco 33718	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
113	100, 101, 111, 112	syl3anc 1230	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
114	26, 1, 42, 43	trlcl 33162	. . . . . . . . . . . . . 14 $/\$ $/\$
115	100, 113, 114	syl2anc 659	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
116		simp12l 1110	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
117	26, 31, 27	clatleglb 16078	. . . . . . . . . . . . 13 $/\$ $/\$
118	99, 115, 116, 117	syl3anc 1230	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
119	118	3expa 1197	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
120	119	pm5.32da 639	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
121	52, 97, 120	3bitr4rd 286	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
122		opex 4654	. . . . . . . . . 10
123		eliin 4276	. . . . . . . . . 10
124	122, 123	ax-mp 5	. . . . . . . . 9
125	121, 124	syl6bbr 263	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
126	49, 125	bitrd 253	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
127	126	exp44 611	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
128	127	imp4a 587	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
129	128	rexlimdv 2893	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
130	36, 129	mpd 15	. . 3 $/\$ $/\$ $/\$ $/\$
131	130	eqrelrdv2 4922	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
132	4, 19, 20, 131	syl21anc 1229	1 $/\$ $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 367 $/\$ w3a 974

wceq 1405

wex 1633

wcel 1842

wne 2598

wral 2753

wrex 2754

cvv 3058

wss 3413

c0 3737

cop 3977

ciin 4271 class class class wbr 4394

ccnv 4821

ccom 4826

wrel 4827

cfv 5568

crio 6238 (class class class)co 6277

cbs 14839

cple 14914

coc 14915

cglb 15894

cjn 15895

cmee 15896

cp1 15990

clat 15997

ccla 16059

col 32172

catm 32261

chlt 32348

clh 32981

cltrn 33098

ctrl 33156

ctendo 33751

cdih 34228

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1639 ax-4 1652 ax-5 1725 ax-6 1771 ax-7 1814 ax-8 1844 ax-9 1846 ax-10 1861 ax-11 1866 ax-12 1878 ax-13 2026 ax-ext 2380 ax-rep 4506 ax-sep 4516 ax-nul 4524 ax-pow 4571 ax-pr 4629 ax-un 6573 ax-cnex 9577 ax-resscn 9578 ax-1cn 9579 ax-icn 9580 ax-addcl 9581 ax-addrcl 9582 ax-mulcl 9583 ax-mulrcl 9584 ax-mulcom 9585 ax-addass 9586 ax-mulass 9587 ax-distr 9588 ax-i2m1 9589 ax-1ne0 9590 ax-1rid 9591 ax-rnegex 9592 ax-rrecex 9593 ax-cnre 9594 ax-pre-lttri 9595 ax-pre-lttrn 9596 ax-pre-ltadd 9597 ax-pre-mulgt0 9598 ax-riotaBAD 31957

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 975 df-3an 976 df-tru 1408 df-fal 1411 df-ex 1634 df-nf 1638 df-sb 1764 df-eu 2242 df-mo 2243 df-clab 2388 df-cleq 2394 df-clel 2397 df-nfc 2552 df-ne 2600 df-nel 2601 df-ral 2758 df-rex 2759 df-reu 2760 df-rmo 2761 df-rab 2762 df-v 3060 df-sbc 3277 df-csb 3373 df-dif 3416 df-un 3418 df-in 3420 df-ss 3427 df-pss 3429 df-nul 3738 df-if 3885 df-pw 3956 df-sn 3972 df-pr 3974 df-tp 3976 df-op 3978 df-uni 4191 df-int 4227 df-iun 4272 df-iin 4273 df-br 4395 df-opab 4453 df-mpt 4454 df-tr 4489 df-eprel 4733 df-id 4737 df-po 4743 df-so 4744 df-fr 4781 df-we 4783 df-xp 4828 df-rel 4829 df-cnv 4830 df-co 4831 df-dm 4832 df-rn 4833 df-res 4834 df-ima 4835 df-pred 5366 df-ord 5412 df-on 5413 df-lim 5414 df-suc 5415 df-iota 5532 df-fun 5570 df-fn 5571 df-f 5572 df-f1 5573 df-fo 5574 df-f1o 5575 df-fv 5576 df-riota 6239 df-ov 6280 df-oprab 6281 df-mpt2 6282 df-om 6683 df-1st 6783 df-2nd 6784 df-tpos 6957 df-undef 7004 df-wrecs 7012 df-recs 7074 df-rdg 7112 df-1o 7166 df-oadd 7170 df-er 7347 df-map 7458 df-en 7554 df-dom 7555 df-sdom 7556 df-fin 7557 df-pnf 9659 df-mnf 9660 df-xr 9661 df-ltxr 9662 df-le 9663 df-sub 9842 df-neg 9843 df-nn 10576 df-2 10634 df-3 10635 df-4 10636 df-5 10637 df-6 10638 df-n0 10836 df-z 10905 df-uz 11127 df-fz 11725 df-struct 14841 df-ndx 14842 df-slot 14843 df-base 14844 df-sets 14845 df-ress 14846 df-plusg 14920 df-mulr 14921 df-sca 14923 df-vsca 14924 df-0g 15054 df-preset 15879 df-poset 15897 df-plt 15910 df-lub 15926 df-glb 15927 df-join 15928 df-meet 15929 df-p0 15991 df-p1 15992 df-lat 15998 df-clat 16060 df-mgm 16194 df-sgrp 16233 df-mnd 16243 df-submnd 16289 df-grp 16379 df-minusg 16380 df-sbg 16381 df-subg 16520 df-cntz 16677 df-lsm 16978 df-cmn 17122 df-abl 17123 df-mgp 17460 df-ur 17472 df-ring 17518 df-oppr 17590 df-dvdsr 17608 df-unit 17609 df-invr 17639 df-dvr 17650 df-drng 17716 df-lmod 17832 df-lss 17897 df-lsp 17936 df-lvec 18067 df-oposet 32174 df-ol 32176 df-oml 32177 df-covers 32264 df-ats 32265 df-atl 32296 df-cvlat 32320 df-hlat 32349 df-llines 32495 df-lplanes 32496 df-lvols 32497 df-lines 32498 df-psubsp 32500 df-pmap 32501 df-padd 32793 df-lhyp 32985 df-laut 32986 df-ldil 33101 df-ltrn 33102 df-trl 33157 df-tendo 33754 df-edring 33756 df-disoa 34029 df-dvech 34079 df-dib 34139 df-dic 34173 df-dih 34229

This theorem is referenced by: dihglbcN 34301

W3C validator