Metamath Proof Explorer

Theorem psrass23

Description: Associative identities for the ring of power series. (Contributed by Mario Carneiro, 7-Jan-2015) (Proof shortened by AV, 25-Nov-2019)

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 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
psrcom.c ⊢ ( 𝜑 → 𝑅 ∈ CRing )
psrass.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
psrass.n ⊢ · = ( ·𝑠 ‘ 𝑆 )
psrass.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
Assertion psrass23 ( 𝜑 → ( ( ( 𝐴 · 𝑋 ) × 𝑌 ) = ( 𝐴 · ( 𝑋 × 𝑌 ) ) ∧ ( 𝑋 × ( 𝐴 · 𝑌 ) ) = ( 𝐴 · ( 𝑋 × 𝑌 ) ) ) )

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 psrcom.c ⊢ ( 𝜑 → 𝑅 ∈ CRing )
10 psrass.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
11 psrass.n ⊢ · = ( ·𝑠 ‘ 𝑆 )
12 psrass.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
13 1 2 3 4 5 6 7 8 10 11 12 psrass23l ⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) × 𝑌 ) = ( 𝐴 · ( 𝑋 × 𝑌 ) ) )
14 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
15 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
16 12 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝐴 ∈ 𝐾 )
17 16 10 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝐴 ∈ ( Base ‘ 𝑅 ) )
18 17 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝐴 ∈ ( Base ‘ 𝑅 ) )
19 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑌 ∈ 𝐵 )
20 ssrab2 ⊢ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ⊆ 𝐷
21 simplr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑘 ∈ 𝐷 )
22 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } )
23 eqid ⊢ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } = { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 }
24 4 23 psrbagconcl ⊢ ( ( 𝑘 ∈ 𝐷 ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑥 ) ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } )
25 21 22 24 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑥 ) ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } )
26 20 25 sselid ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑥 ) ∈ 𝐷 )
27 1 11 14 6 15 4 18 19 26 psrvscaval ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝐴 · 𝑌 ) ‘ ( 𝑘 ∘f − 𝑥 ) ) = ( 𝐴 ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) )
28 27 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ( 𝐴 · 𝑌 ) ‘ ( 𝑘 ∘f − 𝑥 ) ) ) = ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝐴 ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) )
29 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑋 ∈ 𝐵 )
30 1 14 4 6 29 psrelbas ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
31 20 22 sselid ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑥 ∈ 𝐷 )
32 30 31 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑋 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
33 1 14 4 6 19 psrelbas ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑌 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
34 33 26 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ∈ ( Base ‘ 𝑅 ) )
35 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑅 ∈ CRing )
36 14 15 crngcom ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑢 ( .r ‘ 𝑅 ) 𝑣 ) = ( 𝑣 ( .r ‘ 𝑅 ) 𝑢 ) )
37 36 3expb ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑢 ( .r ‘ 𝑅 ) 𝑣 ) = ( 𝑣 ( .r ‘ 𝑅 ) 𝑢 ) )
38 35 37 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑢 ( .r ‘ 𝑅 ) 𝑣 ) = ( 𝑣 ( .r ‘ 𝑅 ) 𝑢 ) )
39 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑅 ∈ Ring )
40 14 15 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ ( Base ‘ 𝑅 ) ∧ 𝑤 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑢 ( .r ‘ 𝑅 ) 𝑣 ) ( .r ‘ 𝑅 ) 𝑤 ) = ( 𝑢 ( .r ‘ 𝑅 ) ( 𝑣 ( .r ‘ 𝑅 ) 𝑤 ) ) )
41 39 40 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ ( Base ‘ 𝑅 ) ∧ 𝑤 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑢 ( .r ‘ 𝑅 ) 𝑣 ) ( .r ‘ 𝑅 ) 𝑤 ) = ( 𝑢 ( .r ‘ 𝑅 ) ( 𝑣 ( .r ‘ 𝑅 ) 𝑤 ) ) )
42 32 18 34 38 41 caov12d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝐴 ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) = ( 𝐴 ( .r ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) )
43 28 42 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ( 𝐴 · 𝑌 ) ‘ ( 𝑘 ∘f − 𝑥 ) ) ) = ( 𝐴 ( .r ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) )
44 43 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ( 𝐴 · 𝑌 ) ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( 𝐴 ( .r ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) )
45 44 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ( 𝐴 · 𝑌 ) ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) = ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( 𝐴 ( .r ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )
46 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
47 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
48 3 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑅 ∈ Ring )
49 4 psrbaglefi ⊢ ( 𝑘 ∈ 𝐷 → { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ∈ Fin )
50 49 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ∈ Fin )
51 14 15 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ∈ ( Base ‘ 𝑅 ) )
52 39 32 34 51 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ∈ ( Base ‘ 𝑅 ) )
53 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
54 4 53 rabex2 ⊢ 𝐷 ∈ V
55 54 mptrabex ⊢ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ∈ V
56 funmpt ⊢ Fun ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) )
57 fvex ⊢ ( 0g ‘ 𝑅 ) ∈ V
58 55 56 57 3pm3.2i ⊢ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ∈ V ∧ Fun ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ∧ ( 0g ‘ 𝑅 ) ∈ V )
59 58 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ∈ V ∧ Fun ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ∧ ( 0g ‘ 𝑅 ) ∈ V ) )
60 suppssdm ⊢ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) supp ( 0g ‘ 𝑅 ) ) ⊆ dom ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) )
61 eqid ⊢ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) )
62 61 dmmptss ⊢ dom ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ⊆ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 }
63 60 62 sstri ⊢ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) supp ( 0g ‘ 𝑅 ) ) ⊆ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 }
64 63 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) supp ( 0g ‘ 𝑅 ) ) ⊆ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } )
65 suppssfifsupp ⊢ ( ( ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ∈ V ∧ Fun ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ∧ ( 0g ‘ 𝑅 ) ∈ V ) ∧ ( { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ∈ Fin ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) supp ( 0g ‘ 𝑅 ) ) ⊆ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) ) → ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) finSupp ( 0g ‘ 𝑅 ) )
66 59 50 64 65 syl12anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) finSupp ( 0g ‘ 𝑅 ) )
67 14 46 47 15 48 50 17 52 66 gsummulc2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( 𝐴 ( .r ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) = ( 𝐴 ( .r ‘ 𝑅 ) ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )
68 45 67 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ( 𝐴 · 𝑌 ) ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) = ( 𝐴 ( .r ‘ 𝑅 ) ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )
69 68 mpteq2dva ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ( 𝐴 · 𝑌 ) ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) = ( 𝑘 ∈ 𝐷 ↦ ( 𝐴 ( .r ‘ 𝑅 ) ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) )
70 1 11 10 6 3 12 8 psrvscacl ⊢ ( 𝜑 → ( 𝐴 · 𝑌 ) ∈ 𝐵 )
71 1 6 15 5 4 7 70 psrmulfval ⊢ ( 𝜑 → ( 𝑋 × ( 𝐴 · 𝑌 ) ) = ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ( 𝐴 · 𝑌 ) ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )
72 1 6 5 3 7 8 psrmulcl ⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) ∈ 𝐵 )
73 1 11 10 6 15 4 12 72 psrvsca ⊢ ( 𝜑 → ( 𝐴 · ( 𝑋 × 𝑌 ) ) = ( ( 𝐷 × { 𝐴 } ) ∘f ( .r ‘ 𝑅 ) ( 𝑋 × 𝑌 ) ) )
74 54 a1i ⊢ ( 𝜑 → 𝐷 ∈ V )
75 ovex ⊢ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ∈ V
76 75 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ∈ V )
77 fconstmpt ⊢ ( 𝐷 × { 𝐴 } ) = ( 𝑘 ∈ 𝐷 ↦ 𝐴 )
78 77 a1i ⊢ ( 𝜑 → ( 𝐷 × { 𝐴 } ) = ( 𝑘 ∈ 𝐷 ↦ 𝐴 ) )
79 1 6 15 5 4 7 8 psrmulfval ⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) = ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )
80 74 16 76 78 79 offval2 ⊢ ( 𝜑 → ( ( 𝐷 × { 𝐴 } ) ∘f ( .r ‘ 𝑅 ) ( 𝑋 × 𝑌 ) ) = ( 𝑘 ∈ 𝐷 ↦ ( 𝐴 ( .r ‘ 𝑅 ) ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) )
81 73 80 eqtrd ⊢ ( 𝜑 → ( 𝐴 · ( 𝑋 × 𝑌 ) ) = ( 𝑘 ∈ 𝐷 ↦ ( 𝐴 ( .r ‘ 𝑅 ) ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) )
82 69 71 81 3eqtr4d ⊢ ( 𝜑 → ( 𝑋 × ( 𝐴 · 𝑌 ) ) = ( 𝐴 · ( 𝑋 × 𝑌 ) ) )
83 13 82 jca ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝑋 ) × 𝑌 ) = ( 𝐴 · ( 𝑋 × 𝑌 ) ) ∧ ( 𝑋 × ( 𝐴 · 𝑌 ) ) = ( 𝐴 · ( 𝑋 × 𝑌 ) ) ) )