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	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝑋 ) × 𝑌 ) = ( 𝐴 · ( 𝑋 × 𝑌 ) ) ∧ ( 𝑋 × ( 𝐴 · 𝑌 ) ) = ( 𝐴 · ( 𝑋 × 𝑌 ) ) ) )