Theorem psrlidm 21912

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 2728	. . . 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 21911	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ 𝐵)
12		psrlidm.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
13	1, 4, 5, 6, 11, 12	psrmulcl 21896	. . . 4 ⊢ (𝜑 → (𝑈 · 𝑋) ∈ 𝐵)
14	1, 2, 3, 4, 13	psrelbas 21886	. . 3 ⊢ (𝜑 → (𝑈 · 𝑋):𝐷⟶(Base‘𝑅))
15	14	ffnd 6728	. 2 ⊢ (𝜑 → (𝑈 · 𝑋) Fn 𝐷)
16	1, 2, 3, 4, 12	psrelbas 21886	. . 3 ⊢ (𝜑 → 𝑋:𝐷⟶(Base‘𝑅))
17	16	ffnd 6728	. 2 ⊢ (𝜑 → 𝑋 Fn 𝐷)
18		eqid 2728	. . . 4 ⊢ (.r‘𝑅) = (.r‘𝑅)
19	11	adantr 479	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑈 ∈ 𝐵)
20	12	adantr 479	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑋 ∈ 𝐵)
21		simpr 483	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦 ∈ 𝐷)
22	1, 4, 18, 5, 3, 19, 20, 21	psrmulval 21894	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑈 · 𝑋)‘𝑦) = (𝑅 Σg (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))))))
23		breq1 5155	. . . . . . . 8 ⊢ (𝑔 = (𝐼 × {0}) → (𝑔 ∘r ≤ 𝑦 ↔ (𝐼 × {0}) ∘r ≤ 𝑦))
24		fconstmpt 5744	. . . . . . . . . 10 ⊢ (𝐼 × {0}) = (𝑥 ∈ 𝐼 ↦ 0)
25	3	fczpsrbag 21863	. . . . . . . . . . 11 ⊢ (𝐼 ∈ 𝑉 → (𝑥 ∈ 𝐼 ↦ 0) ∈ 𝐷)
26	7, 25	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 0) ∈ 𝐷)
27	24, 26	eqeltrid 2833	. . . . . . . . 9 ⊢ (𝜑 → (𝐼 × {0}) ∈ 𝐷)
28	27	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐼 × {0}) ∈ 𝐷)
29	3	psrbagf 21858	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐷 → 𝑦:𝐼⟶ℕ0)
30	29	adantl 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦:𝐼⟶ℕ0)
31	30	ffvelcdmda 7099	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → (𝑦‘𝑥) ∈ ℕ0)
32	31	nn0ge0d 12573	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → 0 ≤ (𝑦‘𝑥))
33	32	ralrimiva 3143	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ∀𝑥 ∈ 𝐼 0 ≤ (𝑦‘𝑥))
34		0nn0 12525	. . . . . . . . . . . 12 ⊢ 0 ∈ ℕ0
35	34	fconst6 6792	. . . . . . . . . . 11 ⊢ (𝐼 × {0}):𝐼⟶ℕ0
36		ffn 6727	. . . . . . . . . . 11 ⊢ ((𝐼 × {0}):𝐼⟶ℕ0 → (𝐼 × {0}) Fn 𝐼)
37	35, 36	mp1i 13	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐼 × {0}) Fn 𝐼)
38	30	ffnd 6728	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦 Fn 𝐼)
39	7	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝐼 ∈ 𝑉)
40		inidm 4221	. . . . . . . . . 10 ⊢ (𝐼 ∩ 𝐼) = 𝐼
41	34	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 0 ∈ ℕ0)
42		fvconst2g 7220	. . . . . . . . . . 11 ⊢ ((0 ∈ ℕ0 ∧ 𝑥 ∈ 𝐼) → ((𝐼 × {0})‘𝑥) = 0)
43	41, 42	sylan 578	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → ((𝐼 × {0})‘𝑥) = 0)
44		eqidd 2729	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → (𝑦‘𝑥) = (𝑦‘𝑥))
45	37, 38, 39, 39, 40, 43, 44	ofrfval 7701	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝐼 × {0}) ∘r ≤ 𝑦 ↔ ∀𝑥 ∈ 𝐼 0 ≤ (𝑦‘𝑥)))
46	33, 45	mpbird 256	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐼 × {0}) ∘r ≤ 𝑦)
47	23, 28, 46	elrabd 3686	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐼 × {0}) ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦})
48	47	snssd 4817	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → {(𝐼 × {0})} ⊆ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦})
49	48	resmptd 6049	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) ↾ {(𝐼 × {0})}) = (𝑧 ∈ {(𝐼 × {0})} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))))
50	49	oveq2d 7442	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) ↾ {(𝐼 × {0})})) = (𝑅 Σg (𝑧 ∈ {(𝐼 × {0})} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))))))
51		ringcmn 20225	. . . . . . 7 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
52	6, 51	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ CMnd)
53	52	adantr 479	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑅 ∈ CMnd)
54		ovex 7459	. . . . . . 7 ⊢ (ℕ0 ↑m 𝐼) ∈ V
55	3, 54	rab2ex 5341	. . . . . 6 ⊢ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∈ V
56	55	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∈ V)
57	6	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑅 ∈ Ring)
58		simpr 483	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦})
59		breq1 5155	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑧 → (𝑔 ∘r ≤ 𝑦 ↔ 𝑧 ∘r ≤ 𝑦))
60	59	elrab 3684	. . . . . . . . . 10 ⊢ (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↔ (𝑧 ∈ 𝐷 ∧ 𝑧 ∘r ≤ 𝑦))
61	58, 60	sylib 217	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → (𝑧 ∈ 𝐷 ∧ 𝑧 ∘r ≤ 𝑦))
62	61	simpld 493	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑧 ∈ 𝐷)
63	1, 2, 3, 4, 19	psrelbas 21886	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑈:𝐷⟶(Base‘𝑅))
64	63	ffvelcdmda 7099	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ 𝐷) → (𝑈‘𝑧) ∈ (Base‘𝑅))
65	62, 64	syldan 589	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → (𝑈‘𝑧) ∈ (Base‘𝑅))
66	16	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑋:𝐷⟶(Base‘𝑅))
67	21	adantr 479	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑦 ∈ 𝐷)
68	3	psrbagf 21858	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐷 → 𝑧:𝐼⟶ℕ0)
69	62, 68	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑧:𝐼⟶ℕ0)
70	61	simprd 494	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑧 ∘r ≤ 𝑦)
71	3	psrbagcon 21870	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝐷 ∧ 𝑧:𝐼⟶ℕ0 ∧ 𝑧 ∘r ≤ 𝑦) → ((𝑦 ∘f − 𝑧) ∈ 𝐷 ∧ (𝑦 ∘f − 𝑧) ∘r ≤ 𝑦))
72	67, 69, 70, 71	syl3anc 1368	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → ((𝑦 ∘f − 𝑧) ∈ 𝐷 ∧ (𝑦 ∘f − 𝑧) ∘r ≤ 𝑦))
73	72	simpld 493	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → (𝑦 ∘f − 𝑧) ∈ 𝐷)
74	66, 73	ffvelcdmd 7100	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → (𝑋‘(𝑦 ∘f − 𝑧)) ∈ (Base‘𝑅))
75	2, 18	ringcl 20197	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ (𝑈‘𝑧) ∈ (Base‘𝑅) ∧ (𝑋‘(𝑦 ∘f − 𝑧)) ∈ (Base‘𝑅)) → ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))) ∈ (Base‘𝑅))
76	57, 65, 74, 75	syl3anc 1368	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))) ∈ (Base‘𝑅))
77	76	fmpttd 7130	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))):{𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}⟶(Base‘𝑅))
78		eldifi 4127	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})}) → 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦})
79	78, 61	sylan2 591	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → (𝑧 ∈ 𝐷 ∧ 𝑧 ∘r ≤ 𝑦))
80	79	simpld 493	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → 𝑧 ∈ 𝐷)
81		eqeq1 2732	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (𝑥 = (𝐼 × {0}) ↔ 𝑧 = (𝐼 × {0})))
82	81	ifbid 4555	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → if(𝑥 = (𝐼 × {0}), 1 , 0 ) = if(𝑧 = (𝐼 × {0}), 1 , 0 ))
83	9	fvexi 6916	. . . . . . . . . . . 12 ⊢ 1 ∈ V
84	8	fvexi 6916	. . . . . . . . . . . 12 ⊢ 0 ∈ V
85	83, 84	ifex 4582	. . . . . . . . . . 11 ⊢ if(𝑧 = (𝐼 × {0}), 1 , 0 ) ∈ V
86	82, 10, 85	fvmpt 7010	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝐷 → (𝑈‘𝑧) = if(𝑧 = (𝐼 × {0}), 1 , 0 ))
87	80, 86	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → (𝑈‘𝑧) = if(𝑧 = (𝐼 × {0}), 1 , 0 ))
88		eldifn 4128	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})}) → ¬ 𝑧 ∈ {(𝐼 × {0})})
89	88	adantl 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → ¬ 𝑧 ∈ {(𝐼 × {0})})
90		velsn 4648	. . . . . . . . . . 11 ⊢ (𝑧 ∈ {(𝐼 × {0})} ↔ 𝑧 = (𝐼 × {0}))
91	89, 90	sylnib 327	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → ¬ 𝑧 = (𝐼 × {0}))
92	91	iffalsed 4543	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → if(𝑧 = (𝐼 × {0}), 1 , 0 ) = 0 )
93	87, 92	eqtrd 2768	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → (𝑈‘𝑧) = 0 )
94	93	oveq1d 7441	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))) = ( 0 (.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))))
95	6	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → 𝑅 ∈ Ring)
96	78, 74	sylan2 591	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → (𝑋‘(𝑦 ∘f − 𝑧)) ∈ (Base‘𝑅))
97	2, 18, 8	ringlz 20236	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ (𝑋‘(𝑦 ∘f − 𝑧)) ∈ (Base‘𝑅)) → ( 0 (.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))) = 0 )
98	95, 96, 97	syl2anc 582	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → ( 0 (.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))) = 0 )
99	94, 98	eqtrd 2768	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))) = 0 )
100	99, 56	suppss2 8212	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) supp 0 ) ⊆ {(𝐼 × {0})})
101	3, 54	rabex2 5340	. . . . . . . 8 ⊢ 𝐷 ∈ V
102	101	mptrabex 7243	. . . . . . 7 ⊢ (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) ∈ V
103	102	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) ∈ V)
104		funmpt 6596	. . . . . . 7 ⊢ Fun (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))))
105	104	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → Fun (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))))
106	84	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 0 ∈ V)
107		snfi 9075	. . . . . . 7 ⊢ {(𝐼 × {0})} ∈ Fin
108	107	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → {(𝐼 × {0})} ∈ Fin)
109		suppssfifsupp 9411	. . . . . 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 1375	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) finSupp 0 )
111	2, 8, 53, 56, 77, 100, 110	gsumres 19875	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) ↾ {(𝐼 × {0})})) = (𝑅 Σg (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))))))
112	6	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑅 ∈ Ring)
113		ringmnd 20190	. . . . . 6 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
114	112, 113	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑅 ∈ Mnd)
115		iftrue 4538	. . . . . . . . . 10 ⊢ (𝑥 = (𝐼 × {0}) → if(𝑥 = (𝐼 × {0}), 1 , 0 ) = 1 )
116	115, 10, 83	fvmpt 7010	. . . . . . . . 9 ⊢ ((𝐼 × {0}) ∈ 𝐷 → (𝑈‘(𝐼 × {0})) = 1 )
117	28, 116	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑈‘(𝐼 × {0})) = 1 )
118		nn0cn 12520	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℕ0 → 𝑧 ∈ ℂ)
119	118	subid1d 11598	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ℕ0 → (𝑧 − 0) = 𝑧)
120	119	adantl 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ℕ0) → (𝑧 − 0) = 𝑧)
121	39, 30, 41, 120	caofid0r 7723	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑦 ∘f − (𝐼 × {0})) = 𝑦)
122	121	fveq2d 6906	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑋‘(𝑦 ∘f − (𝐼 × {0}))) = (𝑋‘𝑦))
123	117, 122	oveq12d 7444	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 × {0})))) = ( 1 (.r‘𝑅)(𝑋‘𝑦)))
124	16	ffvelcdmda 7099	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑋‘𝑦) ∈ (Base‘𝑅))
125	2, 18, 9	ringlidm 20212	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑦) ∈ (Base‘𝑅)) → ( 1 (.r‘𝑅)(𝑋‘𝑦)) = (𝑋‘𝑦))
126	112, 124, 125	syl2anc 582	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ( 1 (.r‘𝑅)(𝑋‘𝑦)) = (𝑋‘𝑦))
127	123, 126	eqtrd 2768	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 × {0})))) = (𝑋‘𝑦))
128	127, 124	eqeltrd 2829	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 × {0})))) ∈ (Base‘𝑅))
129		fveq2 6902	. . . . . . 7 ⊢ (𝑧 = (𝐼 × {0}) → (𝑈‘𝑧) = (𝑈‘(𝐼 × {0})))
130		oveq2 7434	. . . . . . . 8 ⊢ (𝑧 = (𝐼 × {0}) → (𝑦 ∘f − 𝑧) = (𝑦 ∘f − (𝐼 × {0})))
131	130	fveq2d 6906	. . . . . . 7 ⊢ (𝑧 = (𝐼 × {0}) → (𝑋‘(𝑦 ∘f − 𝑧)) = (𝑋‘(𝑦 ∘f − (𝐼 × {0}))))
132	129, 131	oveq12d 7444	. . . . . 6 ⊢ (𝑧 = (𝐼 × {0}) → ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))) = ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 × {0})))))
133	2, 132	gsumsn 19916	. . . . 5 ⊢ ((𝑅 ∈ Mnd ∧ (𝐼 × {0}) ∈ 𝐷 ∧ ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 × {0})))) ∈ (Base‘𝑅)) → (𝑅 Σg (𝑧 ∈ {(𝐼 × {0})} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))))) = ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 × {0})))))
134	114, 28, 128, 133	syl3anc 1368	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg (𝑧 ∈ {(𝐼 × {0})} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))))) = ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 × {0})))))
135	50, 111, 134	3eqtr3d 2776	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))))) = ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 × {0})))))
136	22, 135, 127	3eqtrd 2772	. 2 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑈 · 𝑋)‘𝑦) = (𝑋‘𝑦))
137	15, 17, 136	eqfnfvd 7048	1 ⊢ (𝜑 → (𝑈 · 𝑋) = 𝑋)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 394   = wceq 1533   ∈ wcel 2098  ∀wral 3058  {crab 3430  Vcvv 3473   ∖ cdif 3946   ⊆ wss 3949  ifcif 4532  {csn 4632   class class class wbr 5152   ↦ cmpt 5235   × cxp 5680  ^◡ccnv 5681   ↾ cres 5684   “ cima 5685  Fun wfun 6547   Fn wfn 6548  ⟶wf 6549  ‘cfv 6553  (class class class)co 7426   ∘_f cof 7689   ∘_r cofr 7690   supp csupp 8171   ↑_m cmap 8851  Fincfn 8970   finSupp cfsupp 9393  0cc0 11146   ≤ cle 11287   − cmin 11482  ℕcn 12250  ℕ₀cn0 12510  Basecbs 17187  ._rcmulr 17241  0_gc0g 17428   Σ_g cgsu 17429  Mndcmnd 18701  CMndccmn 19742  1_rcur 20128  Ringcrg 20180   mPwSer cmps 21844

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 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-cnex 11202  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222  ax-pre-mulgt0 11223

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-tp 4637  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-se 5638  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-isom 6562  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-of 7691  df-ofr 7692  df-om 7877  df-1st 7999  df-2nd 8000  df-supp 8172  df-frecs 8293  df-wrecs 8324  df-recs 8398  df-rdg 8437  df-1o 8493  df-er 8731  df-map 8853  df-pm 8854  df-ixp 8923  df-en 8971  df-dom 8972  df-sdom 8973  df-fin 8974  df-fsupp 9394  df-oi 9541  df-card 9970  df-pnf 11288  df-mnf 11289  df-xr 11290  df-ltxr 11291  df-le 11292  df-sub 11484  df-neg 11485  df-nn 12251  df-2 12313  df-3 12314  df-4 12315  df-5 12316  df-6 12317  df-7 12318  df-8 12319  df-9 12320  df-n0 12511  df-z 12597  df-uz 12861  df-fz 13525  df-fzo 13668  df-seq 14007  df-hash 14330  df-struct 17123  df-sets 17140  df-slot 17158  df-ndx 17170  df-base 17188  df-plusg 17253  df-mulr 17254  df-sca 17256  df-vsca 17257  df-tset 17259  df-0g 17430  df-gsum 17431  df-mgm 18607  df-sgrp 18686  df-mnd 18702  df-grp 18900  df-minusg 18901  df-mulg 19031  df-cntz 19275  df-cmn 19744  df-abl 19745  df-mgp 20082  df-rng 20100  df-ur 20129  df-ring 20182  df-psr 21849

This theorem is referenced by:  psrring  21920  psr1  21921