MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-sra Structured version   Visualization version   GIF version

Definition df-sra 19935
Description: Any ring can be regarded as a left algebra over any of its subrings. The function subringAlg associates with any ring and any of its subrings the left algebra consisting in the ring itself regarded as a left algebra over the subring. It has an inner product which is simply the ring product. (Contributed by Mario Carneiro, 27-Nov-2014.) (Revised by Thierry Arnoux, 16-Jun-2019.)
Assertion
Ref Expression
df-sra subringAlg = (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ (((𝑤 sSet ⟨(Scalar‘ndx), (𝑤s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r𝑤)⟩) sSet ⟨(·𝑖‘ndx), (.r𝑤)⟩)))
Distinct variable group:   𝑤,𝑠

Detailed syntax breakdown of Definition df-sra
StepHypRef Expression
1 csra 19931 . 2 class subringAlg
2 vw . . 3 setvar 𝑤
3 cvv 3469 . . 3 class V
4 vs . . . 4 setvar 𝑠
52cv 1537 . . . . . 6 class 𝑤
6 cbs 16474 . . . . . 6 class Base
75, 6cfv 6334 . . . . 5 class (Base‘𝑤)
87cpw 4511 . . . 4 class 𝒫 (Base‘𝑤)
9 cnx 16471 . . . . . . . . 9 class ndx
10 csca 16559 . . . . . . . . 9 class Scalar
119, 10cfv 6334 . . . . . . . 8 class (Scalar‘ndx)
124cv 1537 . . . . . . . . 9 class 𝑠
13 cress 16475 . . . . . . . . 9 class s
145, 12, 13co 7140 . . . . . . . 8 class (𝑤s 𝑠)
1511, 14cop 4545 . . . . . . 7 class ⟨(Scalar‘ndx), (𝑤s 𝑠)⟩
16 csts 16472 . . . . . . 7 class sSet
175, 15, 16co 7140 . . . . . 6 class (𝑤 sSet ⟨(Scalar‘ndx), (𝑤s 𝑠)⟩)
18 cvsca 16560 . . . . . . . 8 class ·𝑠
199, 18cfv 6334 . . . . . . 7 class ( ·𝑠 ‘ndx)
20 cmulr 16557 . . . . . . . 8 class .r
215, 20cfv 6334 . . . . . . 7 class (.r𝑤)
2219, 21cop 4545 . . . . . 6 class ⟨( ·𝑠 ‘ndx), (.r𝑤)⟩
2317, 22, 16co 7140 . . . . 5 class ((𝑤 sSet ⟨(Scalar‘ndx), (𝑤s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r𝑤)⟩)
24 cip 16561 . . . . . . 7 class ·𝑖
259, 24cfv 6334 . . . . . 6 class (·𝑖‘ndx)
2625, 21cop 4545 . . . . 5 class ⟨(·𝑖‘ndx), (.r𝑤)⟩
2723, 26, 16co 7140 . . . 4 class (((𝑤 sSet ⟨(Scalar‘ndx), (𝑤s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r𝑤)⟩) sSet ⟨(·𝑖‘ndx), (.r𝑤)⟩)
284, 8, 27cmpt 5122 . . 3 class (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ (((𝑤 sSet ⟨(Scalar‘ndx), (𝑤s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r𝑤)⟩) sSet ⟨(·𝑖‘ndx), (.r𝑤)⟩))
292, 3, 28cmpt 5122 . 2 class (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ (((𝑤 sSet ⟨(Scalar‘ndx), (𝑤s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r𝑤)⟩) sSet ⟨(·𝑖‘ndx), (.r𝑤)⟩)))
301, 29wceq 1538 1 wff subringAlg = (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ (((𝑤 sSet ⟨(Scalar‘ndx), (𝑤s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r𝑤)⟩) sSet ⟨(·𝑖‘ndx), (.r𝑤)⟩)))
Colors of variables: wff setvar class
This definition is referenced by:  sraval  19939
  Copyright terms: Public domain W3C validator