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

Metamath Proof Explorer

Theorem psrlidm

Proof