psrridm

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)

	Ref	Expression
Hypotheses	psrring.s	$⊢ S = I mPwSer R$
	psrring.i	$⊢ φ \to I \in V$
	psrring.r	$⊢ φ \to R \in Ring$
	psr1cl.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	psr1cl.z	$⊢ \underset{˙}{0} = 0_{R}$
	psr1cl.o	$⊢ \underset{˙}{1} = 1_{R}$
	psr1cl.u	$⊢ U = (x \in D ⟼ if (x = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0}))$
	psr1cl.b	$⊢ B = {Base}_{S}$
	psrlidm.t	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
	psrlidm.x	$⊢ φ \to X \in B$
Assertion	psrridm	$⊢ φ \to X \underset{˙}{\cdot} U = X$

Proof

Step	Hyp	Ref	Expression
1		psrring.s	$⊢ S = I mPwSer R$
2		psrring.i	$⊢ φ \to I \in V$
3		psrring.r	$⊢ φ \to R \in Ring$
4		psr1cl.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
5		psr1cl.z	$⊢ \underset{˙}{0} = 0_{R}$
6		psr1cl.o	$⊢ \underset{˙}{1} = 1_{R}$
7		psr1cl.u	$⊢ U = (x \in D ⟼ if (x = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0}))$
8		psr1cl.b	$⊢ B = {Base}_{S}$
9		psrlidm.t	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
10		psrlidm.x	$⊢ φ \to X \in B$
11		eqid	$⊢ {Base}_{R} = {Base}_{R}$
12	1 2 3 4 5 6 7 8	psr1cl	$⊢ φ \to U \in B$
13	1 8 9 3 10 12	psrmulcl	$⊢ φ \to X \underset{˙}{\cdot} U \in B$
14	1 11 4 8 13	psrelbas	$⊢ φ \to (X \underset{˙}{\cdot} U) : D ⟶ {Base}_{R}$
15	14	ffnd	$⊢ φ \to (X \underset{˙}{\cdot} U) Fn D$
16	1 11 4 8 10	psrelbas	$⊢ φ \to X : D ⟶ {Base}_{R}$
17	16	ffnd	$⊢ φ \to X Fn D$
18		eqid	$⊢ \cdot_{R} = \cdot_{R}$
19	10	adantr	$⊢ (φ \land y \in D) \to X \in B$
20	12	adantr	$⊢ (φ \land y \in D) \to U \in B$
21		simpr	$⊢ (φ \land y \in D) \to y \in D$
22	1 8 18 9 4 19 20 21	psrmulval	$⊢ (φ \land y \in D) \to (X \underset{˙}{\cdot} U) (y) = \underset{z \in \{g \in D \| g \leq_{f} y\}}{\sum_{R}} (X (z) \cdot_{R} U (y -_{f} z))$
23		breq1	$⊢ g = y \to (g \leq_{f} y \leftrightarrow y \leq_{f} y)$
24	2	adantr	$⊢ (φ \land y \in D) \to I \in V$
25	4	psrbagf	$⊢ y \in D \to y : I ⟶ ℕ_{0}$
26	25	adantl	$⊢ (φ \land y \in D) \to y : I ⟶ ℕ_{0}$
27		nn0re	$⊢ z \in ℕ_{0} \to z \in ℝ$
28	27	leidd	$⊢ z \in ℕ_{0} \to z \leq z$
29	28	adantl	$⊢ ((φ \land y \in D) \land z \in ℕ_{0}) \to z \leq z$
30	24 26 29	caofref	$⊢ (φ \land y \in D) \to y \leq_{f} y$
31	23 21 30	elrabd	$⊢ (φ \land y \in D) \to y \in \{g \in D \| g \leq_{f} y\}$
32	31	snssd	$⊢ (φ \land y \in D) \to \{y\} \subseteq \{g \in D \| g \leq_{f} y\}$
33	32	resmptd	$⊢ (φ \land y \in D) \to {(z \in \{g \in D \| g \leq_{f} y\} ⟼ X (z) \cdot_{R} U (y -_{f} z)) ↾}_{\{y\}} = (z \in \{y\} ⟼ X (z) \cdot_{R} U (y -_{f} z))$
34	33	oveq2d	$⊢ (φ \land y \in D) \to \sum_{R} ({(z \in \{g \in D \| g \leq_{f} y\} ⟼ X (z) \cdot_{R} U (y -_{f} z)) ↾}_{\{y\}}) = \underset{z \in \{y\}}{\sum_{R}} (X (z) \cdot_{R} U (y -_{f} z))$
35		ringcmn	$⊢ R \in Ring \to R \in CMnd$
36	3 35	syl	$⊢ φ \to R \in CMnd$
37	36	adantr	$⊢ (φ \land y \in D) \to R \in CMnd$
38		ovex	$⊢ {ℕ_{0}}^{I} \in V$
39	4 38	rab2ex	$⊢ \{g \in D \| g \leq_{f} y\} \in V$
40	39	a1i	$⊢ (φ \land y \in D) \to \{g \in D \| g \leq_{f} y\} \in V$
41	3	ad2antrr	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to R \in Ring$
42	16	ad2antrr	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to X : D ⟶ {Base}_{R}$
43		simpr	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to z \in \{g \in D \| g \leq_{f} y\}$
44		breq1	$⊢ g = z \to (g \leq_{f} y \leftrightarrow z \leq_{f} y)$
45	44	elrab	$⊢ z \in \{g \in D \| g \leq_{f} y\} \leftrightarrow (z \in D \land z \leq_{f} y)$
46	43 45	sylib	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to (z \in D \land z \leq_{f} y)$
47	46	simpld	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to z \in D$
48	42 47	ffvelrnd	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to X (z) \in {Base}_{R}$
49	1 11 4 8 20	psrelbas	$⊢ (φ \land y \in D) \to U : D ⟶ {Base}_{R}$
50	49	adantr	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to U : D ⟶ {Base}_{R}$
51	21	adantr	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to y \in D$
52	4	psrbagf	$⊢ z \in D \to z : I ⟶ ℕ_{0}$
53	47 52	syl	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to z : I ⟶ ℕ_{0}$
54	46	simprd	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to z \leq_{f} y$
55	4	psrbagcon	$⊢ (y \in D \land z : I ⟶ ℕ_{0} \land z \leq_{f} y) \to (y -_{f} z \in D \land (y -_{f} z) \leq_{f} y)$
56	51 53 54 55	syl3anc	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to (y -_{f} z \in D \land (y -_{f} z) \leq_{f} y)$
57	56	simpld	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to y -_{f} z \in D$
58	50 57	ffvelrnd	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to U (y -_{f} z) \in {Base}_{R}$
59	11 18	ringcl	$⊢ (R \in Ring \land X (z) \in {Base}_{R} \land U (y -_{f} z) \in {Base}_{R}) \to X (z) \cdot_{R} U (y -_{f} z) \in {Base}_{R}$
60	41 48 58 59	syl3anc	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to X (z) \cdot_{R} U (y -_{f} z) \in {Base}_{R}$
61	60	fmpttd	$⊢ (φ \land y \in D) \to (z \in \{g \in D \| g \leq_{f} y\} ⟼ X (z) \cdot_{R} U (y -_{f} z)) : \{g \in D \| g \leq_{f} y\} ⟶ {Base}_{R}$
62		eldifi	$⊢ z \in (\{g \in D \| g \leq_{f} y\} ∖ \{y\}) \to z \in \{g \in D \| g \leq_{f} y\}$
63	62 57	sylan2	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{y\})) \to y -_{f} z \in D$
64		eqeq1	$⊢ x = y -_{f} z \to (x = I \times \{0\} \leftrightarrow y -_{f} z = I \times \{0\})$
65	64	ifbid	$⊢ x = y -_{f} z \to if (x = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0}) = if (y -_{f} z = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0})$
66	6	fvexi	$⊢ \underset{˙}{1} \in V$
67	5	fvexi	$⊢ \underset{˙}{0} \in V$
68	66 67	ifex	$⊢ if (y -_{f} z = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0}) \in V$
69	65 7 68	fvmpt	$⊢ y -_{f} z \in D \to U (y -_{f} z) = if (y -_{f} z = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0})$
70	63 69	syl	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{y\})) \to U (y -_{f} z) = if (y -_{f} z = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0})$
71		eldifsni	$⊢ z \in (\{g \in D \| g \leq_{f} y\} ∖ \{y\}) \to z \neq y$
72	71	adantl	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{y\})) \to z \neq y$
73	72	necomd	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{y\})) \to y \neq z$
74	24	adantr	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to I \in V$
75		nn0sscn	$⊢ ℕ_{0} \subseteq ℂ$
76		fss	$⊢ (y : I ⟶ ℕ_{0} \land ℕ_{0} \subseteq ℂ) \to y : I ⟶ ℂ$
77	26 75 76	sylancl	$⊢ (φ \land y \in D) \to y : I ⟶ ℂ$
78	77	adantr	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to y : I ⟶ ℂ$
79		fss	$⊢ (z : I ⟶ ℕ_{0} \land ℕ_{0} \subseteq ℂ) \to z : I ⟶ ℂ$
80	53 75 79	sylancl	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to z : I ⟶ ℂ$
81		ofsubeq0	$⊢ (I \in V \land y : I ⟶ ℂ \land z : I ⟶ ℂ) \to (y -_{f} z = I \times \{0\} \leftrightarrow y = z)$
82	74 78 80 81	syl3anc	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to (y -_{f} z = I \times \{0\} \leftrightarrow y = z)$
83	62 82	sylan2	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{y\})) \to (y -_{f} z = I \times \{0\} \leftrightarrow y = z)$
84	83	necon3bbid	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{y\})) \to (\neg y -_{f} z = I \times \{0\} \leftrightarrow y \neq z)$
85	73 84	mpbird	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{y\})) \to \neg y -_{f} z = I \times \{0\}$
86	85	iffalsed	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{y\})) \to if (y -_{f} z = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0}) = \underset{˙}{0}$
87	70 86	eqtrd	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{y\})) \to U (y -_{f} z) = \underset{˙}{0}$
88	87	oveq2d	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{y\})) \to X (z) \cdot_{R} U (y -_{f} z) = X (z) \cdot_{R} \underset{˙}{0}$
89	11 18 5	ringrz	$⊢ (R \in Ring \land X (z) \in {Base}_{R}) \to X (z) \cdot_{R} \underset{˙}{0} = \underset{˙}{0}$
90	41 48 89	syl2anc	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to X (z) \cdot_{R} \underset{˙}{0} = \underset{˙}{0}$
91	62 90	sylan2	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{y\})) \to X (z) \cdot_{R} \underset{˙}{0} = \underset{˙}{0}$
92	88 91	eqtrd	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{y\})) \to X (z) \cdot_{R} U (y -_{f} z) = \underset{˙}{0}$
93	92 40	suppss2	$⊢ (φ \land y \in D) \to (z \in \{g \in D \| g \leq_{f} y\} ⟼ X (z) \cdot_{R} U (y -_{f} z)) supp \underset{˙}{0} \subseteq \{y\}$
94	40	mptexd	$⊢ (φ \land y \in D) \to (z \in \{g \in D \| g \leq_{f} y\} ⟼ X (z) \cdot_{R} U (y -_{f} z)) \in V$
95		funmpt	$⊢ Fun (z \in \{g \in D \| g \leq_{f} y\} ⟼ X (z) \cdot_{R} U (y -_{f} z))$
96	95	a1i	$⊢ (φ \land y \in D) \to Fun (z \in \{g \in D \| g \leq_{f} y\} ⟼ X (z) \cdot_{R} U (y -_{f} z))$
97	67	a1i	$⊢ (φ \land y \in D) \to \underset{˙}{0} \in V$
98		snfi	$⊢ \{y\} \in Fin$
99	98	a1i	$⊢ (φ \land y \in D) \to \{y\} \in Fin$
100		suppssfifsupp	$⊢ (((z \in \{g \in D \| g \leq_{f} y\} ⟼ X (z) \cdot_{R} U (y -_{f} z)) \in V \land Fun (z \in \{g \in D \| g \leq_{f} y\} ⟼ X (z) \cdot_{R} U (y -_{f} z)) \land \underset{˙}{0} \in V) \land (\{y\} \in Fin \land (z \in \{g \in D \| g \leq_{f} y\} ⟼ X (z) \cdot_{R} U (y -_{f} z)) supp \underset{˙}{0} \subseteq \{y\})) \to {finSupp}_{\underset{˙}{0}} ((z \in \{g \in D \| g \leq_{f} y\} ⟼ X (z) \cdot_{R} U (y -_{f} z)))$
101	94 96 97 99 93 100	syl32anc	$⊢ (φ \land y \in D) \to {finSupp}_{\underset{˙}{0}} ((z \in \{g \in D \| g \leq_{f} y\} ⟼ X (z) \cdot_{R} U (y -_{f} z)))$
102	11 5 37 40 61 93 101	gsumres	$⊢ (φ \land y \in D) \to \sum_{R} ({(z \in \{g \in D \| g \leq_{f} y\} ⟼ X (z) \cdot_{R} U (y -_{f} z)) ↾}_{\{y\}}) = \underset{z \in \{g \in D \| g \leq_{f} y\}}{\sum_{R}} (X (z) \cdot_{R} U (y -_{f} z))$
103	3	adantr	$⊢ (φ \land y \in D) \to R \in Ring$
104		ringmnd	$⊢ R \in Ring \to R \in Mnd$
105	103 104	syl	$⊢ (φ \land y \in D) \to R \in Mnd$
106		eqid	$⊢ y = y$
107		ofsubeq0	$⊢ (I \in V \land y : I ⟶ ℂ \land y : I ⟶ ℂ) \to (y -_{f} y = I \times \{0\} \leftrightarrow y = y)$
108	24 77 77 107	syl3anc	$⊢ (φ \land y \in D) \to (y -_{f} y = I \times \{0\} \leftrightarrow y = y)$
109	106 108	mpbiri	$⊢ (φ \land y \in D) \to y -_{f} y = I \times \{0\}$
110	109	fveq2d	$⊢ (φ \land y \in D) \to U (y -_{f} y) = U (I \times \{0\})$
111		fconstmpt	$⊢ I \times \{0\} = (w \in I ⟼ 0)$
112	4	fczpsrbag	$⊢ I \in V \to (w \in I ⟼ 0) \in D$
113	2 112	syl	$⊢ φ \to (w \in I ⟼ 0) \in D$
114	111 113	eqeltrid	$⊢ φ \to I \times \{0\} \in D$
115	114	adantr	$⊢ (φ \land y \in D) \to I \times \{0\} \in D$
116		iftrue	$⊢ x = I \times \{0\} \to if (x = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0}) = \underset{˙}{1}$
117	116 7 66	fvmpt	$⊢ I \times \{0\} \in D \to U (I \times \{0\}) = \underset{˙}{1}$
118	115 117	syl	$⊢ (φ \land y \in D) \to U (I \times \{0\}) = \underset{˙}{1}$
119	110 118	eqtrd	$⊢ (φ \land y \in D) \to U (y -_{f} y) = \underset{˙}{1}$
120	119	oveq2d	$⊢ (φ \land y \in D) \to X (y) \cdot_{R} U (y -_{f} y) = X (y) \cdot_{R} \underset{˙}{1}$
121	16	ffvelrnda	$⊢ (φ \land y \in D) \to X (y) \in {Base}_{R}$
122	11 18 6	ringridm	$⊢ (R \in Ring \land X (y) \in {Base}_{R}) \to X (y) \cdot_{R} \underset{˙}{1} = X (y)$
123	103 121 122	syl2anc	$⊢ (φ \land y \in D) \to X (y) \cdot_{R} \underset{˙}{1} = X (y)$
124	120 123	eqtrd	$⊢ (φ \land y \in D) \to X (y) \cdot_{R} U (y -_{f} y) = X (y)$
125	124 121	eqeltrd	$⊢ (φ \land y \in D) \to X (y) \cdot_{R} U (y -_{f} y) \in {Base}_{R}$
126		fveq2	$⊢ z = y \to X (z) = X (y)$
127		oveq2	$⊢ z = y \to y -_{f} z = y -_{f} y$
128	127	fveq2d	$⊢ z = y \to U (y -_{f} z) = U (y -_{f} y)$
129	126 128	oveq12d	$⊢ z = y \to X (z) \cdot_{R} U (y -_{f} z) = X (y) \cdot_{R} U (y -_{f} y)$
130	11 129	gsumsn	$⊢ (R \in Mnd \land y \in D \land X (y) \cdot_{R} U (y -_{f} y) \in {Base}_{R}) \to \underset{z \in \{y\}}{\sum_{R}} (X (z) \cdot_{R} U (y -_{f} z)) = X (y) \cdot_{R} U (y -_{f} y)$
131	105 21 125 130	syl3anc	$⊢ (φ \land y \in D) \to \underset{z \in \{y\}}{\sum_{R}} (X (z) \cdot_{R} U (y -_{f} z)) = X (y) \cdot_{R} U (y -_{f} y)$
132	34 102 131	3eqtr3d	$⊢ (φ \land y \in D) \to \underset{z \in \{g \in D \| g \leq_{f} y\}}{\sum_{R}} (X (z) \cdot_{R} U (y -_{f} z)) = X (y) \cdot_{R} U (y -_{f} y)$
133	22 132 124	3eqtrd	$⊢ (φ \land y \in D) \to (X \underset{˙}{\cdot} U) (y) = X (y)$
134	15 17 133	eqfnfvd	$⊢ φ \to X \underset{˙}{\cdot} U = X$

Metamath Proof Explorer

Theorem psrridm

Proof