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 syl5eq ⊢ ( 𝜑 → ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ 𝑖 ) · ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ 𝑗 ) ) ) = ( 𝑥 ∈ 𝐼 , 𝑦 ∈ 𝐽 ↦ ( 𝑋 · 𝑌 ) ) )
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 syl5eq ⊢ ( 𝜑 → ( 𝑖 ∈ 𝐼 ↦ ( 𝑅 Σ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 ( 𝑥 ∈ 𝐼 , 𝑦 ∈ 𝐽 ↦ ( 𝑋 · 𝑌 ) ) ) )