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 ‘ 𝑤 ) ⟩ ) ) )