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 ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
psdmvr.z ⊢ 0 = ( 0g ‘ 𝑆 )
psdmvr.o ⊢ 1 = ( 1r ‘ 𝑆 )
psdmvr.v ⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
psdmvr.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
psdmvr.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
psdmvr.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
psdmvr.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐼 )
Assertion psdmvr ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ ( 𝑉 ‘ 𝑌 ) ) = if ( 𝑋 = 𝑌 , 1 , 0 ) )

Proof

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