Definition df-edring-rN 39622

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	⊢ EDRingR = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {⟨(Base‘ndx), ((TEndo‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))⟩, ⟨(.r‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑡 ∘ 𝑠))⟩}))

Distinct variable group:   𝑤,𝑘,𝑓,𝑠,𝑡

Detailed syntax breakdown of Definition df-edring-rN

Step	Hyp	Ref	Expression
1		cedring-rN 39620	. 2 class EDRingR
2		vk	. . 3 setvar 𝑘
3		cvv 3474	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1540	. . . . 5 class 𝑘
6		clh 38850	. . . . 5 class LHyp
7	5, 6	cfv 6543	. . . 4 class (LHyp‘𝑘)
8		cnx 17125	. . . . . . 7 class ndx
9		cbs 17143	. . . . . . 7 class Base
10	8, 9	cfv 6543	. . . . . 6 class (Base‘ndx)
11	4	cv 1540	. . . . . . 7 class 𝑤
12		ctendo 39618	. . . . . . . 8 class TEndo
13	5, 12	cfv 6543	. . . . . . 7 class (TEndo‘𝑘)
14	11, 13	cfv 6543	. . . . . 6 class ((TEndo‘𝑘)‘𝑤)
15	10, 14	cop 4634	. . . . 5 class ⟨(Base‘ndx), ((TEndo‘𝑘)‘𝑤)⟩
16		cplusg 17196	. . . . . . 7 class +g
17	8, 16	cfv 6543	. . . . . 6 class (+g‘ndx)
18		vs	. . . . . . 7 setvar 𝑠
19		vt	. . . . . . 7 setvar 𝑡
20		vf	. . . . . . . 8 setvar 𝑓
21		cltrn 38967	. . . . . . . . . 10 class LTrn
22	5, 21	cfv 6543	. . . . . . . . 9 class (LTrn‘𝑘)
23	11, 22	cfv 6543	. . . . . . . 8 class ((LTrn‘𝑘)‘𝑤)
24	20	cv 1540	. . . . . . . . . 10 class 𝑓
25	18	cv 1540	. . . . . . . . . 10 class 𝑠
26	24, 25	cfv 6543	. . . . . . . . 9 class (𝑠‘𝑓)
27	19	cv 1540	. . . . . . . . . 10 class 𝑡
28	24, 27	cfv 6543	. . . . . . . . 9 class (𝑡‘𝑓)
29	26, 28	ccom 5680	. . . . . . . 8 class ((𝑠‘𝑓) ∘ (𝑡‘𝑓))
30	20, 23, 29	cmpt 5231	. . . . . . 7 class (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))
31	18, 19, 14, 14, 30	cmpo 7410	. . . . . 6 class (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))
32	17, 31	cop 4634	. . . . 5 class ⟨(+g‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))⟩
33		cmulr 17197	. . . . . . 7 class .r
34	8, 33	cfv 6543	. . . . . 6 class (.r‘ndx)
35	27, 25	ccom 5680	. . . . . . 7 class (𝑡 ∘ 𝑠)
36	18, 19, 14, 14, 35	cmpo 7410	. . . . . 6 class (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑡 ∘ 𝑠))
37	34, 36	cop 4634	. . . . 5 class ⟨(.r‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑡 ∘ 𝑠))⟩
38	15, 32, 37	ctp 4632	. . . 4 class {⟨(Base‘ndx), ((TEndo‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))⟩, ⟨(.r‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑡 ∘ 𝑠))⟩}
39	4, 7, 38	cmpt 5231	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ {⟨(Base‘ndx), ((TEndo‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))⟩, ⟨(.r‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑡 ∘ 𝑠))⟩})
40	2, 3, 39	cmpt 5231	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {⟨(Base‘ndx), ((TEndo‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))⟩, ⟨(.r‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑡 ∘ 𝑠))⟩}))
41	1, 40	wceq 1541	1 wff EDRingR = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {⟨(Base‘ndx), ((TEndo‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))⟩, ⟨(.r‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑡 ∘ 𝑠))⟩}))

This definition is referenced by:  erngfset-rN  39673