df-edring - Mathbox for Norm Megill

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

Definition df-edring 36584

Description: Define division ring on trace-preserving endomorphisms. The multiplication operation is reversed composition, per the definition of E of [Crawley] p. 117, 4th line from bottom. (Contributed by NM, 8-Jun-2013.)

**Assertion**
Ref	Expression
df-edring

Distinct variable group:

**Detailed syntax breakdown of Definition df-edring**
Step	Hyp	Ref	Expression
1		cedring 36580	. 2
2		vk	. . 3
3		cvv 3109	. . 3
4		vw	. . . 4
5	2	cv 1394	. . . . 5
6		clh 35809	. . . . 5
7	5, 6	cfv 5594	. . . 4
8		cnx 14640	. . . . . . 7
9		cbs 14643	. . . . . . 7
10	8, 9	cfv 5594	. . . . . 6
11	4	cv 1394	. . . . . . 7
12		ctendo 36579	. . . . . . . 8
13	5, 12	cfv 5594	. . . . . . 7
14	11, 13	cfv 5594	. . . . . 6
15	10, 14	cop 4038	. . . . 5
16		cplusg 14711	. . . . . . 7
17	8, 16	cfv 5594	. . . . . 6
18		vs	. . . . . . 7
19		vt	. . . . . . 7
20		vf	. . . . . . . 8
21		cltrn 35926	. . . . . . . . . 10
22	5, 21	cfv 5594	. . . . . . . . 9
23	11, 22	cfv 5594	. . . . . . . 8
24	20	cv 1394	. . . . . . . . . 10
25	18	cv 1394	. . . . . . . . . 10
26	24, 25	cfv 5594	. . . . . . . . 9
27	19	cv 1394	. . . . . . . . . 10
28	24, 27	cfv 5594	. . . . . . . . 9
29	26, 28	ccom 5012	. . . . . . . 8
30	20, 23, 29	cmpt 4515	. . . . . . 7
31	18, 19, 14, 14, 30	cmpt2 6298	. . . . . 6
32	17, 31	cop 4038	. . . . 5
33		cmulr 14712	. . . . . . 7
34	8, 33	cfv 5594	. . . . . 6
35	25, 27	ccom 5012	. . . . . . 7
36	18, 19, 14, 14, 35	cmpt2 6298	. . . . . 6
37	34, 36	cop 4038	. . . . 5
38	15, 32, 37	ctp 4036	. . . 4
39	4, 7, 38	cmpt 4515	. . 3
40	2, 3, 39	cmpt 4515	. 2
41	1, 40	wceq 1395	1

Colors of variables: wff setvar class

This definition is referenced by: erngfset 36626

W3C validator