Definition df-edring 40759

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

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

Detailed syntax breakdown of Definition df-edring

Step	Hyp	Ref	Expression
1		cedring 40755	. 2 class EDRing
2		vk	. . 3 setvar 𝑘
3		cvv 3480	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1539	. . . . 5 class 𝑘
6		clh 39986	. . . . 5 class LHyp
7	5, 6	cfv 6561	. . . 4 class (LHyp‘𝑘)
8		cnx 17230	. . . . . . 7 class ndx
9		cbs 17247	. . . . . . 7 class Base
10	8, 9	cfv 6561	. . . . . 6 class (Base‘ndx)
11	4	cv 1539	. . . . . . 7 class 𝑤
12		ctendo 40754	. . . . . . . 8 class TEndo
13	5, 12	cfv 6561	. . . . . . 7 class (TEndo‘𝑘)
14	11, 13	cfv 6561	. . . . . 6 class ((TEndo‘𝑘)‘𝑤)
15	10, 14	cop 4632	. . . . 5 class ⟨(Base‘ndx), ((TEndo‘𝑘)‘𝑤)⟩
16		cplusg 17297	. . . . . . 7 class +g
17	8, 16	cfv 6561	. . . . . 6 class (+g‘ndx)
18		vs	. . . . . . 7 setvar 𝑠
19		vt	. . . . . . 7 setvar 𝑡
20		vf	. . . . . . . 8 setvar 𝑓
21		cltrn 40103	. . . . . . . . . 10 class LTrn
22	5, 21	cfv 6561	. . . . . . . . 9 class (LTrn‘𝑘)
23	11, 22	cfv 6561	. . . . . . . 8 class ((LTrn‘𝑘)‘𝑤)
24	20	cv 1539	. . . . . . . . . 10 class 𝑓
25	18	cv 1539	. . . . . . . . . 10 class 𝑠
26	24, 25	cfv 6561	. . . . . . . . 9 class (𝑠‘𝑓)
27	19	cv 1539	. . . . . . . . . 10 class 𝑡
28	24, 27	cfv 6561	. . . . . . . . 9 class (𝑡‘𝑓)
29	26, 28	ccom 5689	. . . . . . . 8 class ((𝑠‘𝑓) ∘ (𝑡‘𝑓))
30	20, 23, 29	cmpt 5225	. . . . . . 7 class (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))
31	18, 19, 14, 14, 30	cmpo 7433	. . . . . 6 class (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))
32	17, 31	cop 4632	. . . . 5 class ⟨(+g‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))⟩
33		cmulr 17298	. . . . . . 7 class .r
34	8, 33	cfv 6561	. . . . . 6 class (.r‘ndx)
35	25, 27	ccom 5689	. . . . . . 7 class (𝑠 ∘ 𝑡)
36	18, 19, 14, 14, 35	cmpo 7433	. . . . . 6 class (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑠 ∘ 𝑡))
37	34, 36	cop 4632	. . . . 5 class ⟨(.r‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑠 ∘ 𝑡))⟩
38	15, 32, 37	ctp 4630	. . . 4 class {⟨(Base‘ndx), ((TEndo‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))⟩, ⟨(.r‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑠 ∘ 𝑡))⟩}
39	4, 7, 38	cmpt 5225	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ {⟨(Base‘ndx), ((TEndo‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))⟩, ⟨(.r‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑠 ∘ 𝑡))⟩})
40	2, 3, 39	cmpt 5225	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {⟨(Base‘ndx), ((TEndo‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))⟩, ⟨(.r‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑠 ∘ 𝑡))⟩}))
41	1, 40	wceq 1540	1 wff EDRing = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {⟨(Base‘ndx), ((TEndo‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))⟩, ⟨(.r‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑠 ∘ 𝑡))⟩}))

This definition is referenced by:  erngfset  40801