Theorem psrlidm 21878

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 2730	. . . 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 21877	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ 𝐵)
12		psrlidm.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
13	1, 4, 5, 6, 11, 12	psrmulcl 21862	. . . 4 ⊢ (𝜑 → (𝑈 · 𝑋) ∈ 𝐵)
14	1, 2, 3, 4, 13	psrelbas 21850	. . 3 ⊢ (𝜑 → (𝑈 · 𝑋):𝐷⟶(Base‘𝑅))
15	14	ffnd 6692	. 2 ⊢ (𝜑 → (𝑈 · 𝑋) Fn 𝐷)
16	1, 2, 3, 4, 12	psrelbas 21850	. . 3 ⊢ (𝜑 → 𝑋:𝐷⟶(Base‘𝑅))
17	16	ffnd 6692	. 2 ⊢ (𝜑 → 𝑋 Fn 𝐷)
18		eqid 2730	. . . 4 ⊢ (.r‘𝑅) = (.r‘𝑅)
19	11	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑈 ∈ 𝐵)
20	12	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑋 ∈ 𝐵)
21		simpr 484	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦 ∈ 𝐷)
22	1, 4, 18, 5, 3, 19, 20, 21	psrmulval 21860	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑈 · 𝑋)‘𝑦) = (𝑅 Σg (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))))))
23		breq1 5113	. . . . . . . 8 ⊢ (𝑔 = (𝐼 × {0}) → (𝑔 ∘r ≤ 𝑦 ↔ (𝐼 × {0}) ∘r ≤ 𝑦))
24		fconstmpt 5703	. . . . . . . . . 10 ⊢ (𝐼 × {0}) = (𝑥 ∈ 𝐼 ↦ 0)
25	3	fczpsrbag 21837	. . . . . . . . . . 11 ⊢ (𝐼 ∈ 𝑉 → (𝑥 ∈ 𝐼 ↦ 0) ∈ 𝐷)
26	7, 25	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 0) ∈ 𝐷)
27	24, 26	eqeltrid 2833	. . . . . . . . 9 ⊢ (𝜑 → (𝐼 × {0}) ∈ 𝐷)
28	27	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐼 × {0}) ∈ 𝐷)
29	3	psrbagf 21834	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐷 → 𝑦:𝐼⟶ℕ0)
30	29	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦:𝐼⟶ℕ0)
31	30	ffvelcdmda 7059	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → (𝑦‘𝑥) ∈ ℕ0)
32	31	nn0ge0d 12513	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → 0 ≤ (𝑦‘𝑥))
33	32	ralrimiva 3126	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ∀𝑥 ∈ 𝐼 0 ≤ (𝑦‘𝑥))
34		0nn0 12464	. . . . . . . . . . . 12 ⊢ 0 ∈ ℕ0
35	34	fconst6 6753	. . . . . . . . . . 11 ⊢ (𝐼 × {0}):𝐼⟶ℕ0
36		ffn 6691	. . . . . . . . . . 11 ⊢ ((𝐼 × {0}):𝐼⟶ℕ0 → (𝐼 × {0}) Fn 𝐼)
37	35, 36	mp1i 13	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐼 × {0}) Fn 𝐼)
38	30	ffnd 6692	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦 Fn 𝐼)
39	7	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝐼 ∈ 𝑉)
40		inidm 4193	. . . . . . . . . 10 ⊢ (𝐼 ∩ 𝐼) = 𝐼
41	34	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 0 ∈ ℕ0)
42		fvconst2g 7179	. . . . . . . . . . 11 ⊢ ((0 ∈ ℕ0 ∧ 𝑥 ∈ 𝐼) → ((𝐼 × {0})‘𝑥) = 0)
43	41, 42	sylan 580	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → ((𝐼 × {0})‘𝑥) = 0)
44		eqidd 2731	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → (𝑦‘𝑥) = (𝑦‘𝑥))
45	37, 38, 39, 39, 40, 43, 44	ofrfval 7666	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝐼 × {0}) ∘r ≤ 𝑦 ↔ ∀𝑥 ∈ 𝐼 0 ≤ (𝑦‘𝑥)))
46	33, 45	mpbird 257	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐼 × {0}) ∘r ≤ 𝑦)
47	23, 28, 46	elrabd 3664	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐼 × {0}) ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦})
48	47	snssd 4776	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → {(𝐼 × {0})} ⊆ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦})
49	48	resmptd 6014	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) ↾ {(𝐼 × {0})}) = (𝑧 ∈ {(𝐼 × {0})} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))))
50	49	oveq2d 7406	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) ↾ {(𝐼 × {0})})) = (𝑅 Σg (𝑧 ∈ {(𝐼 × {0})} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))))))
51		ringcmn 20198	. . . . . . 7 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
52	6, 51	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ CMnd)
53	52	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑅 ∈ CMnd)
54		ovex 7423	. . . . . . 7 ⊢ (ℕ0 ↑m 𝐼) ∈ V
55	3, 54	rab2ex 5300	. . . . . 6 ⊢ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∈ V
56	55	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∈ V)
57	6	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑅 ∈ Ring)
58		simpr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦})
59		breq1 5113	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑧 → (𝑔 ∘r ≤ 𝑦 ↔ 𝑧 ∘r ≤ 𝑦))
60	59	elrab 3662	. . . . . . . . . 10 ⊢ (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↔ (𝑧 ∈ 𝐷 ∧ 𝑧 ∘r ≤ 𝑦))
61	58, 60	sylib 218	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → (𝑧 ∈ 𝐷 ∧ 𝑧 ∘r ≤ 𝑦))
62	61	simpld 494	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑧 ∈ 𝐷)
63	1, 2, 3, 4, 19	psrelbas 21850	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑈:𝐷⟶(Base‘𝑅))
64	63	ffvelcdmda 7059	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ 𝐷) → (𝑈‘𝑧) ∈ (Base‘𝑅))
65	62, 64	syldan 591	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → (𝑈‘𝑧) ∈ (Base‘𝑅))
66	16	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑋:𝐷⟶(Base‘𝑅))
67	21	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑦 ∈ 𝐷)
68	3	psrbagf 21834	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐷 → 𝑧:𝐼⟶ℕ0)
69	62, 68	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑧:𝐼⟶ℕ0)
70	61	simprd 495	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑧 ∘r ≤ 𝑦)
71	3	psrbagcon 21841	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝐷 ∧ 𝑧:𝐼⟶ℕ0 ∧ 𝑧 ∘r ≤ 𝑦) → ((𝑦 ∘f − 𝑧) ∈ 𝐷 ∧ (𝑦 ∘f − 𝑧) ∘r ≤ 𝑦))
72	67, 69, 70, 71	syl3anc 1373	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → ((𝑦 ∘f − 𝑧) ∈ 𝐷 ∧ (𝑦 ∘f − 𝑧) ∘r ≤ 𝑦))
73	72	simpld 494	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → (𝑦 ∘f − 𝑧) ∈ 𝐷)
74	66, 73	ffvelcdmd 7060	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → (𝑋‘(𝑦 ∘f − 𝑧)) ∈ (Base‘𝑅))
75	2, 18	ringcl 20166	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ (𝑈‘𝑧) ∈ (Base‘𝑅) ∧ (𝑋‘(𝑦 ∘f − 𝑧)) ∈ (Base‘𝑅)) → ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))) ∈ (Base‘𝑅))
76	57, 65, 74, 75	syl3anc 1373	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))) ∈ (Base‘𝑅))
77	76	fmpttd 7090	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))):{𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}⟶(Base‘𝑅))
78		eldifi 4097	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})}) → 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦})
79	78, 61	sylan2 593	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → (𝑧 ∈ 𝐷 ∧ 𝑧 ∘r ≤ 𝑦))
80	79	simpld 494	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → 𝑧 ∈ 𝐷)
81		eqeq1 2734	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (𝑥 = (𝐼 × {0}) ↔ 𝑧 = (𝐼 × {0})))
82	81	ifbid 4515	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → if(𝑥 = (𝐼 × {0}), 1 , 0 ) = if(𝑧 = (𝐼 × {0}), 1 , 0 ))
83	9	fvexi 6875	. . . . . . . . . . . 12 ⊢ 1 ∈ V
84	8	fvexi 6875	. . . . . . . . . . . 12 ⊢ 0 ∈ V
85	83, 84	ifex 4542	. . . . . . . . . . 11 ⊢ if(𝑧 = (𝐼 × {0}), 1 , 0 ) ∈ V
86	82, 10, 85	fvmpt 6971	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝐷 → (𝑈‘𝑧) = if(𝑧 = (𝐼 × {0}), 1 , 0 ))
87	80, 86	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → (𝑈‘𝑧) = if(𝑧 = (𝐼 × {0}), 1 , 0 ))
88		eldifn 4098	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})}) → ¬ 𝑧 ∈ {(𝐼 × {0})})
89	88	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → ¬ 𝑧 ∈ {(𝐼 × {0})})
90		velsn 4608	. . . . . . . . . . 11 ⊢ (𝑧 ∈ {(𝐼 × {0})} ↔ 𝑧 = (𝐼 × {0}))
91	89, 90	sylnib 328	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → ¬ 𝑧 = (𝐼 × {0}))
92	91	iffalsed 4502	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → if(𝑧 = (𝐼 × {0}), 1 , 0 ) = 0 )
93	87, 92	eqtrd 2765	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → (𝑈‘𝑧) = 0 )
94	93	oveq1d 7405	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))) = ( 0 (.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))))
95	6	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → 𝑅 ∈ Ring)
96	78, 74	sylan2 593	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → (𝑋‘(𝑦 ∘f − 𝑧)) ∈ (Base‘𝑅))
97	2, 18, 8	ringlz 20209	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ (𝑋‘(𝑦 ∘f − 𝑧)) ∈ (Base‘𝑅)) → ( 0 (.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))) = 0 )
98	95, 96, 97	syl2anc 584	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → ( 0 (.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))) = 0 )
99	94, 98	eqtrd 2765	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))) = 0 )
100	99, 56	suppss2 8182	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) supp 0 ) ⊆ {(𝐼 × {0})})
101	3, 54	rabex2 5299	. . . . . . . 8 ⊢ 𝐷 ∈ V
102	101	mptrabex 7202	. . . . . . 7 ⊢ (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) ∈ V
103	102	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) ∈ V)
104		funmpt 6557	. . . . . . 7 ⊢ Fun (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))))
105	104	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → Fun (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))))
106	84	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 0 ∈ V)
107		snfi 9017	. . . . . . 7 ⊢ {(𝐼 × {0})} ∈ Fin
108	107	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → {(𝐼 × {0})} ∈ Fin)
109		suppssfifsupp 9338	. . . . . 6 ⊢ ((((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) ∈ V ∧ Fun (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) ∧ 0 ∈ V) ∧ ({(𝐼 × {0})} ∈ Fin ∧ ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) supp 0 ) ⊆ {(𝐼 × {0})})) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) finSupp 0 )
110	103, 105, 106, 108, 100, 109	syl32anc 1380	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) finSupp 0 )
111	2, 8, 53, 56, 77, 100, 110	gsumres 19850	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) ↾ {(𝐼 × {0})})) = (𝑅 Σg (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))))))
112	6	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑅 ∈ Ring)
113		ringmnd 20159	. . . . . 6 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
114	112, 113	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑅 ∈ Mnd)
115		iftrue 4497	. . . . . . . . . 10 ⊢ (𝑥 = (𝐼 × {0}) → if(𝑥 = (𝐼 × {0}), 1 , 0 ) = 1 )
116	115, 10, 83	fvmpt 6971	. . . . . . . . 9 ⊢ ((𝐼 × {0}) ∈ 𝐷 → (𝑈‘(𝐼 × {0})) = 1 )
117	28, 116	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑈‘(𝐼 × {0})) = 1 )
118		nn0cn 12459	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℕ0 → 𝑧 ∈ ℂ)
119	118	subid1d 11529	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ℕ0 → (𝑧 − 0) = 𝑧)
120	119	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ℕ0) → (𝑧 − 0) = 𝑧)
121	39, 30, 41, 120	caofid0r 7690	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑦 ∘f − (𝐼 × {0})) = 𝑦)
122	121	fveq2d 6865	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑋‘(𝑦 ∘f − (𝐼 × {0}))) = (𝑋‘𝑦))
123	117, 122	oveq12d 7408	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 × {0})))) = ( 1 (.r‘𝑅)(𝑋‘𝑦)))
124	16	ffvelcdmda 7059	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑋‘𝑦) ∈ (Base‘𝑅))
125	2, 18, 9	ringlidm 20185	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑦) ∈ (Base‘𝑅)) → ( 1 (.r‘𝑅)(𝑋‘𝑦)) = (𝑋‘𝑦))
126	112, 124, 125	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ( 1 (.r‘𝑅)(𝑋‘𝑦)) = (𝑋‘𝑦))
127	123, 126	eqtrd 2765	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 × {0})))) = (𝑋‘𝑦))
128	127, 124	eqeltrd 2829	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 × {0})))) ∈ (Base‘𝑅))
129		fveq2 6861	. . . . . . 7 ⊢ (𝑧 = (𝐼 × {0}) → (𝑈‘𝑧) = (𝑈‘(𝐼 × {0})))
130		oveq2 7398	. . . . . . . 8 ⊢ (𝑧 = (𝐼 × {0}) → (𝑦 ∘f − 𝑧) = (𝑦 ∘f − (𝐼 × {0})))
131	130	fveq2d 6865	. . . . . . 7 ⊢ (𝑧 = (𝐼 × {0}) → (𝑋‘(𝑦 ∘f − 𝑧)) = (𝑋‘(𝑦 ∘f − (𝐼 × {0}))))
132	129, 131	oveq12d 7408	. . . . . 6 ⊢ (𝑧 = (𝐼 × {0}) → ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))) = ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 × {0})))))
133	2, 132	gsumsn 19891	. . . . 5 ⊢ ((𝑅 ∈ Mnd ∧ (𝐼 × {0}) ∈ 𝐷 ∧ ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 × {0})))) ∈ (Base‘𝑅)) → (𝑅 Σg (𝑧 ∈ {(𝐼 × {0})} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))))) = ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 × {0})))))
134	114, 28, 128, 133	syl3anc 1373	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg (𝑧 ∈ {(𝐼 × {0})} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))))) = ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 × {0})))))
135	50, 111, 134	3eqtr3d 2773	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))))) = ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 × {0})))))
136	22, 135, 127	3eqtrd 2769	. 2 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑈 · 𝑋)‘𝑦) = (𝑋‘𝑦))
137	15, 17, 136	eqfnfvd 7009	1 ⊢ (𝜑 → (𝑈 · 𝑋) = 𝑋)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3045  {crab 3408  Vcvv 3450   ∖ cdif 3914   ⊆ wss 3917  ifcif 4491  {csn 4592   class class class wbr 5110   ↦ cmpt 5191   × cxp 5639  ^◡ccnv 5640   ↾ cres 5643   “ cima 5644  Fun wfun 6508   Fn wfn 6509  ⟶wf 6510  ‘cfv 6514  (class class class)co 7390   ∘_f cof 7654   ∘_r cofr 7655   supp csupp 8142   ↑_m cmap 8802  Fincfn 8921   finSupp cfsupp 9319  0cc0 11075   ≤ cle 11216   − cmin 11412  ℕcn 12193  ℕ₀cn0 12449  Basecbs 17186  ._rcmulr 17228  0_gc0g 17409   Σ_g cgsu 17410  Mndcmnd 18668  CMndccmn 19717  1_rcur 20097  Ringcrg 20149   mPwSer cmps 21820

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-tp 4597  df-op 4599  df-uni 4875  df-int 4914  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-se 5595  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-isom 6523  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-of 7656  df-ofr 7657  df-om 7846  df-1st 7971  df-2nd 7972  df-supp 8143  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-1o 8437  df-er 8674  df-map 8804  df-pm 8805  df-ixp 8874  df-en 8922  df-dom 8923  df-sdom 8924  df-fin 8925  df-fsupp 9320  df-oi 9470  df-card 9899  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221  df-sub 11414  df-neg 11415  df-nn 12194  df-2 12256  df-3 12257  df-4 12258  df-5 12259  df-6 12260  df-7 12261  df-8 12262  df-9 12263  df-n0 12450  df-z 12537  df-uz 12801  df-fz 13476  df-fzo 13623  df-seq 13974  df-hash 14303  df-struct 17124  df-sets 17141  df-slot 17159  df-ndx 17171  df-base 17187  df-plusg 17240  df-mulr 17241  df-sca 17243  df-vsca 17244  df-tset 17246  df-0g 17411  df-gsum 17412  df-mgm 18574  df-sgrp 18653  df-mnd 18669  df-grp 18875  df-minusg 18876  df-mulg 19007  df-cntz 19256  df-cmn 19719  df-abl 19720  df-mgp 20057  df-rng 20069  df-ur 20098  df-ring 20151  df-psr 21825

This theorem is referenced by:  psrring  21886  psr1  21887