This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem psdmvr

Description: The partial derivative of a variable is the Kronecker delta if ( X = Y , .1. , .0. ) . (Contributed by SN, 16-Oct-2025)

Ref Expression
Hypotheses psdmvr.s 
|- S = ( I mPwSer R )
psdmvr.z 
|- .0. = ( 0g ` S )
psdmvr.o 
|- .1. = ( 1r ` S )
psdmvr.v 
|- V = ( I mVar R )
psdmvr.i 
|- ( ph -> I e. W )
psdmvr.r 
|- ( ph -> R e. Ring )
psdmvr.x 
|- ( ph -> X e. I )
psdmvr.y 
|- ( ph -> Y e. I )
Assertion psdmvr 
|- ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( V ` Y ) ) = if ( X = Y , .1. , .0. ) )

Proof

Step Hyp Ref Expression
1 psdmvr.s 
 |-  S = ( I mPwSer R )
2 psdmvr.z 
 |-  .0. = ( 0g ` S )
3 psdmvr.o 
 |-  .1. = ( 1r ` S )
4 psdmvr.v 
 |-  V = ( I mVar R )
5 psdmvr.i 
 |-  ( ph -> I e. W )
6 psdmvr.r 
 |-  ( ph -> R e. Ring )
7 psdmvr.x 
 |-  ( ph -> X e. I )
8 psdmvr.y 
 |-  ( ph -> Y e. I )
9 eqid 
 |-  ( Base ` S ) = ( Base ` S )
10 eqid 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
11 1 4 9 5 6 8 mvrcl2 
 |-  ( ph -> ( V ` Y ) e. ( Base ` S ) )
12 1 9 10 7 11 psdval 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( V ` Y ) ) = ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( ( V ` Y ) ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) )
13 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
14 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
15 5 adantr 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> I e. W )
16 6 adantr 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> R e. Ring )
17 8 adantr 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> Y e. I )
18 simpr 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
19 10 psrbagsn 
 |-  ( I e. W -> ( y e. I |-> if ( y = X , 1 , 0 ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
20 5 19 syl 
 |-  ( ph -> ( y e. I |-> if ( y = X , 1 , 0 ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
21 20 adantr 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( y e. I |-> if ( y = X , 1 , 0 ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
22 10 psrbagaddcl 
 |-  ( ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } /\ ( y e. I |-> if ( y = X , 1 , 0 ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
23 18 21 22 syl2anc 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
24 4 10 13 14 15 16 17 23 mvrval2 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( V ` Y ) ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) = if ( ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = ( y e. I |-> if ( y = Y , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) )
25 1red 
 |-  ( ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = ( y e. I |-> if ( y = Y , 1 , 0 ) ) ) -> 1 e. RR )
26 10 psrbagf 
 |-  ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> k : I --> NN0 )
27 26 ad2antlr 
 |-  ( ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = ( y e. I |-> if ( y = Y , 1 , 0 ) ) ) -> k : I --> NN0 )
28 7 ad2antrr 
 |-  ( ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = ( y e. I |-> if ( y = Y , 1 , 0 ) ) ) -> X e. I )
29 27 28 ffvelcdmd 
 |-  ( ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = ( y e. I |-> if ( y = Y , 1 , 0 ) ) ) -> ( k ` X ) e. NN0 )
30 nn0addge2 
 |-  ( ( 1 e. RR /\ ( k ` X ) e. NN0 ) -> 1 <_ ( ( k ` X ) + 1 ) )
31 25 29 30 syl2anc 
 |-  ( ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = ( y e. I |-> if ( y = Y , 1 , 0 ) ) ) -> 1 <_ ( ( k ` X ) + 1 ) )
32 fveq1 
 |-  ( ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = ( y e. I |-> if ( y = Y , 1 , 0 ) ) -> ( ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ` X ) = ( ( y e. I |-> if ( y = Y , 1 , 0 ) ) ` X ) )
33 32 adantl 
 |-  ( ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = ( y e. I |-> if ( y = Y , 1 , 0 ) ) ) -> ( ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ` X ) = ( ( y e. I |-> if ( y = Y , 1 , 0 ) ) ` X ) )
34 26 ffnd 
 |-  ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> k Fn I )
35 34 adantl 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> k Fn I )
36 1re 
 |-  1 e. RR
37 0re 
 |-  0 e. RR
38 36 37 ifcli 
 |-  if ( y = X , 1 , 0 ) e. RR
39 38 elexi 
 |-  if ( y = X , 1 , 0 ) e. _V
40 eqid 
 |-  ( y e. I |-> if ( y = X , 1 , 0 ) ) = ( y e. I |-> if ( y = X , 1 , 0 ) )
41 39 40 fnmpti 
 |-  ( y e. I |-> if ( y = X , 1 , 0 ) ) Fn I
42 41 a1i 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( y e. I |-> if ( y = X , 1 , 0 ) ) Fn I )
43 inidm 
 |-  ( I i^i I ) = I
44 eqidd 
 |-  ( ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ X e. I ) -> ( k ` X ) = ( k ` X ) )
45 iftrue 
 |-  ( y = X -> if ( y = X , 1 , 0 ) = 1 )
46 1ex 
 |-  1 e. _V
47 45 40 46 fvmpt 
 |-  ( X e. I -> ( ( y e. I |-> if ( y = X , 1 , 0 ) ) ` X ) = 1 )
48 47 adantl 
 |-  ( ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ X e. I ) -> ( ( y e. I |-> if ( y = X , 1 , 0 ) ) ` X ) = 1 )
49 35 42 15 15 43 44 48 ofval 
 |-  ( ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ X e. I ) -> ( ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ` X ) = ( ( k ` X ) + 1 ) )
50 7 49 mpidan 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ` X ) = ( ( k ` X ) + 1 ) )
51 50 adantr 
 |-  ( ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = ( y e. I |-> if ( y = Y , 1 , 0 ) ) ) -> ( ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ` X ) = ( ( k ` X ) + 1 ) )
52 eqid 
 |-  ( y e. I |-> if ( y = Y , 1 , 0 ) ) = ( y e. I |-> if ( y = Y , 1 , 0 ) )
53 eqeq1 
 |-  ( y = X -> ( y = Y <-> X = Y ) )
54 53 ifbid 
 |-  ( y = X -> if ( y = Y , 1 , 0 ) = if ( X = Y , 1 , 0 ) )
55 36 37 ifcli 
 |-  if ( X = Y , 1 , 0 ) e. RR
56 55 a1i 
 |-  ( ph -> if ( X = Y , 1 , 0 ) e. RR )
57 52 54 7 56 fvmptd3 
 |-  ( ph -> ( ( y e. I |-> if ( y = Y , 1 , 0 ) ) ` X ) = if ( X = Y , 1 , 0 ) )
58 57 ad2antrr 
 |-  ( ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = ( y e. I |-> if ( y = Y , 1 , 0 ) ) ) -> ( ( y e. I |-> if ( y = Y , 1 , 0 ) ) ` X ) = if ( X = Y , 1 , 0 ) )
59 33 51 58 3eqtr3d 
 |-  ( ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = ( y e. I |-> if ( y = Y , 1 , 0 ) ) ) -> ( ( k ` X ) + 1 ) = if ( X = Y , 1 , 0 ) )
60 31 59 breqtrd 
 |-  ( ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = ( y e. I |-> if ( y = Y , 1 , 0 ) ) ) -> 1 <_ if ( X = Y , 1 , 0 ) )
61 1le1 
 |-  1 <_ 1
62 0le1 
 |-  0 <_ 1
63 anifp 
 |-  ( ( 1 <_ 1 /\ 0 <_ 1 ) -> if- ( X = Y , 1 <_ 1 , 0 <_ 1 ) )
64 61 62 63 mp2an 
 |-  if- ( X = Y , 1 <_ 1 , 0 <_ 1 )
65 brif1 
 |-  ( if ( X = Y , 1 , 0 ) <_ 1 <-> if- ( X = Y , 1 <_ 1 , 0 <_ 1 ) )
66 64 65 mpbir 
 |-  if ( X = Y , 1 , 0 ) <_ 1
67 36 55 letri3i 
 |-  ( 1 = if ( X = Y , 1 , 0 ) <-> ( 1 <_ if ( X = Y , 1 , 0 ) /\ if ( X = Y , 1 , 0 ) <_ 1 ) )
68 60 66 67 sylanblrc 
 |-  ( ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = ( y e. I |-> if ( y = Y , 1 , 0 ) ) ) -> 1 = if ( X = Y , 1 , 0 ) )
69 68 eqcomd 
 |-  ( ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = ( y e. I |-> if ( y = Y , 1 , 0 ) ) ) -> if ( X = Y , 1 , 0 ) = 1 )
70 ax-1ne0 
 |-  1 =/= 0
71 iftrueb 
 |-  ( 1 =/= 0 -> ( if ( X = Y , 1 , 0 ) = 1 <-> X = Y ) )
72 70 71 ax-mp 
 |-  ( if ( X = Y , 1 , 0 ) = 1 <-> X = Y )
73 69 72 sylib 
 |-  ( ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = ( y e. I |-> if ( y = Y , 1 , 0 ) ) ) -> X = Y )
74 eqeq2 
 |-  ( X = Y -> ( y = X <-> y = Y ) )
75 74 ifbid 
 |-  ( X = Y -> if ( y = X , 1 , 0 ) = if ( y = Y , 1 , 0 ) )
76 75 mpteq2dv 
 |-  ( X = Y -> ( y e. I |-> if ( y = X , 1 , 0 ) ) = ( y e. I |-> if ( y = Y , 1 , 0 ) ) )
77 76 oveq2d 
 |-  ( X = Y -> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = ( k oF + ( y e. I |-> if ( y = Y , 1 , 0 ) ) ) )
78 77 eqeq1d 
 |-  ( X = Y -> ( ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = ( y e. I |-> if ( y = Y , 1 , 0 ) ) <-> ( k oF + ( y e. I |-> if ( y = Y , 1 , 0 ) ) ) = ( y e. I |-> if ( y = Y , 1 , 0 ) ) ) )
79 26 adantl 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> k : I --> NN0 )
80 1nn0 
 |-  1 e. NN0
81 0nn0 
 |-  0 e. NN0
82 80 81 ifcli 
 |-  if ( y = Y , 1 , 0 ) e. NN0
83 82 a1i 
 |-  ( y e. I -> if ( y = Y , 1 , 0 ) e. NN0 )
84 52 83 fmpti 
 |-  ( y e. I |-> if ( y = Y , 1 , 0 ) ) : I --> NN0
85 84 a1i 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( y e. I |-> if ( y = Y , 1 , 0 ) ) : I --> NN0 )
86 nn0cn 
 |-  ( n e. NN0 -> n e. CC )
87 nn0cn 
 |-  ( m e. NN0 -> m e. CC )
88 addcom 
 |-  ( ( n e. CC /\ m e. CC ) -> ( n + m ) = ( m + n ) )
89 88 eqeq1d 
 |-  ( ( n e. CC /\ m e. CC ) -> ( ( n + m ) = m <-> ( m + n ) = m ) )
90 addid0 
 |-  ( ( m e. CC /\ n e. CC ) -> ( ( m + n ) = m <-> n = 0 ) )
91 90 ancoms 
 |-  ( ( n e. CC /\ m e. CC ) -> ( ( m + n ) = m <-> n = 0 ) )
92 89 91 bitrd 
 |-  ( ( n e. CC /\ m e. CC ) -> ( ( n + m ) = m <-> n = 0 ) )
93 86 87 92 syl2an 
 |-  ( ( n e. NN0 /\ m e. NN0 ) -> ( ( n + m ) = m <-> n = 0 ) )
94 93 adantl 
 |-  ( ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( n e. NN0 /\ m e. NN0 ) ) -> ( ( n + m ) = m <-> n = 0 ) )
95 15 79 85 94 caofidlcan 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( k oF + ( y e. I |-> if ( y = Y , 1 , 0 ) ) ) = ( y e. I |-> if ( y = Y , 1 , 0 ) ) <-> k = ( I X. { 0 } ) ) )
96 78 95 sylan9bbr 
 |-  ( ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ X = Y ) -> ( ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = ( y e. I |-> if ( y = Y , 1 , 0 ) ) <-> k = ( I X. { 0 } ) ) )
97 73 96 biadanid 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = ( y e. I |-> if ( y = Y , 1 , 0 ) ) <-> ( X = Y /\ k = ( I X. { 0 } ) ) ) )
98 97 biancomd 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = ( y e. I |-> if ( y = Y , 1 , 0 ) ) <-> ( k = ( I X. { 0 } ) /\ X = Y ) ) )
99 98 ifbid 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> if ( ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = ( y e. I |-> if ( y = Y , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) = if ( ( k = ( I X. { 0 } ) /\ X = Y ) , ( 1r ` R ) , ( 0g ` R ) ) )
100 24 99 eqtrd 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( V ` Y ) ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) = if ( ( k = ( I X. { 0 } ) /\ X = Y ) , ( 1r ` R ) , ( 0g ` R ) ) )
101 100 oveq2d 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( ( V ` Y ) ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) = ( ( ( k ` X ) + 1 ) ( .g ` R ) if ( ( k = ( I X. { 0 } ) /\ X = Y ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
102 ovif2 
 |-  ( ( ( k ` X ) + 1 ) ( .g ` R ) if ( ( k = ( I X. { 0 } ) /\ X = Y ) , ( 1r ` R ) , ( 0g ` R ) ) ) = if ( ( k = ( I X. { 0 } ) /\ X = Y ) , ( ( ( k ` X ) + 1 ) ( .g ` R ) ( 1r ` R ) ) , ( ( ( k ` X ) + 1 ) ( .g ` R ) ( 0g ` R ) ) )
103 fveq1 
 |-  ( k = ( I X. { 0 } ) -> ( k ` X ) = ( ( I X. { 0 } ) ` X ) )
104 103 oveq1d 
 |-  ( k = ( I X. { 0 } ) -> ( ( k ` X ) + 1 ) = ( ( ( I X. { 0 } ) ` X ) + 1 ) )
105 7 adantr 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> X e. I )
106 c0ex 
 |-  0 e. _V
107 106 fvconst2 
 |-  ( X e. I -> ( ( I X. { 0 } ) ` X ) = 0 )
108 105 107 syl 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( I X. { 0 } ) ` X ) = 0 )
109 108 oveq1d 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( I X. { 0 } ) ` X ) + 1 ) = ( 0 + 1 ) )
110 0p1e1 
 |-  ( 0 + 1 ) = 1
111 109 110 eqtrdi 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( I X. { 0 } ) ` X ) + 1 ) = 1 )
112 104 111 sylan9eqr 
 |-  ( ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ k = ( I X. { 0 } ) ) -> ( ( k ` X ) + 1 ) = 1 )
113 112 adantrr 
 |-  ( ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( k = ( I X. { 0 } ) /\ X = Y ) ) -> ( ( k ` X ) + 1 ) = 1 )
114 113 oveq1d 
 |-  ( ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( k = ( I X. { 0 } ) /\ X = Y ) ) -> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( 1r ` R ) ) = ( 1 ( .g ` R ) ( 1r ` R ) ) )
115 eqid 
 |-  ( Base ` R ) = ( Base ` R )
116 115 14 6 ringidcld 
 |-  ( ph -> ( 1r ` R ) e. ( Base ` R ) )
117 eqid 
 |-  ( .g ` R ) = ( .g ` R )
118 115 117 mulg1 
 |-  ( ( 1r ` R ) e. ( Base ` R ) -> ( 1 ( .g ` R ) ( 1r ` R ) ) = ( 1r ` R ) )
119 116 118 syl 
 |-  ( ph -> ( 1 ( .g ` R ) ( 1r ` R ) ) = ( 1r ` R ) )
120 119 ad2antrr 
 |-  ( ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( k = ( I X. { 0 } ) /\ X = Y ) ) -> ( 1 ( .g ` R ) ( 1r ` R ) ) = ( 1r ` R ) )
121 114 120 eqtrd 
 |-  ( ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( k = ( I X. { 0 } ) /\ X = Y ) ) -> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( 1r ` R ) ) = ( 1r ` R ) )
122 6 ringgrpd 
 |-  ( ph -> R e. Grp )
123 122 grpmndd 
 |-  ( ph -> R e. Mnd )
124 123 adantr 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> R e. Mnd )
125 79 105 ffvelcdmd 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( k ` X ) e. NN0 )
126 80 a1i 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> 1 e. NN0 )
127 125 126 nn0addcld 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( k ` X ) + 1 ) e. NN0 )
128 115 117 13 mulgnn0z 
 |-  ( ( R e. Mnd /\ ( ( k ` X ) + 1 ) e. NN0 ) -> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
129 124 127 128 syl2anc 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
130 129 adantr 
 |-  ( ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ -. ( k = ( I X. { 0 } ) /\ X = Y ) ) -> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
131 121 130 ifeq12da 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> if ( ( k = ( I X. { 0 } ) /\ X = Y ) , ( ( ( k ` X ) + 1 ) ( .g ` R ) ( 1r ` R ) ) , ( ( ( k ` X ) + 1 ) ( .g ` R ) ( 0g ` R ) ) ) = if ( ( k = ( I X. { 0 } ) /\ X = Y ) , ( 1r ` R ) , ( 0g ` R ) ) )
132 102 131 eqtrid 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( k ` X ) + 1 ) ( .g ` R ) if ( ( k = ( I X. { 0 } ) /\ X = Y ) , ( 1r ` R ) , ( 0g ` R ) ) ) = if ( ( k = ( I X. { 0 } ) /\ X = Y ) , ( 1r ` R ) , ( 0g ` R ) ) )
133 ancom 
 |-  ( ( k = ( I X. { 0 } ) /\ X = Y ) <-> ( X = Y /\ k = ( I X. { 0 } ) ) )
134 ifbi 
 |-  ( ( ( k = ( I X. { 0 } ) /\ X = Y ) <-> ( X = Y /\ k = ( I X. { 0 } ) ) ) -> if ( ( k = ( I X. { 0 } ) /\ X = Y ) , ( 1r ` R ) , ( 0g ` R ) ) = if ( ( X = Y /\ k = ( I X. { 0 } ) ) , ( 1r ` R ) , ( 0g ` R ) ) )
135 133 134 ax-mp 
 |-  if ( ( k = ( I X. { 0 } ) /\ X = Y ) , ( 1r ` R ) , ( 0g ` R ) ) = if ( ( X = Y /\ k = ( I X. { 0 } ) ) , ( 1r ` R ) , ( 0g ` R ) )
136 ifan 
 |-  if ( ( X = Y /\ k = ( I X. { 0 } ) ) , ( 1r ` R ) , ( 0g ` R ) ) = if ( X = Y , if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) , ( 0g ` R ) )
137 135 136 eqtri 
 |-  if ( ( k = ( I X. { 0 } ) /\ X = Y ) , ( 1r ` R ) , ( 0g ` R ) ) = if ( X = Y , if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) , ( 0g ` R ) )
138 137 a1i 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> if ( ( k = ( I X. { 0 } ) /\ X = Y ) , ( 1r ` R ) , ( 0g ` R ) ) = if ( X = Y , if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) , ( 0g ` R ) ) )
139 101 132 138 3eqtrd 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( ( V ` Y ) ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) = if ( X = Y , if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) , ( 0g ` R ) ) )
140 139 mpteq2dva 
 |-  ( ph -> ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( ( V ` Y ) ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) = ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( X = Y , if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) , ( 0g ` R ) ) ) )
141 ifmpt2v 
 |-  ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( X = Y , if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) , ( 0g ` R ) ) ) = if ( X = Y , ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) , ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( 0g ` R ) ) )
142 1 5 6 10 13 14 3 psr1 
 |-  ( ph -> .1. = ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
143 1 5 122 10 13 2 psr0 
 |-  ( ph -> .0. = ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { ( 0g ` R ) } ) )
144 fconstmpt 
 |-  ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { ( 0g ` R ) } ) = ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( 0g ` R ) )
145 143 144 eqtrdi 
 |-  ( ph -> .0. = ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( 0g ` R ) ) )
146 142 145 ifeq12d 
 |-  ( ph -> if ( X = Y , .1. , .0. ) = if ( X = Y , ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) , ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( 0g ` R ) ) ) )
147 141 146 eqtr4id 
 |-  ( ph -> ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( X = Y , if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) , ( 0g ` R ) ) ) = if ( X = Y , .1. , .0. ) )
148 12 140 147 3eqtrd 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( V ` Y ) ) = if ( X = Y , .1. , .0. ) )