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	$⊢ y \in D \to y : I ⟶ ℕ_{0}$
30	29	adantl	$⊢ (φ \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	21	adantr	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to y \in D$
68	4	psrbagf	$⊢ z \in D \to z : I ⟶ ℕ_{0}$
69	62 68	syl	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to z : I ⟶ ℕ_{0}$
70	61	simprd	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to z \leq_{f} y$
71	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)$
72	67 69 70 71	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)$
73	72	simpld	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to y -_{f} z \in D$
74	66 73	ffvelrnd	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to X (y -_{f} z) \in {Base}_{R}$
75	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}$
76	57 65 74 75	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}$
77	76	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}$
78		eldifi	$⊢ z \in (\{g \in D \| g \leq_{f} y\} ∖ \{I \times \{0\}\}) \to z \in \{g \in D \| g \leq_{f} y\}$
79	78 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)$
80	79	simpld	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{I \times \{0\}\})) \to z \in D$
81		eqeq1	$⊢ x = z \to (x = I \times \{0\} \leftrightarrow z = I \times \{0\})$
82	81	ifbid	$⊢ x = z \to if (x = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0}) = if (z = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0})$
83	6	fvexi	$⊢ \underset{˙}{1} \in V$
84	5	fvexi	$⊢ \underset{˙}{0} \in V$
85	83 84	ifex	$⊢ if (z = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0}) \in V$
86	82 7 85	fvmpt	$⊢ z \in D \to U (z) = if (z = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0})$
87	80 86	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})$
88		eldifn	$⊢ z \in (\{g \in D \| g \leq_{f} y\} ∖ \{I \times \{0\}\}) \to \neg z \in \{I \times \{0\}\}$
89	88	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\}\}$
90		velsn	$⊢ z \in \{I \times \{0\}\} \leftrightarrow z = I \times \{0\}$
91	89 90	sylnib	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{I \times \{0\}\})) \to \neg z = I \times \{0\}$
92	91	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}$
93	87 92	eqtrd	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{I \times \{0\}\})) \to U (z) = \underset{˙}{0}$
94	93	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)$
95	3	ad2antrr	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{I \times \{0\}\})) \to R \in Ring$
96	78 74	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}$
97	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}$
98	95 96 97	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}$
99	94 98	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}$
100	99 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\}\}$
101	4 54	rabex2	$⊢ D \in V$
102	101	mptrabex	$⊢ (z \in \{g \in D \| g \leq_{f} y\} ⟼ U (z) \cdot_{R} X (y -_{f} z)) \in V$
103	102	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$
104		funmpt	$⊢ Fun (z \in \{g \in D \| g \leq_{f} y\} ⟼ U (z) \cdot_{R} X (y -_{f} z))$
105	104	a1i	$⊢ (φ \land y \in D) \to Fun (z \in \{g \in D \| g \leq_{f} y\} ⟼ U (z) \cdot_{R} X (y -_{f} z))$
106	84	a1i	$⊢ (φ \land y \in D) \to \underset{˙}{0} \in V$
107		snfi	$⊢ \{I \times \{0\}\} \in Fin$
108	107	a1i	$⊢ (φ \land y \in D) \to \{I \times \{0\}\} \in Fin$
109		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)))$
110	103 105 106 108 100 109	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)))$
111	11 5 53 56 77 100 110	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))$
112	3	adantr	$⊢ (φ \land y \in D) \to R \in Ring$
113		ringmnd	$⊢ R \in Ring \to R \in Mnd$
114	112 113	syl	$⊢ (φ \land y \in D) \to R \in Mnd$
115		iftrue	$⊢ x = I \times \{0\} \to if (x = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0}) = \underset{˙}{1}$
116	115 7 83	fvmpt	$⊢ I \times \{0\} \in D \to U (I \times \{0\}) = \underset{˙}{1}$
117	28 116	syl	$⊢ (φ \land y \in D) \to U (I \times \{0\}) = \underset{˙}{1}$
118		nn0cn	$⊢ z \in ℕ_{0} \to z \in ℂ$
119	118	subid1d	$⊢ z \in ℕ_{0} \to z - 0 = z$
120	119	adantl	$⊢ ((φ \land y \in D) \land z \in ℕ_{0}) \to z - 0 = z$
121	39 30 41 120	caofid0r	$⊢ (φ \land y \in D) \to y -_{f} (I \times \{0\}) = y$
122	121	fveq2d	$⊢ (φ \land y \in D) \to X (y -_{f} (I \times \{0\})) = X (y)$
123	117 122	oveq12d	$⊢ (φ \land y \in D) \to U (I \times \{0\}) \cdot_{R} X (y -_{f} (I \times \{0\})) = \underset{˙}{1} \cdot_{R} X (y)$
124	16	ffvelrnda	$⊢ (φ \land y \in D) \to X (y) \in {Base}_{R}$
125	11 18 6	ringlidm	$⊢ (R \in Ring \land X (y) \in {Base}_{R}) \to \underset{˙}{1} \cdot_{R} X (y) = X (y)$
126	112 124 125	syl2anc	$⊢ (φ \land y \in D) \to \underset{˙}{1} \cdot_{R} X (y) = X (y)$
127	123 126	eqtrd	$⊢ (φ \land y \in D) \to U (I \times \{0\}) \cdot_{R} X (y -_{f} (I \times \{0\})) = X (y)$
128	127 124	eqeltrd	$⊢ (φ \land y \in D) \to U (I \times \{0\}) \cdot_{R} X (y -_{f} (I \times \{0\})) \in {Base}_{R}$
129		fveq2	$⊢ z = I \times \{0\} \to U (z) = U (I \times \{0\})$
130		oveq2	$⊢ z = I \times \{0\} \to y -_{f} z = y -_{f} (I \times \{0\})$
131	130	fveq2d	$⊢ z = I \times \{0\} \to X (y -_{f} z) = X (y -_{f} (I \times \{0\}))$
132	129 131	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\}))$
133	11 132	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\}))$
134	114 28 128 133	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\}))$
135	50 111 134	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\}))$
136	22 135 127	3eqtrd	$⊢ (φ \land y \in D) \to (U \underset{˙}{\cdot} X) (y) = X (y)$
137	15 17 136	eqfnfvd	$⊢ φ \to U \underset{˙}{\cdot} X = X$

Metamath Proof Explorer

Theorem psrlidm

Proof