Theorem frlmip

Description: The inner product of a free module. (Contributed by Thierry Arnoux, 20-Jun-2019)

	Ref	Expression
Hypotheses	frlmphl.y	⊢ 𝑌 = ( 𝑅 freeLMod 𝐼 )
	frlmphl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	frlmphl.t	⊢ · = ( .r ‘ 𝑅 )
Assertion	frlmip	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑓 ∈ ( 𝐵 ↑m 𝐼 ) , 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) ) ) = ( ·𝑖 ‘ 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		frlmphl.y	⊢ 𝑌 = ( 𝑅 freeLMod 𝐼 )
2		frlmphl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		frlmphl.t	⊢ · = ( .r ‘ 𝑅 )
4		eqid	⊢ ( 𝑅 freeLMod 𝐼 ) = ( 𝑅 freeLMod 𝐼 )
5		eqid	⊢ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) = ( Base ‘ ( 𝑅 freeLMod 𝐼 ) )
6	4 5	frlmpws	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝑅 freeLMod 𝐼 ) = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) )
7	6	ancoms	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 freeLMod 𝐼 ) = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) )
8	2	ressid	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↾s 𝐵 ) = 𝑅 )
9		eqidd	⊢ ( 𝑅 ∈ 𝑉 → ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) = ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) )
10	2	eqimssi	⊢ 𝐵 ⊆ ( Base ‘ 𝑅 )
11	10	a1i	⊢ ( 𝑅 ∈ 𝑉 → 𝐵 ⊆ ( Base ‘ 𝑅 ) )
12	9 11	srasca	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↾s 𝐵 ) = ( Scalar ‘ ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) ) )
13	8 12	eqtr3d	⊢ ( 𝑅 ∈ 𝑉 → 𝑅 = ( Scalar ‘ ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) ) )
14	13	oveq1d	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) = ( ( Scalar ‘ ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) ) Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) )
15	14	adantl	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) = ( ( Scalar ‘ ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) ) Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) )
16		fvex	⊢ ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) ∈ V
17		rlmval	⊢ ( ringLMod ‘ 𝑅 ) = ( ( subringAlg ‘ 𝑅 ) ‘ ( Base ‘ 𝑅 ) )
18	2	fveq2i	⊢ ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) = ( ( subringAlg ‘ 𝑅 ) ‘ ( Base ‘ 𝑅 ) )
19	17 18	eqtr4i	⊢ ( ringLMod ‘ 𝑅 ) = ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 )
20	19	oveq1i	⊢ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) ↑s 𝐼 )
21		eqid	⊢ ( Scalar ‘ ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) ) = ( Scalar ‘ ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) )
22	20 21	pwsval	⊢ ( ( ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) ∈ V ∧ 𝐼 ∈ 𝑊 ) → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( Scalar ‘ ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) ) Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) )
23	16 22	mpan	⊢ ( 𝐼 ∈ 𝑊 → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( Scalar ‘ ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) ) Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) )
24	23	adantr	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑉 ) → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( Scalar ‘ ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) ) Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) )
25	15 24	eqtr4d	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) = ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) )
26	1	fveq2i	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ ( 𝑅 freeLMod 𝐼 ) )
27	26	a1i	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑉 ) → ( Base ‘ 𝑌 ) = ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
28	25 27	oveq12d	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) ↾s ( Base ‘ 𝑌 ) ) = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) )
29	7 28	eqtr4d	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 freeLMod 𝐼 ) = ( ( 𝑅 Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) ↾s ( Base ‘ 𝑌 ) ) )
30	1 29	eqtrid	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑉 ) → 𝑌 = ( ( 𝑅 Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) ↾s ( Base ‘ 𝑌 ) ) )
31	30	fveq2d	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑉 ) → ( ·𝑖 ‘ 𝑌 ) = ( ·𝑖 ‘ ( ( 𝑅 Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) ↾s ( Base ‘ 𝑌 ) ) ) )
32		fvex	⊢ ( Base ‘ 𝑌 ) ∈ V
33		eqid	⊢ ( ( 𝑅 Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) ↾s ( Base ‘ 𝑌 ) ) = ( ( 𝑅 Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) ↾s ( Base ‘ 𝑌 ) )
34		eqid	⊢ ( ·𝑖 ‘ ( 𝑅 Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) ) = ( ·𝑖 ‘ ( 𝑅 Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) )
35	33 34	ressip	⊢ ( ( Base ‘ 𝑌 ) ∈ V → ( ·𝑖 ‘ ( 𝑅 Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) ) = ( ·𝑖 ‘ ( ( 𝑅 Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) ↾s ( Base ‘ 𝑌 ) ) ) )
36	32 35	ax-mp	⊢ ( ·𝑖 ‘ ( 𝑅 Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) ) = ( ·𝑖 ‘ ( ( 𝑅 Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) ↾s ( Base ‘ 𝑌 ) ) )
37		eqid	⊢ ( 𝑅 Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) = ( 𝑅 Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) )
38		simpr	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑉 ) → 𝑅 ∈ 𝑉 )
39		snex	⊢ { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ∈ V
40		xpexg	⊢ ( ( 𝐼 ∈ 𝑊 ∧ { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ∈ V ) → ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ∈ V )
41	39 40	mpan2	⊢ ( 𝐼 ∈ 𝑊 → ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ∈ V )
42	41	adantr	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑉 ) → ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ∈ V )
43		eqid	⊢ ( Base ‘ ( 𝑅 Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) ) = ( Base ‘ ( 𝑅 Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) )
44	16	snnz	⊢ { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ≠ ∅
45		dmxp	⊢ ( { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ≠ ∅ → dom ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) = 𝐼 )
46	44 45	mp1i	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑉 ) → dom ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) = 𝐼 )
47	37 38 42 43 46 34	prdsip	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑉 ) → ( ·𝑖 ‘ ( 𝑅 Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) ) = ( 𝑓 ∈ ( Base ‘ ( 𝑅 Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) ) , 𝑔 ∈ ( Base ‘ ( 𝑅 Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) ) ↦ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
48	37 38 42 43 46	prdsbas	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑉 ) → ( Base ‘ ( 𝑅 Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) ) = X 𝑥 ∈ 𝐼 ( Base ‘ ( ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ‘ 𝑥 ) ) )
49		eqidd	⊢ ( 𝑥 ∈ 𝐼 → ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) = ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) )
50	10	a1i	⊢ ( 𝑥 ∈ 𝐼 → 𝐵 ⊆ ( Base ‘ 𝑅 ) )
51	49 50	srabase	⊢ ( 𝑥 ∈ 𝐼 → ( Base ‘ 𝑅 ) = ( Base ‘ ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) ) )
52	2	a1i	⊢ ( 𝑥 ∈ 𝐼 → 𝐵 = ( Base ‘ 𝑅 ) )
53	16	fvconst2	⊢ ( 𝑥 ∈ 𝐼 → ( ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ‘ 𝑥 ) = ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) )
54	53	fveq2d	⊢ ( 𝑥 ∈ 𝐼 → ( Base ‘ ( ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ‘ 𝑥 ) ) = ( Base ‘ ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) ) )
55	51 52 54	3eqtr4rd	⊢ ( 𝑥 ∈ 𝐼 → ( Base ‘ ( ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ‘ 𝑥 ) ) = 𝐵 )
56	55	adantl	⊢ ( ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐼 ) → ( Base ‘ ( ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ‘ 𝑥 ) ) = 𝐵 )
57	56	ixpeq2dva	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑉 ) → X 𝑥 ∈ 𝐼 ( Base ‘ ( ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ‘ 𝑥 ) ) = X 𝑥 ∈ 𝐼 𝐵 )
58	2	fvexi	⊢ 𝐵 ∈ V
59		ixpconstg	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝐵 ∈ V ) → X 𝑥 ∈ 𝐼 𝐵 = ( 𝐵 ↑m 𝐼 ) )
60	58 59	mpan2	⊢ ( 𝐼 ∈ 𝑊 → X 𝑥 ∈ 𝐼 𝐵 = ( 𝐵 ↑m 𝐼 ) )
61	60	adantr	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑉 ) → X 𝑥 ∈ 𝐼 𝐵 = ( 𝐵 ↑m 𝐼 ) )
62	48 57 61	3eqtrd	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑉 ) → ( Base ‘ ( 𝑅 Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) ) = ( 𝐵 ↑m 𝐼 ) )
63	53 50	sraip	⊢ ( 𝑥 ∈ 𝐼 → ( .r ‘ 𝑅 ) = ( ·𝑖 ‘ ( ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ‘ 𝑥 ) ) )
64	3 63	eqtr2id	⊢ ( 𝑥 ∈ 𝐼 → ( ·𝑖 ‘ ( ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ‘ 𝑥 ) ) = · )
65	64	oveqd	⊢ ( 𝑥 ∈ 𝐼 → ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) )
66	65	mpteq2ia	⊢ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) )
67	66	oveq2i	⊢ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) )
68	67	a1i	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) ) )
69	62 62 68	mpoeq123dv	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑓 ∈ ( Base ‘ ( 𝑅 Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) ) , 𝑔 ∈ ( Base ‘ ( 𝑅 Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) ) ↦ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) = ( 𝑓 ∈ ( 𝐵 ↑m 𝐼 ) , 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
70	47 69	eqtrd	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑉 ) → ( ·𝑖 ‘ ( 𝑅 Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) ) = ( 𝑓 ∈ ( 𝐵 ↑m 𝐼 ) , 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
71	36 70	eqtr3id	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑉 ) → ( ·𝑖 ‘ ( ( 𝑅 Xs ( 𝐼 × { ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) } ) ) ↾s ( Base ‘ 𝑌 ) ) ) = ( 𝑓 ∈ ( 𝐵 ↑m 𝐼 ) , 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
72	31 71	eqtr2d	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑓 ∈ ( 𝐵 ↑m 𝐼 ) , 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) ) ) = ( ·𝑖 ‘ 𝑌 ) )