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 37170

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 37149	. . 3 $/\$
4	3	3ad2ant1 1017	. 2 $/\$ $/\$ $/\$ $/\$
5		simp2r 1023	. . . . . 6 $/\$ $/\$ $/\$ $/\$
6		n0 3803	. . . . . 6
7	5, 6	sylib 196	. . . . 5 $/\$ $/\$ $/\$ $/\$
8		simpr 461	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
9		simpl1 999	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
10	1, 2	dihvalrel 37149	. . . . . . . . 9 $/\$
11	9, 10	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
12	8, 11	jca 532	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
13	12	ex 434	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
14	13	eximdv 1711	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
15	7, 14	mpd 15	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
16		df-rex 2813	. . . 4 $/\$
17	15, 16	sylibr 212	. . 3 $/\$ $/\$ $/\$ $/\$
18		reliin 5133	. . 3
19	17, 18	syl 16	. 2 $/\$ $/\$ $/\$ $/\$
20		id 22	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
21		simp1 996	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
22		simp1l 1020	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
23		hlclat 35226	. . . . . . 7
24	22, 23	syl 16	. . . . . 6 $/\$ $/\$ $/\$ $/\$
25		simp2l 1022	. . . . . 6 $/\$ $/\$ $/\$ $/\$
26		dihglbc.b	. . . . . . 7
27		dihglbc.g	. . . . . . 7
28	26, 27	clatglbcl 15871	. . . . . 6 $/\$
29	24, 25, 28	syl2anc 661	. . . . 5 $/\$ $/\$ $/\$ $/\$
30		simp3 998	. . . . 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 35891	. . . . 5 $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
36	21, 29, 30, 35	syl12anc 1226	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
37		simpl1 999	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
38	29	adantr 465	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
39		simpl3 1001	. . . . . . . . 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 3112	. . . . . . . . . 10
47		vex 3112	. . . . . . . . . 10
48	26, 31, 32, 33, 34, 1, 41, 42, 43, 44, 2, 45, 46, 47	dihopelvalc 37119	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
49	37, 38, 39, 40, 48	syl121anc 1233	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
50		simpl2r 1050	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
51		r19.28zv 3927	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
52	50, 51	syl 16	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
53		simp11 1026	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
54		simp12l 1109	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
55		simp3 998	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
56	54, 55	sseldd 3500	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
57		simp13 1028	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
58		simp11l 1107	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
59	58, 23	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
60	26, 31, 27	clatglble 15882	. . . . . . . . . . . . . . . 16 $/\$ $/\$
61	59, 54, 55, 60	syl3anc 1228	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
62		hllat 35231	. . . . . . . . . . . . . . . . 17
63	58, 62	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
64	29	3ad2ant1 1017	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
65		simp11r 1108	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
66	26, 1	lhpbase 35865	. . . . . . . . . . . . . . . . 17
67	65, 66	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
68	26, 31	lattr 15813	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
69	63, 64, 56, 67, 68	syl13anc 1230	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
70	61, 69	mpand 675	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
71	57, 70	mtod 177	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
72		simp2l 1022	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
73		simp2ll 1063	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
74	26, 34	atbase 35157	. . . . . . . . . . . . . . . . 17
75	73, 74	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
76	26, 33	latmcl 15809	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $./\$
77	63, 64, 67, 76	syl3anc 1228	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$
78	26, 31, 32	latlej1 15817	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $./\$ $.\/$ $./\$
79	63, 75, 77, 78	syl3anc 1228	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
80		simp2r 1023	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
81	79, 80	breqtrd 4480	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
82	26, 31, 63, 75, 64, 56, 81, 61	lattrd 15815	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
83	26, 31, 32, 33, 34	atmod3i1 35731	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $./\$ $.\/$
84	58, 73, 56, 67, 82, 83	syl131anc 1241	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $./\$ $.\/$
85		eqid 2457	. . . . . . . . . . . . . . . . 17
86	31, 32, 85, 34, 1	lhpjat2 35888	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $.\/$
87	53, 72, 86	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$
88	87	oveq2d 6312	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$ $.\/$ $./\$
89		hlol 35229	. . . . . . . . . . . . . . . 16
90	58, 89	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
91	26, 33, 85	olm11 35095	. . . . . . . . . . . . . . 15 $/\$ $./\$
92	90, 56, 91	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$
93	84, 88, 92	3eqtrd 2502	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
94	26, 31, 32, 33, 34, 1, 41, 42, 43, 44, 2, 45, 46, 47	dihopelvalc 37119	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
95	53, 56, 71, 72, 93, 94	syl122anc 1237	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$
96	95	3expa 1196	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$
97	96	ralbidva 2893	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
98		simp11l 1107	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
99	98, 23	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
100		simp11 1026	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$
101		simp3l 1024	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
102		simp3r 1025	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
103	31, 34, 1, 41	lhpocnel2 35886	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
104	100, 103	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$
105		simp2l 1022	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$
106	31, 34, 1, 42, 45	ltrniotacl 36448	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
107	100, 104, 105, 106	syl3anc 1228	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
108	1, 42, 44	tendocl 36636	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
109	100, 102, 107, 108	syl3anc 1228	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
110	1, 42	ltrncnv 36013	. . . . . . . . . . . . . . . 16 $/\$ $/\$
111	100, 109, 110	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
112	1, 42	ltrnco 36588	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
113	100, 101, 111, 112	syl3anc 1228	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
114	26, 1, 42, 43	trlcl 36032	. . . . . . . . . . . . . 14 $/\$ $/\$
115	100, 113, 114	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
116		simp12l 1109	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
117	26, 31, 27	clatleglb 15883	. . . . . . . . . . . . 13 $/\$ $/\$
118	99, 115, 116, 117	syl3anc 1228	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
119	118	3expa 1196	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
120	119	pm5.32da 641	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
121	52, 97, 120	3bitr4rd 286	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
122		opex 4720	. . . . . . . . . 10
123		eliin 4338	. . . . . . . . . 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 2947	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
130	36, 129	mpd 15	. . 3 $/\$ $/\$ $/\$ $/\$
131	130	eqrelrdv2 5111	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
132	4, 19, 20, 131	syl21anc 1227	1 $/\$ $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1395

wex 1613

wcel 1819

wne 2652

wral 2807

wrex 2808

cvv 3109

wss 3471

c0 3793

cop 4038

ciin 4333 class class class wbr 4456

ccnv 5007

ccom 5012

wrel 5013

cfv 5594

crio 6257 (class class class)co 6296

cbs 14644

cple 14719

coc 14720

cglb 15699

cjn 15700

cmee 15701

cp1 15795

clat 15802

ccla 15864

col 35042

catm 35131

chlt 35218

clh 35851

cltrn 35968

ctrl 36026

ctendo 36621

cdih 37098

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586 ax-riotaBAD 34827

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-fal 1401 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-iin 4335 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6700 df-1st 6799 df-2nd 6800 df-tpos 6973 df-undef 7020 df-recs 7060 df-rdg 7094 df-1o 7148 df-oadd 7152 df-er 7329 df-map 7440 df-en 7536 df-dom 7537 df-sdom 7538 df-fin 7539 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-nn 10557 df-2 10615 df-3 10616 df-4 10617 df-5 10618 df-6 10619 df-n0 10817 df-z 10886 df-uz 11107 df-fz 11698 df-struct 14646 df-ndx 14647 df-slot 14648 df-base 14649 df-sets 14650 df-ress 14651 df-plusg 14725 df-mulr 14726 df-sca 14728 df-vsca 14729 df-0g 14859 df-preset 15684 df-poset 15702 df-plt 15715 df-lub 15731 df-glb 15732 df-join 15733 df-meet 15734 df-p0 15796 df-p1 15797 df-lat 15803 df-clat 15865 df-mgm 15999 df-sgrp 16038 df-mnd 16048 df-submnd 16094 df-grp 16184 df-minusg 16185 df-sbg 16186 df-subg 16325 df-cntz 16482 df-lsm 16783 df-cmn 16927 df-abl 16928 df-mgp 17269 df-ur 17281 df-ring 17327 df-oppr 17399 df-dvdsr 17417 df-unit 17418 df-invr 17448 df-dvr 17459 df-drng 17525 df-lmod 17641 df-lss 17706 df-lsp 17745 df-lvec 17876 df-oposet 35044 df-ol 35046 df-oml 35047 df-covers 35134 df-ats 35135 df-atl 35166 df-cvlat 35190 df-hlat 35219 df-llines 35365 df-lplanes 35366 df-lvols 35367 df-lines 35368 df-psubsp 35370 df-pmap 35371 df-padd 35663 df-lhyp 35855 df-laut 35856 df-ldil 35971 df-ltrn 35972 df-trl 36027 df-tendo 36624 df-edring 36626 df-disoa 36899 df-dvech 36949 df-dib 37009 df-dic 37043 df-dih 37099

This theorem is referenced by: dihglbcN 37171

W3C validator