Metamath Proof Explorer

Theorem 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 
|- ( ph -> I e. V )
psrring.r 
|- ( ph -> R e. Ring )
psr1cl.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
psr1cl.z 
|- .0. = ( 0g ` R )
psr1cl.o 
|- .1. = ( 1r ` R )
psr1cl.u 
|- U = ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) )
psr1cl.b 
|- B = ( Base ` S )
psrlidm.t 
|- .x. = ( .r ` S )
psrlidm.x 
|- ( ph -> X e. B )
Assertion psrlidm 
|- ( ph -> ( U .x. X ) = X )

Proof

Step Hyp Ref Expression
1 psrring.s 
 |-  S = ( I mPwSer R )
2 psrring.i 
 |-  ( ph -> I e. V )
3 psrring.r 
 |-  ( ph -> R e. Ring )
4 psr1cl.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
5 psr1cl.z 
 |-  .0. = ( 0g ` R )
6 psr1cl.o 
 |-  .1. = ( 1r ` R )
7 psr1cl.u 
 |-  U = ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) )
8 psr1cl.b 
 |-  B = ( Base ` S )
9 psrlidm.t 
 |-  .x. = ( .r ` S )
10 psrlidm.x 
 |-  ( ph -> X e. B )
11 eqid 
 |-  ( Base ` R ) = ( Base ` R )
12 1 2 3 4 5 6 7 8 psr1cl 
 |-  ( ph -> U e. B )
13 1 8 9 3 12 10 psrmulcl 
 |-  ( ph -> ( U .x. X ) e. B )
14 1 11 4 8 13 psrelbas 
 |-  ( ph -> ( U .x. X ) : D --> ( Base ` R ) )
15 14 ffnd 
 |-  ( ph -> ( U .x. X ) Fn D )
16 1 11 4 8 10 psrelbas 
 |-  ( ph -> X : D --> ( Base ` R ) )
17 16 ffnd 
 |-  ( ph -> X Fn D )
18 eqid 
 |-  ( .r ` R ) = ( .r ` R )
19 12 adantr 
 |-  ( ( ph /\ y e. D ) -> U e. B )
20 10 adantr 
 |-  ( ( ph /\ y e. D ) -> X e. B )
21 simpr 
 |-  ( ( ph /\ y e. D ) -> y e. D )
22 1 8 18 9 4 19 20 21 psrmulval 
 |-  ( ( ph /\ y e. D ) -> ( ( U .x. X ) ` y ) = ( R gsum ( z e. { g e. D | g oR <_ y } |-> ( ( U ` z ) ( .r ` R ) ( X ` ( y oF - z ) ) ) ) ) )
23 breq1 
 |-  ( g = ( I X. { 0 } ) -> ( g oR <_ y <-> ( I X. { 0 } ) oR <_ y ) )
24 fconstmpt 
 |-  ( I X. { 0 } ) = ( x e. I |-> 0 )
25 4 fczpsrbag 
 |-  ( I e. V -> ( x e. I |-> 0 ) e. D )
26 2 25 syl 
 |-  ( ph -> ( x e. I |-> 0 ) e. D )
27 24 26 eqeltrid 
 |-  ( ph -> ( I X. { 0 } ) e. D )
28 27 adantr 
 |-  ( ( ph /\ y e. D ) -> ( I X. { 0 } ) e. D )
29 4 psrbagf 
 |-  ( y e. D -> y : I --> NN0 )
30 29 adantl 
 |-  ( ( ph /\ y e. D ) -> y : I --> NN0 )
31 30 ffvelrnda 
 |-  ( ( ( ph /\ y e. D ) /\ x e. I ) -> ( y ` x ) e. NN0 )
32 31 nn0ge0d 
 |-  ( ( ( ph /\ y e. D ) /\ x e. I ) -> 0 <_ ( y ` x ) )
33 32 ralrimiva 
 |-  ( ( ph /\ y e. D ) -> A. x e. I 0 <_ ( y ` x ) )
34 0nn0 
 |-  0 e. NN0
35 34 fconst6 
 |-  ( I X. { 0 } ) : I --> NN0
36 ffn 
 |-  ( ( I X. { 0 } ) : I --> NN0 -> ( I X. { 0 } ) Fn I )
37 35 36 mp1i 
 |-  ( ( ph /\ y e. D ) -> ( I X. { 0 } ) Fn I )
38 30 ffnd 
 |-  ( ( ph /\ y e. D ) -> y Fn I )
39 2 adantr 
 |-  ( ( ph /\ y e. D ) -> I e. V )
40 inidm 
 |-  ( I i^i I ) = I
41 34 a1i 
 |-  ( ( ph /\ y e. D ) -> 0 e. NN0 )
42 fvconst2g 
 |-  ( ( 0 e. NN0 /\ x e. I ) -> ( ( I X. { 0 } ) ` x ) = 0 )
43 41 42 sylan 
 |-  ( ( ( ph /\ y e. D ) /\ x e. I ) -> ( ( I X. { 0 } ) ` x ) = 0 )
44 eqidd 
 |-  ( ( ( ph /\ y e. D ) /\ x e. I ) -> ( y ` x ) = ( y ` x ) )
45 37 38 39 39 40 43 44 ofrfval 
 |-  ( ( ph /\ y e. D ) -> ( ( I X. { 0 } ) oR <_ y <-> A. x e. I 0 <_ ( y ` x ) ) )
46 33 45 mpbird 
 |-  ( ( ph /\ y e. D ) -> ( I X. { 0 } ) oR <_ y )
47 23 28 46 elrabd 
 |-  ( ( ph /\ y e. D ) -> ( I X. { 0 } ) e. { g e. D | g oR <_ y } )
48 47 snssd 
 |-  ( ( ph /\ y e. D ) -> { ( I X. { 0 } ) } C_ { g e. D | g oR <_ y } )
49 48 resmptd 
 |-  ( ( ph /\ y e. D ) -> ( ( z e. { g e. D | g oR <_ y } |-> ( ( U ` z ) ( .r ` R ) ( X ` ( y oF - z ) ) ) ) |` { ( I X. { 0 } ) } ) = ( z e. { ( I X. { 0 } ) } |-> ( ( U ` z ) ( .r ` R ) ( X ` ( y oF - z ) ) ) ) )
50 49 oveq2d 
 |-  ( ( ph /\ y e. D ) -> ( R gsum ( ( z e. { g e. D | g oR <_ y } |-> ( ( U ` z ) ( .r ` R ) ( X ` ( y oF - z ) ) ) ) |` { ( I X. { 0 } ) } ) ) = ( R gsum ( z e. { ( I X. { 0 } ) } |-> ( ( U ` z ) ( .r ` R ) ( X ` ( y oF - z ) ) ) ) ) )
51 ringcmn 
 |-  ( R e. Ring -> R e. CMnd )
52 3 51 syl 
 |-  ( ph -> R e. CMnd )
53 52 adantr 
 |-  ( ( ph /\ y e. D ) -> R e. CMnd )
54 ovex 
 |-  ( NN0 ^m I ) e. _V
55 4 54 rab2ex 
 |-  { g e. D | g oR <_ y } e. _V
56 55 a1i 
 |-  ( ( ph /\ y e. D ) -> { g e. D | g oR <_ y } e. _V )
57 3 ad2antrr 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> R e. Ring )
58 simpr 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> z e. { g e. D | g oR <_ y } )
59 breq1 
 |-  ( g = z -> ( g oR <_ y <-> z oR <_ y ) )
60 59 elrab 
 |-  ( z e. { g e. D | g oR <_ y } <-> ( z e. D /\ z oR <_ y ) )
61 58 60 sylib 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> ( z e. D /\ z oR <_ y ) )
62 61 simpld 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> z e. D )
63 1 11 4 8 19 psrelbas 
 |-  ( ( ph /\ y e. D ) -> U : D --> ( Base ` R ) )
64 63 ffvelrnda 
 |-  ( ( ( ph /\ y e. D ) /\ z e. D ) -> ( U ` z ) e. ( Base ` R ) )
65 62 64 syldan 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> ( U ` z ) e. ( Base ` R ) )
66 16 ad2antrr 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> X : D --> ( Base ` R ) )
67 21 adantr 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> y e. D )
68 4 psrbagf 
 |-  ( z e. D -> z : I --> NN0 )
69 62 68 syl 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> z : I --> NN0 )
70 61 simprd 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> z oR <_ y )
71 4 psrbagcon 
 |-  ( ( y e. D /\ z : I --> NN0 /\ z oR <_ y ) -> ( ( y oF - z ) e. D /\ ( y oF - z ) oR <_ y ) )
72 67 69 70 71 syl3anc 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> ( ( y oF - z ) e. D /\ ( y oF - z ) oR <_ y ) )
73 72 simpld 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> ( y oF - z ) e. D )
74 66 73 ffvelrnd 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> ( X ` ( y oF - z ) ) e. ( Base ` R ) )
75 11 18 ringcl 
 |-  ( ( R e. Ring /\ ( U ` z ) e. ( Base ` R ) /\ ( X ` ( y oF - z ) ) e. ( Base ` R ) ) -> ( ( U ` z ) ( .r ` R ) ( X ` ( y oF - z ) ) ) e. ( Base ` R ) )
76 57 65 74 75 syl3anc 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> ( ( U ` z ) ( .r ` R ) ( X ` ( y oF - z ) ) ) e. ( Base ` R ) )
77 76 fmpttd 
 |-  ( ( ph /\ y e. D ) -> ( z e. { g e. D | g oR <_ y } |-> ( ( U ` z ) ( .r ` R ) ( X ` ( y oF - z ) ) ) ) : { g e. D | g oR <_ y } --> ( Base ` R ) )
78 eldifi 
 |-  ( z e. ( { g e. D | g oR <_ y } \ { ( I X. { 0 } ) } ) -> z e. { g e. D | g oR <_ y } )
79 78 61 sylan2 
 |-  ( ( ( ph /\ y e. D ) /\ z e. ( { g e. D | g oR <_ y } \ { ( I X. { 0 } ) } ) ) -> ( z e. D /\ z oR <_ y ) )
80 79 simpld 
 |-  ( ( ( ph /\ y e. D ) /\ z e. ( { g e. D | g oR <_ y } \ { ( I X. { 0 } ) } ) ) -> z e. D )
81 eqeq1 
 |-  ( x = z -> ( x = ( I X. { 0 } ) <-> z = ( I X. { 0 } ) ) )
82 81 ifbid 
 |-  ( x = z -> if ( x = ( I X. { 0 } ) , .1. , .0. ) = if ( z = ( I X. { 0 } ) , .1. , .0. ) )
83 6 fvexi 
 |-  .1. e. _V
84 5 fvexi 
 |-  .0. e. _V
85 83 84 ifex 
 |-  if ( z = ( I X. { 0 } ) , .1. , .0. ) e. _V
86 82 7 85 fvmpt 
 |-  ( z e. D -> ( U ` z ) = if ( z = ( I X. { 0 } ) , .1. , .0. ) )
87 80 86 syl 
 |-  ( ( ( ph /\ y e. D ) /\ z e. ( { g e. D | g oR <_ y } \ { ( I X. { 0 } ) } ) ) -> ( U ` z ) = if ( z = ( I X. { 0 } ) , .1. , .0. ) )
88 eldifn 
 |-  ( z e. ( { g e. D | g oR <_ y } \ { ( I X. { 0 } ) } ) -> -. z e. { ( I X. { 0 } ) } )
89 88 adantl 
 |-  ( ( ( ph /\ y e. D ) /\ z e. ( { g e. D | g oR <_ y } \ { ( I X. { 0 } ) } ) ) -> -. z e. { ( I X. { 0 } ) } )
90 velsn 
 |-  ( z e. { ( I X. { 0 } ) } <-> z = ( I X. { 0 } ) )
91 89 90 sylnib 
 |-  ( ( ( ph /\ y e. D ) /\ z e. ( { g e. D | g oR <_ y } \ { ( I X. { 0 } ) } ) ) -> -. z = ( I X. { 0 } ) )
92 91 iffalsed 
 |-  ( ( ( ph /\ y e. D ) /\ z e. ( { g e. D | g oR <_ y } \ { ( I X. { 0 } ) } ) ) -> if ( z = ( I X. { 0 } ) , .1. , .0. ) = .0. )
93 87 92 eqtrd 
 |-  ( ( ( ph /\ y e. D ) /\ z e. ( { g e. D | g oR <_ y } \ { ( I X. { 0 } ) } ) ) -> ( U ` z ) = .0. )
94 93 oveq1d 
 |-  ( ( ( ph /\ y e. D ) /\ z e. ( { g e. D | g oR <_ y } \ { ( I X. { 0 } ) } ) ) -> ( ( U ` z ) ( .r ` R ) ( X ` ( y oF - z ) ) ) = ( .0. ( .r ` R ) ( X ` ( y oF - z ) ) ) )
95 3 ad2antrr 
 |-  ( ( ( ph /\ y e. D ) /\ z e. ( { g e. D | g oR <_ y } \ { ( I X. { 0 } ) } ) ) -> R e. Ring )
96 78 74 sylan2 
 |-  ( ( ( ph /\ y e. D ) /\ z e. ( { g e. D | g oR <_ y } \ { ( I X. { 0 } ) } ) ) -> ( X ` ( y oF - z ) ) e. ( Base ` R ) )
97 11 18 5 ringlz 
 |-  ( ( R e. Ring /\ ( X ` ( y oF - z ) ) e. ( Base ` R ) ) -> ( .0. ( .r ` R ) ( X ` ( y oF - z ) ) ) = .0. )
98 95 96 97 syl2anc 
 |-  ( ( ( ph /\ y e. D ) /\ z e. ( { g e. D | g oR <_ y } \ { ( I X. { 0 } ) } ) ) -> ( .0. ( .r ` R ) ( X ` ( y oF - z ) ) ) = .0. )
99 94 98 eqtrd 
 |-  ( ( ( ph /\ y e. D ) /\ z e. ( { g e. D | g oR <_ y } \ { ( I X. { 0 } ) } ) ) -> ( ( U ` z ) ( .r ` R ) ( X ` ( y oF - z ) ) ) = .0. )
100 99 56 suppss2 
 |-  ( ( ph /\ y e. D ) -> ( ( z e. { g e. D | g oR <_ y } |-> ( ( U ` z ) ( .r ` R ) ( X ` ( y oF - z ) ) ) ) supp .0. ) C_ { ( I X. { 0 } ) } )
101 4 54 rabex2 
 |-  D e. _V
102 101 mptrabex 
 |-  ( z e. { g e. D | g oR <_ y } |-> ( ( U ` z ) ( .r ` R ) ( X ` ( y oF - z ) ) ) ) e. _V
103 102 a1i 
 |-  ( ( ph /\ y e. D ) -> ( z e. { g e. D | g oR <_ y } |-> ( ( U ` z ) ( .r ` R ) ( X ` ( y oF - z ) ) ) ) e. _V )
104 funmpt 
 |-  Fun ( z e. { g e. D | g oR <_ y } |-> ( ( U ` z ) ( .r ` R ) ( X ` ( y oF - z ) ) ) )
105 104 a1i 
 |-  ( ( ph /\ y e. D ) -> Fun ( z e. { g e. D | g oR <_ y } |-> ( ( U ` z ) ( .r ` R ) ( X ` ( y oF - z ) ) ) ) )
106 84 a1i 
 |-  ( ( ph /\ y e. D ) -> .0. e. _V )
107 snfi 
 |-  { ( I X. { 0 } ) } e. Fin
108 107 a1i 
 |-  ( ( ph /\ y e. D ) -> { ( I X. { 0 } ) } e. Fin )
109 suppssfifsupp 
 |-  ( ( ( ( z e. { g e. D | g oR <_ y } |-> ( ( U ` z ) ( .r ` R ) ( X ` ( y oF - z ) ) ) ) e. _V /\ Fun ( z e. { g e. D | g oR <_ y } |-> ( ( U ` z ) ( .r ` R ) ( X ` ( y oF - z ) ) ) ) /\ .0. e. _V ) /\ ( { ( I X. { 0 } ) } e. Fin /\ ( ( z e. { g e. D | g oR <_ y } |-> ( ( U ` z ) ( .r ` R ) ( X ` ( y oF - z ) ) ) ) supp .0. ) C_ { ( I X. { 0 } ) } ) ) -> ( z e. { g e. D | g oR <_ y } |-> ( ( U ` z ) ( .r ` R ) ( X ` ( y oF - z ) ) ) ) finSupp .0. )
110 103 105 106 108 100 109 syl32anc 
 |-  ( ( ph /\ y e. D ) -> ( z e. { g e. D | g oR <_ y } |-> ( ( U ` z ) ( .r ` R ) ( X ` ( y oF - z ) ) ) ) finSupp .0. )
111 11 5 53 56 77 100 110 gsumres 
 |-  ( ( ph /\ y e. D ) -> ( R gsum ( ( z e. { g e. D | g oR <_ y } |-> ( ( U ` z ) ( .r ` R ) ( X ` ( y oF - z ) ) ) ) |` { ( I X. { 0 } ) } ) ) = ( R gsum ( z e. { g e. D | g oR <_ y } |-> ( ( U ` z ) ( .r ` R ) ( X ` ( y oF - z ) ) ) ) ) )
112 3 adantr 
 |-  ( ( ph /\ y e. D ) -> R e. Ring )
113 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
114 112 113 syl 
 |-  ( ( ph /\ y e. D ) -> R e. Mnd )
115 iftrue 
 |-  ( x = ( I X. { 0 } ) -> if ( x = ( I X. { 0 } ) , .1. , .0. ) = .1. )
116 115 7 83 fvmpt 
 |-  ( ( I X. { 0 } ) e. D -> ( U ` ( I X. { 0 } ) ) = .1. )
117 28 116 syl 
 |-  ( ( ph /\ y e. D ) -> ( U ` ( I X. { 0 } ) ) = .1. )
118 nn0cn 
 |-  ( z e. NN0 -> z e. CC )
119 118 subid1d 
 |-  ( z e. NN0 -> ( z - 0 ) = z )
120 119 adantl 
 |-  ( ( ( ph /\ y e. D ) /\ z e. NN0 ) -> ( z - 0 ) = z )
121 39 30 41 120 caofid0r 
 |-  ( ( ph /\ y e. D ) -> ( y oF - ( I X. { 0 } ) ) = y )
122 121 fveq2d 
 |-  ( ( ph /\ y e. D ) -> ( X ` ( y oF - ( I X. { 0 } ) ) ) = ( X ` y ) )
123 117 122 oveq12d 
 |-  ( ( ph /\ y e. D ) -> ( ( U ` ( I X. { 0 } ) ) ( .r ` R ) ( X ` ( y oF - ( I X. { 0 } ) ) ) ) = ( .1. ( .r ` R ) ( X ` y ) ) )
124 16 ffvelrnda 
 |-  ( ( ph /\ y e. D ) -> ( X ` y ) e. ( Base ` R ) )
125 11 18 6 ringlidm 
 |-  ( ( R e. Ring /\ ( X ` y ) e. ( Base ` R ) ) -> ( .1. ( .r ` R ) ( X ` y ) ) = ( X ` y ) )
126 112 124 125 syl2anc 
 |-  ( ( ph /\ y e. D ) -> ( .1. ( .r ` R ) ( X ` y ) ) = ( X ` y ) )
127 123 126 eqtrd 
 |-  ( ( ph /\ y e. D ) -> ( ( U ` ( I X. { 0 } ) ) ( .r ` R ) ( X ` ( y oF - ( I X. { 0 } ) ) ) ) = ( X ` y ) )
128 127 124 eqeltrd 
 |-  ( ( ph /\ y e. D ) -> ( ( U ` ( I X. { 0 } ) ) ( .r ` R ) ( X ` ( y oF - ( I X. { 0 } ) ) ) ) e. ( Base ` R ) )
129 fveq2 
 |-  ( z = ( I X. { 0 } ) -> ( U ` z ) = ( U ` ( I X. { 0 } ) ) )
130 oveq2 
 |-  ( z = ( I X. { 0 } ) -> ( y oF - z ) = ( y oF - ( I X. { 0 } ) ) )
131 130 fveq2d 
 |-  ( z = ( I X. { 0 } ) -> ( X ` ( y oF - z ) ) = ( X ` ( y oF - ( I X. { 0 } ) ) ) )
132 129 131 oveq12d 
 |-  ( z = ( I X. { 0 } ) -> ( ( U ` z ) ( .r ` R ) ( X ` ( y oF - z ) ) ) = ( ( U ` ( I X. { 0 } ) ) ( .r ` R ) ( X ` ( y oF - ( I X. { 0 } ) ) ) ) )
133 11 132 gsumsn 
 |-  ( ( R e. Mnd /\ ( I X. { 0 } ) e. D /\ ( ( U ` ( I X. { 0 } ) ) ( .r ` R ) ( X ` ( y oF - ( I X. { 0 } ) ) ) ) e. ( Base ` R ) ) -> ( R gsum ( z e. { ( I X. { 0 } ) } |-> ( ( U ` z ) ( .r ` R ) ( X ` ( y oF - z ) ) ) ) ) = ( ( U ` ( I X. { 0 } ) ) ( .r ` R ) ( X ` ( y oF - ( I X. { 0 } ) ) ) ) )
134 114 28 128 133 syl3anc 
 |-  ( ( ph /\ y e. D ) -> ( R gsum ( z e. { ( I X. { 0 } ) } |-> ( ( U ` z ) ( .r ` R ) ( X ` ( y oF - z ) ) ) ) ) = ( ( U ` ( I X. { 0 } ) ) ( .r ` R ) ( X ` ( y oF - ( I X. { 0 } ) ) ) ) )
135 50 111 134 3eqtr3d 
 |-  ( ( ph /\ y e. D ) -> ( R gsum ( z e. { g e. D | g oR <_ y } |-> ( ( U ` z ) ( .r ` R ) ( X ` ( y oF - z ) ) ) ) ) = ( ( U ` ( I X. { 0 } ) ) ( .r ` R ) ( X ` ( y oF - ( I X. { 0 } ) ) ) ) )
136 22 135 127 3eqtrd 
 |-  ( ( ph /\ y e. D ) -> ( ( U .x. X ) ` y ) = ( X ` y ) )
137 15 17 136 eqfnfvd 
 |-  ( ph -> ( U .x. X ) = X )