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 35253

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 35232	. . 3 $/\$
4	3	3ad2ant1 1009	. 2 $/\$ $/\$ $/\$ $/\$
5		simp2r 1015	. . . . . 6 $/\$ $/\$ $/\$ $/\$
6		n0 3746	. . . . . 6
7	5, 6	sylib 196	. . . . 5 $/\$ $/\$ $/\$ $/\$
8		simpr 461	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
9		simpl1 991	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
10	1, 2	dihvalrel 35232	. . . . . . . . 9 $/\$
11	9, 10	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
12	8, 11	jca 532	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
13	12	ex 434	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
14	13	eximdv 1677	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
15	7, 14	mpd 15	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
16		df-rex 2801	. . . 4 $/\$
17	15, 16	sylibr 212	. . 3 $/\$ $/\$ $/\$ $/\$
18		reliin 5061	. . 3
19	17, 18	syl 16	. 2 $/\$ $/\$ $/\$ $/\$
20		id 22	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
21		simp1 988	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
22		simp1l 1012	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
23		hlclat 33311	. . . . . . 7
24	22, 23	syl 16	. . . . . 6 $/\$ $/\$ $/\$ $/\$
25		simp2l 1014	. . . . . 6 $/\$ $/\$ $/\$ $/\$
26		dihglbc.b	. . . . . . 7
27		dihglbc.g	. . . . . . 7
28	26, 27	clatglbcl 15388	. . . . . 6 $/\$
29	24, 25, 28	syl2anc 661	. . . . 5 $/\$ $/\$ $/\$ $/\$
30		simp3 990	. . . . 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 33976	. . . . 5 $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
36	21, 29, 30, 35	syl12anc 1217	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
37		simpl1 991	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
38	29	adantr 465	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
39		simpl3 993	. . . . . . . . 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 3073	. . . . . . . . . 10
47		vex 3073	. . . . . . . . . 10
48	26, 31, 32, 33, 34, 1, 41, 42, 43, 44, 2, 45, 46, 47	dihopelvalc 35202	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
49	37, 38, 39, 40, 48	syl121anc 1224	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
50		simpl2r 1042	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
51		r19.28zv 3875	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
52	50, 51	syl 16	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
53		simp11 1018	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
54		simp12l 1101	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
55		simp3 990	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
56	54, 55	sseldd 3457	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
57		simp13 1020	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
58		simp11l 1099	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
59	58, 23	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
60	26, 31, 27	clatglble 15399	. . . . . . . . . . . . . . . 16 $/\$ $/\$
61	59, 54, 55, 60	syl3anc 1219	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
62		hllat 33316	. . . . . . . . . . . . . . . . 17
63	58, 62	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
64	29	3ad2ant1 1009	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
65		simp11r 1100	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
66	26, 1	lhpbase 33950	. . . . . . . . . . . . . . . . 17
67	65, 66	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
68	26, 31	lattr 15330	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
69	63, 64, 56, 67, 68	syl13anc 1221	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
70	61, 69	mpand 675	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
71	57, 70	mtod 177	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
72		simp2l 1014	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
73		simp2ll 1055	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
74	26, 34	atbase 33242	. . . . . . . . . . . . . . . . 17
75	73, 74	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
76	26, 33	latmcl 15326	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $./\$
77	63, 64, 67, 76	syl3anc 1219	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$
78	26, 31, 32	latlej1 15334	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $./\$ $.\/$ $./\$
79	63, 75, 77, 78	syl3anc 1219	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
80		simp2r 1015	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
81	79, 80	breqtrd 4416	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
82	26, 31, 63, 75, 64, 56, 81, 61	lattrd 15332	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
83	26, 31, 32, 33, 34	atmod3i1 33816	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $./\$ $.\/$
84	58, 73, 56, 67, 82, 83	syl131anc 1232	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $./\$ $.\/$
85		eqid 2451	. . . . . . . . . . . . . . . . 17
86	31, 32, 85, 34, 1	lhpjat2 33973	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $.\/$
87	53, 72, 86	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$
88	87	oveq2d 6208	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$ $.\/$ $./\$
89		hlol 33314	. . . . . . . . . . . . . . . 16
90	58, 89	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
91	26, 33, 85	olm11 33180	. . . . . . . . . . . . . . 15 $/\$ $./\$
92	90, 56, 91	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$
93	84, 88, 92	3eqtrd 2496	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
94	26, 31, 32, 33, 34, 1, 41, 42, 43, 44, 2, 45, 46, 47	dihopelvalc 35202	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
95	53, 56, 71, 72, 93, 94	syl122anc 1228	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$
96	95	3expa 1188	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$
97	96	ralbidva 2836	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
98		simp11l 1099	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
99	98, 23	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
100		simp11 1018	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$
101		simp3l 1016	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
102		simp3r 1017	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
103	31, 34, 1, 41	lhpocnel2 33971	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
104	100, 103	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$
105		simp2l 1014	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$
106	31, 34, 1, 42, 45	ltrniotacl 34531	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
107	100, 104, 105, 106	syl3anc 1219	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
108	1, 42, 44	tendocl 34719	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
109	100, 102, 107, 108	syl3anc 1219	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
110	1, 42	ltrncnv 34098	. . . . . . . . . . . . . . . 16 $/\$ $/\$
111	100, 109, 110	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
112	1, 42	ltrnco 34671	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
113	100, 101, 111, 112	syl3anc 1219	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
114	26, 1, 42, 43	trlcl 34116	. . . . . . . . . . . . . 14 $/\$ $/\$
115	100, 113, 114	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
116		simp12l 1101	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
117	26, 31, 27	clatleglb 15400	. . . . . . . . . . . . 13 $/\$ $/\$
118	99, 115, 116, 117	syl3anc 1219	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
119	118	3expa 1188	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
120	119	pm5.32da 641	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
121	52, 97, 120	3bitr4rd 286	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
122		opex 4656	. . . . . . . . . 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 613	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
128	127	imp4a 589	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
129	128	rexlimdv 2938	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
130	36, 129	mpd 15	. . 3 $/\$ $/\$ $/\$ $/\$
131	130	eqrelrdv2 5039	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
132	4, 19, 20, 131	syl21anc 1218	1 $/\$ $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1370

wex 1587

wcel 1758

wne 2644

wral 2795

wrex 2796

cvv 3070

wss 3428

c0 3737

cop 3983

ciin 4272 class class class wbr 4392

ccnv 4939

ccom 4944

wrel 4945

cfv 5518

crio 6152 (class class class)co 6192

cbs 14278

cple 14349

coc 14350

cglb 15217

cjn 15218

cmee 15219

cp1 15312

clat 15319

ccla 15381

col 33127

catm 33216

chlt 33303

clh 33936

cltrn 34053

ctrl 34110

ctendo 34704

cdih 35181

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-rep 4503 ax-sep 4513 ax-nul 4521 ax-pow 4570 ax-pr 4631 ax-un 6474 ax-cnex 9441 ax-resscn 9442 ax-1cn 9443 ax-icn 9444 ax-addcl 9445 ax-addrcl 9446 ax-mulcl 9447 ax-mulrcl 9448 ax-mulcom 9449 ax-addass 9450 ax-mulass 9451 ax-distr 9452 ax-i2m1 9453 ax-1ne0 9454 ax-1rid 9455 ax-rnegex 9456 ax-rrecex 9457 ax-cnre 9458 ax-pre-lttri 9459 ax-pre-lttrn 9460 ax-pre-ltadd 9461 ax-pre-mulgt0 9462 ax-riotaBAD 32912

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-fal 1376 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2264 df-mo 2265 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ne 2646 df-nel 2647 df-ral 2800 df-rex 2801 df-reu 2802 df-rmo 2803 df-rab 2804 df-v 3072 df-sbc 3287 df-csb 3389 df-dif 3431 df-un 3433 df-in 3435 df-ss 3442 df-pss 3444 df-nul 3738 df-if 3892 df-pw 3962 df-sn 3978 df-pr 3980 df-tp 3982 df-op 3984 df-uni 4192 df-int 4229 df-iun 4273 df-iin 4274 df-br 4393 df-opab 4451 df-mpt 4452 df-tr 4486 df-eprel 4732 df-id 4736 df-po 4741 df-so 4742 df-fr 4779 df-we 4781 df-ord 4822 df-on 4823 df-lim 4824 df-suc 4825 df-xp 4946 df-rel 4947 df-cnv 4948 df-co 4949 df-dm 4950 df-rn 4951 df-res 4952 df-ima 4953 df-iota 5481 df-fun 5520 df-fn 5521 df-f 5522 df-f1 5523 df-fo 5524 df-f1o 5525 df-fv 5526 df-riota 6153 df-ov 6195 df-oprab 6196 df-mpt2 6197 df-om 6579 df-1st 6679 df-2nd 6680 df-tpos 6847 df-undef 6894 df-recs 6934 df-rdg 6968 df-1o 7022 df-oadd 7026 df-er 7203 df-map 7318 df-en 7413 df-dom 7414 df-sdom 7415 df-fin 7416 df-pnf 9523 df-mnf 9524 df-xr 9525 df-ltxr 9526 df-le 9527 df-sub 9700 df-neg 9701 df-nn 10426 df-2 10483 df-3 10484 df-4 10485 df-5 10486 df-6 10487 df-n0 10683 df-z 10750 df-uz 10965 df-fz 11541 df-struct 14280 df-ndx 14281 df-slot 14282 df-base 14283 df-sets 14284 df-ress 14285 df-plusg 14355 df-mulr 14356 df-sca 14358 df-vsca 14359 df-0g 14484 df-poset 15220 df-plt 15232 df-lub 15248 df-glb 15249 df-join 15250 df-meet 15251 df-p0 15313 df-p1 15314 df-lat 15320 df-clat 15382 df-mnd 15519 df-submnd 15569 df-grp 15649 df-minusg 15650 df-sbg 15651 df-subg 15782 df-cntz 15939 df-lsm 16241 df-cmn 16385 df-abl 16386 df-mgp 16699 df-ur 16711 df-rng 16755 df-oppr 16823 df-dvdsr 16841 df-unit 16842 df-invr 16872 df-dvr 16883 df-drng 16942 df-lmod 17058 df-lss 17122 df-lsp 17161 df-lvec 17292 df-oposet 33129 df-ol 33131 df-oml 33132 df-covers 33219 df-ats 33220 df-atl 33251 df-cvlat 33275 df-hlat 33304 df-llines 33450 df-lplanes 33451 df-lvols 33452 df-lines 33453 df-psubsp 33455 df-pmap 33456 df-padd 33748 df-lhyp 33940 df-laut 33941 df-ldil 34056 df-ltrn 34057 df-trl 34111 df-tendo 34707 df-edring 34709 df-disoa 34982 df-dvech 35032 df-dib 35092 df-dic 35126 df-dih 35182

This theorem is referenced by: dihglbcN 35254

W3C validator