Metamath Proof Explorer

Theorem psrdi

Description: Distributive law for the ring of power series (left-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 psrdi ( 𝜑 → ( 𝑋 × ( 𝑌 + 𝑍 ) ) = ( ( 𝑋 × 𝑌 ) + ( 𝑋 × 𝑍 ) ) )

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 8 9 psradd ⊢ ( 𝜑 → ( 𝑌 + 𝑍 ) = ( 𝑌 ∘f ( +g ‘ 𝑅 ) 𝑍 ) )
13 12 fveq1d ⊢ ( 𝜑 → ( ( 𝑌 + 𝑍 ) ‘ ( 𝑘 ∘f − 𝑥 ) ) = ( ( 𝑌 ∘f ( +g ‘ 𝑅 ) 𝑍 ) ‘ ( 𝑘 ∘f − 𝑥 ) ) )
14 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑌 + 𝑍 ) ‘ ( 𝑘 ∘f − 𝑥 ) ) = ( ( 𝑌 ∘f ( +g ‘ 𝑅 ) 𝑍 ) ‘ ( 𝑘 ∘f − 𝑥 ) ) )
15 ssrab2 ⊢ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ⊆ 𝐷
16 eqid ⊢ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } = { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 }
17 4 16 psrbagconcl ⊢ ( ( 𝑘 ∈ 𝐷 ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑥 ) ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } )
18 17 adantll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑥 ) ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } )
19 15 18 sselid ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑥 ) ∈ 𝐷 )
20 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
21 1 20 4 6 8 psrelbas ⊢ ( 𝜑 → 𝑌 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
22 21 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑌 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
23 22 ffnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑌 Fn 𝐷 )
24 1 20 4 6 9 psrelbas ⊢ ( 𝜑 → 𝑍 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
25 24 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑍 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
26 25 ffnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑍 Fn 𝐷 )
27 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
28 4 27 rabex2 ⊢ 𝐷 ∈ V
29 28 a1i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝐷 ∈ V )
30 inidm ⊢ ( 𝐷 ∩ 𝐷 ) = 𝐷
31 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) ∧ ( 𝑘 ∘f − 𝑥 ) ∈ 𝐷 ) → ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) = ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) )
32 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) ∧ ( 𝑘 ∘f − 𝑥 ) ∈ 𝐷 ) → ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) = ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) )
33 23 26 29 29 30 31 32 ofval ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) ∧ ( 𝑘 ∘f − 𝑥 ) ∈ 𝐷 ) → ( ( 𝑌 ∘f ( +g ‘ 𝑅 ) 𝑍 ) ‘ ( 𝑘 ∘f − 𝑥 ) ) = ( ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ( +g ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) )
34 19 33 mpdan ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑌 ∘f ( +g ‘ 𝑅 ) 𝑍 ) ‘ ( 𝑘 ∘f − 𝑥 ) ) = ( ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ( +g ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) )
35 14 34 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑌 + 𝑍 ) ‘ ( 𝑘 ∘f − 𝑥 ) ) = ( ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ( +g ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) )
36 35 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ( 𝑌 + 𝑍 ) ‘ ( 𝑘 ∘f − 𝑥 ) ) ) = ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ( +g ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) )
37 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑅 ∈ Ring )
38 1 20 4 6 7 psrelbas ⊢ ( 𝜑 → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
39 38 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
40 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } )
41 15 40 sselid ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑥 ∈ 𝐷 )
42 39 41 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑋 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
43 22 19 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ∈ ( Base ‘ 𝑅 ) )
44 25 19 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ∈ ( Base ‘ 𝑅 ) )
45 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
46 20 11 45 ringdi ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝑋 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ( +g ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) = ( ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) )
47 37 42 43 44 46 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ( +g ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) = ( ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) )
48 36 47 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ( 𝑌 + 𝑍 ) ‘ ( 𝑘 ∘f − 𝑥 ) ) ) = ( ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) )
49 48 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ( 𝑌 + 𝑍 ) ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) )
50 4 psrbaglefi ⊢ ( 𝑘 ∈ 𝐷 → { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ∈ Fin )
51 50 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ∈ Fin )
52 20 45 37 42 43 ringcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ∈ ( Base ‘ 𝑅 ) )
53 20 45 37 42 44 ringcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ∈ ( Base ‘ 𝑅 ) )
54 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) )
55 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) )
56 51 52 53 54 55 offval2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) )
57 49 56 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ( 𝑌 + 𝑍 ) ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) )
58 57 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ( 𝑌 + 𝑍 ) ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) = ( 𝑅 Σg ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )
59 3 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑅 ∈ Ring )
60 59 ringcmnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑅 ∈ CMnd )
61 eqid ⊢ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) )
62 eqid ⊢ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) )
63 20 11 60 51 52 53 61 62 gsummptfidmadd2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑅 Σg ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ( +g ‘ 𝑅 ) ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )
64 58 63 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ( 𝑌 + 𝑍 ) ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ( +g ‘ 𝑅 ) ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )
65 64 mpteq2dva ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ( 𝑌 + 𝑍 ) ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) = ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ( +g ‘ 𝑅 ) ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) )
66 3 ringgrpd ⊢ ( 𝜑 → 𝑅 ∈ Grp )
67 66 grpmgmd ⊢ ( 𝜑 → 𝑅 ∈ Mgm )
68 1 6 10 67 8 9 psraddcl ⊢ ( 𝜑 → ( 𝑌 + 𝑍 ) ∈ 𝐵 )
69 1 6 45 5 4 7 68 psrmulfval ⊢ ( 𝜑 → ( 𝑋 × ( 𝑌 + 𝑍 ) ) = ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ( 𝑌 + 𝑍 ) ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )
70 1 6 5 3 7 8 psrmulcl ⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) ∈ 𝐵 )
71 1 6 5 3 7 9 psrmulcl ⊢ ( 𝜑 → ( 𝑋 × 𝑍 ) ∈ 𝐵 )
72 1 6 11 10 70 71 psradd ⊢ ( 𝜑 → ( ( 𝑋 × 𝑌 ) + ( 𝑋 × 𝑍 ) ) = ( ( 𝑋 × 𝑌 ) ∘f ( +g ‘ 𝑅 ) ( 𝑋 × 𝑍 ) ) )
73 28 a1i ⊢ ( 𝜑 → 𝐷 ∈ V )
74 ovexd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ∈ V )
75 ovexd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ∈ V )
76 1 6 45 5 4 7 8 psrmulfval ⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) = ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )
77 1 6 45 5 4 7 9 psrmulfval ⊢ ( 𝜑 → ( 𝑋 × 𝑍 ) = ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )
78 73 74 75 76 77 offval2 ⊢ ( 𝜑 → ( ( 𝑋 × 𝑌 ) ∘f ( +g ‘ 𝑅 ) ( 𝑋 × 𝑍 ) ) = ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ( +g ‘ 𝑅 ) ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) )
79 72 78 eqtrd ⊢ ( 𝜑 → ( ( 𝑋 × 𝑌 ) + ( 𝑋 × 𝑍 ) ) = ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ( +g ‘ 𝑅 ) ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) )
80 65 69 79 3eqtr4d ⊢ ( 𝜑 → ( 𝑋 × ( 𝑌 + 𝑍 ) ) = ( ( 𝑋 × 𝑌 ) + ( 𝑋 × 𝑍 ) ) )