Metamath Proof Explorer

Theorem psrascl

Description: Value of the scalar injection into the power series algebra. (Contributed by SN, 18-May-2025)

Ref Expression
Hypotheses psrascl.s 
|- S = ( I mPwSer R )
psrascl.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
psrascl.z 
|- .0. = ( 0g ` R )
psrascl.k 
|- K = ( Base ` R )
psrascl.a 
|- A = ( algSc ` S )
psrascl.i 
|- ( ph -> I e. V )
psrascl.r 
|- ( ph -> R e. Ring )
psrascl.x 
|- ( ph -> X e. K )
Assertion psrascl 
|- ( ph -> ( A ` X ) = ( y e. D |-> if ( y = ( I X. { 0 } ) , X , .0. ) ) )

Proof

Step Hyp Ref Expression
1 psrascl.s 
 |-  S = ( I mPwSer R )
2 psrascl.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
3 psrascl.z 
 |-  .0. = ( 0g ` R )
4 psrascl.k 
 |-  K = ( Base ` R )
5 psrascl.a 
 |-  A = ( algSc ` S )
6 psrascl.i 
 |-  ( ph -> I e. V )
7 psrascl.r 
 |-  ( ph -> R e. Ring )
8 psrascl.x 
 |-  ( ph -> X e. K )
9 1 6 7 psrsca 
 |-  ( ph -> R = ( Scalar ` S ) )
10 9 fveq2d 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` S ) ) )
11 4 10 eqtrid 
 |-  ( ph -> K = ( Base ` ( Scalar ` S ) ) )
12 8 11 eleqtrd 
 |-  ( ph -> X e. ( Base ` ( Scalar ` S ) ) )
13 eqid 
 |-  ( Scalar ` S ) = ( Scalar ` S )
14 eqid 
 |-  ( Base ` ( Scalar ` S ) ) = ( Base ` ( Scalar ` S ) )
15 eqid 
 |-  ( .s ` S ) = ( .s ` S )
16 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
17 5 13 14 15 16 asclval 
 |-  ( X e. ( Base ` ( Scalar ` S ) ) -> ( A ` X ) = ( X ( .s ` S ) ( 1r ` S ) ) )
18 12 17 syl 
 |-  ( ph -> ( A ` X ) = ( X ( .s ` S ) ( 1r ` S ) ) )
19 eqid 
 |-  ( Base ` S ) = ( Base ` S )
20 eqid 
 |-  ( .r ` R ) = ( .r ` R )
21 1 6 7 psrring 
 |-  ( ph -> S e. Ring )
22 19 16 ringidcl 
 |-  ( S e. Ring -> ( 1r ` S ) e. ( Base ` S ) )
23 21 22 syl 
 |-  ( ph -> ( 1r ` S ) e. ( Base ` S ) )
24 1 15 4 19 20 2 8 23 psrvsca 
 |-  ( ph -> ( X ( .s ` S ) ( 1r ` S ) ) = ( ( D X. { X } ) oF ( .r ` R ) ( 1r ` S ) ) )
25 fnconstg 
 |-  ( X e. K -> ( D X. { X } ) Fn D )
26 8 25 syl 
 |-  ( ph -> ( D X. { X } ) Fn D )
27 1 4 2 19 23 psrelbas 
 |-  ( ph -> ( 1r ` S ) : D --> K )
28 27 ffnd 
 |-  ( ph -> ( 1r ` S ) Fn D )
29 ovexd 
 |-  ( ph -> ( NN0 ^m I ) e. _V )
30 2 29 rabexd 
 |-  ( ph -> D e. _V )
31 inidm 
 |-  ( D i^i D ) = D
32 fvconst2g 
 |-  ( ( X e. K /\ y e. D ) -> ( ( D X. { X } ) ` y ) = X )
33 8 32 sylan 
 |-  ( ( ph /\ y e. D ) -> ( ( D X. { X } ) ` y ) = X )
34 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
35 1 6 7 2 3 34 16 psr1 
 |-  ( ph -> ( 1r ` S ) = ( d e. D |-> if ( d = ( I X. { 0 } ) , ( 1r ` R ) , .0. ) ) )
36 35 adantr 
 |-  ( ( ph /\ y e. D ) -> ( 1r ` S ) = ( d e. D |-> if ( d = ( I X. { 0 } ) , ( 1r ` R ) , .0. ) ) )
37 36 fveq1d 
 |-  ( ( ph /\ y e. D ) -> ( ( 1r ` S ) ` y ) = ( ( d e. D |-> if ( d = ( I X. { 0 } ) , ( 1r ` R ) , .0. ) ) ` y ) )
38 eqeq1 
 |-  ( d = y -> ( d = ( I X. { 0 } ) <-> y = ( I X. { 0 } ) ) )
39 38 ifbid 
 |-  ( d = y -> if ( d = ( I X. { 0 } ) , ( 1r ` R ) , .0. ) = if ( y = ( I X. { 0 } ) , ( 1r ` R ) , .0. ) )
40 eqid 
 |-  ( d e. D |-> if ( d = ( I X. { 0 } ) , ( 1r ` R ) , .0. ) ) = ( d e. D |-> if ( d = ( I X. { 0 } ) , ( 1r ` R ) , .0. ) )
41 fvex 
 |-  ( 1r ` R ) e. _V
42 3 fvexi 
 |-  .0. e. _V
43 41 42 ifex 
 |-  if ( y = ( I X. { 0 } ) , ( 1r ` R ) , .0. ) e. _V
44 39 40 43 fvmpt 
 |-  ( y e. D -> ( ( d e. D |-> if ( d = ( I X. { 0 } ) , ( 1r ` R ) , .0. ) ) ` y ) = if ( y = ( I X. { 0 } ) , ( 1r ` R ) , .0. ) )
45 44 adantl 
 |-  ( ( ph /\ y e. D ) -> ( ( d e. D |-> if ( d = ( I X. { 0 } ) , ( 1r ` R ) , .0. ) ) ` y ) = if ( y = ( I X. { 0 } ) , ( 1r ` R ) , .0. ) )
46 37 45 eqtrd 
 |-  ( ( ph /\ y e. D ) -> ( ( 1r ` S ) ` y ) = if ( y = ( I X. { 0 } ) , ( 1r ` R ) , .0. ) )
47 26 28 30 30 31 33 46 offval 
 |-  ( ph -> ( ( D X. { X } ) oF ( .r ` R ) ( 1r ` S ) ) = ( y e. D |-> ( X ( .r ` R ) if ( y = ( I X. { 0 } ) , ( 1r ` R ) , .0. ) ) ) )
48 ovif2 
 |-  ( X ( .r ` R ) if ( y = ( I X. { 0 } ) , ( 1r ` R ) , .0. ) ) = if ( y = ( I X. { 0 } ) , ( X ( .r ` R ) ( 1r ` R ) ) , ( X ( .r ` R ) .0. ) )
49 4 20 34 7 8 ringridmd 
 |-  ( ph -> ( X ( .r ` R ) ( 1r ` R ) ) = X )
50 4 20 3 7 8 ringrzd 
 |-  ( ph -> ( X ( .r ` R ) .0. ) = .0. )
51 49 50 ifeq12d 
 |-  ( ph -> if ( y = ( I X. { 0 } ) , ( X ( .r ` R ) ( 1r ` R ) ) , ( X ( .r ` R ) .0. ) ) = if ( y = ( I X. { 0 } ) , X , .0. ) )
52 48 51 eqtrid 
 |-  ( ph -> ( X ( .r ` R ) if ( y = ( I X. { 0 } ) , ( 1r ` R ) , .0. ) ) = if ( y = ( I X. { 0 } ) , X , .0. ) )
53 52 mpteq2dv 
 |-  ( ph -> ( y e. D |-> ( X ( .r ` R ) if ( y = ( I X. { 0 } ) , ( 1r ` R ) , .0. ) ) ) = ( y e. D |-> if ( y = ( I X. { 0 } ) , X , .0. ) ) )
54 47 53 eqtrd 
 |-  ( ph -> ( ( D X. { X } ) oF ( .r ` R ) ( 1r ` S ) ) = ( y e. D |-> if ( y = ( I X. { 0 } ) , X , .0. ) ) )
55 18 24 54 3eqtrd 
 |-  ( ph -> ( A ` X ) = ( y e. D |-> if ( y = ( I X. { 0 } ) , X , .0. ) ) )