This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-sra

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)

Ref Expression
Assertion df-sra subringAlg = ( 𝑤 ∈ V ↦ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ( ( ( 𝑤 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑤 ↾s 𝑠 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩ ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csra ⊢ subringAlg
1 vw ⊢ 𝑤
2 cvv ⊢ V
3 vs ⊢ 𝑠
4 cbs ⊢ Base
5 1 cv ⊢ 𝑤
6 5 4 cfv ⊢ ( Base ‘ 𝑤 )
7 6 cpw ⊢ 𝒫 ( Base ‘ 𝑤 )
8 csts ⊢ sSet
9 csca ⊢ Scalar
10 cnx ⊢ ndx
11 10 9 cfv ⊢ ( Scalar ‘ ndx )
12 cress ⊢ ↾s
13 3 cv ⊢ 𝑠
14 5 13 12 co ⊢ ( 𝑤 ↾s 𝑠 )
15 11 14 cop ⊢ ⟨ ( Scalar ‘ ndx ) , ( 𝑤 ↾s 𝑠 ) ⟩
16 5 15 8 co ⊢ ( 𝑤 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑤 ↾s 𝑠 ) ⟩ )
17 cvsca ⊢ ·𝑠
18 10 17 cfv ⊢ ( ·𝑠 ‘ ndx )
19 cmulr ⊢ .r
20 5 19 cfv ⊢ ( .r ‘ 𝑤 )
21 18 20 cop ⊢ ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩
22 16 21 8 co ⊢ ( ( 𝑤 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑤 ↾s 𝑠 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩ )
23 cip ⊢ ·𝑖
24 10 23 cfv ⊢ ( ·𝑖 ‘ ndx )
25 24 20 cop ⊢ ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩
26 22 25 8 co ⊢ ( ( ( 𝑤 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑤 ↾s 𝑠 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩ )
27 3 7 26 cmpt ⊢ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ( ( ( 𝑤 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑤 ↾s 𝑠 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩ ) )
28 1 2 27 cmpt ⊢ ( 𝑤 ∈ V ↦ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ( ( ( 𝑤 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑤 ↾s 𝑠 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩ ) ) )
29 0 28 wceq ⊢ subringAlg = ( 𝑤 ∈ V ↦ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ( ( ( 𝑤 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑤 ↾s 𝑠 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩ ) ) )