psrlidm

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)

	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	psrlidm	$⊢ φ \to U \underset{˙}{\cdot} X = 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 12 10	psrmulcl	$⊢ φ \to U \underset{˙}{\cdot} X \in B$
14	1 11 4 8 13	psrelbas	$⊢ φ \to (U \underset{˙}{\cdot} X) : D ⟶ {Base}_{R}$
15	14	ffnd	$⊢ φ \to (U \underset{˙}{\cdot} X) 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	12	adantr	$⊢ (φ \land y \in D) \to U \in B$
20	10	adantr	$⊢ (φ \land y \in D) \to X \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 (U \underset{˙}{\cdot} X) (y) = \underset{z \in \{g \in D \| g \leq_{f} y\}}{\sum_{R}} (U (z) \cdot_{R} X (y -_{f} z))$
23		breq1	$⊢ g = I \times \{0\} \to (g \leq_{f} y \leftrightarrow (I \times \{0\}) \leq_{f} y)$
24		fconstmpt	$⊢ I \times \{0\} = (x \in I ⟼ 0)$
25	4	fczpsrbag	$⊢ I \in V \to (x \in I ⟼ 0) \in D$
26	2 25	syl	$⊢ φ \to (x \in I ⟼ 0) \in D$
27	24 26	eqeltrid	$⊢ φ \to I \times \{0\} \in D$
28	27	adantr	$⊢ (φ \land y \in D) \to I \times \{0\} \in D$
29	4	psrbagf	$⊢ (I \in V \land y \in D) \to y : I ⟶ ℕ_{0}$
30	2 29	sylan	$⊢ (φ \land y \in D) \to y : I ⟶ ℕ_{0}$
31	30	ffvelrnda	$⊢ ((φ \land y \in D) \land x \in I) \to y (x) \in ℕ_{0}$
32	31	nn0ge0d	$⊢ ((φ \land y \in D) \land x \in I) \to 0 \leq y (x)$
33	32	ralrimiva	$⊢ (φ \land y \in D) \to \forall x \in I 0 \leq y (x)$
34		0nn0	$⊢ 0 \in ℕ_{0}$
35	34	fconst6	$⊢ (I \times \{0\}) : I ⟶ ℕ_{0}$
36		ffn	$⊢ (I \times \{0\}) : I ⟶ ℕ_{0} \to (I \times \{0\}) Fn I$
37	35 36	mp1i	$⊢ (φ \land y \in D) \to (I \times \{0\}) Fn I$
38	30	ffnd	$⊢ (φ \land y \in D) \to y Fn I$
39	2	adantr	$⊢ (φ \land y \in D) \to I \in V$
40		inidm	$⊢ I \cap I = I$
41	34	a1i	$⊢ (φ \land y \in D) \to 0 \in ℕ_{0}$
42		fvconst2g	$⊢ (0 \in ℕ_{0} \land x \in I) \to (I \times \{0\}) (x) = 0$
43	41 42	sylan	$⊢ ((φ \land y \in D) \land x \in I) \to (I \times \{0\}) (x) = 0$
44		eqidd	$⊢ ((φ \land y \in D) \land x \in I) \to y (x) = y (x)$
45	37 38 39 39 40 43 44	ofrfval	$⊢ (φ \land y \in D) \to ((I \times \{0\}) \leq_{f} y \leftrightarrow \forall x \in I 0 \leq y (x))$
46	33 45	mpbird	$⊢ (φ \land y \in D) \to (I \times \{0\}) \leq_{f} y$
47	23 28 46	elrabd	$⊢ (φ \land y \in D) \to I \times \{0\} \in \{g \in D \| g \leq_{f} y\}$
48	47	snssd	$⊢ (φ \land y \in D) \to \{I \times \{0\}\} \subseteq \{g \in D \| g \leq_{f} y\}$
49	48	resmptd	$⊢ (φ \land y \in D) \to {(z \in \{g \in D \| g \leq_{f} y\} ⟼ U (z) \cdot_{R} X (y -_{f} z)) ↾}_{\{I \times \{0\}\}} = (z \in \{I \times \{0\}\} ⟼ U (z) \cdot_{R} X (y -_{f} z))$
50	49	oveq2d	$⊢ (φ \land y \in D) \to \sum_{R} ({(z \in \{g \in D \| g \leq_{f} y\} ⟼ U (z) \cdot_{R} X (y -_{f} z)) ↾}_{\{I \times \{0\}\}}) = \underset{z \in \{I \times \{0\}\}}{\sum_{R}} (U (z) \cdot_{R} X (y -_{f} z))$
51		ringcmn	$⊢ R \in Ring \to R \in CMnd$
52	3 51	syl	$⊢ φ \to R \in CMnd$
53	52	adantr	$⊢ (φ \land y \in D) \to R \in CMnd$
54		ovex	$⊢ {ℕ_{0}}^{I} \in V$
55	4 54	rab2ex	$⊢ \{g \in D \| g \leq_{f} y\} \in V$
56	55	a1i	$⊢ (φ \land y \in D) \to \{g \in D \| g \leq_{f} y\} \in V$
57	3	ad2antrr	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to R \in Ring$
58		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\}$
59		breq1	$⊢ g = z \to (g \leq_{f} y \leftrightarrow z \leq_{f} y)$
60	59	elrab	$⊢ z \in \{g \in D \| g \leq_{f} y\} \leftrightarrow (z \in D \land z \leq_{f} y)$
61	58 60	sylib	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to (z \in D \land z \leq_{f} y)$
62	61	simpld	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to z \in D$
63	1 11 4 8 19	psrelbas	$⊢ (φ \land y \in D) \to U : D ⟶ {Base}_{R}$
64	63	ffvelrnda	$⊢ ((φ \land y \in D) \land z \in D) \to U (z) \in {Base}_{R}$
65	62 64	syldan	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to U (z) \in {Base}_{R}$
66	16	ad2antrr	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to X : D ⟶ {Base}_{R}$
67	2	ad2antrr	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to I \in V$
68	21	adantr	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to y \in D$
69	4	psrbagf	$⊢ (I \in V \land z \in D) \to z : I ⟶ ℕ_{0}$
70	67 62 69	syl2anc	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to z : I ⟶ ℕ_{0}$
71	61	simprd	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to z \leq_{f} y$
72	4	psrbagcon	$⊢ (I \in V \land (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)$
73	67 68 70 71 72	syl13anc	$⊢ ((φ \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)$
74	73	simpld	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to y -_{f} z \in D$
75	66 74	ffvelrnd	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to X (y -_{f} z) \in {Base}_{R}$
76	11 18	ringcl	$⊢ (R \in Ring \land U (z) \in {Base}_{R} \land X (y -_{f} z) \in {Base}_{R}) \to U (z) \cdot_{R} X (y -_{f} z) \in {Base}_{R}$
77	57 65 75 76	syl3anc	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to U (z) \cdot_{R} X (y -_{f} z) \in {Base}_{R}$
78	77	fmpttd	$⊢ (φ \land y \in D) \to (z \in \{g \in D \| g \leq_{f} y\} ⟼ U (z) \cdot_{R} X (y -_{f} z)) : \{g \in D \| g \leq_{f} y\} ⟶ {Base}_{R}$
79		eldifi	$⊢ z \in (\{g \in D \| g \leq_{f} y\} ∖ \{I \times \{0\}\}) \to z \in \{g \in D \| g \leq_{f} y\}$
80	79 61	sylan2	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{I \times \{0\}\})) \to (z \in D \land z \leq_{f} y)$
81	80	simpld	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{I \times \{0\}\})) \to z \in D$
82		eqeq1	$⊢ x = z \to (x = I \times \{0\} \leftrightarrow z = I \times \{0\})$
83	82	ifbid	$⊢ x = z \to if (x = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0}) = if (z = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0})$
84	6	fvexi	$⊢ \underset{˙}{1} \in V$
85	5	fvexi	$⊢ \underset{˙}{0} \in V$
86	84 85	ifex	$⊢ if (z = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0}) \in V$
87	83 7 86	fvmpt	$⊢ z \in D \to U (z) = if (z = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0})$
88	81 87	syl	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{I \times \{0\}\})) \to U (z) = if (z = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0})$
89		eldifn	$⊢ z \in (\{g \in D \| g \leq_{f} y\} ∖ \{I \times \{0\}\}) \to \neg z \in \{I \times \{0\}\}$
90	89	adantl	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{I \times \{0\}\})) \to \neg z \in \{I \times \{0\}\}$
91		velsn	$⊢ z \in \{I \times \{0\}\} \leftrightarrow z = I \times \{0\}$
92	90 91	sylnib	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{I \times \{0\}\})) \to \neg z = I \times \{0\}$
93	92	iffalsed	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{I \times \{0\}\})) \to if (z = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0}) = \underset{˙}{0}$
94	88 93	eqtrd	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{I \times \{0\}\})) \to U (z) = \underset{˙}{0}$
95	94	oveq1d	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{I \times \{0\}\})) \to U (z) \cdot_{R} X (y -_{f} z) = \underset{˙}{0} \cdot_{R} X (y -_{f} z)$
96	3	ad2antrr	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{I \times \{0\}\})) \to R \in Ring$
97	79 75	sylan2	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{I \times \{0\}\})) \to X (y -_{f} z) \in {Base}_{R}$
98	11 18 5	ringlz	$⊢ (R \in Ring \land X (y -_{f} z) \in {Base}_{R}) \to \underset{˙}{0} \cdot_{R} X (y -_{f} z) = \underset{˙}{0}$
99	96 97 98	syl2anc	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{I \times \{0\}\})) \to \underset{˙}{0} \cdot_{R} X (y -_{f} z) = \underset{˙}{0}$
100	95 99	eqtrd	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{I \times \{0\}\})) \to U (z) \cdot_{R} X (y -_{f} z) = \underset{˙}{0}$
101	100 56	suppss2	$⊢ (φ \land y \in D) \to (z \in \{g \in D \| g \leq_{f} y\} ⟼ U (z) \cdot_{R} X (y -_{f} z)) supp \underset{˙}{0} \subseteq \{I \times \{0\}\}$
102	4 54	rabex2	$⊢ D \in V$
103	102	mptrabex	$⊢ (z \in \{g \in D \| g \leq_{f} y\} ⟼ U (z) \cdot_{R} X (y -_{f} z)) \in V$
104	103	a1i	$⊢ (φ \land y \in D) \to (z \in \{g \in D \| g \leq_{f} y\} ⟼ U (z) \cdot_{R} X (y -_{f} z)) \in V$
105		funmpt	$⊢ Fun (z \in \{g \in D \| g \leq_{f} y\} ⟼ U (z) \cdot_{R} X (y -_{f} z))$
106	105	a1i	$⊢ (φ \land y \in D) \to Fun (z \in \{g \in D \| g \leq_{f} y\} ⟼ U (z) \cdot_{R} X (y -_{f} z))$
107	85	a1i	$⊢ (φ \land y \in D) \to \underset{˙}{0} \in V$
108		snfi	$⊢ \{I \times \{0\}\} \in Fin$
109	108	a1i	$⊢ (φ \land y \in D) \to \{I \times \{0\}\} \in Fin$
110		suppssfifsupp	$⊢ (((z \in \{g \in D \| g \leq_{f} y\} ⟼ U (z) \cdot_{R} X (y -_{f} z)) \in V \land Fun (z \in \{g \in D \| g \leq_{f} y\} ⟼ U (z) \cdot_{R} X (y -_{f} z)) \land \underset{˙}{0} \in V) \land (\{I \times \{0\}\} \in Fin \land (z \in \{g \in D \| g \leq_{f} y\} ⟼ U (z) \cdot_{R} X (y -_{f} z)) supp \underset{˙}{0} \subseteq \{I \times \{0\}\})) \to {finSupp}_{\underset{˙}{0}} ((z \in \{g \in D \| g \leq_{f} y\} ⟼ U (z) \cdot_{R} X (y -_{f} z)))$
111	104 106 107 109 101 110	syl32anc	$⊢ (φ \land y \in D) \to {finSupp}_{\underset{˙}{0}} ((z \in \{g \in D \| g \leq_{f} y\} ⟼ U (z) \cdot_{R} X (y -_{f} z)))$
112	11 5 53 56 78 101 111	gsumres	$⊢ (φ \land y \in D) \to \sum_{R} ({(z \in \{g \in D \| g \leq_{f} y\} ⟼ U (z) \cdot_{R} X (y -_{f} z)) ↾}_{\{I \times \{0\}\}}) = \underset{z \in \{g \in D \| g \leq_{f} y\}}{\sum_{R}} (U (z) \cdot_{R} X (y -_{f} z))$
113	3	adantr	$⊢ (φ \land y \in D) \to R \in Ring$
114		ringmnd	$⊢ R \in Ring \to R \in Mnd$
115	113 114	syl	$⊢ (φ \land y \in D) \to R \in Mnd$
116		iftrue	$⊢ x = I \times \{0\} \to if (x = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0}) = \underset{˙}{1}$
117	116 7 84	fvmpt	$⊢ I \times \{0\} \in D \to U (I \times \{0\}) = \underset{˙}{1}$
118	28 117	syl	$⊢ (φ \land y \in D) \to U (I \times \{0\}) = \underset{˙}{1}$
119		nn0cn	$⊢ z \in ℕ_{0} \to z \in ℂ$
120	119	subid1d	$⊢ z \in ℕ_{0} \to z - 0 = z$
121	120	adantl	$⊢ ((φ \land y \in D) \land z \in ℕ_{0}) \to z - 0 = z$
122	39 30 41 121	caofid0r	$⊢ (φ \land y \in D) \to y -_{f} (I \times \{0\}) = y$
123	122	fveq2d	$⊢ (φ \land y \in D) \to X (y -_{f} (I \times \{0\})) = X (y)$
124	118 123	oveq12d	$⊢ (φ \land y \in D) \to U (I \times \{0\}) \cdot_{R} X (y -_{f} (I \times \{0\})) = \underset{˙}{1} \cdot_{R} X (y)$
125	16	ffvelrnda	$⊢ (φ \land y \in D) \to X (y) \in {Base}_{R}$
126	11 18 6	ringlidm	$⊢ (R \in Ring \land X (y) \in {Base}_{R}) \to \underset{˙}{1} \cdot_{R} X (y) = X (y)$
127	113 125 126	syl2anc	$⊢ (φ \land y \in D) \to \underset{˙}{1} \cdot_{R} X (y) = X (y)$
128	124 127	eqtrd	$⊢ (φ \land y \in D) \to U (I \times \{0\}) \cdot_{R} X (y -_{f} (I \times \{0\})) = X (y)$
129	128 125	eqeltrd	$⊢ (φ \land y \in D) \to U (I \times \{0\}) \cdot_{R} X (y -_{f} (I \times \{0\})) \in {Base}_{R}$
130		fveq2	$⊢ z = I \times \{0\} \to U (z) = U (I \times \{0\})$
131		oveq2	$⊢ z = I \times \{0\} \to y -_{f} z = y -_{f} (I \times \{0\})$
132	131	fveq2d	$⊢ z = I \times \{0\} \to X (y -_{f} z) = X (y -_{f} (I \times \{0\}))$
133	130 132	oveq12d	$⊢ z = I \times \{0\} \to U (z) \cdot_{R} X (y -_{f} z) = U (I \times \{0\}) \cdot_{R} X (y -_{f} (I \times \{0\}))$
134	11 133	gsumsn	$⊢ (R \in Mnd \land I \times \{0\} \in D \land U (I \times \{0\}) \cdot_{R} X (y -_{f} (I \times \{0\})) \in {Base}_{R}) \to \underset{z \in \{I \times \{0\}\}}{\sum_{R}} (U (z) \cdot_{R} X (y -_{f} z)) = U (I \times \{0\}) \cdot_{R} X (y -_{f} (I \times \{0\}))$
135	115 28 129 134	syl3anc	$⊢ (φ \land y \in D) \to \underset{z \in \{I \times \{0\}\}}{\sum_{R}} (U (z) \cdot_{R} X (y -_{f} z)) = U (I \times \{0\}) \cdot_{R} X (y -_{f} (I \times \{0\}))$
136	50 112 135	3eqtr3d	$⊢ (φ \land y \in D) \to \underset{z \in \{g \in D \| g \leq_{f} y\}}{\sum_{R}} (U (z) \cdot_{R} X (y -_{f} z)) = U (I \times \{0\}) \cdot_{R} X (y -_{f} (I \times \{0\}))$
137	22 136 128	3eqtrd	$⊢ (φ \land y \in D) \to (U \underset{˙}{\cdot} X) (y) = X (y)$
138	15 17 137	eqfnfvd	$⊢ φ \to U \underset{˙}{\cdot} X = X$

Metamath Proof Explorer

Theorem psrlidm

Proof