Metamath Proof Explorer

Theorem 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 
|- ( 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 psrridm 
|- ( ph -> ( X .x. U ) = 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 10 12 psrmulcl 
 |-  ( ph -> ( X .x. U ) e. B )
14 1 11 4 8 13 psrelbas 
 |-  ( ph -> ( X .x. U ) : D --> ( Base ` R ) )
15 14 ffnd 
 |-  ( ph -> ( X .x. U ) 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 10 adantr 
 |-  ( ( ph /\ y e. D ) -> X e. B )
20 12 adantr 
 |-  ( ( ph /\ y e. D ) -> U 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 ) -> ( ( X .x. U ) ` y ) = ( R gsum ( z e. { g e. D | g oR <_ y } |-> ( ( X ` z ) ( .r ` R ) ( U ` ( y oF - z ) ) ) ) ) )
23 breq1 
 |-  ( g = y -> ( g oR <_ y <-> y oR <_ y ) )
24 2 adantr 
 |-  ( ( ph /\ y e. D ) -> I e. V )
25 4 psrbagf 
 |-  ( ( I e. V /\ y e. D ) -> y : I --> NN0 )
26 2 25 sylan 
 |-  ( ( ph /\ y e. D ) -> y : I --> NN0 )
27 nn0re 
 |-  ( z e. NN0 -> z e. RR )
28 27 leidd 
 |-  ( z e. NN0 -> z <_ z )
29 28 adantl 
 |-  ( ( ( ph /\ y e. D ) /\ z e. NN0 ) -> z <_ z )
30 24 26 29 caofref 
 |-  ( ( ph /\ y e. D ) -> y oR <_ y )
31 23 21 30 elrabd 
 |-  ( ( ph /\ y e. D ) -> y e. { g e. D | g oR <_ y } )
32 31 snssd 
 |-  ( ( ph /\ y e. D ) -> { y } C_ { g e. D | g oR <_ y } )
33 32 resmptd 
 |-  ( ( ph /\ y e. D ) -> ( ( z e. { g e. D | g oR <_ y } |-> ( ( X ` z ) ( .r ` R ) ( U ` ( y oF - z ) ) ) ) |` { y } ) = ( z e. { y } |-> ( ( X ` z ) ( .r ` R ) ( U ` ( y oF - z ) ) ) ) )
34 33 oveq2d 
 |-  ( ( ph /\ y e. D ) -> ( R gsum ( ( z e. { g e. D | g oR <_ y } |-> ( ( X ` z ) ( .r ` R ) ( U ` ( y oF - z ) ) ) ) |` { y } ) ) = ( R gsum ( z e. { y } |-> ( ( X ` z ) ( .r ` R ) ( U ` ( y oF - z ) ) ) ) ) )
35 ringcmn 
 |-  ( R e. Ring -> R e. CMnd )
36 3 35 syl 
 |-  ( ph -> R e. CMnd )
37 36 adantr 
 |-  ( ( ph /\ y e. D ) -> R e. CMnd )
38 ovex 
 |-  ( NN0 ^m I ) e. _V
39 4 38 rab2ex 
 |-  { g e. D | g oR <_ y } e. _V
40 39 a1i 
 |-  ( ( ph /\ y e. D ) -> { g e. D | g oR <_ y } e. _V )
41 3 ad2antrr 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> R e. Ring )
42 16 ad2antrr 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> X : D --> ( Base ` R ) )
43 simpr 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> z e. { g e. D | g oR <_ y } )
44 breq1 
 |-  ( g = z -> ( g oR <_ y <-> z oR <_ y ) )
45 44 elrab 
 |-  ( z e. { g e. D | g oR <_ y } <-> ( z e. D /\ z oR <_ y ) )
46 43 45 sylib 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> ( z e. D /\ z oR <_ y ) )
47 46 simpld 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> z e. D )
48 42 47 ffvelrnd 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> ( X ` z ) e. ( Base ` R ) )
49 1 11 4 8 20 psrelbas 
 |-  ( ( ph /\ y e. D ) -> U : D --> ( Base ` R ) )
50 49 adantr 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> U : D --> ( Base ` R ) )
51 2 ad2antrr 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> I e. V )
52 21 adantr 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> y e. D )
53 4 psrbagf 
 |-  ( ( I e. V /\ z e. D ) -> z : I --> NN0 )
54 51 47 53 syl2anc 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> z : I --> NN0 )
55 46 simprd 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> z oR <_ y )
56 4 psrbagcon 
 |-  ( ( I e. V /\ ( y e. D /\ z : I --> NN0 /\ z oR <_ y ) ) -> ( ( y oF - z ) e. D /\ ( y oF - z ) oR <_ y ) )
57 51 52 54 55 56 syl13anc 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> ( ( y oF - z ) e. D /\ ( y oF - z ) oR <_ y ) )
58 57 simpld 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> ( y oF - z ) e. D )
59 50 58 ffvelrnd 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> ( U ` ( y oF - z ) ) e. ( Base ` R ) )
60 11 18 ringcl 
 |-  ( ( R e. Ring /\ ( X ` z ) e. ( Base ` R ) /\ ( U ` ( y oF - z ) ) e. ( Base ` R ) ) -> ( ( X ` z ) ( .r ` R ) ( U ` ( y oF - z ) ) ) e. ( Base ` R ) )
61 41 48 59 60 syl3anc 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> ( ( X ` z ) ( .r ` R ) ( U ` ( y oF - z ) ) ) e. ( Base ` R ) )
62 61 fmpttd 
 |-  ( ( ph /\ y e. D ) -> ( z e. { g e. D | g oR <_ y } |-> ( ( X ` z ) ( .r ` R ) ( U ` ( y oF - z ) ) ) ) : { g e. D | g oR <_ y } --> ( Base ` R ) )
63 eldifi 
 |-  ( z e. ( { g e. D | g oR <_ y } \ { y } ) -> z e. { g e. D | g oR <_ y } )
64 63 58 sylan2 
 |-  ( ( ( ph /\ y e. D ) /\ z e. ( { g e. D | g oR <_ y } \ { y } ) ) -> ( y oF - z ) e. D )
65 eqeq1 
 |-  ( x = ( y oF - z ) -> ( x = ( I X. { 0 } ) <-> ( y oF - z ) = ( I X. { 0 } ) ) )
66 65 ifbid 
 |-  ( x = ( y oF - z ) -> if ( x = ( I X. { 0 } ) , .1. , .0. ) = if ( ( y oF - z ) = ( I X. { 0 } ) , .1. , .0. ) )
67 6 fvexi 
 |-  .1. e. _V
68 5 fvexi 
 |-  .0. e. _V
69 67 68 ifex 
 |-  if ( ( y oF - z ) = ( I X. { 0 } ) , .1. , .0. ) e. _V
70 66 7 69 fvmpt 
 |-  ( ( y oF - z ) e. D -> ( U ` ( y oF - z ) ) = if ( ( y oF - z ) = ( I X. { 0 } ) , .1. , .0. ) )
71 64 70 syl 
 |-  ( ( ( ph /\ y e. D ) /\ z e. ( { g e. D | g oR <_ y } \ { y } ) ) -> ( U ` ( y oF - z ) ) = if ( ( y oF - z ) = ( I X. { 0 } ) , .1. , .0. ) )
72 eldifsni 
 |-  ( z e. ( { g e. D | g oR <_ y } \ { y } ) -> z =/= y )
73 72 adantl 
 |-  ( ( ( ph /\ y e. D ) /\ z e. ( { g e. D | g oR <_ y } \ { y } ) ) -> z =/= y )
74 73 necomd 
 |-  ( ( ( ph /\ y e. D ) /\ z e. ( { g e. D | g oR <_ y } \ { y } ) ) -> y =/= z )
75 nn0sscn 
 |-  NN0 C_ CC
76 fss 
 |-  ( ( y : I --> NN0 /\ NN0 C_ CC ) -> y : I --> CC )
77 26 75 76 sylancl 
 |-  ( ( ph /\ y e. D ) -> y : I --> CC )
78 77 adantr 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> y : I --> CC )
79 fss 
 |-  ( ( z : I --> NN0 /\ NN0 C_ CC ) -> z : I --> CC )
80 54 75 79 sylancl 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> z : I --> CC )
81 ofsubeq0 
 |-  ( ( I e. V /\ y : I --> CC /\ z : I --> CC ) -> ( ( y oF - z ) = ( I X. { 0 } ) <-> y = z ) )
82 51 78 80 81 syl3anc 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> ( ( y oF - z ) = ( I X. { 0 } ) <-> y = z ) )
83 63 82 sylan2 
 |-  ( ( ( ph /\ y e. D ) /\ z e. ( { g e. D | g oR <_ y } \ { y } ) ) -> ( ( y oF - z ) = ( I X. { 0 } ) <-> y = z ) )
84 83 necon3bbid 
 |-  ( ( ( ph /\ y e. D ) /\ z e. ( { g e. D | g oR <_ y } \ { y } ) ) -> ( -. ( y oF - z ) = ( I X. { 0 } ) <-> y =/= z ) )
85 74 84 mpbird 
 |-  ( ( ( ph /\ y e. D ) /\ z e. ( { g e. D | g oR <_ y } \ { y } ) ) -> -. ( y oF - z ) = ( I X. { 0 } ) )
86 85 iffalsed 
 |-  ( ( ( ph /\ y e. D ) /\ z e. ( { g e. D | g oR <_ y } \ { y } ) ) -> if ( ( y oF - z ) = ( I X. { 0 } ) , .1. , .0. ) = .0. )
87 71 86 eqtrd 
 |-  ( ( ( ph /\ y e. D ) /\ z e. ( { g e. D | g oR <_ y } \ { y } ) ) -> ( U ` ( y oF - z ) ) = .0. )
88 87 oveq2d 
 |-  ( ( ( ph /\ y e. D ) /\ z e. ( { g e. D | g oR <_ y } \ { y } ) ) -> ( ( X ` z ) ( .r ` R ) ( U ` ( y oF - z ) ) ) = ( ( X ` z ) ( .r ` R ) .0. ) )
89 11 18 5 ringrz 
 |-  ( ( R e. Ring /\ ( X ` z ) e. ( Base ` R ) ) -> ( ( X ` z ) ( .r ` R ) .0. ) = .0. )
90 41 48 89 syl2anc 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { g e. D | g oR <_ y } ) -> ( ( X ` z ) ( .r ` R ) .0. ) = .0. )
91 63 90 sylan2 
 |-  ( ( ( ph /\ y e. D ) /\ z e. ( { g e. D | g oR <_ y } \ { y } ) ) -> ( ( X ` z ) ( .r ` R ) .0. ) = .0. )
92 88 91 eqtrd 
 |-  ( ( ( ph /\ y e. D ) /\ z e. ( { g e. D | g oR <_ y } \ { y } ) ) -> ( ( X ` z ) ( .r ` R ) ( U ` ( y oF - z ) ) ) = .0. )
93 92 40 suppss2 
 |-  ( ( ph /\ y e. D ) -> ( ( z e. { g e. D | g oR <_ y } |-> ( ( X ` z ) ( .r ` R ) ( U ` ( y oF - z ) ) ) ) supp .0. ) C_ { y } )
94 40 mptexd 
 |-  ( ( ph /\ y e. D ) -> ( z e. { g e. D | g oR <_ y } |-> ( ( X ` z ) ( .r ` R ) ( U ` ( y oF - z ) ) ) ) e. _V )
95 funmpt 
 |-  Fun ( z e. { g e. D | g oR <_ y } |-> ( ( X ` z ) ( .r ` R ) ( U ` ( y oF - z ) ) ) )
96 95 a1i 
 |-  ( ( ph /\ y e. D ) -> Fun ( z e. { g e. D | g oR <_ y } |-> ( ( X ` z ) ( .r ` R ) ( U ` ( y oF - z ) ) ) ) )
97 68 a1i 
 |-  ( ( ph /\ y e. D ) -> .0. e. _V )
98 snfi 
 |-  { y } e. Fin
99 98 a1i 
 |-  ( ( ph /\ y e. D ) -> { y } e. Fin )
100 suppssfifsupp 
 |-  ( ( ( ( z e. { g e. D | g oR <_ y } |-> ( ( X ` z ) ( .r ` R ) ( U ` ( y oF - z ) ) ) ) e. _V /\ Fun ( z e. { g e. D | g oR <_ y } |-> ( ( X ` z ) ( .r ` R ) ( U ` ( y oF - z ) ) ) ) /\ .0. e. _V ) /\ ( { y } e. Fin /\ ( ( z e. { g e. D | g oR <_ y } |-> ( ( X ` z ) ( .r ` R ) ( U ` ( y oF - z ) ) ) ) supp .0. ) C_ { y } ) ) -> ( z e. { g e. D | g oR <_ y } |-> ( ( X ` z ) ( .r ` R ) ( U ` ( y oF - z ) ) ) ) finSupp .0. )
101 94 96 97 99 93 100 syl32anc 
 |-  ( ( ph /\ y e. D ) -> ( z e. { g e. D | g oR <_ y } |-> ( ( X ` z ) ( .r ` R ) ( U ` ( y oF - z ) ) ) ) finSupp .0. )
102 11 5 37 40 62 93 101 gsumres 
 |-  ( ( ph /\ y e. D ) -> ( R gsum ( ( z e. { g e. D | g oR <_ y } |-> ( ( X ` z ) ( .r ` R ) ( U ` ( y oF - z ) ) ) ) |` { y } ) ) = ( R gsum ( z e. { g e. D | g oR <_ y } |-> ( ( X ` z ) ( .r ` R ) ( U ` ( y oF - z ) ) ) ) ) )
103 3 adantr 
 |-  ( ( ph /\ y e. D ) -> R e. Ring )
104 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
105 103 104 syl 
 |-  ( ( ph /\ y e. D ) -> R e. Mnd )
106 eqid 
 |-  y = y
107 ofsubeq0 
 |-  ( ( I e. V /\ y : I --> CC /\ y : I --> CC ) -> ( ( y oF - y ) = ( I X. { 0 } ) <-> y = y ) )
108 24 77 77 107 syl3anc 
 |-  ( ( ph /\ y e. D ) -> ( ( y oF - y ) = ( I X. { 0 } ) <-> y = y ) )
109 106 108 mpbiri 
 |-  ( ( ph /\ y e. D ) -> ( y oF - y ) = ( I X. { 0 } ) )
110 109 fveq2d 
 |-  ( ( ph /\ y e. D ) -> ( U ` ( y oF - y ) ) = ( U ` ( I X. { 0 } ) ) )
111 fconstmpt 
 |-  ( I X. { 0 } ) = ( w e. I |-> 0 )
112 4 fczpsrbag 
 |-  ( I e. V -> ( w e. I |-> 0 ) e. D )
113 2 112 syl 
 |-  ( ph -> ( w e. I |-> 0 ) e. D )
114 111 113 eqeltrid 
 |-  ( ph -> ( I X. { 0 } ) e. D )
115 114 adantr 
 |-  ( ( ph /\ y e. D ) -> ( I X. { 0 } ) e. D )
116 iftrue 
 |-  ( x = ( I X. { 0 } ) -> if ( x = ( I X. { 0 } ) , .1. , .0. ) = .1. )
117 116 7 67 fvmpt 
 |-  ( ( I X. { 0 } ) e. D -> ( U ` ( I X. { 0 } ) ) = .1. )
118 115 117 syl 
 |-  ( ( ph /\ y e. D ) -> ( U ` ( I X. { 0 } ) ) = .1. )
119 110 118 eqtrd 
 |-  ( ( ph /\ y e. D ) -> ( U ` ( y oF - y ) ) = .1. )
120 119 oveq2d 
 |-  ( ( ph /\ y e. D ) -> ( ( X ` y ) ( .r ` R ) ( U ` ( y oF - y ) ) ) = ( ( X ` y ) ( .r ` R ) .1. ) )
121 16 ffvelrnda 
 |-  ( ( ph /\ y e. D ) -> ( X ` y ) e. ( Base ` R ) )
122 11 18 6 ringridm 
 |-  ( ( R e. Ring /\ ( X ` y ) e. ( Base ` R ) ) -> ( ( X ` y ) ( .r ` R ) .1. ) = ( X ` y ) )
123 103 121 122 syl2anc 
 |-  ( ( ph /\ y e. D ) -> ( ( X ` y ) ( .r ` R ) .1. ) = ( X ` y ) )
124 120 123 eqtrd 
 |-  ( ( ph /\ y e. D ) -> ( ( X ` y ) ( .r ` R ) ( U ` ( y oF - y ) ) ) = ( X ` y ) )
125 124 121 eqeltrd 
 |-  ( ( ph /\ y e. D ) -> ( ( X ` y ) ( .r ` R ) ( U ` ( y oF - y ) ) ) e. ( Base ` R ) )
126 fveq2 
 |-  ( z = y -> ( X ` z ) = ( X ` y ) )
127 oveq2 
 |-  ( z = y -> ( y oF - z ) = ( y oF - y ) )
128 127 fveq2d 
 |-  ( z = y -> ( U ` ( y oF - z ) ) = ( U ` ( y oF - y ) ) )
129 126 128 oveq12d 
 |-  ( z = y -> ( ( X ` z ) ( .r ` R ) ( U ` ( y oF - z ) ) ) = ( ( X ` y ) ( .r ` R ) ( U ` ( y oF - y ) ) ) )
130 11 129 gsumsn 
 |-  ( ( R e. Mnd /\ y e. D /\ ( ( X ` y ) ( .r ` R ) ( U ` ( y oF - y ) ) ) e. ( Base ` R ) ) -> ( R gsum ( z e. { y } |-> ( ( X ` z ) ( .r ` R ) ( U ` ( y oF - z ) ) ) ) ) = ( ( X ` y ) ( .r ` R ) ( U ` ( y oF - y ) ) ) )
131 105 21 125 130 syl3anc 
 |-  ( ( ph /\ y e. D ) -> ( R gsum ( z e. { y } |-> ( ( X ` z ) ( .r ` R ) ( U ` ( y oF - z ) ) ) ) ) = ( ( X ` y ) ( .r ` R ) ( U ` ( y oF - y ) ) ) )
132 34 102 131 3eqtr3d 
 |-  ( ( ph /\ y e. D ) -> ( R gsum ( z e. { g e. D | g oR <_ y } |-> ( ( X ` z ) ( .r ` R ) ( U ` ( y oF - z ) ) ) ) ) = ( ( X ` y ) ( .r ` R ) ( U ` ( y oF - y ) ) ) )
133 22 132 124 3eqtrd 
 |-  ( ( ph /\ y e. D ) -> ( ( X .x. U ) ` y ) = ( X ` y ) )
134 15 17 133 eqfnfvd 
 |-  ( ph -> ( X .x. U ) = X )