Metamath Proof Explorer

Theorem psrdir

Description: Distributive law for the ring of power series (right-distributivity). (Contributed by Mario Carneiro, 7-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 psrring.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psrring.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
3 psrring.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
4 psrass.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
5 psrass.t ⊢ × = ( .r ‘ 𝑆 )
6 psrass.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
7 psrass.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8 psrass.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9 psrass.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
10 psrdi.a ⊢ + = ( +g ‘ 𝑆 )
11 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
12 1 6 11 10 7 8 psradd ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) = ( 𝑋 ∘f ( +g ‘ 𝑅 ) 𝑌 ) )
13 12 fveq1d ⊢ ( 𝜑 → ( ( 𝑋 + 𝑌 ) ‘ 𝑥 ) = ( ( 𝑋 ∘f ( +g ‘ 𝑅 ) 𝑌 ) ‘ 𝑥 ) )
14 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑋 + 𝑌 ) ‘ 𝑥 ) = ( ( 𝑋 ∘f ( +g ‘ 𝑅 ) 𝑌 ) ‘ 𝑥 ) )
15 ssrab2 ⊢ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ⊆ 𝐷
16 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } )
17 15 16 sseldi ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑥 ∈ 𝐷 )
18 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
19 1 18 4 6 7 psrelbas ⊢ ( 𝜑 → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
20 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
21 20 ffnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑋 Fn 𝐷 )
22 1 18 4 6 8 psrelbas ⊢ ( 𝜑 → 𝑌 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
23 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑌 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
24 23 ffnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑌 Fn 𝐷 )
25 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
26 4 25 rabex2 ⊢ 𝐷 ∈ V
27 26 a1i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝐷 ∈ V )
28 inidm ⊢ ( 𝐷 ∩ 𝐷 ) = 𝐷
29 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) ∧ 𝑥 ∈ 𝐷 ) → ( 𝑋 ‘ 𝑥 ) = ( 𝑋 ‘ 𝑥 ) )
30 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) ∧ 𝑥 ∈ 𝐷 ) → ( 𝑌 ‘ 𝑥 ) = ( 𝑌 ‘ 𝑥 ) )
31 21 24 27 27 28 29 30 ofval ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑋 ∘f ( +g ‘ 𝑅 ) 𝑌 ) ‘ 𝑥 ) = ( ( 𝑋 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( 𝑌 ‘ 𝑥 ) ) )
32 17 31 mpdan ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑋 ∘f ( +g ‘ 𝑅 ) 𝑌 ) ‘ 𝑥 ) = ( ( 𝑋 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( 𝑌 ‘ 𝑥 ) ) )
33 14 32 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑋 + 𝑌 ) ‘ 𝑥 ) = ( ( 𝑋 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( 𝑌 ‘ 𝑥 ) ) )
34 33 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( ( 𝑋 + 𝑌 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) = ( ( ( 𝑋 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( 𝑌 ‘ 𝑥 ) ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) )
35 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑅 ∈ Ring )
36 20 17 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑋 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
37 23 17 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑌 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
38 1 18 4 6 9 psrelbas ⊢ ( 𝜑 → 𝑍 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
39 38 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑍 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
40 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝐼 ∈ 𝑉 )
41 simplr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑘 ∈ 𝐷 )
42 eqid ⊢ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } = { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 }
43 4 42 psrbagconcl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑘 ∈ 𝐷 ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑥 ) ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } )
44 40 41 16 43 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑥 ) ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } )
45 15 44 sseldi ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑥 ) ∈ 𝐷 )
46 39 45 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ∈ ( Base ‘ 𝑅 ) )
47 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
48 18 11 47 ringdir ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝑋 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑌 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ∈ ( Base ‘ 𝑅 ) ) ) → ( ( ( 𝑋 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( 𝑌 ‘ 𝑥 ) ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) = ( ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ( +g ‘ 𝑅 ) ( ( 𝑌 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) )
49 35 36 37 46 48 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( ( 𝑋 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( 𝑌 ‘ 𝑥 ) ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) = ( ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ( +g ‘ 𝑅 ) ( ( 𝑌 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) )
50 34 49 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( ( 𝑋 + 𝑌 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) = ( ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ( +g ‘ 𝑅 ) ( ( 𝑌 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) )
51 50 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑋 + 𝑌 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ( +g ‘ 𝑅 ) ( ( 𝑌 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) )
52 4 psrbaglefi ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑘 ∈ 𝐷 ) → { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ∈ Fin )
53 2 52 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ∈ Fin )
54 18 47 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ∈ ( Base ‘ 𝑅 ) )
55 35 36 46 54 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ∈ ( Base ‘ 𝑅 ) )
56 18 47 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑌 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑌 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ∈ ( Base ‘ 𝑅 ) )
57 35 37 46 56 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑌 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ∈ ( Base ‘ 𝑅 ) )
58 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) )
59 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑌 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑌 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) )
60 53 55 57 58 59 offval2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑌 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ( +g ‘ 𝑅 ) ( ( 𝑌 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) )
61 51 60 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑋 + 𝑌 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑌 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) )
62 61 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑋 + 𝑌 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) = ( 𝑅 Σg ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑌 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )
63 3 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑅 ∈ Ring )
64 ringcmn ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
65 63 64 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑅 ∈ CMnd )
66 eqid ⊢ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) )
67 eqid ⊢ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑌 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑌 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) )
68 18 11 65 53 55 57 66 67 gsummptfidmadd2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑅 Σg ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑌 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ( +g ‘ 𝑅 ) ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑌 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )
69 62 68 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑋 + 𝑌 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ( +g ‘ 𝑅 ) ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑌 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )
70 69 mpteq2dva ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑋 + 𝑌 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) = ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ( +g ‘ 𝑅 ) ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑌 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) )
71 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
72 3 71 syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
73 1 6 10 72 7 8 psraddcl ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝐵 )
74 1 6 47 5 4 73 9 psrmulfval ⊢ ( 𝜑 → ( ( 𝑋 + 𝑌 ) × 𝑍 ) = ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑋 + 𝑌 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )
75 1 6 5 3 7 9 psrmulcl ⊢ ( 𝜑 → ( 𝑋 × 𝑍 ) ∈ 𝐵 )
76 1 6 5 3 8 9 psrmulcl ⊢ ( 𝜑 → ( 𝑌 × 𝑍 ) ∈ 𝐵 )
77 1 6 11 10 75 76 psradd ⊢ ( 𝜑 → ( ( 𝑋 × 𝑍 ) + ( 𝑌 × 𝑍 ) ) = ( ( 𝑋 × 𝑍 ) ∘f ( +g ‘ 𝑅 ) ( 𝑌 × 𝑍 ) ) )
78 26 a1i ⊢ ( 𝜑 → 𝐷 ∈ V )
79 ovexd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ∈ V )
80 ovexd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑌 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ∈ V )
81 1 6 47 5 4 7 9 psrmulfval ⊢ ( 𝜑 → ( 𝑋 × 𝑍 ) = ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )
82 1 6 47 5 4 8 9 psrmulfval ⊢ ( 𝜑 → ( 𝑌 × 𝑍 ) = ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑌 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )
83 78 79 80 81 82 offval2 ⊢ ( 𝜑 → ( ( 𝑋 × 𝑍 ) ∘f ( +g ‘ 𝑅 ) ( 𝑌 × 𝑍 ) ) = ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ( +g ‘ 𝑅 ) ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑌 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) )
84 77 83 eqtrd ⊢ ( 𝜑 → ( ( 𝑋 × 𝑍 ) + ( 𝑌 × 𝑍 ) ) = ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ( +g ‘ 𝑅 ) ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑌 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) )
85 70 74 84 3eqtr4d ⊢ ( 𝜑 → ( ( 𝑋 + 𝑌 ) × 𝑍 ) = ( ( 𝑋 × 𝑍 ) + ( 𝑌 × 𝑍 ) ) )