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		breq1	$⊢ g = z \to (g \leq_{f} y \leftrightarrow z \leq_{f} y)$
44	43	elrab	$⊢ z \in \{g \in D \| g \leq_{f} y\} \leftrightarrow (z \in D \land z \leq_{f} y)$
45	44	bilani	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to (z \in D \land z \leq_{f} y)$
46	45	simpld	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to z \in D$
47	42 46	ffvelcdmd	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to X (z) \in {Base}_{R}$
48	1 11 4 8 20	psrelbas	$⊢ (φ \land y \in D) \to U : D ⟶ {Base}_{R}$
49	48	adantr	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to U : D ⟶ {Base}_{R}$
50	21	adantr	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to y \in D$
51	4	psrbagf	$⊢ z \in D \to z : I ⟶ ℕ_{0}$
52	46 51	syl	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to z : I ⟶ ℕ_{0}$
53	45	simprd	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to z \leq_{f} y$
54	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)$
55	50 52 53 54	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)$
56	55	simpld	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to y -_{f} z \in D$
57	49 56	ffvelcdmd	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to U (y -_{f} z) \in {Base}_{R}$
58	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}$
59	41 47 57 58	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}$
60	59	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}$
61		eldifi	$⊢ z \in (\{g \in D \| g \leq_{f} y\} ∖ \{y\}) \to z \in \{g \in D \| g \leq_{f} y\}$
62	61 56	sylan2	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{y\})) \to y -_{f} z \in D$
63		eqeq1	$⊢ x = y -_{f} z \to (x = I \times \{0\} \leftrightarrow y -_{f} z = I \times \{0\})$
64	63	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})$
65	6	fvexi	$⊢ \underset{˙}{1} \in V$
66	5	fvexi	$⊢ \underset{˙}{0} \in V$
67	65 66	ifex	$⊢ if (y -_{f} z = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0}) \in V$
68	64 7 67	fvmpt	$⊢ y -_{f} z \in D \to U (y -_{f} z) = if (y -_{f} z = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0})$
69	62 68	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})$
70		eldifsni	$⊢ z \in (\{g \in D \| g \leq_{f} y\} ∖ \{y\}) \to z \neq y$
71	70	adantl	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{y\})) \to z \neq y$
72	71	necomd	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{y\})) \to y \neq z$
73	24	adantr	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to I \in V$
74		nn0sscn	$⊢ ℕ_{0} \subseteq ℂ$
75		fss	$⊢ (y : I ⟶ ℕ_{0} \land ℕ_{0} \subseteq ℂ) \to y : I ⟶ ℂ$
76	26 74 75	sylancl	$⊢ (φ \land y \in D) \to y : I ⟶ ℂ$
77	76	adantr	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to y : I ⟶ ℂ$
78		fss	$⊢ (z : I ⟶ ℕ_{0} \land ℕ_{0} \subseteq ℂ) \to z : I ⟶ ℂ$
79	52 74 78	sylancl	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to z : I ⟶ ℂ$
80		ofsubeq0	$⊢ (I \in V \land y : I ⟶ ℂ \land z : I ⟶ ℂ) \to (y -_{f} z = I \times \{0\} \leftrightarrow y = z)$
81	73 77 79 80	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)$
82	61 81	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)$
83	82	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)$
84	72 83	mpbird	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{y\})) \to \neg y -_{f} z = I \times \{0\}$
85	84	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}$
86	69 85	eqtrd	$⊢ ((φ \land y \in D) \land z \in (\{g \in D \| g \leq_{f} y\} ∖ \{y\})) \to U (y -_{f} z) = \underset{˙}{0}$
87	86	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}$
88	11 18 5	ringrz	$⊢ (R \in Ring \land X (z) \in {Base}_{R}) \to X (z) \cdot_{R} \underset{˙}{0} = \underset{˙}{0}$
89	41 47 88	syl2anc	$⊢ ((φ \land y \in D) \land z \in \{g \in D \| g \leq_{f} y\}) \to X (z) \cdot_{R} \underset{˙}{0} = \underset{˙}{0}$
90	61 89	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}$
91	87 90	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}$
92	91 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\}$
93	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$
94		funmpt	$⊢ Fun (z \in \{g \in D \| g \leq_{f} y\} ⟼ X (z) \cdot_{R} U (y -_{f} z))$
95	94	a1i	$⊢ (φ \land y \in D) \to Fun (z \in \{g \in D \| g \leq_{f} y\} ⟼ X (z) \cdot_{R} U (y -_{f} z))$
96	66	a1i	$⊢ (φ \land y \in D) \to \underset{˙}{0} \in V$
97		snfi	$⊢ \{y\} \in Fin$
98	97	a1i	$⊢ (φ \land y \in D) \to \{y\} \in Fin$
99		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)))$
100	93 95 96 98 92 99	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)))$
101	11 5 37 40 60 92 100	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))$
102	3	adantr	$⊢ (φ \land y \in D) \to R \in Ring$
103		ringmnd	$⊢ R \in Ring \to R \in Mnd$
104	102 103	syl	$⊢ (φ \land y \in D) \to R \in Mnd$
105		eqid	$⊢ y = y$
106		ofsubeq0	$⊢ (I \in V \land y : I ⟶ ℂ \land y : I ⟶ ℂ) \to (y -_{f} y = I \times \{0\} \leftrightarrow y = y)$
107	24 76 76 106	syl3anc	$⊢ (φ \land y \in D) \to (y -_{f} y = I \times \{0\} \leftrightarrow y = y)$
108	105 107	mpbiri	$⊢ (φ \land y \in D) \to y -_{f} y = I \times \{0\}$
109	108	fveq2d	$⊢ (φ \land y \in D) \to U (y -_{f} y) = U (I \times \{0\})$
110		fconstmpt	$⊢ I \times \{0\} = (w \in I ⟼ 0)$
111	4	fczpsrbag	$⊢ I \in V \to (w \in I ⟼ 0) \in D$
112	2 111	syl	$⊢ φ \to (w \in I ⟼ 0) \in D$
113	110 112	eqeltrid	$⊢ φ \to I \times \{0\} \in D$
114	113	adantr	$⊢ (φ \land y \in D) \to I \times \{0\} \in D$
115		iftrue	$⊢ x = I \times \{0\} \to if (x = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0}) = \underset{˙}{1}$
116	115 7 65	fvmpt	$⊢ I \times \{0\} \in D \to U (I \times \{0\}) = \underset{˙}{1}$
117	114 116	syl	$⊢ (φ \land y \in D) \to U (I \times \{0\}) = \underset{˙}{1}$
118	109 117	eqtrd	$⊢ (φ \land y \in D) \to U (y -_{f} y) = \underset{˙}{1}$
119	118	oveq2d	$⊢ (φ \land y \in D) \to X (y) \cdot_{R} U (y -_{f} y) = X (y) \cdot_{R} \underset{˙}{1}$
120	16	ffvelcdmda	$⊢ (φ \land y \in D) \to X (y) \in {Base}_{R}$
121	11 18 6	ringridm	$⊢ (R \in Ring \land X (y) \in {Base}_{R}) \to X (y) \cdot_{R} \underset{˙}{1} = X (y)$
122	102 120 121	syl2anc	$⊢ (φ \land y \in D) \to X (y) \cdot_{R} \underset{˙}{1} = X (y)$
123	119 122	eqtrd	$⊢ (φ \land y \in D) \to X (y) \cdot_{R} U (y -_{f} y) = X (y)$
124	123 120	eqeltrd	$⊢ (φ \land y \in D) \to X (y) \cdot_{R} U (y -_{f} y) \in {Base}_{R}$
125		fveq2	$⊢ z = y \to X (z) = X (y)$
126		oveq2	$⊢ z = y \to y -_{f} z = y -_{f} y$
127	126	fveq2d	$⊢ z = y \to U (y -_{f} z) = U (y -_{f} y)$
128	125 127	oveq12d	$⊢ z = y \to X (z) \cdot_{R} U (y -_{f} z) = X (y) \cdot_{R} U (y -_{f} y)$
129	11 128	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)$
130	104 21 124 129	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)$
131	34 101 130	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)$
132	22 131 123	3eqtrd	$⊢ (φ \land y \in D) \to (X \underset{˙}{\cdot} U) (y) = X (y)$
133	15 17 132	eqfnfvd	$⊢ φ \to X \underset{˙}{\cdot} U = X$

Metamath Proof Explorer

Theorem psrridm

Proof