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