Metamath Proof Explorer


Theorem psrass1

Description: Associative identity for the ring of power series. (Contributed by Mario Carneiro, 5-Jan-2015)

Ref Expression
Hypotheses psrring.s 𝑆 = ( 𝐼 mPwSer 𝑅 )
psrring.i ( 𝜑𝐼𝑉 )
psrring.r ( 𝜑𝑅 ∈ Ring )
psrass.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
psrass.t × = ( .r𝑆 )
psrass.b 𝐵 = ( Base ‘ 𝑆 )
psrass.x ( 𝜑𝑋𝐵 )
psrass.y ( 𝜑𝑌𝐵 )
psrass.z ( 𝜑𝑍𝐵 )
Assertion psrass1 ( 𝜑 → ( ( 𝑋 × 𝑌 ) × 𝑍 ) = ( 𝑋 × ( 𝑌 × 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 psrring.s 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psrring.i ( 𝜑𝐼𝑉 )
3 psrring.r ( 𝜑𝑅 ∈ Ring )
4 psrass.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
5 psrass.t × = ( .r𝑆 )
6 psrass.b 𝐵 = ( Base ‘ 𝑆 )
7 psrass.x ( 𝜑𝑋𝐵 )
8 psrass.y ( 𝜑𝑌𝐵 )
9 psrass.z ( 𝜑𝑍𝐵 )
10 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
11 1 6 5 3 7 8 psrmulcl ( 𝜑 → ( 𝑋 × 𝑌 ) ∈ 𝐵 )
12 1 6 5 3 11 9 psrmulcl ( 𝜑 → ( ( 𝑋 × 𝑌 ) × 𝑍 ) ∈ 𝐵 )
13 1 10 4 6 12 psrelbas ( 𝜑 → ( ( 𝑋 × 𝑌 ) × 𝑍 ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
14 13 ffnd ( 𝜑 → ( ( 𝑋 × 𝑌 ) × 𝑍 ) Fn 𝐷 )
15 1 6 5 3 8 9 psrmulcl ( 𝜑 → ( 𝑌 × 𝑍 ) ∈ 𝐵 )
16 1 6 5 3 7 15 psrmulcl ( 𝜑 → ( 𝑋 × ( 𝑌 × 𝑍 ) ) ∈ 𝐵 )
17 1 10 4 6 16 psrelbas ( 𝜑 → ( 𝑋 × ( 𝑌 × 𝑍 ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
18 17 ffnd ( 𝜑 → ( 𝑋 × ( 𝑌 × 𝑍 ) ) Fn 𝐷 )
19 eqid { 𝑔𝐷𝑔r𝑥 } = { 𝑔𝐷𝑔r𝑥 }
20 simpr ( ( 𝜑𝑥𝐷 ) → 𝑥𝐷 )
21 ringcmn ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
22 3 21 syl ( 𝜑𝑅 ∈ CMnd )
23 22 adantr ( ( 𝜑𝑥𝐷 ) → 𝑅 ∈ CMnd )
24 3 ad2antrr ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) → 𝑅 ∈ Ring )
25 24 adantr ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ) → 𝑅 ∈ Ring )
26 1 10 4 6 7 psrelbas ( 𝜑𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
27 26 ad2antrr ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
28 simpr ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) → 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } )
29 breq1 ( 𝑔 = 𝑗 → ( 𝑔r𝑥𝑗r𝑥 ) )
30 29 elrab ( 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ↔ ( 𝑗𝐷𝑗r𝑥 ) )
31 28 30 sylib ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) → ( 𝑗𝐷𝑗r𝑥 ) )
32 31 simpld ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) → 𝑗𝐷 )
33 27 32 ffvelrnd ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) → ( 𝑋𝑗 ) ∈ ( Base ‘ 𝑅 ) )
34 33 adantr ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ) → ( 𝑋𝑗 ) ∈ ( Base ‘ 𝑅 ) )
35 1 10 4 6 8 psrelbas ( 𝜑𝑌 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
36 35 ad3antrrr ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ) → 𝑌 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
37 simpr ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ) → 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } )
38 breq1 ( = 𝑛 → ( r ≤ ( 𝑥f𝑗 ) ↔ 𝑛r ≤ ( 𝑥f𝑗 ) ) )
39 38 elrab ( 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ↔ ( 𝑛𝐷𝑛r ≤ ( 𝑥f𝑗 ) ) )
40 37 39 sylib ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ) → ( 𝑛𝐷𝑛r ≤ ( 𝑥f𝑗 ) ) )
41 40 simpld ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ) → 𝑛𝐷 )
42 36 41 ffvelrnd ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ) → ( 𝑌𝑛 ) ∈ ( Base ‘ 𝑅 ) )
43 1 10 4 6 9 psrelbas ( 𝜑𝑍 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
44 43 ad3antrrr ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ) → 𝑍 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
45 simplr ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) → 𝑥𝐷 )
46 4 psrbagf ( 𝑗𝐷𝑗 : 𝐼 ⟶ ℕ0 )
47 32 46 syl ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) → 𝑗 : 𝐼 ⟶ ℕ0 )
48 31 simprd ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) → 𝑗r𝑥 )
49 4 psrbagcon ( ( 𝑥𝐷𝑗 : 𝐼 ⟶ ℕ0𝑗r𝑥 ) → ( ( 𝑥f𝑗 ) ∈ 𝐷 ∧ ( 𝑥f𝑗 ) ∘r𝑥 ) )
50 45 47 48 49 syl3anc ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) → ( ( 𝑥f𝑗 ) ∈ 𝐷 ∧ ( 𝑥f𝑗 ) ∘r𝑥 ) )
51 50 simpld ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) → ( 𝑥f𝑗 ) ∈ 𝐷 )
52 51 adantr ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ) → ( 𝑥f𝑗 ) ∈ 𝐷 )
53 4 psrbagf ( 𝑛𝐷𝑛 : 𝐼 ⟶ ℕ0 )
54 41 53 syl ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ) → 𝑛 : 𝐼 ⟶ ℕ0 )
55 40 simprd ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ) → 𝑛r ≤ ( 𝑥f𝑗 ) )
56 4 psrbagcon ( ( ( 𝑥f𝑗 ) ∈ 𝐷𝑛 : 𝐼 ⟶ ℕ0𝑛r ≤ ( 𝑥f𝑗 ) ) → ( ( ( 𝑥f𝑗 ) ∘f𝑛 ) ∈ 𝐷 ∧ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ∘r ≤ ( 𝑥f𝑗 ) ) )
57 52 54 55 56 syl3anc ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ) → ( ( ( 𝑥f𝑗 ) ∘f𝑛 ) ∈ 𝐷 ∧ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ∘r ≤ ( 𝑥f𝑗 ) ) )
58 57 simpld ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ) → ( ( 𝑥f𝑗 ) ∘f𝑛 ) ∈ 𝐷 )
59 44 58 ffvelrnd ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ) → ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ∈ ( Base ‘ 𝑅 ) )
60 eqid ( .r𝑅 ) = ( .r𝑅 )
61 10 60 ringcl ( ( 𝑅 ∈ Ring ∧ ( 𝑌𝑛 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) ∈ ( Base ‘ 𝑅 ) )
62 25 42 59 61 syl3anc ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ) → ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) ∈ ( Base ‘ 𝑅 ) )
63 10 60 ringcl ( ( 𝑅 ∈ Ring ∧ ( 𝑋𝑗 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑋𝑗 ) ( .r𝑅 ) ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
64 25 34 62 63 syl3anc ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ) → ( ( 𝑋𝑗 ) ( .r𝑅 ) ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
65 64 anasss ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ∧ 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ) ) → ( ( 𝑋𝑗 ) ( .r𝑅 ) ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
66 fveq2 ( 𝑛 = ( 𝑘f𝑗 ) → ( 𝑌𝑛 ) = ( 𝑌 ‘ ( 𝑘f𝑗 ) ) )
67 oveq2 ( 𝑛 = ( 𝑘f𝑗 ) → ( ( 𝑥f𝑗 ) ∘f𝑛 ) = ( ( 𝑥f𝑗 ) ∘f − ( 𝑘f𝑗 ) ) )
68 67 fveq2d ( 𝑛 = ( 𝑘f𝑗 ) → ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) = ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f − ( 𝑘f𝑗 ) ) ) )
69 66 68 oveq12d ( 𝑛 = ( 𝑘f𝑗 ) → ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) = ( ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f − ( 𝑘f𝑗 ) ) ) ) )
70 69 oveq2d ( 𝑛 = ( 𝑘f𝑗 ) → ( ( 𝑋𝑗 ) ( .r𝑅 ) ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) ) = ( ( 𝑋𝑗 ) ( .r𝑅 ) ( ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f − ( 𝑘f𝑗 ) ) ) ) ) )
71 4 19 20 10 23 65 70 psrass1lem ( ( 𝜑𝑥𝐷 ) → ( 𝑅 Σg ( 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ↦ ( 𝑅 Σg ( 𝑗 ∈ { 𝐷r𝑘 } ↦ ( ( 𝑋𝑗 ) ( .r𝑅 ) ( ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f − ( 𝑘f𝑗 ) ) ) ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ↦ ( 𝑅 Σg ( 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ↦ ( ( 𝑋𝑗 ) ( .r𝑅 ) ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) ) ) ) ) ) )
72 7 ad2antrr ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) → 𝑋𝐵 )
73 8 ad2antrr ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) → 𝑌𝐵 )
74 simpr ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) → 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } )
75 breq1 ( 𝑔 = 𝑘 → ( 𝑔r𝑥𝑘r𝑥 ) )
76 75 elrab ( 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ↔ ( 𝑘𝐷𝑘r𝑥 ) )
77 74 76 sylib ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) → ( 𝑘𝐷𝑘r𝑥 ) )
78 77 simpld ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) → 𝑘𝐷 )
79 1 6 60 5 4 72 73 78 psrmulval ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) → ( ( 𝑋 × 𝑌 ) ‘ 𝑘 ) = ( 𝑅 Σg ( 𝑗 ∈ { 𝐷r𝑘 } ↦ ( ( 𝑋𝑗 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ) ) ) )
80 79 oveq1d ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) → ( ( ( 𝑋 × 𝑌 ) ‘ 𝑘 ) ( .r𝑅 ) ( 𝑍 ‘ ( 𝑥f𝑘 ) ) ) = ( ( 𝑅 Σg ( 𝑗 ∈ { 𝐷r𝑘 } ↦ ( ( 𝑋𝑗 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ) ) ) ( .r𝑅 ) ( 𝑍 ‘ ( 𝑥f𝑘 ) ) ) )
81 eqid ( 0g𝑅 ) = ( 0g𝑅 )
82 eqid ( +g𝑅 ) = ( +g𝑅 )
83 3 ad2antrr ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) → 𝑅 ∈ Ring )
84 4 psrbaglefi ( 𝑘𝐷 → { 𝐷r𝑘 } ∈ Fin )
85 78 84 syl ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) → { 𝐷r𝑘 } ∈ Fin )
86 43 ad2antrr ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) → 𝑍 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
87 simplr ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) → 𝑥𝐷 )
88 4 psrbagf ( 𝑘𝐷𝑘 : 𝐼 ⟶ ℕ0 )
89 78 88 syl ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) → 𝑘 : 𝐼 ⟶ ℕ0 )
90 77 simprd ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) → 𝑘r𝑥 )
91 4 psrbagcon ( ( 𝑥𝐷𝑘 : 𝐼 ⟶ ℕ0𝑘r𝑥 ) → ( ( 𝑥f𝑘 ) ∈ 𝐷 ∧ ( 𝑥f𝑘 ) ∘r𝑥 ) )
92 87 89 90 91 syl3anc ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) → ( ( 𝑥f𝑘 ) ∈ 𝐷 ∧ ( 𝑥f𝑘 ) ∘r𝑥 ) )
93 92 simpld ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) → ( 𝑥f𝑘 ) ∈ 𝐷 )
94 86 93 ffvelrnd ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) → ( 𝑍 ‘ ( 𝑥f𝑘 ) ) ∈ ( Base ‘ 𝑅 ) )
95 83 adantr ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → 𝑅 ∈ Ring )
96 26 ad3antrrr ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
97 simpr ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → 𝑗 ∈ { 𝐷r𝑘 } )
98 breq1 ( = 𝑗 → ( r𝑘𝑗r𝑘 ) )
99 98 elrab ( 𝑗 ∈ { 𝐷r𝑘 } ↔ ( 𝑗𝐷𝑗r𝑘 ) )
100 97 99 sylib ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → ( 𝑗𝐷𝑗r𝑘 ) )
101 100 simpld ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → 𝑗𝐷 )
102 96 101 ffvelrnd ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → ( 𝑋𝑗 ) ∈ ( Base ‘ 𝑅 ) )
103 35 ad3antrrr ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → 𝑌 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
104 78 adantr ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → 𝑘𝐷 )
105 101 46 syl ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → 𝑗 : 𝐼 ⟶ ℕ0 )
106 100 simprd ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → 𝑗r𝑘 )
107 4 psrbagcon ( ( 𝑘𝐷𝑗 : 𝐼 ⟶ ℕ0𝑗r𝑘 ) → ( ( 𝑘f𝑗 ) ∈ 𝐷 ∧ ( 𝑘f𝑗 ) ∘r𝑘 ) )
108 104 105 106 107 syl3anc ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → ( ( 𝑘f𝑗 ) ∈ 𝐷 ∧ ( 𝑘f𝑗 ) ∘r𝑘 ) )
109 108 simpld ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → ( 𝑘f𝑗 ) ∈ 𝐷 )
110 103 109 ffvelrnd ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ∈ ( Base ‘ 𝑅 ) )
111 10 60 ringcl ( ( 𝑅 ∈ Ring ∧ ( 𝑋𝑗 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑋𝑗 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ) ∈ ( Base ‘ 𝑅 ) )
112 95 102 110 111 syl3anc ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → ( ( 𝑋𝑗 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ) ∈ ( Base ‘ 𝑅 ) )
113 eqid ( 𝑗 ∈ { 𝐷r𝑘 } ↦ ( ( 𝑋𝑗 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ) ) = ( 𝑗 ∈ { 𝐷r𝑘 } ↦ ( ( 𝑋𝑗 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ) )
114 fvex ( 0g𝑅 ) ∈ V
115 114 a1i ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) → ( 0g𝑅 ) ∈ V )
116 113 85 112 115 fsuppmptdm ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) → ( 𝑗 ∈ { 𝐷r𝑘 } ↦ ( ( 𝑋𝑗 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ) ) finSupp ( 0g𝑅 ) )
117 10 81 82 60 83 85 94 112 116 gsummulc1 ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) → ( 𝑅 Σg ( 𝑗 ∈ { 𝐷r𝑘 } ↦ ( ( ( 𝑋𝑗 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ) ( .r𝑅 ) ( 𝑍 ‘ ( 𝑥f𝑘 ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑗 ∈ { 𝐷r𝑘 } ↦ ( ( 𝑋𝑗 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ) ) ) ( .r𝑅 ) ( 𝑍 ‘ ( 𝑥f𝑘 ) ) ) )
118 94 adantr ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → ( 𝑍 ‘ ( 𝑥f𝑘 ) ) ∈ ( Base ‘ 𝑅 ) )
119 10 60 ringass ( ( 𝑅 ∈ Ring ∧ ( ( 𝑋𝑗 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑍 ‘ ( 𝑥f𝑘 ) ) ∈ ( Base ‘ 𝑅 ) ) ) → ( ( ( 𝑋𝑗 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ) ( .r𝑅 ) ( 𝑍 ‘ ( 𝑥f𝑘 ) ) ) = ( ( 𝑋𝑗 ) ( .r𝑅 ) ( ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ( .r𝑅 ) ( 𝑍 ‘ ( 𝑥f𝑘 ) ) ) ) )
120 95 102 110 118 119 syl13anc ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → ( ( ( 𝑋𝑗 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ) ( .r𝑅 ) ( 𝑍 ‘ ( 𝑥f𝑘 ) ) ) = ( ( 𝑋𝑗 ) ( .r𝑅 ) ( ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ( .r𝑅 ) ( 𝑍 ‘ ( 𝑥f𝑘 ) ) ) ) )
121 4 psrbagf ( 𝑥𝐷𝑥 : 𝐼 ⟶ ℕ0 )
122 121 adantl ( ( 𝜑𝑥𝐷 ) → 𝑥 : 𝐼 ⟶ ℕ0 )
123 122 ad2antrr ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → 𝑥 : 𝐼 ⟶ ℕ0 )
124 123 ffvelrnda ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) ∧ 𝑧𝐼 ) → ( 𝑥𝑧 ) ∈ ℕ0 )
125 89 adantr ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → 𝑘 : 𝐼 ⟶ ℕ0 )
126 125 ffvelrnda ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) ∧ 𝑧𝐼 ) → ( 𝑘𝑧 ) ∈ ℕ0 )
127 105 ffvelrnda ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) ∧ 𝑧𝐼 ) → ( 𝑗𝑧 ) ∈ ℕ0 )
128 nn0cn ( ( 𝑥𝑧 ) ∈ ℕ0 → ( 𝑥𝑧 ) ∈ ℂ )
129 nn0cn ( ( 𝑘𝑧 ) ∈ ℕ0 → ( 𝑘𝑧 ) ∈ ℂ )
130 nn0cn ( ( 𝑗𝑧 ) ∈ ℕ0 → ( 𝑗𝑧 ) ∈ ℂ )
131 nnncan2 ( ( ( 𝑥𝑧 ) ∈ ℂ ∧ ( 𝑘𝑧 ) ∈ ℂ ∧ ( 𝑗𝑧 ) ∈ ℂ ) → ( ( ( 𝑥𝑧 ) − ( 𝑗𝑧 ) ) − ( ( 𝑘𝑧 ) − ( 𝑗𝑧 ) ) ) = ( ( 𝑥𝑧 ) − ( 𝑘𝑧 ) ) )
132 128 129 130 131 syl3an ( ( ( 𝑥𝑧 ) ∈ ℕ0 ∧ ( 𝑘𝑧 ) ∈ ℕ0 ∧ ( 𝑗𝑧 ) ∈ ℕ0 ) → ( ( ( 𝑥𝑧 ) − ( 𝑗𝑧 ) ) − ( ( 𝑘𝑧 ) − ( 𝑗𝑧 ) ) ) = ( ( 𝑥𝑧 ) − ( 𝑘𝑧 ) ) )
133 124 126 127 132 syl3anc ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) ∧ 𝑧𝐼 ) → ( ( ( 𝑥𝑧 ) − ( 𝑗𝑧 ) ) − ( ( 𝑘𝑧 ) − ( 𝑗𝑧 ) ) ) = ( ( 𝑥𝑧 ) − ( 𝑘𝑧 ) ) )
134 133 mpteq2dva ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → ( 𝑧𝐼 ↦ ( ( ( 𝑥𝑧 ) − ( 𝑗𝑧 ) ) − ( ( 𝑘𝑧 ) − ( 𝑗𝑧 ) ) ) ) = ( 𝑧𝐼 ↦ ( ( 𝑥𝑧 ) − ( 𝑘𝑧 ) ) ) )
135 2 ad2antrr ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) → 𝐼𝑉 )
136 135 adantr ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → 𝐼𝑉 )
137 ovexd ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) ∧ 𝑧𝐼 ) → ( ( 𝑥𝑧 ) − ( 𝑗𝑧 ) ) ∈ V )
138 ovexd ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) ∧ 𝑧𝐼 ) → ( ( 𝑘𝑧 ) − ( 𝑗𝑧 ) ) ∈ V )
139 123 feqmptd ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → 𝑥 = ( 𝑧𝐼 ↦ ( 𝑥𝑧 ) ) )
140 105 feqmptd ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → 𝑗 = ( 𝑧𝐼 ↦ ( 𝑗𝑧 ) ) )
141 136 124 127 139 140 offval2 ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → ( 𝑥f𝑗 ) = ( 𝑧𝐼 ↦ ( ( 𝑥𝑧 ) − ( 𝑗𝑧 ) ) ) )
142 125 feqmptd ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → 𝑘 = ( 𝑧𝐼 ↦ ( 𝑘𝑧 ) ) )
143 136 126 127 142 140 offval2 ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → ( 𝑘f𝑗 ) = ( 𝑧𝐼 ↦ ( ( 𝑘𝑧 ) − ( 𝑗𝑧 ) ) ) )
144 136 137 138 141 143 offval2 ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → ( ( 𝑥f𝑗 ) ∘f − ( 𝑘f𝑗 ) ) = ( 𝑧𝐼 ↦ ( ( ( 𝑥𝑧 ) − ( 𝑗𝑧 ) ) − ( ( 𝑘𝑧 ) − ( 𝑗𝑧 ) ) ) ) )
145 136 124 126 139 142 offval2 ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → ( 𝑥f𝑘 ) = ( 𝑧𝐼 ↦ ( ( 𝑥𝑧 ) − ( 𝑘𝑧 ) ) ) )
146 134 144 145 3eqtr4d ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → ( ( 𝑥f𝑗 ) ∘f − ( 𝑘f𝑗 ) ) = ( 𝑥f𝑘 ) )
147 146 fveq2d ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f − ( 𝑘f𝑗 ) ) ) = ( 𝑍 ‘ ( 𝑥f𝑘 ) ) )
148 147 oveq2d ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → ( ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f − ( 𝑘f𝑗 ) ) ) ) = ( ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ( .r𝑅 ) ( 𝑍 ‘ ( 𝑥f𝑘 ) ) ) )
149 148 oveq2d ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → ( ( 𝑋𝑗 ) ( .r𝑅 ) ( ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f − ( 𝑘f𝑗 ) ) ) ) ) = ( ( 𝑋𝑗 ) ( .r𝑅 ) ( ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ( .r𝑅 ) ( 𝑍 ‘ ( 𝑥f𝑘 ) ) ) ) )
150 120 149 eqtr4d ( ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) ∧ 𝑗 ∈ { 𝐷r𝑘 } ) → ( ( ( 𝑋𝑗 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ) ( .r𝑅 ) ( 𝑍 ‘ ( 𝑥f𝑘 ) ) ) = ( ( 𝑋𝑗 ) ( .r𝑅 ) ( ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f − ( 𝑘f𝑗 ) ) ) ) ) )
151 150 mpteq2dva ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) → ( 𝑗 ∈ { 𝐷r𝑘 } ↦ ( ( ( 𝑋𝑗 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ) ( .r𝑅 ) ( 𝑍 ‘ ( 𝑥f𝑘 ) ) ) ) = ( 𝑗 ∈ { 𝐷r𝑘 } ↦ ( ( 𝑋𝑗 ) ( .r𝑅 ) ( ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f − ( 𝑘f𝑗 ) ) ) ) ) ) )
152 151 oveq2d ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) → ( 𝑅 Σg ( 𝑗 ∈ { 𝐷r𝑘 } ↦ ( ( ( 𝑋𝑗 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ) ( .r𝑅 ) ( 𝑍 ‘ ( 𝑥f𝑘 ) ) ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ { 𝐷r𝑘 } ↦ ( ( 𝑋𝑗 ) ( .r𝑅 ) ( ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f − ( 𝑘f𝑗 ) ) ) ) ) ) ) )
153 80 117 152 3eqtr2d ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ) → ( ( ( 𝑋 × 𝑌 ) ‘ 𝑘 ) ( .r𝑅 ) ( 𝑍 ‘ ( 𝑥f𝑘 ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ { 𝐷r𝑘 } ↦ ( ( 𝑋𝑗 ) ( .r𝑅 ) ( ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f − ( 𝑘f𝑗 ) ) ) ) ) ) ) )
154 153 mpteq2dva ( ( 𝜑𝑥𝐷 ) → ( 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ↦ ( ( ( 𝑋 × 𝑌 ) ‘ 𝑘 ) ( .r𝑅 ) ( 𝑍 ‘ ( 𝑥f𝑘 ) ) ) ) = ( 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ↦ ( 𝑅 Σg ( 𝑗 ∈ { 𝐷r𝑘 } ↦ ( ( 𝑋𝑗 ) ( .r𝑅 ) ( ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f − ( 𝑘f𝑗 ) ) ) ) ) ) ) ) )
155 154 oveq2d ( ( 𝜑𝑥𝐷 ) → ( 𝑅 Σg ( 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ↦ ( ( ( 𝑋 × 𝑌 ) ‘ 𝑘 ) ( .r𝑅 ) ( 𝑍 ‘ ( 𝑥f𝑘 ) ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ↦ ( 𝑅 Σg ( 𝑗 ∈ { 𝐷r𝑘 } ↦ ( ( 𝑋𝑗 ) ( .r𝑅 ) ( ( 𝑌 ‘ ( 𝑘f𝑗 ) ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f − ( 𝑘f𝑗 ) ) ) ) ) ) ) ) ) )
156 8 ad2antrr ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) → 𝑌𝐵 )
157 9 ad2antrr ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) → 𝑍𝐵 )
158 1 6 60 5 4 156 157 51 psrmulval ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) → ( ( 𝑌 × 𝑍 ) ‘ ( 𝑥f𝑗 ) ) = ( 𝑅 Σg ( 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ↦ ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) ) ) )
159 158 oveq2d ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) → ( ( 𝑋𝑗 ) ( .r𝑅 ) ( ( 𝑌 × 𝑍 ) ‘ ( 𝑥f𝑗 ) ) ) = ( ( 𝑋𝑗 ) ( .r𝑅 ) ( 𝑅 Σg ( 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ↦ ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) ) ) ) )
160 4 psrbaglefi ( ( 𝑥f𝑗 ) ∈ 𝐷 → { 𝐷r ≤ ( 𝑥f𝑗 ) } ∈ Fin )
161 51 160 syl ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) → { 𝐷r ≤ ( 𝑥f𝑗 ) } ∈ Fin )
162 ovex ( ℕ0m 𝐼 ) ∈ V
163 4 162 rab2ex { 𝐷r ≤ ( 𝑥f𝑗 ) } ∈ V
164 163 mptex ( 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ↦ ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) ) ∈ V
165 funmpt Fun ( 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ↦ ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) )
166 164 165 114 3pm3.2i ( ( 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ↦ ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) ) ∈ V ∧ Fun ( 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ↦ ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) ) ∧ ( 0g𝑅 ) ∈ V )
167 166 a1i ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) → ( ( 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ↦ ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) ) ∈ V ∧ Fun ( 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ↦ ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) ) ∧ ( 0g𝑅 ) ∈ V ) )
168 suppssdm ( ( 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ↦ ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) ) supp ( 0g𝑅 ) ) ⊆ dom ( 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ↦ ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) )
169 eqid ( 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ↦ ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) ) = ( 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ↦ ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) )
170 169 dmmptss dom ( 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ↦ ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) ) ⊆ { 𝐷r ≤ ( 𝑥f𝑗 ) }
171 168 170 sstri ( ( 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ↦ ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) ) supp ( 0g𝑅 ) ) ⊆ { 𝐷r ≤ ( 𝑥f𝑗 ) }
172 171 a1i ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) → ( ( 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ↦ ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) ) supp ( 0g𝑅 ) ) ⊆ { 𝐷r ≤ ( 𝑥f𝑗 ) } )
173 suppssfifsupp ( ( ( ( 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ↦ ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) ) ∈ V ∧ Fun ( 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ↦ ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) ) ∧ ( 0g𝑅 ) ∈ V ) ∧ ( { 𝐷r ≤ ( 𝑥f𝑗 ) } ∈ Fin ∧ ( ( 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ↦ ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) ) supp ( 0g𝑅 ) ) ⊆ { 𝐷r ≤ ( 𝑥f𝑗 ) } ) ) → ( 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ↦ ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) ) finSupp ( 0g𝑅 ) )
174 167 161 172 173 syl12anc ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) → ( 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ↦ ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) ) finSupp ( 0g𝑅 ) )
175 10 81 82 60 24 161 33 62 174 gsummulc2 ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) → ( 𝑅 Σg ( 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ↦ ( ( 𝑋𝑗 ) ( .r𝑅 ) ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) ) ) ) = ( ( 𝑋𝑗 ) ( .r𝑅 ) ( 𝑅 Σg ( 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ↦ ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) ) ) ) )
176 159 175 eqtr4d ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ) → ( ( 𝑋𝑗 ) ( .r𝑅 ) ( ( 𝑌 × 𝑍 ) ‘ ( 𝑥f𝑗 ) ) ) = ( 𝑅 Σg ( 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ↦ ( ( 𝑋𝑗 ) ( .r𝑅 ) ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) ) ) ) )
177 176 mpteq2dva ( ( 𝜑𝑥𝐷 ) → ( 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ↦ ( ( 𝑋𝑗 ) ( .r𝑅 ) ( ( 𝑌 × 𝑍 ) ‘ ( 𝑥f𝑗 ) ) ) ) = ( 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ↦ ( 𝑅 Σg ( 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ↦ ( ( 𝑋𝑗 ) ( .r𝑅 ) ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) ) ) ) ) )
178 177 oveq2d ( ( 𝜑𝑥𝐷 ) → ( 𝑅 Σg ( 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ↦ ( ( 𝑋𝑗 ) ( .r𝑅 ) ( ( 𝑌 × 𝑍 ) ‘ ( 𝑥f𝑗 ) ) ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ↦ ( 𝑅 Σg ( 𝑛 ∈ { 𝐷r ≤ ( 𝑥f𝑗 ) } ↦ ( ( 𝑋𝑗 ) ( .r𝑅 ) ( ( 𝑌𝑛 ) ( .r𝑅 ) ( 𝑍 ‘ ( ( 𝑥f𝑗 ) ∘f𝑛 ) ) ) ) ) ) ) ) )
179 71 155 178 3eqtr4d ( ( 𝜑𝑥𝐷 ) → ( 𝑅 Σg ( 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ↦ ( ( ( 𝑋 × 𝑌 ) ‘ 𝑘 ) ( .r𝑅 ) ( 𝑍 ‘ ( 𝑥f𝑘 ) ) ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ↦ ( ( 𝑋𝑗 ) ( .r𝑅 ) ( ( 𝑌 × 𝑍 ) ‘ ( 𝑥f𝑗 ) ) ) ) ) )
180 11 adantr ( ( 𝜑𝑥𝐷 ) → ( 𝑋 × 𝑌 ) ∈ 𝐵 )
181 9 adantr ( ( 𝜑𝑥𝐷 ) → 𝑍𝐵 )
182 1 6 60 5 4 180 181 20 psrmulval ( ( 𝜑𝑥𝐷 ) → ( ( ( 𝑋 × 𝑌 ) × 𝑍 ) ‘ 𝑥 ) = ( 𝑅 Σg ( 𝑘 ∈ { 𝑔𝐷𝑔r𝑥 } ↦ ( ( ( 𝑋 × 𝑌 ) ‘ 𝑘 ) ( .r𝑅 ) ( 𝑍 ‘ ( 𝑥f𝑘 ) ) ) ) ) )
183 7 adantr ( ( 𝜑𝑥𝐷 ) → 𝑋𝐵 )
184 15 adantr ( ( 𝜑𝑥𝐷 ) → ( 𝑌 × 𝑍 ) ∈ 𝐵 )
185 1 6 60 5 4 183 184 20 psrmulval ( ( 𝜑𝑥𝐷 ) → ( ( 𝑋 × ( 𝑌 × 𝑍 ) ) ‘ 𝑥 ) = ( 𝑅 Σg ( 𝑗 ∈ { 𝑔𝐷𝑔r𝑥 } ↦ ( ( 𝑋𝑗 ) ( .r𝑅 ) ( ( 𝑌 × 𝑍 ) ‘ ( 𝑥f𝑗 ) ) ) ) ) )
186 179 182 185 3eqtr4d ( ( 𝜑𝑥𝐷 ) → ( ( ( 𝑋 × 𝑌 ) × 𝑍 ) ‘ 𝑥 ) = ( ( 𝑋 × ( 𝑌 × 𝑍 ) ) ‘ 𝑥 ) )
187 14 18 186 eqfnfvd ( 𝜑 → ( ( 𝑋 × 𝑌 ) × 𝑍 ) = ( 𝑋 × ( 𝑌 × 𝑍 ) ) )