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