df-lcv - Mathbox for Norm Megill

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

Definition df-lcv 35141

Description: Define the covering relation for subspaces of a left vector space. Similar to Definition 3.2.18 of [PtakPulmannova] p. 68. Ptak/Pulmannova's notation

is read "

covers

" or "

is covered by

" , and it means that

is larger than

and there is nothing in between. See lcvbr 35143 for binary relation. (df-cv 27396 analog.) (Contributed by NM, 7-Jan-2015.)

**Assertion**
Ref	Expression
df-lcv	_L $/\$ $/\$ $/\$ $/\$

Distinct variable group:

**Detailed syntax breakdown of Definition df-lcv**
Step	Hyp	Ref	Expression
1		clcv 35140	. 2 _L
2		vw	. . 3
3		cvv 3106	. . 3
4		vt	. . . . . . . 8
5	4	cv 1397	. . . . . . 7
6	2	cv 1397	. . . . . . . 8
7		clss 17773	. . . . . . . 8
8	6, 7	cfv 5570	. . . . . . 7
9	5, 8	wcel 1823	. . . . . 6
10		vu	. . . . . . . 8
11	10	cv 1397	. . . . . . 7
12	11, 8	wcel 1823	. . . . . 6
13	9, 12	wa 367	. . . . 5 $/\$
14	5, 11	wpss 3462	. . . . . 6
15		vs	. . . . . . . . . . 11
16	15	cv 1397	. . . . . . . . . 10
17	5, 16	wpss 3462	. . . . . . . . 9
18	16, 11	wpss 3462	. . . . . . . . 9
19	17, 18	wa 367	. . . . . . . 8 $/\$
20	19, 15, 8	wrex 2805	. . . . . . 7 $/\$
21	20	wn 3	. . . . . 6 $/\$
22	14, 21	wa 367	. . . . 5 $/\$ $/\$
23	13, 22	wa 367	. . . 4 $/\$ $/\$ $/\$ $/\$
24	23, 4, 10	copab 4496	. . 3 $/\$ $/\$ $/\$ $/\$
25	2, 3, 24	cmpt 4497	. 2 $/\$ $/\$ $/\$ $/\$
26	1, 25	wceq 1398	1 _L $/\$ $/\$ $/\$ $/\$

Colors of variables: wff setvar class

This definition is referenced by: lcvfbr 35142

W3C validator