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 ) )