selvply1rhmlema

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

Metamath Proof Explorer

Theorem selvply1rhmlema

Proof