df-edring-rN - Mathbox for Norm Megill

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

Definition df-edring-rN 36044

Description: Define division ring on trace-preserving endomorphisms. Definition of E of [Crawley] p. 117, 4th line from bottom. (Contributed by NM, 8-Jun-2013.)

**Assertion**
Ref	Expression
df-edring-rN

Distinct variable group:

**Detailed syntax breakdown of Definition df-edring-rN**
Step	Hyp	Ref	Expression
1		cedring-rN 36042	. 2
2		vk	. . 3
3		cvv 3200	. . 3
4		vw	. . . 4
5	2	cv 1482	. . . . 5
6		clh 35270	. . . . 5
7	5, 6	cfv 5888	. . . 4
8		cnx 15854	. . . . . . 7
9		cbs 15857	. . . . . . 7
10	8, 9	cfv 5888	. . . . . 6
11	4	cv 1482	. . . . . . 7
12		ctendo 36040	. . . . . . . 8
13	5, 12	cfv 5888	. . . . . . 7
14	11, 13	cfv 5888	. . . . . 6
15	10, 14	cop 4183	. . . . 5
16		cplusg 15941	. . . . . . 7
17	8, 16	cfv 5888	. . . . . 6
18		vs	. . . . . . 7
19		vt	. . . . . . 7
20		vf	. . . . . . . 8
21		cltrn 35387	. . . . . . . . . 10
22	5, 21	cfv 5888	. . . . . . . . 9
23	11, 22	cfv 5888	. . . . . . . 8
24	20	cv 1482	. . . . . . . . . 10
25	18	cv 1482	. . . . . . . . . 10
26	24, 25	cfv 5888	. . . . . . . . 9
27	19	cv 1482	. . . . . . . . . 10
28	24, 27	cfv 5888	. . . . . . . . 9
29	26, 28	ccom 5118	. . . . . . . 8
30	20, 23, 29	cmpt 4729	. . . . . . 7
31	18, 19, 14, 14, 30	cmpt2 6652	. . . . . 6
32	17, 31	cop 4183	. . . . 5
33		cmulr 15942	. . . . . . 7
34	8, 33	cfv 5888	. . . . . 6
35	27, 25	ccom 5118	. . . . . . 7
36	18, 19, 14, 14, 35	cmpt2 6652	. . . . . 6
37	34, 36	cop 4183	. . . . 5
38	15, 32, 37	ctp 4181	. . . 4
39	4, 7, 38	cmpt 4729	. . 3
40	2, 3, 39	cmpt 4729	. 2
41	1, 40	wceq 1483	1

Colors of variables: wff setvar class

This definition is referenced by: erngfset-rN 36095

W3C validator