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 35974

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 35953	. . 3 $/\$
4	3	3ad2ant1 1012	. 2 $/\$ $/\$ $/\$ $/\$
5		simp2r 1018	. . . . . 6 $/\$ $/\$ $/\$ $/\$
6		n0 3789	. . . . . 6
7	5, 6	sylib 196	. . . . 5 $/\$ $/\$ $/\$ $/\$
8		simpr 461	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
9		simpl1 994	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
10	1, 2	dihvalrel 35953	. . . . . . . . 9 $/\$
11	9, 10	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
12	8, 11	jca 532	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
13	12	ex 434	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
14	13	eximdv 1681	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
15	7, 14	mpd 15	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
16		df-rex 2815	. . . 4 $/\$
17	15, 16	sylibr 212	. . 3 $/\$ $/\$ $/\$ $/\$
18		reliin 5117	. . 3
19	17, 18	syl 16	. 2 $/\$ $/\$ $/\$ $/\$
20		id 22	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
21		simp1 991	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
22		simp1l 1015	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
23		hlclat 34032	. . . . . . 7
24	22, 23	syl 16	. . . . . 6 $/\$ $/\$ $/\$ $/\$
25		simp2l 1017	. . . . . 6 $/\$ $/\$ $/\$ $/\$
26		dihglbc.b	. . . . . . 7
27		dihglbc.g	. . . . . . 7
28	26, 27	clatglbcl 15592	. . . . . 6 $/\$
29	24, 25, 28	syl2anc 661	. . . . 5 $/\$ $/\$ $/\$ $/\$
30		simp3 993	. . . . 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 34697	. . . . 5 $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
36	21, 29, 30, 35	syl12anc 1221	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
37		simpl1 994	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
38	29	adantr 465	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
39		simpl3 996	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
40		simpr 461	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$
41		dihglbcpre.p	. . . . . . . . . 10
42		dihglbcpre.t	. . . . . . . . . 10
43		dihglbcpre.r	. . . . . . . . . 10
44		dihglbcpre.e	. . . . . . . . . 10
45		dihglbcpre.f	. . . . . . . . . 10
46		vex 3111	. . . . . . . . . 10
47		vex 3111	. . . . . . . . . 10
48	26, 31, 32, 33, 34, 1, 41, 42, 43, 44, 2, 45, 46, 47	dihopelvalc 35923	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
49	37, 38, 39, 40, 48	syl121anc 1228	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
50		simpl2r 1045	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
51		r19.28zv 3918	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
52	50, 51	syl 16	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
53		simp11 1021	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
54		simp12l 1104	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
55		simp3 993	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
56	54, 55	sseldd 3500	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
57		simp13 1023	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
58		simp11l 1102	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
59	58, 23	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
60	26, 31, 27	clatglble 15603	. . . . . . . . . . . . . . . 16 $/\$ $/\$
61	59, 54, 55, 60	syl3anc 1223	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
62		hllat 34037	. . . . . . . . . . . . . . . . 17
63	58, 62	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
64	29	3ad2ant1 1012	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
65		simp11r 1103	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
66	26, 1	lhpbase 34671	. . . . . . . . . . . . . . . . 17
67	65, 66	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
68	26, 31	lattr 15534	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
69	63, 64, 56, 67, 68	syl13anc 1225	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
70	61, 69	mpand 675	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
71	57, 70	mtod 177	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
72		simp2l 1017	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
73		simp2ll 1058	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
74	26, 34	atbase 33963	. . . . . . . . . . . . . . . . 17
75	73, 74	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
76	26, 33	latmcl 15530	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $./\$
77	63, 64, 67, 76	syl3anc 1223	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$
78	26, 31, 32	latlej1 15538	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $./\$ $.\/$ $./\$
79	63, 75, 77, 78	syl3anc 1223	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
80		simp2r 1018	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
81	79, 80	breqtrd 4466	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
82	26, 31, 63, 75, 64, 56, 81, 61	lattrd 15536	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
83	26, 31, 32, 33, 34	atmod3i1 34537	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $./\$ $.\/$
84	58, 73, 56, 67, 82, 83	syl131anc 1236	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $./\$ $.\/$
85		eqid 2462	. . . . . . . . . . . . . . . . 17
86	31, 32, 85, 34, 1	lhpjat2 34694	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $.\/$
87	53, 72, 86	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$
88	87	oveq2d 6293	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$ $.\/$ $./\$
89		hlol 34035	. . . . . . . . . . . . . . . 16
90	58, 89	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
91	26, 33, 85	olm11 33901	. . . . . . . . . . . . . . 15 $/\$ $./\$
92	90, 56, 91	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$
93	84, 88, 92	3eqtrd 2507	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
94	26, 31, 32, 33, 34, 1, 41, 42, 43, 44, 2, 45, 46, 47	dihopelvalc 35923	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
95	53, 56, 71, 72, 93, 94	syl122anc 1232	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$
96	95	3expa 1191	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$
97	96	ralbidva 2895	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
98		simp11l 1102	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
99	98, 23	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
100		simp11 1021	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$
101		simp3l 1019	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
102		simp3r 1020	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
103	31, 34, 1, 41	lhpocnel2 34692	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
104	100, 103	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$
105		simp2l 1017	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$
106	31, 34, 1, 42, 45	ltrniotacl 35252	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
107	100, 104, 105, 106	syl3anc 1223	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
108	1, 42, 44	tendocl 35440	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
109	100, 102, 107, 108	syl3anc 1223	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
110	1, 42	ltrncnv 34819	. . . . . . . . . . . . . . . 16 $/\$ $/\$
111	100, 109, 110	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
112	1, 42	ltrnco 35392	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
113	100, 101, 111, 112	syl3anc 1223	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
114	26, 1, 42, 43	trlcl 34837	. . . . . . . . . . . . . 14 $/\$ $/\$
115	100, 113, 114	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
116		simp12l 1104	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
117	26, 31, 27	clatleglb 15604	. . . . . . . . . . . . 13 $/\$ $/\$
118	99, 115, 116, 117	syl3anc 1223	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
119	118	3expa 1191	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
120	119	pm5.32da 641	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
121	52, 97, 120	3bitr4rd 286	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
122		opex 4706	. . . . . . . . . 10
123		eliin 4326	. . . . . . . . . 10
124	122, 123	ax-mp 5	. . . . . . . . 9
125	121, 124	syl6bbr 263	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
126	49, 125	bitrd 253	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
127	126	exp44 613	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
128	127	imp4a 589	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
129	128	rexlimdv 2948	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
130	36, 129	mpd 15	. . 3 $/\$ $/\$ $/\$ $/\$
131	130	eqrelrdv2 5095	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
132	4, 19, 20, 131	syl21anc 1222	1 $/\$ $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 968

wceq 1374

wex 1591

wcel 1762

wne 2657

wral 2809

wrex 2810

cvv 3108

wss 3471

c0 3780

cop 4028

ciin 4321 class class class wbr 4442

ccnv 4993

ccom 4998

wrel 4999

cfv 5581

crio 6237 (class class class)co 6277

cbs 14481

cple 14553

coc 14554

cglb 15421

cjn 15422

cmee 15423

cp1 15516

clat 15523

ccla 15585

col 33848

catm 33937

chlt 34024

clh 34657

cltrn 34774

ctrl 34831

ctendo 35425

cdih 35902

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1714 ax-7 1734 ax-8 1764 ax-9 1766 ax-10 1781 ax-11 1786 ax-12 1798 ax-13 1963 ax-ext 2440 ax-rep 4553 ax-sep 4563 ax-nul 4571 ax-pow 4620 ax-pr 4681 ax-un 6569 ax-cnex 9539 ax-resscn 9540 ax-1cn 9541 ax-icn 9542 ax-addcl 9543 ax-addrcl 9544 ax-mulcl 9545 ax-mulrcl 9546 ax-mulcom 9547 ax-addass 9548 ax-mulass 9549 ax-distr 9550 ax-i2m1 9551 ax-1ne0 9552 ax-1rid 9553 ax-rnegex 9554 ax-rrecex 9555 ax-cnre 9556 ax-pre-lttri 9557 ax-pre-lttrn 9558 ax-pre-ltadd 9559 ax-pre-mulgt0 9560 ax-riotaBAD 33633

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 969 df-3an 970 df-tru 1377 df-fal 1380 df-ex 1592 df-nf 1595 df-sb 1707 df-eu 2274 df-mo 2275 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2612 df-ne 2659 df-nel 2660 df-ral 2814 df-rex 2815 df-reu 2816 df-rmo 2817 df-rab 2818 df-v 3110 df-sbc 3327 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3781 df-if 3935 df-pw 4007 df-sn 4023 df-pr 4025 df-tp 4027 df-op 4029 df-uni 4241 df-int 4278 df-iun 4322 df-iin 4323 df-br 4443 df-opab 4501 df-mpt 4502 df-tr 4536 df-eprel 4786 df-id 4790 df-po 4795 df-so 4796 df-fr 4833 df-we 4835 df-ord 4876 df-on 4877 df-lim 4878 df-suc 4879 df-xp 5000 df-rel 5001 df-cnv 5002 df-co 5003 df-dm 5004 df-rn 5005 df-res 5006 df-ima 5007 df-iota 5544 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-riota 6238 df-ov 6280 df-oprab 6281 df-mpt2 6282 df-om 6674 df-1st 6776 df-2nd 6777 df-tpos 6947 df-undef 6994 df-recs 7034 df-rdg 7068 df-1o 7122 df-oadd 7126 df-er 7303 df-map 7414 df-en 7509 df-dom 7510 df-sdom 7511 df-fin 7512 df-pnf 9621 df-mnf 9622 df-xr 9623 df-ltxr 9624 df-le 9625 df-sub 9798 df-neg 9799 df-nn 10528 df-2 10585 df-3 10586 df-4 10587 df-5 10588 df-6 10589 df-n0 10787 df-z 10856 df-uz 11074 df-fz 11664 df-struct 14483 df-ndx 14484 df-slot 14485 df-base 14486 df-sets 14487 df-ress 14488 df-plusg 14559 df-mulr 14560 df-sca 14562 df-vsca 14563 df-0g 14688 df-poset 15424 df-plt 15436 df-lub 15452 df-glb 15453 df-join 15454 df-meet 15455 df-p0 15517 df-p1 15518 df-lat 15524 df-clat 15586 df-mnd 15723 df-submnd 15773 df-grp 15853 df-minusg 15854 df-sbg 15855 df-subg 15988 df-cntz 16145 df-lsm 16447 df-cmn 16591 df-abl 16592 df-mgp 16927 df-ur 16939 df-rng 16983 df-oppr 17051 df-dvdsr 17069 df-unit 17070 df-invr 17100 df-dvr 17111 df-drng 17176 df-lmod 17292 df-lss 17357 df-lsp 17396 df-lvec 17527 df-oposet 33850 df-ol 33852 df-oml 33853 df-covers 33940 df-ats 33941 df-atl 33972 df-cvlat 33996 df-hlat 34025 df-llines 34171 df-lplanes 34172 df-lvols 34173 df-lines 34174 df-psubsp 34176 df-pmap 34177 df-padd 34469 df-lhyp 34661 df-laut 34662 df-ldil 34777 df-ltrn 34778 df-trl 34832 df-tendo 35428 df-edring 35430 df-disoa 35703 df-dvech 35753 df-dib 35813 df-dic 35847 df-dih 35903

This theorem is referenced by: dihglbcN 35975

W3C validator