Theorem selvply1rhmlem1

Description: Lemma for selvply1rhm . (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 )
Assertion	selvply1rhmlem1	⊢ ( 𝜑 → 𝐻 : 𝐵 ⟶ ( Base ‘ 𝑄 ) )

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		fvexd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) → ( Base ‘ 𝑈 ) ∈ V )
10		ovexd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) → ( ℕ0 ↑m 1o ) ∈ V )
11		eqid	⊢ ( { 𝑋 } mPoly 𝑈 ) = ( { 𝑋 } mPoly 𝑈 )
12		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
13		eqid	⊢ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) = ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) )
14		eqid	⊢ { ℎ ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ℎ finSupp 0 }
15	14	psrbasfsupp	⊢ { ℎ ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
16	8	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) → 𝑅 ∈ CRing )
17	7	snssd	⊢ ( 𝜑 → { 𝑋 } ⊆ 𝐼 )
18	17	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) → { 𝑋 } ⊆ 𝐼 )
19		simpr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) → 𝑓 ∈ 𝐵 )
20	2 1 3 11 13 16 18 19	selvcl	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) → ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) ∈ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) )
21	11 12 13 15 20	mplelf	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) → ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) : { ℎ ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ℎ finSupp 0 } ⟶ ( Base ‘ 𝑈 ) )
22	21	adantr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) : { ℎ ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ℎ finSupp 0 } ⟶ ( Base ‘ 𝑈 ) )
23		breq1	⊢ ( ℎ = { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } → ( ℎ finSupp 0 ↔ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } finSupp 0 ) )
24		nn0ex	⊢ ℕ0 ∈ V
25	24	a1i	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ℕ0 ∈ V )
26		snex	⊢ { 𝑋 } ∈ V
27	26	a1i	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { 𝑋 } ∈ V )
28	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → 𝑋 ∈ 𝐼 )
29		simpr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → 𝑛 ∈ ( ℕ0 ↑m 1o ) )
30	29	elmaprd	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → 𝑛 : 1o ⟶ ℕ0 )
31		0lt1o	⊢ ∅ ∈ 1o
32	31	a1i	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ∅ ∈ 1o )
33	30 32	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝑛 ‘ ∅ ) ∈ ℕ0 )
34	28 33	fsnd	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } : { 𝑋 } ⟶ ℕ0 )
35	25 27 34	elmapdd	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∈ ( ℕ0 ↑m { 𝑋 } ) )
36		c0ex	⊢ 0 ∈ V
37	36	a1i	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → 0 ∈ V )
38		snopfsupp	⊢ ( ( 𝑋 ∈ 𝐼 ∧ ( 𝑛 ‘ ∅ ) ∈ ℕ0 ∧ 0 ∈ V ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } finSupp 0 )
39	28 33 37 38	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } finSupp 0 )
40	23 35 39	elrabd	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∈ { ℎ ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ℎ finSupp 0 } )
41	22 40	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ∈ ( Base ‘ 𝑈 ) )
42	41	fmpttd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) → ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) : ( ℕ0 ↑m 1o ) ⟶ ( Base ‘ 𝑈 ) )
43	9 10 42	elmapdd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) → ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) ∈ ( ( Base ‘ 𝑈 ) ↑m ( ℕ0 ↑m 1o ) ) )
44		eqid	⊢ ( 1o mPwSer 𝑈 ) = ( 1o mPwSer 𝑈 )
45		psr1baslem	⊢ ( ℕ0 ↑m 1o ) = { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
46		eqid	⊢ ( Base ‘ ( 1o mPwSer 𝑈 ) ) = ( Base ‘ ( 1o mPwSer 𝑈 ) )
47		1oex	⊢ 1o ∈ V
48	47	a1i	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) → 1o ∈ V )
49	44 12 45 46 48	psrbas	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) → ( Base ‘ ( 1o mPwSer 𝑈 ) ) = ( ( Base ‘ 𝑈 ) ↑m ( ℕ0 ↑m 1o ) ) )
50	43 49	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) → ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) ∈ ( Base ‘ ( 1o mPwSer 𝑈 ) ) )
51	21 40	cofmpt	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) → ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) ∘ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) = ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
52		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
53	11 13 52 20	mplelsfi	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) → ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) finSupp ( 0g ‘ 𝑈 ) )
54	35	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) → ∀ 𝑛 ∈ ( ℕ0 ↑m 1o ) { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∈ ( ℕ0 ↑m { 𝑋 } ) )
55	28	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) ∧ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) → 𝑋 ∈ 𝐼 )
56		fvexd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) ∧ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) → ( 𝑛 ‘ ∅ ) ∈ V )
57		opex	⊢ ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ ∈ V
58	57	sneqr	⊢ ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } → ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ = ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ )
59	58	adantl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) ∧ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) → ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ = ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ )
60		opthg	⊢ ( ( 𝑋 ∈ 𝐼 ∧ ( 𝑛 ‘ ∅ ) ∈ V ) → ( ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ = ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ ↔ ( 𝑋 = 𝑋 ∧ ( 𝑛 ‘ ∅ ) = ( 𝑚 ‘ ∅ ) ) ) )
61	60	simplbda	⊢ ( ( ( 𝑋 ∈ 𝐼 ∧ ( 𝑛 ‘ ∅ ) ∈ V ) ∧ ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ = ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ ) → ( 𝑛 ‘ ∅ ) = ( 𝑚 ‘ ∅ ) )
62	55 56 59 61	syl21anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) ∧ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) → ( 𝑛 ‘ ∅ ) = ( 𝑚 ‘ ∅ ) )
63		0ex	⊢ ∅ ∈ V
64	63	a1i	⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) ∧ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) → ∅ ∈ V )
65		df1o2	⊢ 1o = { ∅ }
66	30	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) ∧ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) → 𝑛 : 1o ⟶ ℕ0 )
67	66	ffnd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) ∧ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) → 𝑛 Fn 1o )
68		simplr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) ∧ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) → 𝑚 ∈ ( ℕ0 ↑m 1o ) )
69	68	elmaprd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) ∧ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) → 𝑚 : 1o ⟶ ℕ0 )
70	69	ffnd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) ∧ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) → 𝑚 Fn 1o )
71	64 65 67 70	fsneq	⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) ∧ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) → ( 𝑛 = 𝑚 ↔ ( 𝑛 ‘ ∅ ) = ( 𝑚 ‘ ∅ ) ) )
72	62 71	mpbird	⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) ∧ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) → 𝑛 = 𝑚 )
73	72	ex	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) → ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } → 𝑛 = 𝑚 ) )
74	73	anasss	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) ) → ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } → 𝑛 = 𝑚 ) )
75	74	ralrimivva	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) → ∀ 𝑛 ∈ ( ℕ0 ↑m 1o ) ∀ 𝑚 ∈ ( ℕ0 ↑m 1o ) ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } → 𝑛 = 𝑚 ) )
76		eqid	⊢ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) = ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } )
77		fveq1	⊢ ( 𝑛 = 𝑚 → ( 𝑛 ‘ ∅ ) = ( 𝑚 ‘ ∅ ) )
78	77	opeq2d	⊢ ( 𝑛 = 𝑚 → ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ = ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ )
79	78	sneqd	⊢ ( 𝑛 = 𝑚 → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } )
80	76 79	f1mpt	⊢ ( ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) : ( ℕ0 ↑m 1o ) –1-1→ ( ℕ0 ↑m { 𝑋 } ) ↔ ( ∀ 𝑛 ∈ ( ℕ0 ↑m 1o ) { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∈ ( ℕ0 ↑m { 𝑋 } ) ∧ ∀ 𝑛 ∈ ( ℕ0 ↑m 1o ) ∀ 𝑚 ∈ ( ℕ0 ↑m 1o ) ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } → 𝑛 = 𝑚 ) ) )
81	54 75 80	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) → ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) : ( ℕ0 ↑m 1o ) –1-1→ ( ℕ0 ↑m { 𝑋 } ) )
82		fvexd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) → ( 0g ‘ 𝑈 ) ∈ V )
83	53 81 82 20	fsuppco	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) → ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) ∘ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) finSupp ( 0g ‘ 𝑈 ) )
84	51 83	eqbrtrrd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) → ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) finSupp ( 0g ‘ 𝑈 ) )
85		eqid	⊢ ( 1o mPoly 𝑈 ) = ( 1o mPoly 𝑈 )
86		eqid	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
87	4 86	ply1bas	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ ( 1o mPoly 𝑈 ) )
88	85 44 46 52 87	mplelbas	⊢ ( ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) ∈ ( Base ‘ 𝑄 ) ↔ ( ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) ∈ ( Base ‘ ( 1o mPwSer 𝑈 ) ) ∧ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) finSupp ( 0g ‘ 𝑈 ) ) )
89	50 84 88	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) → ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) ∈ ( Base ‘ 𝑄 ) )
90	89 5	fmptd	⊢ ( 𝜑 → 𝐻 : 𝐵 ⟶ ( Base ‘ 𝑄 ) )