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

Metamath Proof Explorer

Theorem selvply1rhm0

Proof