Theorem selvply1rhm0

Description: The ring homomorphism H built in selvply1rhm is injective. (Contributed by Thierry Arnoux, 4-May-2026)

	Ref	Expression
Hypotheses	selvply1rhm.1	⊢ 𝐵 = ( Base ‘ 𝑃 )
	selvply1rhm.2	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	selvply1rhm.3	⊢ 𝑈 = ( ( 𝐼 ∖ { 𝑋 } ) mPoly 𝑅 )
	selvply1rhm.4	⊢ 𝑄 = ( Poly1 ‘ 𝑈 )
	selvply1rhm.5	⊢ 𝐻 = ( 𝑓 ∈ 𝐵 ↦ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
	selvply1rhm.6	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	selvply1rhm.7	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
	selvply1rhm.8	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	selvply1rhm0.1	⊢ 0 = ( 0g ‘ 𝑄 )
	selvply1rhm0.2	⊢ 𝑍 = ( 0g ‘ 𝑃 )
	selvply1rhm0.3	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	selvply1rhm0.4	⊢ ( 𝜑 → ( 𝐻 ‘ 𝐹 ) = 0 )
Assertion	selvply1rhm0	⊢ ( 𝜑 → 𝐹 = 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		selvply1rhm.1	⊢ 𝐵 = ( Base ‘ 𝑃 )
2		selvply1rhm.2	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
3		selvply1rhm.3	⊢ 𝑈 = ( ( 𝐼 ∖ { 𝑋 } ) mPoly 𝑅 )
4		selvply1rhm.4	⊢ 𝑄 = ( Poly1 ‘ 𝑈 )
5		selvply1rhm.5	⊢ 𝐻 = ( 𝑓 ∈ 𝐵 ↦ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
6		selvply1rhm.6	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
7		selvply1rhm.7	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
8		selvply1rhm.8	⊢ ( 𝜑 → 𝑅 ∈ CRing )
9		selvply1rhm0.1	⊢ 0 = ( 0g ‘ 𝑄 )
10		selvply1rhm0.2	⊢ 𝑍 = ( 0g ‘ 𝑃 )
11		selvply1rhm0.3	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
12		selvply1rhm0.4	⊢ ( 𝜑 → ( 𝐻 ‘ 𝐹 ) = 0 )
13		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
14		eqid	⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
15	14	psrbasfsupp	⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
16	2 13 1 15 11	mplelf	⊢ ( 𝜑 → 𝐹 : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ⟶ ( Base ‘ 𝑅 ) )
17	16	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝐹 ‘ 𝑝 ) ) )
18		nn0ex	⊢ ℕ0 ∈ V
19	18	a1i	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ℕ0 ∈ V )
20		1oex	⊢ 1o ∈ V
21	20	a1i	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 1o ∈ V )
22		df1o2	⊢ 1o = { ∅ }
23	22	eqcomi	⊢ { ∅ } = 1o
24	23	a1i	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → { ∅ } = 1o )
25		0ex	⊢ ∅ ∈ V
26	25	a1i	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ∅ ∈ V )
27		ssrab2	⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ⊆ ( ℕ0 ↑m 𝐼 )
28	27	a1i	⊢ ( 𝜑 → { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ⊆ ( ℕ0 ↑m 𝐼 ) )
29	28	sselda	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑝 ∈ ( ℕ0 ↑m 𝐼 ) )
30	29	elmaprd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑝 : 𝐼 ⟶ ℕ0 )
31	7	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑋 ∈ 𝐼 )
32	30 31	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑝 ‘ 𝑋 ) ∈ ℕ0 )
33	26 32	fsnd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → { ⟨ ∅ , ( 𝑝 ‘ 𝑋 ) ⟩ } : { ∅ } ⟶ ℕ0 )
34	24 33	feq2dd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → { ⟨ ∅ , ( 𝑝 ‘ 𝑋 ) ⟩ } : 1o ⟶ ℕ0 )
35	19 21 34	elmapdd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → { ⟨ ∅ , ( 𝑝 ‘ 𝑋 ) ⟩ } ∈ ( ℕ0 ↑m 1o ) )
36		psr1baslem	⊢ ( ℕ0 ↑m 1o ) = { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
37		eqid	⊢ { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ℎ finSupp 0 }
38	37	psrbasfsupp	⊢ { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
39	36 38	eqtr4i	⊢ ( ℕ0 ↑m 1o ) = { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ℎ finSupp 0 }
40	35 39	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → { ⟨ ∅ , ( 𝑝 ‘ 𝑋 ) ⟩ } ∈ { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ℎ finSupp 0 } )
41		fvex	⊢ ( 0g ‘ 𝑈 ) ∈ V
42	41	fvconst2	⊢ ( { ⟨ ∅ , ( 𝑝 ‘ 𝑋 ) ⟩ } ∈ { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ℎ finSupp 0 } → ( ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ℎ finSupp 0 } × { ( 0g ‘ 𝑈 ) } ) ‘ { ⟨ ∅ , ( 𝑝 ‘ 𝑋 ) ⟩ } ) = ( 0g ‘ 𝑈 ) )
43	40 42	syl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ℎ finSupp 0 } × { ( 0g ‘ 𝑈 ) } ) ‘ { ⟨ ∅ , ( 𝑝 ‘ 𝑋 ) ⟩ } ) = ( 0g ‘ 𝑈 ) )
44	30	ffnd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑝 Fn 𝐼 )
45		fnressn	⊢ ( ( 𝑝 Fn 𝐼 ∧ 𝑋 ∈ 𝐼 ) → ( 𝑝 ↾ { 𝑋 } ) = { ⟨ 𝑋 , ( 𝑝 ‘ 𝑋 ) ⟩ } )
46	44 31 45	syl2anc	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑝 ↾ { 𝑋 } ) = { ⟨ 𝑋 , ( 𝑝 ‘ 𝑋 ) ⟩ } )
47		fvex	⊢ ( 𝑝 ‘ 𝑋 ) ∈ V
48	25 47	fvsn	⊢ ( { ⟨ ∅ , ( 𝑝 ‘ 𝑋 ) ⟩ } ‘ ∅ ) = ( 𝑝 ‘ 𝑋 )
49	48	opeq2i	⊢ ⟨ 𝑋 , ( { ⟨ ∅ , ( 𝑝 ‘ 𝑋 ) ⟩ } ‘ ∅ ) ⟩ = ⟨ 𝑋 , ( 𝑝 ‘ 𝑋 ) ⟩
50	49	sneqi	⊢ { ⟨ 𝑋 , ( { ⟨ ∅ , ( 𝑝 ‘ 𝑋 ) ⟩ } ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑝 ‘ 𝑋 ) ⟩ }
51	46 50	eqtr4di	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑝 ↾ { 𝑋 } ) = { ⟨ 𝑋 , ( { ⟨ ∅ , ( 𝑝 ‘ 𝑋 ) ⟩ } ‘ ∅ ) ⟩ } )
52	51	fveq2d	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ ( 𝑝 ↾ { 𝑋 } ) ) = ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ { ⟨ 𝑋 , ( { ⟨ ∅ , ( 𝑝 ‘ 𝑋 ) ⟩ } ‘ ∅ ) ⟩ } ) )
53	6	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝐼 ∈ 𝑉 )
54	8	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑅 ∈ CRing )
55	11	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝐹 ∈ 𝐵 )
56	1 2 3 4 5 53 31 54 55 35	selvply1rhmlem3	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( ( 𝐻 ‘ 𝐹 ) ‘ { ⟨ ∅ , ( 𝑝 ‘ 𝑋 ) ⟩ } ) = ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ { ⟨ 𝑋 , ( { ⟨ ∅ , ( 𝑝 ‘ 𝑋 ) ⟩ } ‘ ∅ ) ⟩ } ) )
57		eqid	⊢ ( 1o mPoly 𝑈 ) = ( 1o mPoly 𝑈 )
58		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
59	57 4 9	ply1mpl0	⊢ 0 = ( 0g ‘ ( 1o mPoly 𝑈 ) )
60	20	a1i	⊢ ( 𝜑 → 1o ∈ V )
61	6	difexd	⊢ ( 𝜑 → ( 𝐼 ∖ { 𝑋 } ) ∈ V )
62	8	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
63	3 61 62	mplringd	⊢ ( 𝜑 → 𝑈 ∈ Ring )
64	63	ringgrpd	⊢ ( 𝜑 → 𝑈 ∈ Grp )
65	57 38 58 59 60 64	mpl0	⊢ ( 𝜑 → 0 = ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ℎ finSupp 0 } × { ( 0g ‘ 𝑈 ) } ) )
66	12 65	eqtrd	⊢ ( 𝜑 → ( 𝐻 ‘ 𝐹 ) = ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ℎ finSupp 0 } × { ( 0g ‘ 𝑈 ) } ) )
67	66	fveq1d	⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝐹 ) ‘ { ⟨ ∅ , ( 𝑝 ‘ 𝑋 ) ⟩ } ) = ( ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ℎ finSupp 0 } × { ( 0g ‘ 𝑈 ) } ) ‘ { ⟨ ∅ , ( 𝑝 ‘ 𝑋 ) ⟩ } ) )
68	67	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( ( 𝐻 ‘ 𝐹 ) ‘ { ⟨ ∅ , ( 𝑝 ‘ 𝑋 ) ⟩ } ) = ( ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ℎ finSupp 0 } × { ( 0g ‘ 𝑈 ) } ) ‘ { ⟨ ∅ , ( 𝑝 ‘ 𝑋 ) ⟩ } ) )
69	52 56 68	3eqtr2rd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ℎ finSupp 0 } × { ( 0g ‘ 𝑈 ) } ) ‘ { ⟨ ∅ , ( 𝑝 ‘ 𝑋 ) ⟩ } ) = ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ ( 𝑝 ↾ { 𝑋 } ) ) )
70		eqid	⊢ { ℎ ∈ ( ℕ0 ↑m ( 𝐼 ∖ { 𝑋 } ) ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m ( 𝐼 ∖ { 𝑋 } ) ) ∣ ℎ finSupp 0 }
71	70	psrbasfsupp	⊢ { ℎ ∈ ( ℕ0 ↑m ( 𝐼 ∖ { 𝑋 } ) ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m ( 𝐼 ∖ { 𝑋 } ) ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
72		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
73	61	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝐼 ∖ { 𝑋 } ) ∈ V )
74	62	ringgrpd	⊢ ( 𝜑 → 𝑅 ∈ Grp )
75	74	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑅 ∈ Grp )
76	3 71 72 58 73 75	mpl0	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 0g ‘ 𝑈 ) = ( { ℎ ∈ ( ℕ0 ↑m ( 𝐼 ∖ { 𝑋 } ) ) ∣ ℎ finSupp 0 } × { ( 0g ‘ 𝑅 ) } ) )
77	43 69 76	3eqtr3d	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ ( 𝑝 ↾ { 𝑋 } ) ) = ( { ℎ ∈ ( ℕ0 ↑m ( 𝐼 ∖ { 𝑋 } ) ) ∣ ℎ finSupp 0 } × { ( 0g ‘ 𝑅 ) } ) )
78	77	fveq1d	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ ( 𝑝 ↾ { 𝑋 } ) ) ‘ ( 𝑝 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) = ( ( { ℎ ∈ ( ℕ0 ↑m ( 𝐼 ∖ { 𝑋 } ) ) ∣ ℎ finSupp 0 } × { ( 0g ‘ 𝑅 ) } ) ‘ ( 𝑝 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) )
79	7	snssd	⊢ ( 𝜑 → { 𝑋 } ⊆ 𝐼 )
80	79	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → { 𝑋 } ⊆ 𝐼 )
81		simpr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
82	15 2 1 54 80 55 81	selvvvval	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ ( 𝑝 ↾ { 𝑋 } ) ) ‘ ( 𝑝 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) = ( 𝐹 ‘ 𝑝 ) )
83		breq1	⊢ ( ℎ = ( 𝑝 ↾ ( 𝐼 ∖ { 𝑋 } ) ) → ( ℎ finSupp 0 ↔ ( 𝑝 ↾ ( 𝐼 ∖ { 𝑋 } ) ) finSupp 0 ) )
84		difssd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝐼 ∖ { 𝑋 } ) ⊆ 𝐼 )
85	29 84	elmapssresd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑝 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ∈ ( ℕ0 ↑m ( 𝐼 ∖ { 𝑋 } ) ) )
86		breq1	⊢ ( ℎ = 𝑝 → ( ℎ finSupp 0 ↔ 𝑝 finSupp 0 ) )
87	86 81	elrabrd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑝 finSupp 0 )
88		c0ex	⊢ 0 ∈ V
89	88	a1i	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 0 ∈ V )
90	87 89	fsuppres	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑝 ↾ ( 𝐼 ∖ { 𝑋 } ) ) finSupp 0 )
91	83 85 90	elrabd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑝 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ∈ { ℎ ∈ ( ℕ0 ↑m ( 𝐼 ∖ { 𝑋 } ) ) ∣ ℎ finSupp 0 } )
92		fvex	⊢ ( 0g ‘ 𝑅 ) ∈ V
93	92	fvconst2	⊢ ( ( 𝑝 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ∈ { ℎ ∈ ( ℕ0 ↑m ( 𝐼 ∖ { 𝑋 } ) ) ∣ ℎ finSupp 0 } → ( ( { ℎ ∈ ( ℕ0 ↑m ( 𝐼 ∖ { 𝑋 } ) ) ∣ ℎ finSupp 0 } × { ( 0g ‘ 𝑅 ) } ) ‘ ( 𝑝 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) = ( 0g ‘ 𝑅 ) )
94	91 93	syl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( ( { ℎ ∈ ( ℕ0 ↑m ( 𝐼 ∖ { 𝑋 } ) ) ∣ ℎ finSupp 0 } × { ( 0g ‘ 𝑅 ) } ) ‘ ( 𝑝 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) = ( 0g ‘ 𝑅 ) )
95	78 82 94	3eqtr3d	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝐹 ‘ 𝑝 ) = ( 0g ‘ 𝑅 ) )
96	95	mpteq2dva	⊢ ( 𝜑 → ( 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝐹 ‘ 𝑝 ) ) = ( 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 0g ‘ 𝑅 ) ) )
97	2 15 72 10 6 74	mpl0	⊢ ( 𝜑 → 𝑍 = ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } × { ( 0g ‘ 𝑅 ) } ) )
98		fconstmpt	⊢ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } × { ( 0g ‘ 𝑅 ) } ) = ( 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 0g ‘ 𝑅 ) )
99	97 98	eqtr2di	⊢ ( 𝜑 → ( 𝑝 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 0g ‘ 𝑅 ) ) = 𝑍 )
100	17 96 99	3eqtrd	⊢ ( 𝜑 → 𝐹 = 𝑍 )