Metamath Proof Explorer


Theorem gsumdixp

Description: Distribute a binary product of sums to a sum of binary products in a ring. (Contributed by Mario Carneiro, 8-Mar-2015) (Revised by AV, 10-Jul-2019)

Ref Expression
Hypotheses gsumdixp.b 𝐵 = ( Base ‘ 𝑅 )
gsumdixp.t · = ( .r𝑅 )
gsumdixp.z 0 = ( 0g𝑅 )
gsumdixp.i ( 𝜑𝐼𝑉 )
gsumdixp.j ( 𝜑𝐽𝑊 )
gsumdixp.r ( 𝜑𝑅 ∈ Ring )
gsumdixp.x ( ( 𝜑𝑥𝐼 ) → 𝑋𝐵 )
gsumdixp.y ( ( 𝜑𝑦𝐽 ) → 𝑌𝐵 )
gsumdixp.xf ( 𝜑 → ( 𝑥𝐼𝑋 ) finSupp 0 )
gsumdixp.yf ( 𝜑 → ( 𝑦𝐽𝑌 ) finSupp 0 )
Assertion gsumdixp ( 𝜑 → ( ( 𝑅 Σg ( 𝑥𝐼𝑋 ) ) · ( 𝑅 Σg ( 𝑦𝐽𝑌 ) ) ) = ( 𝑅 Σg ( 𝑥𝐼 , 𝑦𝐽 ↦ ( 𝑋 · 𝑌 ) ) ) )

Proof

Step Hyp Ref Expression
1 gsumdixp.b 𝐵 = ( Base ‘ 𝑅 )
2 gsumdixp.t · = ( .r𝑅 )
3 gsumdixp.z 0 = ( 0g𝑅 )
4 gsumdixp.i ( 𝜑𝐼𝑉 )
5 gsumdixp.j ( 𝜑𝐽𝑊 )
6 gsumdixp.r ( 𝜑𝑅 ∈ Ring )
7 gsumdixp.x ( ( 𝜑𝑥𝐼 ) → 𝑋𝐵 )
8 gsumdixp.y ( ( 𝜑𝑦𝐽 ) → 𝑌𝐵 )
9 gsumdixp.xf ( 𝜑 → ( 𝑥𝐼𝑋 ) finSupp 0 )
10 gsumdixp.yf ( 𝜑 → ( 𝑦𝐽𝑌 ) finSupp 0 )
11 ringcmn ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
12 6 11 syl ( 𝜑𝑅 ∈ CMnd )
13 5 adantr ( ( 𝜑𝑖𝐼 ) → 𝐽𝑊 )
14 6 adantr ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) → 𝑅 ∈ Ring )
15 7 fmpttd ( 𝜑 → ( 𝑥𝐼𝑋 ) : 𝐼𝐵 )
16 simpl ( ( 𝑖𝐼𝑗𝐽 ) → 𝑖𝐼 )
17 ffvelrn ( ( ( 𝑥𝐼𝑋 ) : 𝐼𝐵𝑖𝐼 ) → ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) ∈ 𝐵 )
18 15 16 17 syl2an ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) → ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) ∈ 𝐵 )
19 8 fmpttd ( 𝜑 → ( 𝑦𝐽𝑌 ) : 𝐽𝐵 )
20 simpr ( ( 𝑖𝐼𝑗𝐽 ) → 𝑗𝐽 )
21 ffvelrn ( ( ( 𝑦𝐽𝑌 ) : 𝐽𝐵𝑗𝐽 ) → ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ∈ 𝐵 )
22 19 20 21 syl2an ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) → ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ∈ 𝐵 )
23 1 2 ringcl ( ( 𝑅 ∈ Ring ∧ ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) ∈ 𝐵 ∧ ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ∈ 𝐵 ) → ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) ∈ 𝐵 )
24 14 18 22 23 syl3anc ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) → ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) ∈ 𝐵 )
25 9 fsuppimpd ( 𝜑 → ( ( 𝑥𝐼𝑋 ) supp 0 ) ∈ Fin )
26 10 fsuppimpd ( 𝜑 → ( ( 𝑦𝐽𝑌 ) supp 0 ) ∈ Fin )
27 xpfi ( ( ( ( 𝑥𝐼𝑋 ) supp 0 ) ∈ Fin ∧ ( ( 𝑦𝐽𝑌 ) supp 0 ) ∈ Fin ) → ( ( ( 𝑥𝐼𝑋 ) supp 0 ) × ( ( 𝑦𝐽𝑌 ) supp 0 ) ) ∈ Fin )
28 25 26 27 syl2anc ( 𝜑 → ( ( ( 𝑥𝐼𝑋 ) supp 0 ) × ( ( 𝑦𝐽𝑌 ) supp 0 ) ) ∈ Fin )
29 ianor ( ¬ ( 𝑖 ∈ ( ( 𝑥𝐼𝑋 ) supp 0 ) ∧ 𝑗 ∈ ( ( 𝑦𝐽𝑌 ) supp 0 ) ) ↔ ( ¬ 𝑖 ∈ ( ( 𝑥𝐼𝑋 ) supp 0 ) ∨ ¬ 𝑗 ∈ ( ( 𝑦𝐽𝑌 ) supp 0 ) ) )
30 brxp ( 𝑖 ( ( ( 𝑥𝐼𝑋 ) supp 0 ) × ( ( 𝑦𝐽𝑌 ) supp 0 ) ) 𝑗 ↔ ( 𝑖 ∈ ( ( 𝑥𝐼𝑋 ) supp 0 ) ∧ 𝑗 ∈ ( ( 𝑦𝐽𝑌 ) supp 0 ) ) )
31 29 30 xchnxbir ( ¬ 𝑖 ( ( ( 𝑥𝐼𝑋 ) supp 0 ) × ( ( 𝑦𝐽𝑌 ) supp 0 ) ) 𝑗 ↔ ( ¬ 𝑖 ∈ ( ( 𝑥𝐼𝑋 ) supp 0 ) ∨ ¬ 𝑗 ∈ ( ( 𝑦𝐽𝑌 ) supp 0 ) ) )
32 simprl ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) → 𝑖𝐼 )
33 eldif ( 𝑖 ∈ ( 𝐼 ∖ ( ( 𝑥𝐼𝑋 ) supp 0 ) ) ↔ ( 𝑖𝐼 ∧ ¬ 𝑖 ∈ ( ( 𝑥𝐼𝑋 ) supp 0 ) ) )
34 33 biimpri ( ( 𝑖𝐼 ∧ ¬ 𝑖 ∈ ( ( 𝑥𝐼𝑋 ) supp 0 ) ) → 𝑖 ∈ ( 𝐼 ∖ ( ( 𝑥𝐼𝑋 ) supp 0 ) ) )
35 32 34 sylan ( ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) ∧ ¬ 𝑖 ∈ ( ( 𝑥𝐼𝑋 ) supp 0 ) ) → 𝑖 ∈ ( 𝐼 ∖ ( ( 𝑥𝐼𝑋 ) supp 0 ) ) )
36 15 adantr ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) → ( 𝑥𝐼𝑋 ) : 𝐼𝐵 )
37 ssidd ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) → ( ( 𝑥𝐼𝑋 ) supp 0 ) ⊆ ( ( 𝑥𝐼𝑋 ) supp 0 ) )
38 4 adantr ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) → 𝐼𝑉 )
39 3 fvexi 0 ∈ V
40 39 a1i ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) → 0 ∈ V )
41 36 37 38 40 suppssr ( ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) ∧ 𝑖 ∈ ( 𝐼 ∖ ( ( 𝑥𝐼𝑋 ) supp 0 ) ) ) → ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) = 0 )
42 35 41 syldan ( ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) ∧ ¬ 𝑖 ∈ ( ( 𝑥𝐼𝑋 ) supp 0 ) ) → ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) = 0 )
43 42 oveq1d ( ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) ∧ ¬ 𝑖 ∈ ( ( 𝑥𝐼𝑋 ) supp 0 ) ) → ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) = ( 0 · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) )
44 1 2 3 ringlz ( ( 𝑅 ∈ Ring ∧ ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ∈ 𝐵 ) → ( 0 · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) = 0 )
45 14 22 44 syl2anc ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) → ( 0 · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) = 0 )
46 45 adantr ( ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) ∧ ¬ 𝑖 ∈ ( ( 𝑥𝐼𝑋 ) supp 0 ) ) → ( 0 · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) = 0 )
47 43 46 eqtrd ( ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) ∧ ¬ 𝑖 ∈ ( ( 𝑥𝐼𝑋 ) supp 0 ) ) → ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) = 0 )
48 simprr ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) → 𝑗𝐽 )
49 eldif ( 𝑗 ∈ ( 𝐽 ∖ ( ( 𝑦𝐽𝑌 ) supp 0 ) ) ↔ ( 𝑗𝐽 ∧ ¬ 𝑗 ∈ ( ( 𝑦𝐽𝑌 ) supp 0 ) ) )
50 49 biimpri ( ( 𝑗𝐽 ∧ ¬ 𝑗 ∈ ( ( 𝑦𝐽𝑌 ) supp 0 ) ) → 𝑗 ∈ ( 𝐽 ∖ ( ( 𝑦𝐽𝑌 ) supp 0 ) ) )
51 48 50 sylan ( ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) ∧ ¬ 𝑗 ∈ ( ( 𝑦𝐽𝑌 ) supp 0 ) ) → 𝑗 ∈ ( 𝐽 ∖ ( ( 𝑦𝐽𝑌 ) supp 0 ) ) )
52 19 adantr ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) → ( 𝑦𝐽𝑌 ) : 𝐽𝐵 )
53 ssidd ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) → ( ( 𝑦𝐽𝑌 ) supp 0 ) ⊆ ( ( 𝑦𝐽𝑌 ) supp 0 ) )
54 5 adantr ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) → 𝐽𝑊 )
55 52 53 54 40 suppssr ( ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) ∧ 𝑗 ∈ ( 𝐽 ∖ ( ( 𝑦𝐽𝑌 ) supp 0 ) ) ) → ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) = 0 )
56 51 55 syldan ( ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) ∧ ¬ 𝑗 ∈ ( ( 𝑦𝐽𝑌 ) supp 0 ) ) → ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) = 0 )
57 56 oveq2d ( ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) ∧ ¬ 𝑗 ∈ ( ( 𝑦𝐽𝑌 ) supp 0 ) ) → ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) = ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) · 0 ) )
58 1 2 3 ringrz ( ( 𝑅 ∈ Ring ∧ ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) ∈ 𝐵 ) → ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) · 0 ) = 0 )
59 14 18 58 syl2anc ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) → ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) · 0 ) = 0 )
60 59 adantr ( ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) ∧ ¬ 𝑗 ∈ ( ( 𝑦𝐽𝑌 ) supp 0 ) ) → ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) · 0 ) = 0 )
61 57 60 eqtrd ( ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) ∧ ¬ 𝑗 ∈ ( ( 𝑦𝐽𝑌 ) supp 0 ) ) → ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) = 0 )
62 47 61 jaodan ( ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) ∧ ( ¬ 𝑖 ∈ ( ( 𝑥𝐼𝑋 ) supp 0 ) ∨ ¬ 𝑗 ∈ ( ( 𝑦𝐽𝑌 ) supp 0 ) ) ) → ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) = 0 )
63 31 62 sylan2b ( ( ( 𝜑 ∧ ( 𝑖𝐼𝑗𝐽 ) ) ∧ ¬ 𝑖 ( ( ( 𝑥𝐼𝑋 ) supp 0 ) × ( ( 𝑦𝐽𝑌 ) supp 0 ) ) 𝑗 ) → ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) = 0 )
64 63 anasss ( ( 𝜑 ∧ ( ( 𝑖𝐼𝑗𝐽 ) ∧ ¬ 𝑖 ( ( ( 𝑥𝐼𝑋 ) supp 0 ) × ( ( 𝑦𝐽𝑌 ) supp 0 ) ) 𝑗 ) ) → ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) = 0 )
65 1 3 12 4 13 24 28 64 gsum2d2 ( 𝜑 → ( 𝑅 Σg ( 𝑖𝐼 , 𝑗𝐽 ↦ ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) ) ) = ( 𝑅 Σg ( 𝑖𝐼 ↦ ( 𝑅 Σg ( 𝑗𝐽 ↦ ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) ) ) ) ) )
66 nffvmpt1 𝑥 ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 )
67 nfcv 𝑥 ·
68 nfcv 𝑥 ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 )
69 66 67 68 nfov 𝑥 ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) )
70 nfcv 𝑦 ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 )
71 nfcv 𝑦 ·
72 nffvmpt1 𝑦 ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 )
73 70 71 72 nfov 𝑦 ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) )
74 nfcv 𝑖 ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑥 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑦 ) )
75 nfcv 𝑗 ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑥 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑦 ) )
76 fveq2 ( 𝑖 = 𝑥 → ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) = ( ( 𝑥𝐼𝑋 ) ‘ 𝑥 ) )
77 fveq2 ( 𝑗 = 𝑦 → ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) = ( ( 𝑦𝐽𝑌 ) ‘ 𝑦 ) )
78 76 77 oveqan12d ( ( 𝑖 = 𝑥𝑗 = 𝑦 ) → ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) = ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑥 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑦 ) ) )
79 69 73 74 75 78 cbvmpo ( 𝑖𝐼 , 𝑗𝐽 ↦ ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) ) = ( 𝑥𝐼 , 𝑦𝐽 ↦ ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑥 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑦 ) ) )
80 simp2 ( ( 𝜑𝑥𝐼𝑦𝐽 ) → 𝑥𝐼 )
81 7 3adant3 ( ( 𝜑𝑥𝐼𝑦𝐽 ) → 𝑋𝐵 )
82 eqid ( 𝑥𝐼𝑋 ) = ( 𝑥𝐼𝑋 )
83 82 fvmpt2 ( ( 𝑥𝐼𝑋𝐵 ) → ( ( 𝑥𝐼𝑋 ) ‘ 𝑥 ) = 𝑋 )
84 80 81 83 syl2anc ( ( 𝜑𝑥𝐼𝑦𝐽 ) → ( ( 𝑥𝐼𝑋 ) ‘ 𝑥 ) = 𝑋 )
85 simp3 ( ( 𝜑𝑥𝐼𝑦𝐽 ) → 𝑦𝐽 )
86 eqid ( 𝑦𝐽𝑌 ) = ( 𝑦𝐽𝑌 )
87 86 fvmpt2 ( ( 𝑦𝐽𝑌𝐵 ) → ( ( 𝑦𝐽𝑌 ) ‘ 𝑦 ) = 𝑌 )
88 85 8 87 3imp3i2an ( ( 𝜑𝑥𝐼𝑦𝐽 ) → ( ( 𝑦𝐽𝑌 ) ‘ 𝑦 ) = 𝑌 )
89 84 88 oveq12d ( ( 𝜑𝑥𝐼𝑦𝐽 ) → ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑥 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑦 ) ) = ( 𝑋 · 𝑌 ) )
90 89 mpoeq3dva ( 𝜑 → ( 𝑥𝐼 , 𝑦𝐽 ↦ ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑥 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑦 ) ) ) = ( 𝑥𝐼 , 𝑦𝐽 ↦ ( 𝑋 · 𝑌 ) ) )
91 79 90 eqtrid ( 𝜑 → ( 𝑖𝐼 , 𝑗𝐽 ↦ ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) ) = ( 𝑥𝐼 , 𝑦𝐽 ↦ ( 𝑋 · 𝑌 ) ) )
92 91 oveq2d ( 𝜑 → ( 𝑅 Σg ( 𝑖𝐼 , 𝑗𝐽 ↦ ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) ) ) = ( 𝑅 Σg ( 𝑥𝐼 , 𝑦𝐽 ↦ ( 𝑋 · 𝑌 ) ) ) )
93 nfcv 𝑥 𝑅
94 nfcv 𝑥 Σg
95 nfcv 𝑥 𝐽
96 95 69 nfmpt 𝑥 ( 𝑗𝐽 ↦ ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) )
97 93 94 96 nfov 𝑥 ( 𝑅 Σg ( 𝑗𝐽 ↦ ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) ) )
98 nfcv 𝑖 ( 𝑅 Σg ( 𝑦𝐽 ↦ ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑥 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑦 ) ) ) )
99 76 oveq1d ( 𝑖 = 𝑥 → ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) = ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑥 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) )
100 99 mpteq2dv ( 𝑖 = 𝑥 → ( 𝑗𝐽 ↦ ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) ) = ( 𝑗𝐽 ↦ ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑥 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) ) )
101 nfcv 𝑦 ( ( 𝑥𝐼𝑋 ) ‘ 𝑥 )
102 101 71 72 nfov 𝑦 ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑥 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) )
103 77 oveq2d ( 𝑗 = 𝑦 → ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑥 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) = ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑥 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑦 ) ) )
104 102 75 103 cbvmpt ( 𝑗𝐽 ↦ ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑥 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) ) = ( 𝑦𝐽 ↦ ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑥 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑦 ) ) )
105 100 104 eqtrdi ( 𝑖 = 𝑥 → ( 𝑗𝐽 ↦ ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) ) = ( 𝑦𝐽 ↦ ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑥 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑦 ) ) ) )
106 105 oveq2d ( 𝑖 = 𝑥 → ( 𝑅 Σg ( 𝑗𝐽 ↦ ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) ) ) = ( 𝑅 Σg ( 𝑦𝐽 ↦ ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑥 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑦 ) ) ) ) )
107 97 98 106 cbvmpt ( 𝑖𝐼 ↦ ( 𝑅 Σg ( 𝑗𝐽 ↦ ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) ) ) ) = ( 𝑥𝐼 ↦ ( 𝑅 Σg ( 𝑦𝐽 ↦ ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑥 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑦 ) ) ) ) )
108 89 3expa ( ( ( 𝜑𝑥𝐼 ) ∧ 𝑦𝐽 ) → ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑥 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑦 ) ) = ( 𝑋 · 𝑌 ) )
109 108 mpteq2dva ( ( 𝜑𝑥𝐼 ) → ( 𝑦𝐽 ↦ ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑥 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑦 ) ) ) = ( 𝑦𝐽 ↦ ( 𝑋 · 𝑌 ) ) )
110 109 oveq2d ( ( 𝜑𝑥𝐼 ) → ( 𝑅 Σg ( 𝑦𝐽 ↦ ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑥 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑦 ) ) ) ) = ( 𝑅 Σg ( 𝑦𝐽 ↦ ( 𝑋 · 𝑌 ) ) ) )
111 110 mpteq2dva ( 𝜑 → ( 𝑥𝐼 ↦ ( 𝑅 Σg ( 𝑦𝐽 ↦ ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑥 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑦 ) ) ) ) ) = ( 𝑥𝐼 ↦ ( 𝑅 Σg ( 𝑦𝐽 ↦ ( 𝑋 · 𝑌 ) ) ) ) )
112 107 111 eqtrid ( 𝜑 → ( 𝑖𝐼 ↦ ( 𝑅 Σg ( 𝑗𝐽 ↦ ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) ) ) ) = ( 𝑥𝐼 ↦ ( 𝑅 Σg ( 𝑦𝐽 ↦ ( 𝑋 · 𝑌 ) ) ) ) )
113 112 oveq2d ( 𝜑 → ( 𝑅 Σg ( 𝑖𝐼 ↦ ( 𝑅 Σg ( 𝑗𝐽 ↦ ( ( ( 𝑥𝐼𝑋 ) ‘ 𝑖 ) · ( ( 𝑦𝐽𝑌 ) ‘ 𝑗 ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑥𝐼 ↦ ( 𝑅 Σg ( 𝑦𝐽 ↦ ( 𝑋 · 𝑌 ) ) ) ) ) )
114 65 92 113 3eqtr3d ( 𝜑 → ( 𝑅 Σg ( 𝑥𝐼 , 𝑦𝐽 ↦ ( 𝑋 · 𝑌 ) ) ) = ( 𝑅 Σg ( 𝑥𝐼 ↦ ( 𝑅 Σg ( 𝑦𝐽 ↦ ( 𝑋 · 𝑌 ) ) ) ) ) )
115 eqid ( +g𝑅 ) = ( +g𝑅 )
116 6 adantr ( ( 𝜑𝑥𝐼 ) → 𝑅 ∈ Ring )
117 5 adantr ( ( 𝜑𝑥𝐼 ) → 𝐽𝑊 )
118 8 adantlr ( ( ( 𝜑𝑥𝐼 ) ∧ 𝑦𝐽 ) → 𝑌𝐵 )
119 10 adantr ( ( 𝜑𝑥𝐼 ) → ( 𝑦𝐽𝑌 ) finSupp 0 )
120 1 3 115 2 116 117 7 118 119 gsummulc2 ( ( 𝜑𝑥𝐼 ) → ( 𝑅 Σg ( 𝑦𝐽 ↦ ( 𝑋 · 𝑌 ) ) ) = ( 𝑋 · ( 𝑅 Σg ( 𝑦𝐽𝑌 ) ) ) )
121 120 mpteq2dva ( 𝜑 → ( 𝑥𝐼 ↦ ( 𝑅 Σg ( 𝑦𝐽 ↦ ( 𝑋 · 𝑌 ) ) ) ) = ( 𝑥𝐼 ↦ ( 𝑋 · ( 𝑅 Σg ( 𝑦𝐽𝑌 ) ) ) ) )
122 121 oveq2d ( 𝜑 → ( 𝑅 Σg ( 𝑥𝐼 ↦ ( 𝑅 Σg ( 𝑦𝐽 ↦ ( 𝑋 · 𝑌 ) ) ) ) ) = ( 𝑅 Σg ( 𝑥𝐼 ↦ ( 𝑋 · ( 𝑅 Σg ( 𝑦𝐽𝑌 ) ) ) ) ) )
123 1 3 12 5 19 10 gsumcl ( 𝜑 → ( 𝑅 Σg ( 𝑦𝐽𝑌 ) ) ∈ 𝐵 )
124 1 3 115 2 6 4 123 7 9 gsummulc1 ( 𝜑 → ( 𝑅 Σg ( 𝑥𝐼 ↦ ( 𝑋 · ( 𝑅 Σg ( 𝑦𝐽𝑌 ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑥𝐼𝑋 ) ) · ( 𝑅 Σg ( 𝑦𝐽𝑌 ) ) ) )
125 114 122 124 3eqtrrd ( 𝜑 → ( ( 𝑅 Σg ( 𝑥𝐼𝑋 ) ) · ( 𝑅 Σg ( 𝑦𝐽𝑌 ) ) ) = ( 𝑅 Σg ( 𝑥𝐼 , 𝑦𝐽 ↦ ( 𝑋 · 𝑌 ) ) ) )