Metamath Proof Explorer

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 syl5eq ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑉 ) → 𝑌 = ( ( 𝑅 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 syl5req ⊢ ( 𝑥 ∈ 𝐼 → ( ·𝑖 ‘ ( ( 𝐼 × { ( ( 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 ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) ) ) = ( ·𝑖 ‘ 𝑌 ) )