Theorem selvply1rhmlema

Description: Lemma for selvply1rhm . (Contributed by Thierry Arnoux, 4-May-2026)

	Ref	Expression
Hypotheses	selvply1rhmlema.1	⊢ 𝐵 = ( Base ‘ 𝑃 )
	selvply1rhmlema.2	⊢ 𝑃 = ( { 𝑋 } mPoly 𝑅 )
	selvply1rhmlema.3	⊢ · = ( .r ‘ 𝑃 )
	selvply1rhmlema.4	⊢ × = ( .r ‘ 𝑄 )
	selvply1rhmlema.5	⊢ 𝑄 = ( Poly1 ‘ 𝑅 )
	selvply1rhmlema.6	⊢ 𝑀 = ( 𝑓 ∈ 𝐵 ↦ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑓 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
	selvply1rhmlema.7	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	selvply1rhmlema.8	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	selvply1rhmlema.9	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
Assertion	selvply1rhmlema	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐹 ) ∈ ( Base ‘ 𝑄 ) )

Proof

Step	Hyp	Ref	Expression
1		selvply1rhmlema.1	⊢ 𝐵 = ( Base ‘ 𝑃 )
2		selvply1rhmlema.2	⊢ 𝑃 = ( { 𝑋 } mPoly 𝑅 )
3		selvply1rhmlema.3	⊢ · = ( .r ‘ 𝑃 )
4		selvply1rhmlema.4	⊢ × = ( .r ‘ 𝑄 )
5		selvply1rhmlema.5	⊢ 𝑄 = ( Poly1 ‘ 𝑅 )
6		selvply1rhmlema.6	⊢ 𝑀 = ( 𝑓 ∈ 𝐵 ↦ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑓 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
7		selvply1rhmlema.7	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
8		selvply1rhmlema.8	⊢ ( 𝜑 → 𝑅 ∈ Ring )
9		selvply1rhmlema.9	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
10		fvexd	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) ∈ V )
11		ovexd	⊢ ( 𝜑 → ( ℕ0 ↑m 1o ) ∈ V )
12		fvexd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝐹 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ∈ V )
13		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) = ( 𝐹 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) )
14	13	mpteq2dv	⊢ ( 𝑓 = 𝐹 → ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑓 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) = ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝐹 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
15	11	mptexd	⊢ ( 𝜑 → ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝐹 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) ∈ V )
16	6 14 9 15	fvmptd3	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐹 ) = ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝐹 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
17		fveq1	⊢ ( 𝑛 = 𝑚 → ( 𝑛 ‘ ∅ ) = ( 𝑚 ‘ ∅ ) )
18	17	opeq2d	⊢ ( 𝑛 = 𝑚 → ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ = ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ )
19	18	sneqd	⊢ ( 𝑛 = 𝑚 → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } )
20	19	fveq2d	⊢ ( 𝑛 = 𝑚 → ( 𝐹 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) = ( 𝐹 ‘ { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) )
21	16	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝑀 ‘ 𝐹 ) = ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝐹 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
22		simpr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) → 𝑚 ∈ ( ℕ0 ↑m 1o ) )
23		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
24		eqid	⊢ { ℎ ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ℎ finSupp 0 }
25	24	psrbasfsupp	⊢ { ℎ ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
26	9	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) → 𝐹 ∈ 𝐵 )
27	2 23 1 25 26	mplelf	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) → 𝐹 : { ℎ ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ℎ finSupp 0 } ⟶ ( Base ‘ 𝑅 ) )
28		breq1	⊢ ( ℎ = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } → ( ℎ finSupp 0 ↔ { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } finSupp 0 ) )
29		nn0ex	⊢ ℕ0 ∈ V
30	29	a1i	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) → ℕ0 ∈ V )
31		snex	⊢ { 𝑋 } ∈ V
32	31	a1i	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) → { 𝑋 } ∈ V )
33	7	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) → 𝑋 ∈ 𝑉 )
34	22	elmaprd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) → 𝑚 : 1o ⟶ ℕ0 )
35		0lt1o	⊢ ∅ ∈ 1o
36	35	a1i	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) → ∅ ∈ 1o )
37	34 36	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝑚 ‘ ∅ ) ∈ ℕ0 )
38	33 37	fsnd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) → { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } : { 𝑋 } ⟶ ℕ0 )
39	30 32 38	elmapdd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) → { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ∈ ( ℕ0 ↑m { 𝑋 } ) )
40		snfi	⊢ { 𝑋 } ∈ Fin
41	40	a1i	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) → { 𝑋 } ∈ Fin )
42		c0ex	⊢ 0 ∈ V
43	42	a1i	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) → 0 ∈ V )
44	38 41 43	fdmfifsupp	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) → { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } finSupp 0 )
45	28 39 44	elrabd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) → { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ∈ { ℎ ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ℎ finSupp 0 } )
46	27 45	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝐹 ‘ { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) ∈ ( Base ‘ 𝑅 ) )
47	20 21 22 46	fvmptd4	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) → ( ( 𝑀 ‘ 𝐹 ) ‘ 𝑚 ) = ( 𝐹 ‘ { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) )
48	47 46	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) → ( ( 𝑀 ‘ 𝐹 ) ‘ 𝑚 ) ∈ ( Base ‘ 𝑅 ) )
49	12 16 48	fmpt2d	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐹 ) : ( ℕ0 ↑m 1o ) ⟶ ( Base ‘ 𝑅 ) )
50	10 11 49	elmapdd	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐹 ) ∈ ( ( Base ‘ 𝑅 ) ↑m ( ℕ0 ↑m 1o ) ) )
51		eqid	⊢ ( 1o mPwSer 𝑅 ) = ( 1o mPwSer 𝑅 )
52		psr1baslem	⊢ ( ℕ0 ↑m 1o ) = { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
53		eqid	⊢ ( Base ‘ ( 1o mPwSer 𝑅 ) ) = ( Base ‘ ( 1o mPwSer 𝑅 ) )
54		1oex	⊢ 1o ∈ V
55	54	a1i	⊢ ( 𝜑 → 1o ∈ V )
56	51 23 52 53 55	psrbas	⊢ ( 𝜑 → ( Base ‘ ( 1o mPwSer 𝑅 ) ) = ( ( Base ‘ 𝑅 ) ↑m ( ℕ0 ↑m 1o ) ) )
57	50 56	eleqtrrd	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐹 ) ∈ ( Base ‘ ( 1o mPwSer 𝑅 ) ) )
58	2 23 1 25 9	mplelf	⊢ ( 𝜑 → 𝐹 : { ℎ ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ℎ finSupp 0 } ⟶ ( Base ‘ 𝑅 ) )
59		breq1	⊢ ( ℎ = { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } → ( ℎ finSupp 0 ↔ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } finSupp 0 ) )
60	29	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ℕ0 ∈ V )
61	31	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { 𝑋 } ∈ V )
62	7	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → 𝑋 ∈ 𝑉 )
63		simpr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → 𝑛 ∈ ( ℕ0 ↑m 1o ) )
64	63	elmaprd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → 𝑛 : 1o ⟶ ℕ0 )
65	35	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ∅ ∈ 1o )
66	64 65	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝑛 ‘ ∅ ) ∈ ℕ0 )
67	62 66	fsnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } : { 𝑋 } ⟶ ℕ0 )
68	60 61 67	elmapdd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∈ ( ℕ0 ↑m { 𝑋 } ) )
69	40	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { 𝑋 } ∈ Fin )
70	42	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → 0 ∈ V )
71	67 69 70	fdmfifsupp	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } finSupp 0 )
72	59 68 71	elrabd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∈ { ℎ ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ℎ finSupp 0 } )
73	58 72	cofmpt	⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) = ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝐹 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
74		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
75	2 1 74 9	mplelsfi	⊢ ( 𝜑 → 𝐹 finSupp ( 0g ‘ 𝑅 ) )
76	68	ralrimiva	⊢ ( 𝜑 → ∀ 𝑛 ∈ ( ℕ0 ↑m 1o ) { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∈ ( ℕ0 ↑m { 𝑋 } ) )
77	62	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) ∧ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) → 𝑋 ∈ 𝑉 )
78		fvexd	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) ∧ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) → ( 𝑛 ‘ ∅ ) ∈ V )
79		opex	⊢ ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ ∈ V
80	79	sneqr	⊢ ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } → ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ = ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ )
81	80	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) ∧ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) → ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ = ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ )
82		opthg	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑛 ‘ ∅ ) ∈ V ) → ( ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ = ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ ↔ ( 𝑋 = 𝑋 ∧ ( 𝑛 ‘ ∅ ) = ( 𝑚 ‘ ∅ ) ) ) )
83	82	simplbda	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑛 ‘ ∅ ) ∈ V ) ∧ ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ = ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ ) → ( 𝑛 ‘ ∅ ) = ( 𝑚 ‘ ∅ ) )
84	77 78 81 83	syl21anc	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) ∧ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) → ( 𝑛 ‘ ∅ ) = ( 𝑚 ‘ ∅ ) )
85		0ex	⊢ ∅ ∈ V
86	85	a1i	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) ∧ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) → ∅ ∈ V )
87		df1o2	⊢ 1o = { ∅ }
88	64	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) ∧ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) → 𝑛 : 1o ⟶ ℕ0 )
89	88	ffnd	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) ∧ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) → 𝑛 Fn 1o )
90	34	ad4ant13	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) ∧ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) → 𝑚 : 1o ⟶ ℕ0 )
91	90	ffnd	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) ∧ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) → 𝑚 Fn 1o )
92	86 87 89 91	fsneq	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) ∧ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) → ( 𝑛 = 𝑚 ↔ ( 𝑛 ‘ ∅ ) = ( 𝑚 ‘ ∅ ) ) )
93	84 92	mpbird	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) ∧ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) → 𝑛 = 𝑚 )
94	93	ex	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) → ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } → 𝑛 = 𝑚 ) )
95	94	anasss	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ∧ 𝑚 ∈ ( ℕ0 ↑m 1o ) ) ) → ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } → 𝑛 = 𝑚 ) )
96	95	ralrimivva	⊢ ( 𝜑 → ∀ 𝑛 ∈ ( ℕ0 ↑m 1o ) ∀ 𝑚 ∈ ( ℕ0 ↑m 1o ) ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } → 𝑛 = 𝑚 ) )
97		eqid	⊢ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) = ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } )
98	97 19	f1mpt	⊢ ( ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) : ( ℕ0 ↑m 1o ) –1-1→ ( ℕ0 ↑m { 𝑋 } ) ↔ ( ∀ 𝑛 ∈ ( ℕ0 ↑m 1o ) { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∈ ( ℕ0 ↑m { 𝑋 } ) ∧ ∀ 𝑛 ∈ ( ℕ0 ↑m 1o ) ∀ 𝑚 ∈ ( ℕ0 ↑m 1o ) ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } → 𝑛 = 𝑚 ) ) )
99	76 96 98	sylanbrc	⊢ ( 𝜑 → ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) : ( ℕ0 ↑m 1o ) –1-1→ ( ℕ0 ↑m { 𝑋 } ) )
100		fvexd	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ V )
101	75 99 100 9	fsuppco	⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) finSupp ( 0g ‘ 𝑅 ) )
102	73 101	eqbrtrrd	⊢ ( 𝜑 → ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝐹 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) finSupp ( 0g ‘ 𝑅 ) )
103	16 102	eqbrtrd	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐹 ) finSupp ( 0g ‘ 𝑅 ) )
104		eqid	⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
105		eqid	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
106	5 105	ply1bas	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
107	104 51 53 74 106	mplelbas	⊢ ( ( 𝑀 ‘ 𝐹 ) ∈ ( Base ‘ 𝑄 ) ↔ ( ( 𝑀 ‘ 𝐹 ) ∈ ( Base ‘ ( 1o mPwSer 𝑅 ) ) ∧ ( 𝑀 ‘ 𝐹 ) finSupp ( 0g ‘ 𝑅 ) ) )
108	57 103 107	sylanbrc	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐹 ) ∈ ( Base ‘ 𝑄 ) )