Metamath Proof Explorer

Theorem psd1

Description: The derivative of one is zero. (Contributed by SN, 25-Apr-2025)

Ref Expression
Hypotheses psd1.s 
|- S = ( I mPwSer R )
psd1.u 
|- .1. = ( 1r ` S )
psd1.z 
|- .0. = ( 0g ` S )
psd1.i 
|- ( ph -> I e. V )
psd1.r 
|- ( ph -> R e. CRing )
psd1.x 
|- ( ph -> X e. I )
Assertion psd1 
|- ( ph -> ( ( ( I mPSDer R ) ` X ) ` .1. ) = .0. )

Proof

Step Hyp Ref Expression
1 psd1.s 
 |-  S = ( I mPwSer R )
2 psd1.u 
 |-  .1. = ( 1r ` S )
3 psd1.z 
 |-  .0. = ( 0g ` S )
4 psd1.i 
 |-  ( ph -> I e. V )
5 psd1.r 
 |-  ( ph -> R e. CRing )
6 psd1.x 
 |-  ( ph -> X e. I )
7 eqid 
 |-  ( Base ` S ) = ( Base ` S )
8 eqid 
 |-  ( +g ` S ) = ( +g ` S )
9 eqid 
 |-  ( .r ` S ) = ( .r ` S )
10 1 4 5 psrcrng 
 |-  ( ph -> S e. CRing )
11 10 crngringd 
 |-  ( ph -> S e. Ring )
12 7 2 ringidcl 
 |-  ( S e. Ring -> .1. e. ( Base ` S ) )
13 11 12 syl 
 |-  ( ph -> .1. e. ( Base ` S ) )
14 1 7 8 9 4 5 6 13 13 psdmul 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( .1. ( .r ` S ) .1. ) ) = ( ( ( ( ( I mPSDer R ) ` X ) ` .1. ) ( .r ` S ) .1. ) ( +g ` S ) ( .1. ( .r ` S ) ( ( ( I mPSDer R ) ` X ) ` .1. ) ) ) )
15 7 9 2 11 13 ringlidmd 
 |-  ( ph -> ( .1. ( .r ` S ) .1. ) = .1. )
16 15 fveq2d 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( .1. ( .r ` S ) .1. ) ) = ( ( ( I mPSDer R ) ` X ) ` .1. ) )
17 5 crnggrpd 
 |-  ( ph -> R e. Grp )
18 17 grpmgmd 
 |-  ( ph -> R e. Mgm )
19 1 7 4 18 6 13 psdcl 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` .1. ) e. ( Base ` S ) )
20 7 9 2 11 19 ringridmd 
 |-  ( ph -> ( ( ( ( I mPSDer R ) ` X ) ` .1. ) ( .r ` S ) .1. ) = ( ( ( I mPSDer R ) ` X ) ` .1. ) )
21 7 9 2 11 19 ringlidmd 
 |-  ( ph -> ( .1. ( .r ` S ) ( ( ( I mPSDer R ) ` X ) ` .1. ) ) = ( ( ( I mPSDer R ) ` X ) ` .1. ) )
22 20 21 oveq12d 
 |-  ( ph -> ( ( ( ( ( I mPSDer R ) ` X ) ` .1. ) ( .r ` S ) .1. ) ( +g ` S ) ( .1. ( .r ` S ) ( ( ( I mPSDer R ) ` X ) ` .1. ) ) ) = ( ( ( ( I mPSDer R ) ` X ) ` .1. ) ( +g ` S ) ( ( ( I mPSDer R ) ` X ) ` .1. ) ) )
23 14 16 22 3eqtr3rd 
 |-  ( ph -> ( ( ( ( I mPSDer R ) ` X ) ` .1. ) ( +g ` S ) ( ( ( I mPSDer R ) ` X ) ` .1. ) ) = ( ( ( I mPSDer R ) ` X ) ` .1. ) )
24 10 crnggrpd 
 |-  ( ph -> S e. Grp )
25 7 8 3 grpid 
 |-  ( ( S e. Grp /\ ( ( ( I mPSDer R ) ` X ) ` .1. ) e. ( Base ` S ) ) -> ( ( ( ( ( I mPSDer R ) ` X ) ` .1. ) ( +g ` S ) ( ( ( I mPSDer R ) ` X ) ` .1. ) ) = ( ( ( I mPSDer R ) ` X ) ` .1. ) <-> .0. = ( ( ( I mPSDer R ) ` X ) ` .1. ) ) )
26 24 19 25 syl2anc 
 |-  ( ph -> ( ( ( ( ( I mPSDer R ) ` X ) ` .1. ) ( +g ` S ) ( ( ( I mPSDer R ) ` X ) ` .1. ) ) = ( ( ( I mPSDer R ) ` X ) ` .1. ) <-> .0. = ( ( ( I mPSDer R ) ` X ) ` .1. ) ) )
27 23 26 mpbid 
 |-  ( ph -> .0. = ( ( ( I mPSDer R ) ` X ) ` .1. ) )
28 27 eqcomd 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` .1. ) = .0. )