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 ˙ = 0 S
psdmvr.o ⊢ 1 ˙ = 1 S
psdmvr.v ⊢ V = I mVar R
psdmvr.i ⊢ φ → I ∈ W
psdmvr.r ⊢ φ → R ∈ Ring
psdmvr.x ⊢ φ → X ∈ I
psdmvr.y ⊢ φ → Y ∈ I
Assertion psdmvr ⊢ φ → 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 ˙ = 0 S
3 psdmvr.o ⊢ 1 ˙ = 1 S
4 psdmvr.v ⊢ V = I mVar R
5 psdmvr.i ⊢ φ → I ∈ W
6 psdmvr.r ⊢ φ → R ∈ Ring
7 psdmvr.x ⊢ φ → X ∈ I
8 psdmvr.y ⊢ φ → Y ∈ I
9 eqid ⊢ Base S = Base S
10 eqid ⊢ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin = h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
11 1 4 9 5 6 8 mvrcl2 ⊢ φ → V ⁡ Y ∈ Base S
12 1 9 10 7 11 psdval ⊢ φ → I mPSDer R ⁡ X ⁡ V ⁡ Y = k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ k ⁡ X + 1 ⋅ R V ⁡ Y ⁡ k + f y ∈ I ⟼ if y = X 1 0
13 eqid ⊢ 0 R = 0 R
14 eqid ⊢ 1 R = 1 R
15 5 adantr ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → I ∈ W
16 6 adantr ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → R ∈ Ring
17 8 adantr ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → Y ∈ I
18 simpr ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
19 10 psrbagsn ⊢ I ∈ W → y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
20 5 19 syl ⊢ φ → y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
21 20 adantr ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
22 10 psrbagaddcl ⊢ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k + f y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
23 18 21 22 syl2anc ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k + f y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
24 4 10 13 14 15 16 17 23 mvrval2 ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → V ⁡ Y ⁡ k + f y ∈ I ⟼ if y = X 1 0 = if k + f y ∈ I ⟼ if y = X 1 0 = y ∈ I ⟼ if y = Y 1 0 1 R 0 R
25 1red ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ k + f y ∈ I ⟼ if y = X 1 0 = y ∈ I ⟼ if y = Y 1 0 → 1 ∈ ℝ
26 10 psrbagf ⊢ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k : I ⟶ ℕ 0
27 26 ad2antlr ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ k + f y ∈ I ⟼ if y = X 1 0 = y ∈ I ⟼ if y = Y 1 0 → k : I ⟶ ℕ 0
28 7 ad2antrr ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ k + f y ∈ I ⟼ if y = X 1 0 = y ∈ I ⟼ if y = Y 1 0 → X ∈ I
29 27 28 ffvelcdmd ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ k + f y ∈ I ⟼ if y = X 1 0 = y ∈ I ⟼ if y = Y 1 0 → k ⁡ X ∈ ℕ 0
30 nn0addge2 ⊢ 1 ∈ ℝ ∧ k ⁡ X ∈ ℕ 0 → 1 ≤ k ⁡ X + 1
31 25 29 30 syl2anc ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ k + f y ∈ I ⟼ if y = X 1 0 = y ∈ I ⟼ if y = Y 1 0 → 1 ≤ k ⁡ X + 1
32 fveq1 ⊢ k + f y ∈ I ⟼ if y = X 1 0 = y ∈ I ⟼ if y = Y 1 0 → k + f y ∈ I ⟼ if y = X 1 0 ⁡ X = y ∈ I ⟼ if y = Y 1 0 ⁡ X
33 32 adantl ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ k + f y ∈ I ⟼ if y = X 1 0 = y ∈ I ⟼ if y = Y 1 0 → k + f y ∈ I ⟼ if y = X 1 0 ⁡ X = y ∈ I ⟼ if y = Y 1 0 ⁡ X
34 26 ffnd ⊢ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k Fn I
35 34 adantl ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k Fn I
36 1re ⊢ 1 ∈ ℝ
37 0re ⊢ 0 ∈ ℝ
38 36 37 ifcli ⊢ if y = X 1 0 ∈ ℝ
39 38 elexi ⊢ if y = X 1 0 ∈ V
40 eqid ⊢ y ∈ I ⟼ if y = X 1 0 = y ∈ I ⟼ if y = X 1 0
41 39 40 fnmpti ⊢ y ∈ I ⟼ if y = X 1 0 Fn I
42 41 a1i ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → y ∈ I ⟼ if y = X 1 0 Fn I
43 inidm ⊢ I ∩ I = I
44 eqidd ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ X ∈ I → k ⁡ X = k ⁡ X
45 iftrue ⊢ y = X → if y = X 1 0 = 1
46 1ex ⊢ 1 ∈ V
47 45 40 46 fvmpt ⊢ X ∈ I → y ∈ I ⟼ if y = X 1 0 ⁡ X = 1
48 47 adantl ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ X ∈ I → y ∈ I ⟼ if y = X 1 0 ⁡ X = 1
49 35 42 15 15 43 44 48 ofval ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ X ∈ I → k + f y ∈ I ⟼ if y = X 1 0 ⁡ X = k ⁡ X + 1
50 7 49 mpidan ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k + f y ∈ I ⟼ if y = X 1 0 ⁡ X = k ⁡ X + 1
51 50 adantr ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ k + f y ∈ I ⟼ if y = X 1 0 = y ∈ I ⟼ if y = Y 1 0 → k + f y ∈ I ⟼ if y = X 1 0 ⁡ X = k ⁡ X + 1
52 eqid ⊢ y ∈ I ⟼ if y = Y 1 0 = y ∈ 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 ∈ ℝ
56 55 a1i ⊢ φ → if X = Y 1 0 ∈ ℝ
57 52 54 7 56 fvmptd3 ⊢ φ → y ∈ I ⟼ if y = Y 1 0 ⁡ X = if X = Y 1 0
58 57 ad2antrr ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ k + f y ∈ I ⟼ if y = X 1 0 = y ∈ I ⟼ if y = Y 1 0 → y ∈ I ⟼ if y = Y 1 0 ⁡ X = if X = Y 1 0
59 33 51 58 3eqtr3d ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ k + f y ∈ I ⟼ if y = X 1 0 = y ∈ I ⟼ if y = Y 1 0 → k ⁡ X + 1 = if X = Y 1 0
60 31 59 breqtrd ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ k + f y ∈ I ⟼ if y = X 1 0 = y ∈ 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 ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ k + f y ∈ I ⟼ if y = X 1 0 = y ∈ I ⟼ if y = Y 1 0 → 1 = if X = Y 1 0
69 68 eqcomd ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ k + f y ∈ I ⟼ if y = X 1 0 = y ∈ 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 ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ k + f y ∈ I ⟼ if y = X 1 0 = y ∈ 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 ∈ I ⟼ if y = X 1 0 = y ∈ I ⟼ if y = Y 1 0
77 76 oveq2d ⊢ X = Y → k + f y ∈ I ⟼ if y = X 1 0 = k + f y ∈ I ⟼ if y = Y 1 0
78 77 eqeq1d ⊢ X = Y → k + f y ∈ I ⟼ if y = X 1 0 = y ∈ I ⟼ if y = Y 1 0 ↔ k + f y ∈ I ⟼ if y = Y 1 0 = y ∈ I ⟼ if y = Y 1 0
79 26 adantl ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k : I ⟶ ℕ 0
80 1nn0 ⊢ 1 ∈ ℕ 0
81 0nn0 ⊢ 0 ∈ ℕ 0
82 80 81 ifcli ⊢ if y = Y 1 0 ∈ ℕ 0
83 82 a1i ⊢ y ∈ I → if y = Y 1 0 ∈ ℕ 0
84 52 83 fmpti ⊢ y ∈ I ⟼ if y = Y 1 0 : I ⟶ ℕ 0
85 84 a1i ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → y ∈ I ⟼ if y = Y 1 0 : I ⟶ ℕ 0
86 nn0cn ⊢ n ∈ ℕ 0 → n ∈ ℂ
87 nn0cn ⊢ m ∈ ℕ 0 → m ∈ ℂ
88 addcom ⊢ n ∈ ℂ ∧ m ∈ ℂ → n + m = m + n
89 88 eqeq1d ⊢ n ∈ ℂ ∧ m ∈ ℂ → n + m = m ↔ m + n = m
90 addid0 ⊢ m ∈ ℂ ∧ n ∈ ℂ → m + n = m ↔ n = 0
91 90 ancoms ⊢ n ∈ ℂ ∧ m ∈ ℂ → m + n = m ↔ n = 0
92 89 91 bitrd ⊢ n ∈ ℂ ∧ m ∈ ℂ → n + m = m ↔ n = 0
93 86 87 92 syl2an ⊢ n ∈ ℕ 0 ∧ m ∈ ℕ 0 → n + m = m ↔ n = 0
94 93 adantl ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ n ∈ ℕ 0 ∧ m ∈ ℕ 0 → n + m = m ↔ n = 0
95 15 79 85 94 caofidlcan ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k + f y ∈ I ⟼ if y = Y 1 0 = y ∈ I ⟼ if y = Y 1 0 ↔ k = I × 0
96 78 95 sylan9bbr ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ X = Y → k + f y ∈ I ⟼ if y = X 1 0 = y ∈ I ⟼ if y = Y 1 0 ↔ k = I × 0
97 73 96 biadanid ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k + f y ∈ I ⟼ if y = X 1 0 = y ∈ I ⟼ if y = Y 1 0 ↔ X = Y ∧ k = I × 0
98 97 biancomd ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k + f y ∈ I ⟼ if y = X 1 0 = y ∈ I ⟼ if y = Y 1 0 ↔ k = I × 0 ∧ X = Y
99 98 ifbid ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → if k + f y ∈ I ⟼ if y = X 1 0 = y ∈ I ⟼ if y = Y 1 0 1 R 0 R = if k = I × 0 ∧ X = Y 1 R 0 R
100 24 99 eqtrd ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → V ⁡ Y ⁡ k + f y ∈ I ⟼ if y = X 1 0 = if k = I × 0 ∧ X = Y 1 R 0 R
101 100 oveq2d ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k ⁡ X + 1 ⋅ R V ⁡ Y ⁡ k + f y ∈ I ⟼ if y = X 1 0 = k ⁡ X + 1 ⋅ R if k = I × 0 ∧ X = Y 1 R 0 R
102 ovif2 ⊢ k ⁡ X + 1 ⋅ R if k = I × 0 ∧ X = Y 1 R 0 R = if k = I × 0 ∧ X = Y k ⁡ X + 1 ⋅ R 1 R k ⁡ X + 1 ⋅ R 0 R
103 fveq1 ⊢ k = I × 0 → k ⁡ X = I × 0 ⁡ X
104 103 oveq1d ⊢ k = I × 0 → k ⁡ X + 1 = I × 0 ⁡ X + 1
105 7 adantr ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → X ∈ I
106 c0ex ⊢ 0 ∈ V
107 106 fvconst2 ⊢ X ∈ I → I × 0 ⁡ X = 0
108 105 107 syl ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → I × 0 ⁡ X = 0
109 108 oveq1d ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → I × 0 ⁡ X + 1 = 0 + 1
110 0p1e1 ⊢ 0 + 1 = 1
111 109 110 eqtrdi ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → I × 0 ⁡ X + 1 = 1
112 104 111 sylan9eqr ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ k = I × 0 → k ⁡ X + 1 = 1
113 112 adantrr ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ k = I × 0 ∧ X = Y → k ⁡ X + 1 = 1
114 113 oveq1d ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ k = I × 0 ∧ X = Y → k ⁡ X + 1 ⋅ R 1 R = 1 ⋅ R 1 R
115 eqid ⊢ Base R = Base R
116 115 14 6 ringidcld ⊢ φ → 1 R ∈ Base R
117 eqid ⊢ ⋅ R = ⋅ R
118 115 117 mulg1 ⊢ 1 R ∈ Base R → 1 ⋅ R 1 R = 1 R
119 116 118 syl ⊢ φ → 1 ⋅ R 1 R = 1 R
120 119 ad2antrr ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ k = I × 0 ∧ X = Y → 1 ⋅ R 1 R = 1 R
121 114 120 eqtrd ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ k = I × 0 ∧ X = Y → k ⁡ X + 1 ⋅ R 1 R = 1 R
122 6 ringgrpd ⊢ φ → R ∈ Grp
123 122 grpmndd ⊢ φ → R ∈ Mnd
124 123 adantr ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → R ∈ Mnd
125 79 105 ffvelcdmd ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k ⁡ X ∈ ℕ 0
126 80 a1i ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → 1 ∈ ℕ 0
127 125 126 nn0addcld ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k ⁡ X + 1 ∈ ℕ 0
128 115 117 13 mulgnn0z ⊢ R ∈ Mnd ∧ k ⁡ X + 1 ∈ ℕ 0 → k ⁡ X + 1 ⋅ R 0 R = 0 R
129 124 127 128 syl2anc ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k ⁡ X + 1 ⋅ R 0 R = 0 R
130 129 adantr ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ ¬ k = I × 0 ∧ X = Y → k ⁡ X + 1 ⋅ R 0 R = 0 R
131 121 130 ifeq12da ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → if k = I × 0 ∧ X = Y k ⁡ X + 1 ⋅ R 1 R k ⁡ X + 1 ⋅ R 0 R = if k = I × 0 ∧ X = Y 1 R 0 R
132 102 131 eqtrid ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k ⁡ X + 1 ⋅ R if k = I × 0 ∧ X = Y 1 R 0 R = if k = I × 0 ∧ X = Y 1 R 0 R
133 ancom ⊢ k = I × 0 ∧ X = Y ↔ X = Y ∧ k = I × 0
134 ifbi ⊢ k = I × 0 ∧ X = Y ↔ X = Y ∧ k = I × 0 → if k = I × 0 ∧ X = Y 1 R 0 R = if X = Y ∧ k = I × 0 1 R 0 R
135 133 134 ax-mp ⊢ if k = I × 0 ∧ X = Y 1 R 0 R = if X = Y ∧ k = I × 0 1 R 0 R
136 ifan ⊢ if X = Y ∧ k = I × 0 1 R 0 R = if X = Y if k = I × 0 1 R 0 R 0 R
137 135 136 eqtri ⊢ if k = I × 0 ∧ X = Y 1 R 0 R = if X = Y if k = I × 0 1 R 0 R 0 R
138 137 a1i ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → if k = I × 0 ∧ X = Y 1 R 0 R = if X = Y if k = I × 0 1 R 0 R 0 R
139 101 132 138 3eqtrd ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k ⁡ X + 1 ⋅ R V ⁡ Y ⁡ k + f y ∈ I ⟼ if y = X 1 0 = if X = Y if k = I × 0 1 R 0 R 0 R
140 139 mpteq2dva ⊢ φ → k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ k ⁡ X + 1 ⋅ R V ⁡ Y ⁡ k + f y ∈ I ⟼ if y = X 1 0 = k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ if X = Y if k = I × 0 1 R 0 R 0 R
141 ifmpt2v ⊢ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ if X = Y if k = I × 0 1 R 0 R 0 R = if X = Y k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ if k = I × 0 1 R 0 R k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ 0 R
142 1 5 6 10 13 14 3 psr1 ⊢ φ → 1 ˙ = k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ if k = I × 0 1 R 0 R
143 1 5 122 10 13 2 psr0 ⊢ φ → 0 ˙ = h ∈ ℕ 0 I | h -1 ℕ ∈ Fin × 0 R
144 fconstmpt ⊢ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin × 0 R = k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ 0 R
145 143 144 eqtrdi ⊢ φ → 0 ˙ = k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ 0 R
146 142 145 ifeq12d ⊢ φ → if X = Y 1 ˙ 0 ˙ = if X = Y k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ if k = I × 0 1 R 0 R k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ 0 R
147 141 146 eqtr4id ⊢ φ → k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ if X = Y if k = I × 0 1 R 0 R 0 R = if X = Y 1 ˙ 0 ˙
148 12 140 147 3eqtrd ⊢ φ → I mPSDer R ⁡ X ⁡ V ⁡ Y = if X = Y 1 ˙ 0 ˙