Theorem psrlidm 22276

Description: The identity element of the ring of power series is a left 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
psrlidm	⊢ (𝜑 → (𝑈 · 𝑋) = 𝑋)

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

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

Proof of Theorem psrlidm

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

Step	Hyp	Ref	Expression
1		psrring.s	. . . 4 ⊢ 𝑆 = (𝐼 mPwSer 𝑅)
2		eqid 2760	. . . 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		psrring.i	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
8		psr1cl.z	. . . . . 6 ⊢ 0 = (0g‘𝑅)
9		psr1cl.o	. . . . . 6 ⊢ 1 = (1r‘𝑅)
10		psr1cl.u	. . . . . 6 ⊢ 𝑈 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = (𝐼 × {0}), 1 , 0 ))
11	1, 7, 6, 3, 8, 9, 10, 4	psr1cl 22275	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ 𝐵)
12		psrlidm.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
13	1, 4, 5, 6, 11, 12	psrmulcl 22261	. . . 4 ⊢ (𝜑 → (𝑈 · 𝑋) ∈ 𝐵)
14	1, 2, 3, 4, 13	psrelbas 22250	. . 3 ⊢ (𝜑 → (𝑈 · 𝑋):𝐷⟶(Base‘𝑅))
15	14	ffnd 6713	. 2 ⊢ (𝜑 → (𝑈 · 𝑋) Fn 𝐷)
16	1, 2, 3, 4, 12	psrelbas 22250	. . 3 ⊢ (𝜑 → 𝑋:𝐷⟶(Base‘𝑅))
17	16	ffnd 6713	. 2 ⊢ (𝜑 → 𝑋 Fn 𝐷)
18		eqid 2760	. . . 4 ⊢ (.r‘𝑅) = (.r‘𝑅)
19	11	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑈 ∈ 𝐵)
20	12	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑋 ∈ 𝐵)
21		simpr 490	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦 ∈ 𝐷)
22	1, 4, 18, 5, 3, 19, 20, 21	psrmulval 22259	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑈 · 𝑋)‘𝑦) = (𝑅 Σg (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))))))
23		breq1 5105	. . . . . . . 8 ⊢ (𝑔 = (𝐼 × {0}) → (𝑔 ∘r ≤ 𝑦 ↔ (𝐼 × {0}) ∘r ≤ 𝑦))
24		fconstmpt 5712	. . . . . . . . . 10 ⊢ (𝐼 × {0}) = (𝑥 ∈ 𝐼 ↦ 0)
25	3	fczpsrbag 22236	. . . . . . . . . . 11 ⊢ (𝐼 ∈ 𝑉 → (𝑥 ∈ 𝐼 ↦ 0) ∈ 𝐷)
26	7, 25	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 0) ∈ 𝐷)
27	24, 26	eqeltrid 2864	. . . . . . . . 9 ⊢ (𝜑 → (𝐼 × {0}) ∈ 𝐷)
28	27	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐼 × {0}) ∈ 𝐷)
29	3	psrbagf 22233	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐷 → 𝑦:𝐼⟶ℕ0)
30	29	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦:𝐼⟶ℕ0)
31	30	ffvelcdmda 7087	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → (𝑦‘𝑥) ∈ ℕ0)
32	31	nn0ge0d 12675	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → 0 ≤ (𝑦‘𝑥))
33	32	ralrimiva 3154	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ∀𝑥 ∈ 𝐼 0 ≤ (𝑦‘𝑥))
34		0nn0 12626	. . . . . . . . . . . 12 ⊢ 0 ∈ ℕ0
35	34	fconst6 6775	. . . . . . . . . . 11 ⊢ (𝐼 × {0}):𝐼⟶ℕ0
36		ffn 6712	. . . . . . . . . . 11 ⊢ ((𝐼 × {0}):𝐼⟶ℕ0 → (𝐼 × {0}) Fn 𝐼)
37	35, 36	mp1i 14	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐼 × {0}) Fn 𝐼)
38	30	ffnd 6713	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦 Fn 𝐼)
39	7	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝐼 ∈ 𝑉)
40		inidm 4122	. . . . . . . . . 10 ⊢ (𝐼 ∩ 𝐼) = 𝐼
41	34	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 0 ∈ ℕ0)
42		fvconst2g 7210	. . . . . . . . . . 11 ⊢ ((0 ∈ ℕ0 ∧ 𝑥 ∈ 𝐼) → ((𝐼 × {0})‘𝑥) = 0)
43	41, 42	sylan 592	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → ((𝐼 × {0})‘𝑥) = 0)
44		eqidd 2761	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → (𝑦‘𝑥) = (𝑦‘𝑥))
45	37, 38, 39, 39, 40, 43, 44	ofrfval 7705	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝐼 × {0}) ∘r ≤ 𝑦 ↔ ∀𝑥 ∈ 𝐼 0 ≤ (𝑦‘𝑥)))
46	33, 45	mpbird 260	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐼 × {0}) ∘r ≤ 𝑦)
47	23, 28, 46	elrabd 3646	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐼 × {0}) ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦})
48	47	snssd 4743	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → {(𝐼 × {0})} ⊆ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦})
49	48	resmptd 6033	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) ↾ {(𝐼 × {0})}) = (𝑧 ∈ {(𝐼 × {0})} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))))
50	49	oveq2d 7438	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) ↾ {(𝐼 × {0})})) = (𝑅 Σg (𝑧 ∈ {(𝐼 × {0})} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))))))
51		ringcmn 20518	. . . . . . 7 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
52	6, 51	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ CMnd)
53	52	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑅 ∈ CMnd)
54		ovex 7455	. . . . . . 7 ⊢ (ℕ0 ↑m 𝐼) ∈ V
55	3, 54	rab2ex 5302	. . . . . 6 ⊢ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∈ V
56	55	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∈ V)
57	6	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑅 ∈ Ring)
58		breq1 5105	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑧 → (𝑔 ∘r ≤ 𝑦 ↔ 𝑧 ∘r ≤ 𝑦))
59	58	elrab 3644	. . . . . . . . . 10 ⊢ (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↔ (𝑧 ∈ 𝐷 ∧ 𝑧 ∘r ≤ 𝑦))
60	59	bilani 510	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → (𝑧 ∈ 𝐷 ∧ 𝑧 ∘r ≤ 𝑦))
61	60	simpld 500	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑧 ∈ 𝐷)
62	1, 2, 3, 4, 19	psrelbas 22250	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑈:𝐷⟶(Base‘𝑅))
63	62	ffvelcdmda 7087	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ 𝐷) → (𝑈‘𝑧) ∈ (Base‘𝑅))
64	61, 63	syldan 603	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → (𝑈‘𝑧) ∈ (Base‘𝑅))
65	16	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑋:𝐷⟶(Base‘𝑅))
66	21	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑦 ∈ 𝐷)
67	3	psrbagf 22233	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐷 → 𝑧:𝐼⟶ℕ0)
68	61, 67	syl 18	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑧:𝐼⟶ℕ0)
69	60	simprd 501	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑧 ∘r ≤ 𝑦)
70	3	psrbagcon 22240	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝐷 ∧ 𝑧:𝐼⟶ℕ0 ∧ 𝑧 ∘r ≤ 𝑦) → ((𝑦 ∘f − 𝑧) ∈ 𝐷 ∧ (𝑦 ∘f − 𝑧) ∘r ≤ 𝑦))
71	66, 68, 69, 70	syl3anc 1398	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → ((𝑦 ∘f − 𝑧) ∈ 𝐷 ∧ (𝑦 ∘f − 𝑧) ∘r ≤ 𝑦))
72	71	simpld 500	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → (𝑦 ∘f − 𝑧) ∈ 𝐷)
73	65, 72	ffvelcdmd 7088	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → (𝑋‘(𝑦 ∘f − 𝑧)) ∈ (Base‘𝑅))
74	2, 18	ringcl 20484	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ (𝑈‘𝑧) ∈ (Base‘𝑅) ∧ (𝑋‘(𝑦 ∘f − 𝑧)) ∈ (Base‘𝑅)) → ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))) ∈ (Base‘𝑅))
75	57, 64, 73, 74	syl3anc 1398	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))) ∈ (Base‘𝑅))
76	75	fmpttd 7118	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))):{𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}⟶(Base‘𝑅))
77		eldifi 4066	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})}) → 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦})
78	77, 60	sylan2 605	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → (𝑧 ∈ 𝐷 ∧ 𝑧 ∘r ≤ 𝑦))
79	78	simpld 500	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → 𝑧 ∈ 𝐷)
80		eqeq1 2764	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (𝑥 = (𝐼 × {0}) ↔ 𝑧 = (𝐼 × {0})))
81	80	ifbid 4505	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → if(𝑥 = (𝐼 × {0}), 1 , 0 ) = if(𝑧 = (𝐼 × {0}), 1 , 0 ))
82	9	fvexi 6902	. . . . . . . . . . . 12 ⊢ 1 ∈ V
83	8	fvexi 6902	. . . . . . . . . . . 12 ⊢ 0 ∈ V
84	82, 83	ifex 4532	. . . . . . . . . . 11 ⊢ if(𝑧 = (𝐼 × {0}), 1 , 0 ) ∈ V
85	81, 10, 84	fvmpt 6996	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝐷 → (𝑈‘𝑧) = if(𝑧 = (𝐼 × {0}), 1 , 0 ))
86	79, 85	syl 18	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → (𝑈‘𝑧) = if(𝑧 = (𝐼 × {0}), 1 , 0 ))
87		eldifn 4067	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})}) → ¬ 𝑧 ∈ {(𝐼 × {0})})
88	87	adantl 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → ¬ 𝑧 ∈ {(𝐼 × {0})})
89		velsn 4596	. . . . . . . . . . 11 ⊢ (𝑧 ∈ {(𝐼 × {0})} ↔ 𝑧 = (𝐼 × {0}))
90	88, 89	sylnib 331	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → ¬ 𝑧 = (𝐼 × {0}))
91	90	iffalsed 4492	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → if(𝑧 = (𝐼 × {0}), 1 , 0 ) = 0 )
92	86, 91	eqtrd 2795	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → (𝑈‘𝑧) = 0 )
93	92	oveq1d 7437	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))) = ( 0 (.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))))
94	6	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → 𝑅 ∈ Ring)
95	77, 73	sylan2 605	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → (𝑋‘(𝑦 ∘f − 𝑧)) ∈ (Base‘𝑅))
96	2, 18, 8	ringlz 20531	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ (𝑋‘(𝑦 ∘f − 𝑧)) ∈ (Base‘𝑅)) → ( 0 (.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))) = 0 )
97	94, 95, 96	syl2anc 596	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → ( 0 (.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))) = 0 )
98	93, 97	eqtrd 2795	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))) = 0 )
99	98, 56	suppss2 8222	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) supp 0 ) ⊆ {(𝐼 × {0})})
100	3, 54	rabex2 5301	. . . . . . . 8 ⊢ 𝐷 ∈ V
101	100	mptrabex 7233	. . . . . . 7 ⊢ (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) ∈ V
102	101	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) ∈ V)
103		funmpt 6581	. . . . . . 7 ⊢ Fun (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))))
104	103	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → Fun (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))))
105	83	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 0 ∈ V)
106		snfi 9076	. . . . . . 7 ⊢ {(𝐼 × {0})} ∈ Fin
107	106	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → {(𝐼 × {0})} ∈ Fin)
108		suppssfifsupp 9377	. . . . . 6 ⊢ ((((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) ∈ V ∧ Fun (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) ∧ 0 ∈ V) ∧ ({(𝐼 × {0})} ∈ Fin ∧ ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) supp 0 ) ⊆ {(𝐼 × {0})})) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) finSupp 0 )
109	102, 104, 105, 107, 99, 108	syl32anc 1405	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) finSupp 0 )
110	2, 8, 53, 56, 76, 99, 109	gsumres 20134	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) ↾ {(𝐼 × {0})})) = (𝑅 Σg (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))))))
111	6	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑅 ∈ Ring)
112		ringmnd 20477	. . . . . 6 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
113	111, 112	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑅 ∈ Mnd)
114		iftrue 4487	. . . . . . . . . 10 ⊢ (𝑥 = (𝐼 × {0}) → if(𝑥 = (𝐼 × {0}), 1 , 0 ) = 1 )
115	114, 10, 82	fvmpt 6996	. . . . . . . . 9 ⊢ ((𝐼 × {0}) ∈ 𝐷 → (𝑈‘(𝐼 × {0})) = 1 )
116	28, 115	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑈‘(𝐼 × {0})) = 1 )
117		nn0cn 12621	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℕ0 → 𝑧 ∈ ℂ)
118	117	subid1d 11663	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ℕ0 → (𝑧 − 0) = 𝑧)
119	118	adantl 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ℕ0) → (𝑧 − 0) = 𝑧)
120	39, 30, 41, 119	caofid0r 7729	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑦 ∘f − (𝐼 × {0})) = 𝑦)
121	120	fveq2d 6892	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑋‘(𝑦 ∘f − (𝐼 × {0}))) = (𝑋‘𝑦))
122	116, 121	oveq12d 7440	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 × {0})))) = ( 1 (.r‘𝑅)(𝑋‘𝑦)))
123	16	ffvelcdmda 7087	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑋‘𝑦) ∈ (Base‘𝑅))
124	2, 18, 9	ringlidm 20505	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑦) ∈ (Base‘𝑅)) → ( 1 (.r‘𝑅)(𝑋‘𝑦)) = (𝑋‘𝑦))
125	111, 123, 124	syl2anc 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ( 1 (.r‘𝑅)(𝑋‘𝑦)) = (𝑋‘𝑦))
126	122, 125	eqtrd 2795	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 × {0})))) = (𝑋‘𝑦))
127	126, 123	eqeltrd 2860	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 × {0})))) ∈ (Base‘𝑅))
128		fveq2 6888	. . . . . . 7 ⊢ (𝑧 = (𝐼 × {0}) → (𝑈‘𝑧) = (𝑈‘(𝐼 × {0})))
129		oveq2 7430	. . . . . . . 8 ⊢ (𝑧 = (𝐼 × {0}) → (𝑦 ∘f − 𝑧) = (𝑦 ∘f − (𝐼 × {0})))
130	129	fveq2d 6892	. . . . . . 7 ⊢ (𝑧 = (𝐼 × {0}) → (𝑋‘(𝑦 ∘f − 𝑧)) = (𝑋‘(𝑦 ∘f − (𝐼 × {0}))))
131	128, 130	oveq12d 7440	. . . . . 6 ⊢ (𝑧 = (𝐼 × {0}) → ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))) = ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 × {0})))))
132	2, 131	gsumsn 20175	. . . . 5 ⊢ ((𝑅 ∈ Mnd ∧ (𝐼 × {0}) ∈ 𝐷 ∧ ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 × {0})))) ∈ (Base‘𝑅)) → (𝑅 Σg (𝑧 ∈ {(𝐼 × {0})} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))))) = ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 × {0})))))
133	113, 28, 127, 132	syl3anc 1398	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg (𝑧 ∈ {(𝐼 × {0})} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))))) = ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 × {0})))))
134	50, 110, 133	3eqtr3d 2803	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))))) = ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 × {0})))))
135	22, 134, 126	3eqtrd 2799	. 2 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑈 · 𝑋)‘𝑦) = (𝑋‘𝑦))
136	15, 17, 135	eqfnfvd 7035	1 ⊢ (𝜑 → (𝑈 · 𝑋) = 𝑋)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ∀wral 3076  {crab 3412  Vcvv 3450   ⊆ wss 3896   ∖ cdif 4044  ifcif 4481  {csn 4584   class class class wbr 5102   ↦ cmpt 5185   × cxp 5648  ^◡ccnv 5649   ↾ cres 5652   “ cima 5653  Fun wfun 6535   Fn wfn 6536  ⟶wf 6537  ‘cfv 6541  (class class class)co 7422   ∘_f cof 7693   ∘_r cofr 7694   supp csupp 8181   ↑_m cmap 8852  Fincfn 8978   finSupp cfsupp 9358  0cc0 11205   ≤ cle 11349   − cmin 11546  ℕcn 12340  ℕ₀cn0 12611  Basecbs 17394  ._rcmulr 17436  0_gc0g 17617   Σ_g cgsu 17618  Mndcmnd 18930  CMndccmn 20001  1_rcur 20414  Ringcrg 20466   mPwSer cmps 22219

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7753  ax-cnex 11261  ax-resscn 11262  ax-1cn 11263  ax-icn 11264  ax-addcl 11265  ax-addrcl 11266  ax-mulcl 11267  ax-mulrcl 11268  ax-mulcom 11269  ax-addass 11270  ax-mulass 11271  ax-distr 11272  ax-i2m1 11273  ax-1ne0 11274  ax-1rid 11275  ax-rnegex 11276  ax-rrecex 11277  ax-cnre 11278  ax-pre-lttri 11279  ax-pre-lttrn 11280  ax-pre-ltadd 11281  ax-pre-mulgt0 11282

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4835  df-uni 4867  df-int 4907  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-se 5604  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-isom 6550  df-riota 7379  df-ov 7425  df-oprab 7426  df-mpo 7427  df-of 7695  df-ofr 7696  df-om 7880  df-1st 8003  df-2nd 8004  df-supp 8182  df-frecs 8304  df-wrecs 8335  df-recs 8384  df-rdg 8423  df-1o 8481  df-er 8722  df-map 8854  df-pm 8855  df-ixp 8931  df-en 8979  df-dom 8980  df-sdom 8981  df-fin 8982  df-fsupp 9359  df-oi 9509  df-card 10025  df-pnf 11350  df-mnf 11351  df-xr 11352  df-ltxr 11353  df-le 11354  df-sub 11548  df-neg 11549  df-nn 12341  df-2 12410  df-3 12411  df-4 12412  df-5 12413  df-6 12414  df-7 12415  df-8 12416  df-9 12417  df-n0 12612  df-z 12699  df-uz 12971  df-fz 13645  df-fzo 13794  df-seq 14150  df-hash 14480  df-struct 17332  df-sets 17349  df-slot 17367  df-ndx 17379  df-base 17395  df-plusg 17448  df-mulr 17449  df-sca 17451  df-vsca 17452  df-tset 17454  df-0g 17619  df-gsum 17620  df-mgm 18823  df-sgrp 18915  df-mnd 18931  df-grp 19154  df-minusg 19155  df-mulg 19285  df-cntz 19538  df-cmn 20003  df-abl 20004  df-mgp 20368  df-rng 20382  df-ur 20415  df-ring 20468  df-psr 22224

This theorem is used by:  psrring  22284  psr1  22285