Theorem psrass23l 21870

Description: Associative identity for the ring of power series. Part of psrass23 21872 which does not require the scalar ring to be commutative. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 14-Aug-2019.)

Hypotheses

Ref	Expression
psrring.s	⊢ 𝑆 = (𝐼 mPwSer 𝑅)
psrring.i	⊢ (𝜑 → 𝐼 ∈ 𝑉)
psrring.r	⊢ (𝜑 → 𝑅 ∈ Ring)
psrass.d	⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}
psrass.t	⊢ × = (.r‘𝑆)
psrass.b	⊢ 𝐵 = (Base‘𝑆)
psrass.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)
psrass.y	⊢ (𝜑 → 𝑌 ∈ 𝐵)
psrass23l.k	⊢ 𝐾 = (Base‘𝑅)
psrass23l.n	⊢ · = ( ·𝑠 ‘𝑆)
psrass23l.a	⊢ (𝜑 → 𝐴 ∈ 𝐾)

Assertion

Ref	Expression
psrass23l	⊢ (𝜑 → ((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌)))

Distinct variable groups:   𝑓,𝐼   𝑅,𝑓   𝑓,𝑋   𝑓,𝑌

Allowed substitution hints:   𝜑(𝑓)   𝐴(𝑓)   𝐵(𝑓)   𝐷(𝑓)   𝑆(𝑓)   · (𝑓)   × (𝑓)   𝐾(𝑓)   𝑉(𝑓)

Proof of Theorem psrass23l

Dummy variables 𝑥 𝑘 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		psrring.s	. . . . . . . . 9 ⊢ 𝑆 = (𝐼 mPwSer 𝑅)
2		psrass23l.n	. . . . . . . . 9 ⊢ · = ( ·𝑠 ‘𝑆)
3		eqid 2726	. . . . . . . . 9 ⊢ (Base‘𝑅) = (Base‘𝑅)
4		psrass.b	. . . . . . . . 9 ⊢ 𝐵 = (Base‘𝑆)
5		eqid 2726	. . . . . . . . 9 ⊢ (.r‘𝑅) = (.r‘𝑅)
6		psrass.d	. . . . . . . . 9 ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}
7		psrass23l.a	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ 𝐾)
8	7	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝐴 ∈ 𝐾)
9		psrass23l.k	. . . . . . . . . . 11 ⊢ 𝐾 = (Base‘𝑅)
10	8, 9	eleqtrdi 2837	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝐴 ∈ (Base‘𝑅))
11	10	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝐴 ∈ (Base‘𝑅))
12		psrass.x	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
13	12	ad2antrr 723	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑋 ∈ 𝐵)
14		ssrab2 4072	. . . . . . . . . 10 ⊢ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ⊆ 𝐷
15		simpr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘})
16	14, 15	sselid 3975	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑥 ∈ 𝐷)
17	1, 2, 3, 4, 5, 6, 11, 13, 16	psrvscaval 21853	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝐴 · 𝑋)‘𝑥) = (𝐴(.r‘𝑅)(𝑋‘𝑥)))
18	17	oveq1d 7420	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (((𝐴 · 𝑋)‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))) = ((𝐴(.r‘𝑅)(𝑋‘𝑥))(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))
19		psrring.r	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ Ring)
20	19	ad2antrr 723	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑅 ∈ Ring)
21	1, 3, 6, 4, 13	psrelbas 21839	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑋:𝐷⟶(Base‘𝑅))
22	21, 16	ffvelcdmd 7081	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑋‘𝑥) ∈ (Base‘𝑅))
23		psrass.y	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
24	23	ad2antrr 723	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑌 ∈ 𝐵)
25	1, 3, 6, 4, 24	psrelbas 21839	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑌:𝐷⟶(Base‘𝑅))
26		eqid 2726	. . . . . . . . . . . 12 ⊢ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}
27	6, 26	psrbagconcl 21828	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ 𝐷 ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑘 ∘f − 𝑥) ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘})
28	27	adantll 711	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑘 ∘f − 𝑥) ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘})
29	14, 28	sselid 3975	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑘 ∘f − 𝑥) ∈ 𝐷)
30	25, 29	ffvelcdmd 7081	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑌‘(𝑘 ∘f − 𝑥)) ∈ (Base‘𝑅))
31	3, 5	ringass 20158	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ (Base‘𝑅) ∧ (𝑋‘𝑥) ∈ (Base‘𝑅) ∧ (𝑌‘(𝑘 ∘f − 𝑥)) ∈ (Base‘𝑅))) → ((𝐴(.r‘𝑅)(𝑋‘𝑥))(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))) = (𝐴(.r‘𝑅)((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))
32	20, 11, 22, 30, 31	syl13anc 1369	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝐴(.r‘𝑅)(𝑋‘𝑥))(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))) = (𝐴(.r‘𝑅)((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))
33	18, 32	eqtrd 2766	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (((𝐴 · 𝑋)‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))) = (𝐴(.r‘𝑅)((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))
34	33	mpteq2dva 5241	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ (((𝐴 · 𝑋)‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ (𝐴(.r‘𝑅)((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))))
35	34	oveq2d 7421	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ (((𝐴 · 𝑋)‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))) = (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ (𝐴(.r‘𝑅)((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))))
36		eqid 2726	. . . . 5 ⊢ (0g‘𝑅) = (0g‘𝑅)
37	19	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑅 ∈ Ring)
38	6	psrbaglefi 21826	. . . . . 6 ⊢ (𝑘 ∈ 𝐷 → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ∈ Fin)
39	38	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ∈ Fin)
40	3, 5, 20, 22, 30	ringcld 20162	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))) ∈ (Base‘𝑅))
41		ovex 7438	. . . . . . . . . 10 ⊢ (ℕ0 ↑m 𝐼) ∈ V
42	6, 41	rabex2 5327	. . . . . . . . 9 ⊢ 𝐷 ∈ V
43	42	mptrabex 7222	. . . . . . . 8 ⊢ (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) ∈ V
44		funmpt 6580	. . . . . . . 8 ⊢ Fun (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))
45		fvex 6898	. . . . . . . 8 ⊢ (0g‘𝑅) ∈ V
46	43, 44, 45	3pm3.2i 1336	. . . . . . 7 ⊢ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) ∈ V ∧ Fun (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) ∧ (0g‘𝑅) ∈ V)
47	46	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) ∈ V ∧ Fun (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) ∧ (0g‘𝑅) ∈ V))
48		suppssdm 8162	. . . . . . . 8 ⊢ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) supp (0g‘𝑅)) ⊆ dom (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))
49		eqid 2726	. . . . . . . . 9 ⊢ (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))
50	49	dmmptss 6234	. . . . . . . 8 ⊢ dom (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) ⊆ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}
51	48, 50	sstri 3986	. . . . . . 7 ⊢ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) supp (0g‘𝑅)) ⊆ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}
52	51	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) supp (0g‘𝑅)) ⊆ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘})
53		suppssfifsupp 9380	. . . . . 6 ⊢ ((((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) ∈ V ∧ Fun (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) ∧ (0g‘𝑅) ∈ V) ∧ ({𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ∈ Fin ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) supp (0g‘𝑅)) ⊆ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘})) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) finSupp (0g‘𝑅))
54	47, 39, 52, 53	syl12anc 834	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) finSupp (0g‘𝑅))
55	3, 36, 5, 37, 39, 10, 40, 54	gsummulc2 20216	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ (𝐴(.r‘𝑅)((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))) = (𝐴(.r‘𝑅)(𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))))
56	35, 55	eqtrd 2766	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ (((𝐴 · 𝑋)‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))) = (𝐴(.r‘𝑅)(𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))))
57	56	mpteq2dva 5241	. 2 ⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ (((𝐴 · 𝑋)‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))) = (𝑘 ∈ 𝐷 ↦ (𝐴(.r‘𝑅)(𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))))))
58		psrass.t	. . 3 ⊢ × = (.r‘𝑆)
59	1, 2, 9, 4, 19, 7, 12	psrvscacl 21854	. . 3 ⊢ (𝜑 → (𝐴 · 𝑋) ∈ 𝐵)
60	1, 4, 5, 58, 6, 59, 23	psrmulfval 21846	. 2 ⊢ (𝜑 → ((𝐴 · 𝑋) × 𝑌) = (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ (((𝐴 · 𝑋)‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))))
61	1, 4, 58, 19, 12, 23	psrmulcl 21849	. . . 4 ⊢ (𝜑 → (𝑋 × 𝑌) ∈ 𝐵)
62	1, 2, 9, 4, 5, 6, 7, 61	psrvsca 21852	. . 3 ⊢ (𝜑 → (𝐴 · (𝑋 × 𝑌)) = ((𝐷 × {𝐴}) ∘f (.r‘𝑅)(𝑋 × 𝑌)))
63	42	a1i 11	. . . 4 ⊢ (𝜑 → 𝐷 ∈ V)
64		ovexd 7440	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))) ∈ V)
65		fconstmpt 5731	. . . . 5 ⊢ (𝐷 × {𝐴}) = (𝑘 ∈ 𝐷 ↦ 𝐴)
66	65	a1i 11	. . . 4 ⊢ (𝜑 → (𝐷 × {𝐴}) = (𝑘 ∈ 𝐷 ↦ 𝐴))
67	1, 4, 5, 58, 6, 12, 23	psrmulfval 21846	. . . 4 ⊢ (𝜑 → (𝑋 × 𝑌) = (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))))
68	63, 8, 64, 66, 67	offval2 7687	. . 3 ⊢ (𝜑 → ((𝐷 × {𝐴}) ∘f (.r‘𝑅)(𝑋 × 𝑌)) = (𝑘 ∈ 𝐷 ↦ (𝐴(.r‘𝑅)(𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))))))
69	62, 68	eqtrd 2766	. 2 ⊢ (𝜑 → (𝐴 · (𝑋 × 𝑌)) = (𝑘 ∈ 𝐷 ↦ (𝐴(.r‘𝑅)(𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))))))
70	57, 60, 69	3eqtr4d 2776	1 ⊢ (𝜑 → ((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌)))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  {crab 3426  Vcvv 3468   ⊆ wss 3943  {csn 4623   class class class wbr 5141   ↦ cmpt 5224   × cxp 5667  ^◡ccnv 5668  dom cdm 5669   “ cima 5672  Fun wfun 6531  ‘cfv 6537  (class class class)co 7405   ∘_f cof 7665   ∘_r cofr 7666   supp csupp 8146   ↑_m cmap 8822  Fincfn 8941   finSupp cfsupp 9363   ≤ cle 11253   − cmin 11448  ℕcn 12216  ℕ₀cn0 12476  Basecbs 17153  ._rcmulr 17207   ·_𝑠 cvsca 17210  0_gc0g 17394   Σ_g cgsu 17395  Ringcrg 20138   mPwSer cmps 21798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-se 5625  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7667  df-ofr 7668  df-om 7853  df-1st 7974  df-2nd 7975  df-supp 8147  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-1o 8467  df-er 8705  df-map 8824  df-pm 8825  df-ixp 8894  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9364  df-oi 9507  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-nn 12217  df-2 12279  df-3 12280  df-4 12281  df-5 12282  df-6 12283  df-7 12284  df-8 12285  df-9 12286  df-n0 12477  df-z 12563  df-uz 12827  df-fz 13491  df-fzo 13634  df-seq 13973  df-hash 14296  df-struct 17089  df-sets 17106  df-slot 17124  df-ndx 17136  df-base 17154  df-plusg 17219  df-mulr 17220  df-sca 17222  df-vsca 17223  df-tset 17225  df-0g 17396  df-gsum 17397  df-mgm 18573  df-sgrp 18652  df-mnd 18668  df-mhm 18713  df-grp 18866  df-minusg 18867  df-ghm 19139  df-cntz 19233  df-cmn 19702  df-abl 19703  df-mgp 20040  df-ur 20087  df-ring 20140  df-psr 21803

This theorem is referenced by:  psrass23  21872  ply1ass23l  22100