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 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ 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 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ 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 ( ℕ0m 𝐼 ) ∈ 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 ( 𝜑 → ( 𝑋 × ( 𝑌 + 𝑍 ) ) = ( ( 𝑋 × 𝑌 ) + ( 𝑋 × 𝑍 ) ) )