Theorem psrridm 21373

Description: The identity element of the ring of power series is a right identity. (Contributed by Mario Carneiro, 29-Dec-2014.) (Proof shortened by AV, 8-Jul-2019.)

Hypotheses

Ref	Expression
psrring.s	⊢ 𝑆 = (𝐼 mPwSer 𝑅)
psrring.i	⊢ (𝜑 → 𝐼 ∈ 𝑉)
psrring.r	⊢ (𝜑 → 𝑅 ∈ Ring)
psr1cl.d	⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}
psr1cl.z	⊢ 0 = (0g‘𝑅)
psr1cl.o	⊢ 1 = (1r‘𝑅)
psr1cl.u	⊢ 𝑈 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = (𝐼 × {0}), 1 , 0 ))
psr1cl.b	⊢ 𝐵 = (Base‘𝑆)
psrlidm.t	⊢ · = (.r‘𝑆)
psrlidm.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)

Assertion

Ref	Expression
psrridm	⊢ (𝜑 → (𝑋 · 𝑈) = 𝑋)

Distinct variable groups:   𝑥,𝑓, 0   𝑓,𝐼,𝑥   𝑥,𝐵   𝑅,𝑓,𝑥   𝑥,𝐷   𝑓,𝑋,𝑥   𝜑,𝑥   𝑥,𝑉   𝑥, ·   𝑥,𝑆   𝑥, 1

Allowed substitution hints:   𝜑(𝑓)   𝐵(𝑓)   𝐷(𝑓)   𝑆(𝑓)   · (𝑓)   𝑈(𝑥,𝑓)   1 (𝑓)   𝑉(𝑓)

Proof of Theorem psrridm

Dummy variables 𝑦 𝑧 𝑔 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		psrring.s	. . . 4 ⊢ 𝑆 = (𝐼 mPwSer 𝑅)
2		eqid 2736	. . . 4 ⊢ (Base‘𝑅) = (Base‘𝑅)
3		psr1cl.d	. . . 4 ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}
4		psr1cl.b	. . . 4 ⊢ 𝐵 = (Base‘𝑆)
5		psrlidm.t	. . . . 5 ⊢ · = (.r‘𝑆)
6		psrring.r	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ Ring)
7		psrlidm.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
8		psrring.i	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
9		psr1cl.z	. . . . . 6 ⊢ 0 = (0g‘𝑅)
10		psr1cl.o	. . . . . 6 ⊢ 1 = (1r‘𝑅)
11		psr1cl.u	. . . . . 6 ⊢ 𝑈 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = (𝐼 × {0}), 1 , 0 ))
12	1, 8, 6, 3, 9, 10, 11, 4	psr1cl 21371	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ 𝐵)
13	1, 4, 5, 6, 7, 12	psrmulcl 21356	. . . 4 ⊢ (𝜑 → (𝑋 · 𝑈) ∈ 𝐵)
14	1, 2, 3, 4, 13	psrelbas 21347	. . 3 ⊢ (𝜑 → (𝑋 · 𝑈):𝐷⟶(Base‘𝑅))
15	14	ffnd 6669	. 2 ⊢ (𝜑 → (𝑋 · 𝑈) Fn 𝐷)
16	1, 2, 3, 4, 7	psrelbas 21347	. . 3 ⊢ (𝜑 → 𝑋:𝐷⟶(Base‘𝑅))
17	16	ffnd 6669	. 2 ⊢ (𝜑 → 𝑋 Fn 𝐷)
18		eqid 2736	. . . 4 ⊢ (.r‘𝑅) = (.r‘𝑅)
19	7	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑋 ∈ 𝐵)
20	12	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑈 ∈ 𝐵)
21		simpr 485	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦 ∈ 𝐷)
22	1, 4, 18, 5, 3, 19, 20, 21	psrmulval 21354	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑋 · 𝑈)‘𝑦) = (𝑅 Σg (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧))))))
23		breq1 5108	. . . . . . . 8 ⊢ (𝑔 = 𝑦 → (𝑔 ∘r ≤ 𝑦 ↔ 𝑦 ∘r ≤ 𝑦))
24	8	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝐼 ∈ 𝑉)
25	3	psrbagf 21320	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝐷 → 𝑦:𝐼⟶ℕ0)
26	25	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦:𝐼⟶ℕ0)
27		nn0re 12422	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ℕ0 → 𝑧 ∈ ℝ)
28	27	leidd 11721	. . . . . . . . . 10 ⊢ (𝑧 ∈ ℕ0 → 𝑧 ≤ 𝑧)
29	28	adantl 482	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ℕ0) → 𝑧 ≤ 𝑧)
30	24, 26, 29	caofref 7646	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦 ∘r ≤ 𝑦)
31	23, 21, 30	elrabd 3647	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦})
32	31	snssd 4769	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → {𝑦} ⊆ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦})
33	32	resmptd 5994	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧)))) ↾ {𝑦}) = (𝑧 ∈ {𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧)))))
34	33	oveq2d 7373	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧)))) ↾ {𝑦})) = (𝑅 Σg (𝑧 ∈ {𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧))))))
35		ringcmn 20003	. . . . . . 7 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
36	6, 35	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ CMnd)
37	36	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑅 ∈ CMnd)
38		ovex 7390	. . . . . . 7 ⊢ (ℕ0 ↑m 𝐼) ∈ V
39	3, 38	rab2ex 5292	. . . . . 6 ⊢ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∈ V
40	39	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∈ V)
41	6	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑅 ∈ Ring)
42	16	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑋:𝐷⟶(Base‘𝑅))
43		simpr 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦})
44		breq1 5108	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑧 → (𝑔 ∘r ≤ 𝑦 ↔ 𝑧 ∘r ≤ 𝑦))
45	44	elrab 3645	. . . . . . . . . 10 ⊢ (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↔ (𝑧 ∈ 𝐷 ∧ 𝑧 ∘r ≤ 𝑦))
46	43, 45	sylib 217	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → (𝑧 ∈ 𝐷 ∧ 𝑧 ∘r ≤ 𝑦))
47	46	simpld 495	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑧 ∈ 𝐷)
48	42, 47	ffvelcdmd 7036	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → (𝑋‘𝑧) ∈ (Base‘𝑅))
49	1, 2, 3, 4, 20	psrelbas 21347	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑈:𝐷⟶(Base‘𝑅))
50	49	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑈:𝐷⟶(Base‘𝑅))
51	21	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑦 ∈ 𝐷)
52	3	psrbagf 21320	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐷 → 𝑧:𝐼⟶ℕ0)
53	47, 52	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑧:𝐼⟶ℕ0)
54	46	simprd 496	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑧 ∘r ≤ 𝑦)
55	3	psrbagcon 21332	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝐷 ∧ 𝑧:𝐼⟶ℕ0 ∧ 𝑧 ∘r ≤ 𝑦) → ((𝑦 ∘f − 𝑧) ∈ 𝐷 ∧ (𝑦 ∘f − 𝑧) ∘r ≤ 𝑦))
56	51, 53, 54, 55	syl3anc 1371	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → ((𝑦 ∘f − 𝑧) ∈ 𝐷 ∧ (𝑦 ∘f − 𝑧) ∘r ≤ 𝑦))
57	56	simpld 495	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → (𝑦 ∘f − 𝑧) ∈ 𝐷)
58	50, 57	ffvelcdmd 7036	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → (𝑈‘(𝑦 ∘f − 𝑧)) ∈ (Base‘𝑅))
59	2, 18	ringcl 19981	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑧) ∈ (Base‘𝑅) ∧ (𝑈‘(𝑦 ∘f − 𝑧)) ∈ (Base‘𝑅)) → ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧))) ∈ (Base‘𝑅))
60	41, 48, 58, 59	syl3anc 1371	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧))) ∈ (Base‘𝑅))
61	60	fmpttd 7063	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧)))):{𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}⟶(Base‘𝑅))
62		eldifi 4086	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {𝑦}) → 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦})
63	62, 57	sylan2 593	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {𝑦})) → (𝑦 ∘f − 𝑧) ∈ 𝐷)
64		eqeq1 2740	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑦 ∘f − 𝑧) → (𝑥 = (𝐼 × {0}) ↔ (𝑦 ∘f − 𝑧) = (𝐼 × {0})))
65	64	ifbid 4509	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑦 ∘f − 𝑧) → if(𝑥 = (𝐼 × {0}), 1 , 0 ) = if((𝑦 ∘f − 𝑧) = (𝐼 × {0}), 1 , 0 ))
66	10	fvexi 6856	. . . . . . . . . . . 12 ⊢ 1 ∈ V
67	9	fvexi 6856	. . . . . . . . . . . 12 ⊢ 0 ∈ V
68	66, 67	ifex 4536	. . . . . . . . . . 11 ⊢ if((𝑦 ∘f − 𝑧) = (𝐼 × {0}), 1 , 0 ) ∈ V
69	65, 11, 68	fvmpt 6948	. . . . . . . . . 10 ⊢ ((𝑦 ∘f − 𝑧) ∈ 𝐷 → (𝑈‘(𝑦 ∘f − 𝑧)) = if((𝑦 ∘f − 𝑧) = (𝐼 × {0}), 1 , 0 ))
70	63, 69	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {𝑦})) → (𝑈‘(𝑦 ∘f − 𝑧)) = if((𝑦 ∘f − 𝑧) = (𝐼 × {0}), 1 , 0 ))
71		eldifsni 4750	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {𝑦}) → 𝑧 ≠ 𝑦)
72	71	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {𝑦})) → 𝑧 ≠ 𝑦)
73	72	necomd 2999	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {𝑦})) → 𝑦 ≠ 𝑧)
74	24	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝐼 ∈ 𝑉)
75		nn0sscn 12418	. . . . . . . . . . . . . . . 16 ⊢ ℕ0 ⊆ ℂ
76		fss 6685	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦:𝐼⟶ℕ0 ∧ ℕ0 ⊆ ℂ) → 𝑦:𝐼⟶ℂ)
77	26, 75, 76	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦:𝐼⟶ℂ)
78	77	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑦:𝐼⟶ℂ)
79		fss 6685	. . . . . . . . . . . . . . 15 ⊢ ((𝑧:𝐼⟶ℕ0 ∧ ℕ0 ⊆ ℂ) → 𝑧:𝐼⟶ℂ)
80	53, 75, 79	sylancl 586	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑧:𝐼⟶ℂ)
81		ofsubeq0 12150	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑦:𝐼⟶ℂ ∧ 𝑧:𝐼⟶ℂ) → ((𝑦 ∘f − 𝑧) = (𝐼 × {0}) ↔ 𝑦 = 𝑧))
82	74, 78, 80, 81	syl3anc 1371	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → ((𝑦 ∘f − 𝑧) = (𝐼 × {0}) ↔ 𝑦 = 𝑧))
83	62, 82	sylan2 593	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {𝑦})) → ((𝑦 ∘f − 𝑧) = (𝐼 × {0}) ↔ 𝑦 = 𝑧))
84	83	necon3bbid 2981	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {𝑦})) → (¬ (𝑦 ∘f − 𝑧) = (𝐼 × {0}) ↔ 𝑦 ≠ 𝑧))
85	73, 84	mpbird 256	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {𝑦})) → ¬ (𝑦 ∘f − 𝑧) = (𝐼 × {0}))
86	85	iffalsed 4497	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {𝑦})) → if((𝑦 ∘f − 𝑧) = (𝐼 × {0}), 1 , 0 ) = 0 )
87	70, 86	eqtrd 2776	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {𝑦})) → (𝑈‘(𝑦 ∘f − 𝑧)) = 0 )
88	87	oveq2d 7373	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {𝑦})) → ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧))) = ((𝑋‘𝑧)(.r‘𝑅) 0 ))
89	2, 18, 9	ringrz 20012	. . . . . . . . 9 ⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑧) ∈ (Base‘𝑅)) → ((𝑋‘𝑧)(.r‘𝑅) 0 ) = 0 )
90	41, 48, 89	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → ((𝑋‘𝑧)(.r‘𝑅) 0 ) = 0 )
91	62, 90	sylan2 593	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {𝑦})) → ((𝑋‘𝑧)(.r‘𝑅) 0 ) = 0 )
92	88, 91	eqtrd 2776	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {𝑦})) → ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧))) = 0 )
93	92, 40	suppss2 8131	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧)))) supp 0 ) ⊆ {𝑦})
94	40	mptexd 7174	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧)))) ∈ V)
95		funmpt 6539	. . . . . . 7 ⊢ Fun (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧))))
96	95	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → Fun (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧)))))
97	67	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 0 ∈ V)
98		snfi 8988	. . . . . . 7 ⊢ {𝑦} ∈ Fin
99	98	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → {𝑦} ∈ Fin)
100		suppssfifsupp 9320	. . . . . 6 ⊢ ((((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧)))) ∈ V ∧ Fun (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧)))) ∧ 0 ∈ V) ∧ ({𝑦} ∈ Fin ∧ ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧)))) supp 0 ) ⊆ {𝑦})) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧)))) finSupp 0 )
101	94, 96, 97, 99, 93, 100	syl32anc 1378	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧)))) finSupp 0 )
102	2, 9, 37, 40, 61, 93, 101	gsumres 19690	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧)))) ↾ {𝑦})) = (𝑅 Σg (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧))))))
103	6	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑅 ∈ Ring)
104		ringmnd 19974	. . . . . 6 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
105	103, 104	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑅 ∈ Mnd)
106		eqid 2736	. . . . . . . . . . 11 ⊢ 𝑦 = 𝑦
107		ofsubeq0 12150	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑦:𝐼⟶ℂ ∧ 𝑦:𝐼⟶ℂ) → ((𝑦 ∘f − 𝑦) = (𝐼 × {0}) ↔ 𝑦 = 𝑦))
108	24, 77, 77, 107	syl3anc 1371	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑦 ∘f − 𝑦) = (𝐼 × {0}) ↔ 𝑦 = 𝑦))
109	106, 108	mpbiri 257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑦 ∘f − 𝑦) = (𝐼 × {0}))
110	109	fveq2d 6846	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑈‘(𝑦 ∘f − 𝑦)) = (𝑈‘(𝐼 × {0})))
111		fconstmpt 5694	. . . . . . . . . . . 12 ⊢ (𝐼 × {0}) = (𝑤 ∈ 𝐼 ↦ 0)
112	3	fczpsrbag 21325	. . . . . . . . . . . . 13 ⊢ (𝐼 ∈ 𝑉 → (𝑤 ∈ 𝐼 ↦ 0) ∈ 𝐷)
113	8, 112	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑤 ∈ 𝐼 ↦ 0) ∈ 𝐷)
114	111, 113	eqeltrid 2842	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐼 × {0}) ∈ 𝐷)
115	114	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐼 × {0}) ∈ 𝐷)
116		iftrue 4492	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐼 × {0}) → if(𝑥 = (𝐼 × {0}), 1 , 0 ) = 1 )
117	116, 11, 66	fvmpt 6948	. . . . . . . . . 10 ⊢ ((𝐼 × {0}) ∈ 𝐷 → (𝑈‘(𝐼 × {0})) = 1 )
118	115, 117	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑈‘(𝐼 × {0})) = 1 )
119	110, 118	eqtrd 2776	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑈‘(𝑦 ∘f − 𝑦)) = 1 )
120	119	oveq2d 7373	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑋‘𝑦)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑦))) = ((𝑋‘𝑦)(.r‘𝑅) 1 ))
121	16	ffvelcdmda 7035	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑋‘𝑦) ∈ (Base‘𝑅))
122	2, 18, 10	ringridm 19993	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑦) ∈ (Base‘𝑅)) → ((𝑋‘𝑦)(.r‘𝑅) 1 ) = (𝑋‘𝑦))
123	103, 121, 122	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑋‘𝑦)(.r‘𝑅) 1 ) = (𝑋‘𝑦))
124	120, 123	eqtrd 2776	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑋‘𝑦)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑦))) = (𝑋‘𝑦))
125	124, 121	eqeltrd 2838	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑋‘𝑦)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑦))) ∈ (Base‘𝑅))
126		fveq2 6842	. . . . . . 7 ⊢ (𝑧 = 𝑦 → (𝑋‘𝑧) = (𝑋‘𝑦))
127		oveq2 7365	. . . . . . . 8 ⊢ (𝑧 = 𝑦 → (𝑦 ∘f − 𝑧) = (𝑦 ∘f − 𝑦))
128	127	fveq2d 6846	. . . . . . 7 ⊢ (𝑧 = 𝑦 → (𝑈‘(𝑦 ∘f − 𝑧)) = (𝑈‘(𝑦 ∘f − 𝑦)))
129	126, 128	oveq12d 7375	. . . . . 6 ⊢ (𝑧 = 𝑦 → ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧))) = ((𝑋‘𝑦)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑦))))
130	2, 129	gsumsn 19731	. . . . 5 ⊢ ((𝑅 ∈ Mnd ∧ 𝑦 ∈ 𝐷 ∧ ((𝑋‘𝑦)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑦))) ∈ (Base‘𝑅)) → (𝑅 Σg (𝑧 ∈ {𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧))))) = ((𝑋‘𝑦)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑦))))
131	105, 21, 125, 130	syl3anc 1371	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg (𝑧 ∈ {𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧))))) = ((𝑋‘𝑦)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑦))))
132	34, 102, 131	3eqtr3d 2784	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧))))) = ((𝑋‘𝑦)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑦))))
133	22, 132, 124	3eqtrd 2780	. 2 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑋 · 𝑈)‘𝑦) = (𝑋‘𝑦))
134	15, 17, 133	eqfnfvd 6985	1 ⊢ (𝜑 → (𝑋 · 𝑈) = 𝑋)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106   ≠ wne 2943  {crab 3407  Vcvv 3445   ∖ cdif 3907   ⊆ wss 3910  ifcif 4486  {csn 4586   class class class wbr 5105   ↦ cmpt 5188   × cxp 5631  ^◡ccnv 5632   ↾ cres 5635   “ cima 5636  Fun wfun 6490  ⟶wf 6492  ‘cfv 6496  (class class class)co 7357   ∘_f cof 7615   ∘_r cofr 7616   supp csupp 8092   ↑_m cmap 8765  Fincfn 8883   finSupp cfsupp 9305  ℂcc 11049  0cc0 11051   ≤ cle 11190   − cmin 11385  ℕcn 12153  ℕ₀cn0 12413  Basecbs 17083  ._rcmulr 17134  0_gc0g 17321   Σ_g cgsu 17322  Mndcmnd 18556  CMndccmn 19562  1_rcur 19913  Ringcrg 19964   mPwSer cmps 21306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-ofr 7618  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-map 8767  df-pm 8768  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-uz 12764  df-fz 13425  df-fzo 13568  df-seq 13907  df-hash 14231  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-plusg 17146  df-mulr 17147  df-sca 17149  df-vsca 17150  df-tset 17152  df-0g 17323  df-gsum 17324  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-grp 18751  df-minusg 18752  df-mulg 18873  df-cntz 19097  df-cmn 19564  df-abl 19565  df-mgp 19897  df-ur 19914  df-ring 19966  df-psr 21311

This theorem is referenced by:  psrring  21380  psr1  21381