Theorem psrridm 19225

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 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ 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 2610	. . . 4 ⊢ (Base‘𝑅) = (Base‘𝑅)
3		psr1cl.d	. . . 4 ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ 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 19223	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ 𝐵)
13	1, 4, 5, 6, 7, 12	psrmulcl 19209	. . . 4 ⊢ (𝜑 → (𝑋 · 𝑈) ∈ 𝐵)
14	1, 2, 3, 4, 13	psrelbas 19200	. . 3 ⊢ (𝜑 → (𝑋 · 𝑈):𝐷⟶(Base‘𝑅))
15	14	ffnd 5959	. 2 ⊢ (𝜑 → (𝑋 · 𝑈) Fn 𝐷)
16	1, 2, 3, 4, 7	psrelbas 19200	. . 3 ⊢ (𝜑 → 𝑋:𝐷⟶(Base‘𝑅))
17	16	ffnd 5959	. 2 ⊢ (𝜑 → 𝑋 Fn 𝐷)
18		eqid 2610	. . . 4 ⊢ (.r‘𝑅) = (.r‘𝑅)
19	7	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑋 ∈ 𝐵)
20	12	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑈 ∈ 𝐵)
21		simpr 476	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦 ∈ 𝐷)
22	1, 4, 18, 5, 3, 19, 20, 21	psrmulval 19207	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑋 · 𝑈)‘𝑦) = (𝑅 Σg (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑧))))))
23	8	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝐼 ∈ 𝑉)
24	3	psrbagf 19186	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑦 ∈ 𝐷) → 𝑦:𝐼⟶ℕ0)
25	8, 24	sylan 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦:𝐼⟶ℕ0)
26		nn0re 11178	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ℕ0 → 𝑧 ∈ ℝ)
27	26	leidd 10473	. . . . . . . . . 10 ⊢ (𝑧 ∈ ℕ0 → 𝑧 ≤ 𝑧)
28	27	adantl 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ℕ0) → 𝑧 ≤ 𝑧)
29	23, 25, 28	caofref 6821	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦 ∘𝑟 ≤ 𝑦)
30		breq1 4586	. . . . . . . . 9 ⊢ (𝑔 = 𝑦 → (𝑔 ∘𝑟 ≤ 𝑦 ↔ 𝑦 ∘𝑟 ≤ 𝑦))
31	30	elrab 3331	. . . . . . . 8 ⊢ (𝑦 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↔ (𝑦 ∈ 𝐷 ∧ 𝑦 ∘𝑟 ≤ 𝑦))
32	21, 29, 31	sylanbrc 695	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦})
33	32	snssd 4281	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → {𝑦} ⊆ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦})
34	33	resmptd 5371	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑧)))) ↾ {𝑦}) = (𝑧 ∈ {𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑧)))))
35	34	oveq2d 6565	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑧)))) ↾ {𝑦})) = (𝑅 Σg (𝑧 ∈ {𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑧))))))
36		ringcmn 18404	. . . . . . 7 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
37	6, 36	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ CMnd)
38	37	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑅 ∈ CMnd)
39		ovex 6577	. . . . . . 7 ⊢ (ℕ0 ↑𝑚 𝐼) ∈ V
40	3, 39	rab2ex 4743	. . . . . 6 ⊢ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∈ V
41	40	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∈ V)
42	6	ad2antrr 758	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → 𝑅 ∈ Ring)
43	16	ad2antrr 758	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → 𝑋:𝐷⟶(Base‘𝑅))
44		simpr 476	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦})
45		breq1 4586	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑧 → (𝑔 ∘𝑟 ≤ 𝑦 ↔ 𝑧 ∘𝑟 ≤ 𝑦))
46	45	elrab 3331	. . . . . . . . . 10 ⊢ (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↔ (𝑧 ∈ 𝐷 ∧ 𝑧 ∘𝑟 ≤ 𝑦))
47	44, 46	sylib 207	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → (𝑧 ∈ 𝐷 ∧ 𝑧 ∘𝑟 ≤ 𝑦))
48	47	simpld 474	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → 𝑧 ∈ 𝐷)
49	43, 48	ffvelrnd 6268	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → (𝑋‘𝑧) ∈ (Base‘𝑅))
50	1, 2, 3, 4, 20	psrelbas 19200	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑈:𝐷⟶(Base‘𝑅))
51	50	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → 𝑈:𝐷⟶(Base‘𝑅))
52	8	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → 𝐼 ∈ 𝑉)
53	21	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → 𝑦 ∈ 𝐷)
54	3	psrbagf 19186	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝐷) → 𝑧:𝐼⟶ℕ0)
55	52, 48, 54	syl2anc 691	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → 𝑧:𝐼⟶ℕ0)
56	47	simprd 478	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → 𝑧 ∘𝑟 ≤ 𝑦)
57	3	psrbagcon 19192	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ 𝐷 ∧ 𝑧:𝐼⟶ℕ0 ∧ 𝑧 ∘𝑟 ≤ 𝑦)) → ((𝑦 ∘𝑓 − 𝑧) ∈ 𝐷 ∧ (𝑦 ∘𝑓 − 𝑧) ∘𝑟 ≤ 𝑦))
58	52, 53, 55, 56, 57	syl13anc 1320	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → ((𝑦 ∘𝑓 − 𝑧) ∈ 𝐷 ∧ (𝑦 ∘𝑓 − 𝑧) ∘𝑟 ≤ 𝑦))
59	58	simpld 474	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → (𝑦 ∘𝑓 − 𝑧) ∈ 𝐷)
60	51, 59	ffvelrnd 6268	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → (𝑈‘(𝑦 ∘𝑓 − 𝑧)) ∈ (Base‘𝑅))
61	2, 18	ringcl 18384	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑧) ∈ (Base‘𝑅) ∧ (𝑈‘(𝑦 ∘𝑓 − 𝑧)) ∈ (Base‘𝑅)) → ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑧))) ∈ (Base‘𝑅))
62	42, 49, 60, 61	syl3anc 1318	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑧))) ∈ (Base‘𝑅))
63		eqid 2610	. . . . . 6 ⊢ (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑧)))) = (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑧))))
64	62, 63	fmptd 6292	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑧)))):{𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}⟶(Base‘𝑅))
65		eldifi 3694	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {𝑦}) → 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦})
66	65, 59	sylan2 490	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {𝑦})) → (𝑦 ∘𝑓 − 𝑧) ∈ 𝐷)
67		eqeq1 2614	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑦 ∘𝑓 − 𝑧) → (𝑥 = (𝐼 × {0}) ↔ (𝑦 ∘𝑓 − 𝑧) = (𝐼 × {0})))
68	67	ifbid 4058	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑦 ∘𝑓 − 𝑧) → if(𝑥 = (𝐼 × {0}), 1 , 0 ) = if((𝑦 ∘𝑓 − 𝑧) = (𝐼 × {0}), 1 , 0 ))
69		fvex 6113	. . . . . . . . . . . . 13 ⊢ (1r‘𝑅) ∈ V
70	10, 69	eqeltri 2684	. . . . . . . . . . . 12 ⊢ 1 ∈ V
71		fvex 6113	. . . . . . . . . . . . 13 ⊢ (0g‘𝑅) ∈ V
72	9, 71	eqeltri 2684	. . . . . . . . . . . 12 ⊢ 0 ∈ V
73	70, 72	ifex 4106	. . . . . . . . . . 11 ⊢ if((𝑦 ∘𝑓 − 𝑧) = (𝐼 × {0}), 1 , 0 ) ∈ V
74	68, 11, 73	fvmpt 6191	. . . . . . . . . 10 ⊢ ((𝑦 ∘𝑓 − 𝑧) ∈ 𝐷 → (𝑈‘(𝑦 ∘𝑓 − 𝑧)) = if((𝑦 ∘𝑓 − 𝑧) = (𝐼 × {0}), 1 , 0 ))
75	66, 74	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {𝑦})) → (𝑈‘(𝑦 ∘𝑓 − 𝑧)) = if((𝑦 ∘𝑓 − 𝑧) = (𝐼 × {0}), 1 , 0 ))
76		eldifsni 4261	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {𝑦}) → 𝑧 ≠ 𝑦)
77	76	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {𝑦})) → 𝑧 ≠ 𝑦)
78	77	necomd 2837	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {𝑦})) → 𝑦 ≠ 𝑧)
79		nn0sscn 11174	. . . . . . . . . . . . . . . 16 ⊢ ℕ0 ⊆ ℂ
80		fss 5969	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦:𝐼⟶ℕ0 ∧ ℕ0 ⊆ ℂ) → 𝑦:𝐼⟶ℂ)
81	25, 79, 80	sylancl 693	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦:𝐼⟶ℂ)
82	81	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → 𝑦:𝐼⟶ℂ)
83		fss 5969	. . . . . . . . . . . . . . 15 ⊢ ((𝑧:𝐼⟶ℕ0 ∧ ℕ0 ⊆ ℂ) → 𝑧:𝐼⟶ℂ)
84	55, 79, 83	sylancl 693	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → 𝑧:𝐼⟶ℂ)
85		ofsubeq0 10894	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑦:𝐼⟶ℂ ∧ 𝑧:𝐼⟶ℂ) → ((𝑦 ∘𝑓 − 𝑧) = (𝐼 × {0}) ↔ 𝑦 = 𝑧))
86	52, 82, 84, 85	syl3anc 1318	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → ((𝑦 ∘𝑓 − 𝑧) = (𝐼 × {0}) ↔ 𝑦 = 𝑧))
87	65, 86	sylan2 490	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {𝑦})) → ((𝑦 ∘𝑓 − 𝑧) = (𝐼 × {0}) ↔ 𝑦 = 𝑧))
88	87	necon3bbid 2819	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {𝑦})) → (¬ (𝑦 ∘𝑓 − 𝑧) = (𝐼 × {0}) ↔ 𝑦 ≠ 𝑧))
89	78, 88	mpbird 246	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {𝑦})) → ¬ (𝑦 ∘𝑓 − 𝑧) = (𝐼 × {0}))
90	89	iffalsed 4047	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {𝑦})) → if((𝑦 ∘𝑓 − 𝑧) = (𝐼 × {0}), 1 , 0 ) = 0 )
91	75, 90	eqtrd 2644	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {𝑦})) → (𝑈‘(𝑦 ∘𝑓 − 𝑧)) = 0 )
92	91	oveq2d 6565	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {𝑦})) → ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑧))) = ((𝑋‘𝑧)(.r‘𝑅) 0 ))
93	2, 18, 9	ringrz 18411	. . . . . . . . 9 ⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑧) ∈ (Base‘𝑅)) → ((𝑋‘𝑧)(.r‘𝑅) 0 ) = 0 )
94	42, 49, 93	syl2anc 691	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → ((𝑋‘𝑧)(.r‘𝑅) 0 ) = 0 )
95	65, 94	sylan2 490	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {𝑦})) → ((𝑋‘𝑧)(.r‘𝑅) 0 ) = 0 )
96	92, 95	eqtrd 2644	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {𝑦})) → ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑧))) = 0 )
97	96, 41	suppss2 7216	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑧)))) supp 0 ) ⊆ {𝑦})
98		mptexg 6389	. . . . . . 7 ⊢ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∈ V → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑧)))) ∈ V)
99	41, 98	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑧)))) ∈ V)
100		funmpt 5840	. . . . . . 7 ⊢ Fun (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑧))))
101	100	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → Fun (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑧)))))
102	72	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 0 ∈ V)
103		snfi 7923	. . . . . . 7 ⊢ {𝑦} ∈ Fin
104	103	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → {𝑦} ∈ Fin)
105		suppssfifsupp 8173	. . . . . 6 ⊢ ((((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑧)))) ∈ V ∧ Fun (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑧)))) ∧ 0 ∈ V) ∧ ({𝑦} ∈ Fin ∧ ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑧)))) supp 0 ) ⊆ {𝑦})) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑧)))) finSupp 0 )
106	99, 101, 102, 104, 97, 105	syl32anc 1326	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑧)))) finSupp 0 )
107	2, 9, 38, 41, 64, 97, 106	gsumres 18137	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑧)))) ↾ {𝑦})) = (𝑅 Σg (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑧))))))
108	6	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑅 ∈ Ring)
109		ringmnd 18379	. . . . . 6 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
110	108, 109	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑅 ∈ Mnd)
111		eqid 2610	. . . . . . . . . . 11 ⊢ 𝑦 = 𝑦
112		ofsubeq0 10894	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑦:𝐼⟶ℂ ∧ 𝑦:𝐼⟶ℂ) → ((𝑦 ∘𝑓 − 𝑦) = (𝐼 × {0}) ↔ 𝑦 = 𝑦))
113	23, 81, 81, 112	syl3anc 1318	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑦 ∘𝑓 − 𝑦) = (𝐼 × {0}) ↔ 𝑦 = 𝑦))
114	111, 113	mpbiri 247	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑦 ∘𝑓 − 𝑦) = (𝐼 × {0}))
115	114	fveq2d 6107	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑈‘(𝑦 ∘𝑓 − 𝑦)) = (𝑈‘(𝐼 × {0})))
116		fconstmpt 5085	. . . . . . . . . . . 12 ⊢ (𝐼 × {0}) = (𝑤 ∈ 𝐼 ↦ 0)
117	3	fczpsrbag 19188	. . . . . . . . . . . . 13 ⊢ (𝐼 ∈ 𝑉 → (𝑤 ∈ 𝐼 ↦ 0) ∈ 𝐷)
118	8, 117	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑤 ∈ 𝐼 ↦ 0) ∈ 𝐷)
119	116, 118	syl5eqel 2692	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐼 × {0}) ∈ 𝐷)
120	119	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐼 × {0}) ∈ 𝐷)
121		iftrue 4042	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐼 × {0}) → if(𝑥 = (𝐼 × {0}), 1 , 0 ) = 1 )
122	121, 11, 70	fvmpt 6191	. . . . . . . . . 10 ⊢ ((𝐼 × {0}) ∈ 𝐷 → (𝑈‘(𝐼 × {0})) = 1 )
123	120, 122	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑈‘(𝐼 × {0})) = 1 )
124	115, 123	eqtrd 2644	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑈‘(𝑦 ∘𝑓 − 𝑦)) = 1 )
125	124	oveq2d 6565	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑋‘𝑦)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑦))) = ((𝑋‘𝑦)(.r‘𝑅) 1 ))
126	16	ffvelrnda 6267	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑋‘𝑦) ∈ (Base‘𝑅))
127	2, 18, 10	ringridm 18395	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑦) ∈ (Base‘𝑅)) → ((𝑋‘𝑦)(.r‘𝑅) 1 ) = (𝑋‘𝑦))
128	108, 126, 127	syl2anc 691	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑋‘𝑦)(.r‘𝑅) 1 ) = (𝑋‘𝑦))
129	125, 128	eqtrd 2644	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑋‘𝑦)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑦))) = (𝑋‘𝑦))
130	129, 126	eqeltrd 2688	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑋‘𝑦)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑦))) ∈ (Base‘𝑅))
131		fveq2 6103	. . . . . . 7 ⊢ (𝑧 = 𝑦 → (𝑋‘𝑧) = (𝑋‘𝑦))
132		oveq2 6557	. . . . . . . 8 ⊢ (𝑧 = 𝑦 → (𝑦 ∘𝑓 − 𝑧) = (𝑦 ∘𝑓 − 𝑦))
133	132	fveq2d 6107	. . . . . . 7 ⊢ (𝑧 = 𝑦 → (𝑈‘(𝑦 ∘𝑓 − 𝑧)) = (𝑈‘(𝑦 ∘𝑓 − 𝑦)))
134	131, 133	oveq12d 6567	. . . . . 6 ⊢ (𝑧 = 𝑦 → ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑧))) = ((𝑋‘𝑦)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑦))))
135	2, 134	gsumsn 18177	. . . . 5 ⊢ ((𝑅 ∈ Mnd ∧ 𝑦 ∈ 𝐷 ∧ ((𝑋‘𝑦)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑦))) ∈ (Base‘𝑅)) → (𝑅 Σg (𝑧 ∈ {𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑧))))) = ((𝑋‘𝑦)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑦))))
136	110, 21, 130, 135	syl3anc 1318	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg (𝑧 ∈ {𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑧))))) = ((𝑋‘𝑦)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑦))))
137	35, 107, 136	3eqtr3d 2652	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑧))))) = ((𝑋‘𝑦)(.r‘𝑅)(𝑈‘(𝑦 ∘𝑓 − 𝑦))))
138	22, 137, 129	3eqtrd 2648	. 2 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑋 · 𝑈)‘𝑦) = (𝑋‘𝑦))
139	15, 17, 138	eqfnfvd 6222	1 ⊢ (𝜑 → (𝑋 · 𝑈) = 𝑋)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  {crab 2900  Vcvv 3173   ∖ cdif 3537   ⊆ wss 3540  ifcif 4036  {csn 4125   class class class wbr 4583   ↦ cmpt 4643   × cxp 5036  ^◡ccnv 5037   ↾ cres 5040   “ cima 5041  Fun wfun 5798  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ∘_𝑓 cof 6793   ∘_𝑟 cofr 6794   supp csupp 7182   ↑_𝑚 cmap 7744  Fincfn 7841   finSupp cfsupp 8158  ℂcc 9813  0cc0 9815   ≤ cle 9954   − cmin 10145  ℕcn 10897  ℕ₀cn0 11169  Basecbs 15695  ._rcmulr 15769  0_gc0g 15923   Σ_g cgsu 15924  Mndcmnd 17117  CMndccmn 18016  1_rcur 18324  Ringcrg 18370   mPwSer cmps 19172

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-ofr 6796  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fsupp 8159  df-oi 8298  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-fzo 12335  df-seq 12664  df-hash 12980  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-plusg 15781  df-mulr 15782  df-sca 15784  df-vsca 15785  df-tset 15787  df-0g 15925  df-gsum 15926  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-grp 17248  df-minusg 17249  df-mulg 17364  df-cntz 17573  df-cmn 18018  df-abl 18019  df-mgp 18313  df-ur 18325  df-ring 18372  df-psr 19177

This theorem is referenced by:  psrring  19232  psr1  19233