Theorem selvply1rhm0 33882

Description: The ring homomorphism 𝐻 built in selvply1rhm 33881 is injective. (Contributed by Thierry Arnoux, 4-May-2026.)

Hypotheses

Ref	Expression
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)
selvply1rhm0.1	⊢ 0 = (0g‘𝑄)
selvply1rhm0.2	⊢ 𝑍 = (0g‘𝑃)
selvply1rhm0.3	⊢ (𝜑 → 𝐹 ∈ 𝐵)
selvply1rhm0.4	⊢ (𝜑 → (𝐻‘𝐹) = 0 )

Assertion

Ref	Expression
selvply1rhm0	⊢ (𝜑 → 𝐹 = 𝑍)

Distinct variable groups:   𝐵,𝑓,𝑛   𝑛,𝐻   𝑓,𝐼,𝑛   𝑃,𝑓,𝑛   𝑄,𝑓,𝑛   𝑅,𝑓,𝑛   𝑈,𝑓,𝑛   𝑓,𝑋,𝑛   𝜑,𝑓,𝑛   𝑓,𝐹,𝑛

Allowed substitution hints:   𝐻(𝑓)   𝑉(𝑓,𝑛)   0 (𝑓,𝑛)   𝑍(𝑓,𝑛)

Proof of Theorem selvply1rhm0

Dummy variables ℎ 𝑝 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		selvply1rhm.2	. . . 4 ⊢ 𝑃 = (𝐼 mPoly 𝑅)
2		eqid 2761	. . . 4 ⊢ (Base‘𝑅) = (Base‘𝑅)
3		selvply1rhm.1	. . . 4 ⊢ 𝐵 = (Base‘𝑃)
4		eqid 2761	. . . . 5 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}
5	4	psrbasfsupp 33867	. . . 4 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}
6		selvply1rhm0.3	. . . 4 ⊢ (𝜑 → 𝐹 ∈ 𝐵)
7	1, 2, 3, 5, 6	mplelf 22126	. . 3 ⊢ (𝜑 → 𝐹:{ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}⟶(Base‘𝑅))
8	7	feqmptd 6949	. 2 ⊢ (𝜑 → 𝐹 = (𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝐹‘𝑝)))
9		nn0ex 12509	. . . . . . . . . 10 ⊢ ℕ0 ∈ V
10	9	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → ℕ0 ∈ V)
11		1oex 8462	. . . . . . . . . 10 ⊢ 1o ∈ V
12	11	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 1o ∈ V)
13		df1o2 8459	. . . . . . . . . . . 12 ⊢ 1o = {∅}
14	13	eqcomi 2770	. . . . . . . . . . 11 ⊢ {∅} = 1o
15	14	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → {∅} = 1o)
16		0ex 5269	. . . . . . . . . . . 12 ⊢ ∅ ∈ V
17	16	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → ∅ ∈ V)
18		selvply1rhm.6	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
19	18	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝐼 ∈ 𝑉)
20		ssrab2 4033	. . . . . . . . . . . . . . 15 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ⊆ (ℕ0 ↑m 𝐼)
21	20	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ⊆ (ℕ0 ↑m 𝐼))
22	21	sselda 3936	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑝 ∈ (ℕ0 ↑m 𝐼))
23	19, 10, 22	elmaprd 32991	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑝:𝐼⟶ℕ0)
24		selvply1rhm.7	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋 ∈ 𝐼)
25	24	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑋 ∈ 𝐼)
26	23, 25	ffvelcdmd 7080	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑝‘𝑋) ∈ ℕ0)
27	17, 26	fsnd 6865	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → {⟨∅, (𝑝‘𝑋)⟩}:{∅}⟶ℕ0)
28	15, 27	feq2dd 6691	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → {⟨∅, (𝑝‘𝑋)⟩}:1o⟶ℕ0)
29	10, 12, 28	elmapdd 8837	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → {⟨∅, (𝑝‘𝑋)⟩} ∈ (ℕ0 ↑m 1o))
30		psr1baslem 22324	. . . . . . . . 9 ⊢ (ℕ0 ↑m 1o) = {ℎ ∈ (ℕ0 ↑m 1o) ∣ (◡ℎ “ ℕ) ∈ Fin}
31		eqid 2761	. . . . . . . . . 10 ⊢ {ℎ ∈ (ℕ0 ↑m 1o) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ0 ↑m 1o) ∣ ℎ finSupp 0}
32	31	psrbasfsupp 33867	. . . . . . . . 9 ⊢ {ℎ ∈ (ℕ0 ↑m 1o) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ0 ↑m 1o) ∣ (◡ℎ “ ℕ) ∈ Fin}
33	30, 32	eqtr4i 2787	. . . . . . . 8 ⊢ (ℕ0 ↑m 1o) = {ℎ ∈ (ℕ0 ↑m 1o) ∣ ℎ finSupp 0}
34	29, 33	eleqtrdi 2871	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → {⟨∅, (𝑝‘𝑋)⟩} ∈ {ℎ ∈ (ℕ0 ↑m 1o) ∣ ℎ finSupp 0})
35		fvex 6894	. . . . . . . 8 ⊢ (0g‘𝑈) ∈ V
36	35	fvconst2 7202	. . . . . . 7 ⊢ ({⟨∅, (𝑝‘𝑋)⟩} ∈ {ℎ ∈ (ℕ0 ↑m 1o) ∣ ℎ finSupp 0} → (({ℎ ∈ (ℕ0 ↑m 1o) ∣ ℎ finSupp 0} × {(0g‘𝑈)})‘{⟨∅, (𝑝‘𝑋)⟩}) = (0g‘𝑈))
37	34, 36	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (({ℎ ∈ (ℕ0 ↑m 1o) ∣ ℎ finSupp 0} × {(0g‘𝑈)})‘{⟨∅, (𝑝‘𝑋)⟩}) = (0g‘𝑈))
38	23	ffnd 6706	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑝 Fn 𝐼)
39		fnressn 7155	. . . . . . . . . 10 ⊢ ((𝑝 Fn 𝐼 ∧ 𝑋 ∈ 𝐼) → (𝑝 ↾ {𝑋}) = {⟨𝑋, (𝑝‘𝑋)⟩})
40	38, 25, 39	syl2anc 595	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑝 ↾ {𝑋}) = {⟨𝑋, (𝑝‘𝑋)⟩})
41		fvex 6894	. . . . . . . . . . . 12 ⊢ (𝑝‘𝑋) ∈ V
42	16, 41	fvsn 7179	. . . . . . . . . . 11 ⊢ ({⟨∅, (𝑝‘𝑋)⟩}‘∅) = (𝑝‘𝑋)
43	42	opeq2i 4841	. . . . . . . . . 10 ⊢ ⟨𝑋, ({⟨∅, (𝑝‘𝑋)⟩}‘∅)⟩ = ⟨𝑋, (𝑝‘𝑋)⟩
44	43	sneqi 4599	. . . . . . . . 9 ⊢ {⟨𝑋, ({⟨∅, (𝑝‘𝑋)⟩}‘∅)⟩} = {⟨𝑋, (𝑝‘𝑋)⟩}
45	40, 44	eqtr4di 2814	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑝 ↾ {𝑋}) = {⟨𝑋, ({⟨∅, (𝑝‘𝑋)⟩}‘∅)⟩})
46	45	fveq2d 6885	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → ((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹)‘(𝑝 ↾ {𝑋})) = ((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹)‘{⟨𝑋, ({⟨∅, (𝑝‘𝑋)⟩}‘∅)⟩}))
47		selvply1rhm.3	. . . . . . . 8 ⊢ 𝑈 = ((𝐼 ∖ {𝑋}) mPoly 𝑅)
48		selvply1rhm.4	. . . . . . . 8 ⊢ 𝑄 = (Poly1‘𝑈)
49		selvply1rhm.5	. . . . . . . 8 ⊢ 𝐻 = (𝑓 ∈ 𝐵 ↦ (𝑛 ∈ (ℕ0 ↑m 1o) ↦ ((((𝐼 selectVars 𝑅)‘{𝑋})‘𝑓)‘{⟨𝑋, (𝑛‘∅)⟩})))
50		selvply1rhm.8	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ CRing)
51	50	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑅 ∈ CRing)
52	6	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝐹 ∈ 𝐵)
53	3, 1, 47, 48, 49, 19, 25, 51, 52, 29	selvply1rhmlem3 33878	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → ((𝐻‘𝐹)‘{⟨∅, (𝑝‘𝑋)⟩}) = ((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹)‘{⟨𝑋, ({⟨∅, (𝑝‘𝑋)⟩}‘∅)⟩}))
54		selvply1rhm0.4	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻‘𝐹) = 0 )
55		eqid 2761	. . . . . . . . . . 11 ⊢ (1o mPoly 𝑈) = (1o mPoly 𝑈)
56		eqid 2761	. . . . . . . . . . 11 ⊢ (0g‘𝑈) = (0g‘𝑈)
57		selvply1rhm0.1	. . . . . . . . . . . 12 ⊢ 0 = (0g‘𝑄)
58	55, 48, 57	ply1mpl0 22395	. . . . . . . . . . 11 ⊢ 0 = (0g‘(1o mPoly 𝑈))
59	11	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 1o ∈ V)
60	18	difexd 5301	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐼 ∖ {𝑋}) ∈ V)
61	50	crngringd 20327	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 ∈ Ring)
62	47, 60, 61	mplringd 22151	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ Ring)
63	62	ringgrpd 20323	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ∈ Grp)
64	55, 32, 56, 58, 59, 63	mpl0 22134	. . . . . . . . . 10 ⊢ (𝜑 → 0 = ({ℎ ∈ (ℕ0 ↑m 1o) ∣ ℎ finSupp 0} × {(0g‘𝑈)}))
65	54, 64	eqtrd 2796	. . . . . . . . 9 ⊢ (𝜑 → (𝐻‘𝐹) = ({ℎ ∈ (ℕ0 ↑m 1o) ∣ ℎ finSupp 0} × {(0g‘𝑈)}))
66	65	fveq1d 6883	. . . . . . . 8 ⊢ (𝜑 → ((𝐻‘𝐹)‘{⟨∅, (𝑝‘𝑋)⟩}) = (({ℎ ∈ (ℕ0 ↑m 1o) ∣ ℎ finSupp 0} × {(0g‘𝑈)})‘{⟨∅, (𝑝‘𝑋)⟩}))
67	66	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → ((𝐻‘𝐹)‘{⟨∅, (𝑝‘𝑋)⟩}) = (({ℎ ∈ (ℕ0 ↑m 1o) ∣ ℎ finSupp 0} × {(0g‘𝑈)})‘{⟨∅, (𝑝‘𝑋)⟩}))
68	46, 53, 67	3eqtr2rd 2803	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (({ℎ ∈ (ℕ0 ↑m 1o) ∣ ℎ finSupp 0} × {(0g‘𝑈)})‘{⟨∅, (𝑝‘𝑋)⟩}) = ((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹)‘(𝑝 ↾ {𝑋})))
69		eqid 2761	. . . . . . . 8 ⊢ {ℎ ∈ (ℕ0 ↑m (𝐼 ∖ {𝑋})) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ0 ↑m (𝐼 ∖ {𝑋})) ∣ ℎ finSupp 0}
70	69	psrbasfsupp 33867	. . . . . . 7 ⊢ {ℎ ∈ (ℕ0 ↑m (𝐼 ∖ {𝑋})) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ0 ↑m (𝐼 ∖ {𝑋})) ∣ (◡ℎ “ ℕ) ∈ Fin}
71		eqid 2761	. . . . . . 7 ⊢ (0g‘𝑅) = (0g‘𝑅)
72	60	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝐼 ∖ {𝑋}) ∈ V)
73	61	ringgrpd 20323	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ Grp)
74	73	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑅 ∈ Grp)
75	47, 70, 71, 56, 72, 74	mpl0 22134	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (0g‘𝑈) = ({ℎ ∈ (ℕ0 ↑m (𝐼 ∖ {𝑋})) ∣ ℎ finSupp 0} × {(0g‘𝑅)}))
76	37, 68, 75	3eqtr3d 2804	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → ((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹)‘(𝑝 ↾ {𝑋})) = ({ℎ ∈ (ℕ0 ↑m (𝐼 ∖ {𝑋})) ∣ ℎ finSupp 0} × {(0g‘𝑅)}))
77	76	fveq1d 6883	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹)‘(𝑝 ↾ {𝑋}))‘(𝑝 ↾ (𝐼 ∖ {𝑋}))) = (({ℎ ∈ (ℕ0 ↑m (𝐼 ∖ {𝑋})) ∣ ℎ finSupp 0} × {(0g‘𝑅)})‘(𝑝 ↾ (𝐼 ∖ {𝑋}))))
78	24	snssd 4751	. . . . . 6 ⊢ (𝜑 → {𝑋} ⊆ 𝐼)
79	78	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → {𝑋} ⊆ 𝐼)
80		simpr 489	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
81	5, 1, 3, 51, 79, 52, 80	selvvvval 22272	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹)‘(𝑝 ↾ {𝑋}))‘(𝑝 ↾ (𝐼 ∖ {𝑋}))) = (𝐹‘𝑝))
82		breq1 5111	. . . . . 6 ⊢ (ℎ = (𝑝 ↾ (𝐼 ∖ {𝑋})) → (ℎ finSupp 0 ↔ (𝑝 ↾ (𝐼 ∖ {𝑋})) finSupp 0))
83		difssd 4090	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝐼 ∖ {𝑋}) ⊆ 𝐼)
84	22, 83	elmapssresd 8864	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑝 ↾ (𝐼 ∖ {𝑋})) ∈ (ℕ0 ↑m (𝐼 ∖ {𝑋})))
85		breq1 5111	. . . . . . . 8 ⊢ (ℎ = 𝑝 → (ℎ finSupp 0 ↔ 𝑝 finSupp 0))
86	85, 80	elrabrd 3652	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑝 finSupp 0)
87		c0ex 11199	. . . . . . . 8 ⊢ 0 ∈ V
88	87	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 0 ∈ V)
89	86, 88	fsuppres 9352	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑝 ↾ (𝐼 ∖ {𝑋})) finSupp 0)
90	82, 84, 89	elrabd 3651	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑝 ↾ (𝐼 ∖ {𝑋})) ∈ {ℎ ∈ (ℕ0 ↑m (𝐼 ∖ {𝑋})) ∣ ℎ finSupp 0})
91		fvex 6894	. . . . . 6 ⊢ (0g‘𝑅) ∈ V
92	91	fvconst2 7202	. . . . 5 ⊢ ((𝑝 ↾ (𝐼 ∖ {𝑋})) ∈ {ℎ ∈ (ℕ0 ↑m (𝐼 ∖ {𝑋})) ∣ ℎ finSupp 0} → (({ℎ ∈ (ℕ0 ↑m (𝐼 ∖ {𝑋})) ∣ ℎ finSupp 0} × {(0g‘𝑅)})‘(𝑝 ↾ (𝐼 ∖ {𝑋}))) = (0g‘𝑅))
93	90, 92	syl 18	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (({ℎ ∈ (ℕ0 ↑m (𝐼 ∖ {𝑋})) ∣ ℎ finSupp 0} × {(0g‘𝑅)})‘(𝑝 ↾ (𝐼 ∖ {𝑋}))) = (0g‘𝑅))
94	77, 81, 93	3eqtr3d 2804	. . 3 ⊢ ((𝜑 ∧ 𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝐹‘𝑝) = (0g‘𝑅))
95	94	mpteq2dva 5203	. 2 ⊢ (𝜑 → (𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝐹‘𝑝)) = (𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (0g‘𝑅)))
96		selvply1rhm0.2	. . . 4 ⊢ 𝑍 = (0g‘𝑃)
97	1, 5, 71, 96, 18, 73	mpl0 22134	. . 3 ⊢ (𝜑 → 𝑍 = ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} × {(0g‘𝑅)}))
98		fconstmpt 5723	. . 3 ⊢ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} × {(0g‘𝑅)}) = (𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (0g‘𝑅))
99	97, 98	eqtr2di 2813	. 2 ⊢ (𝜑 → (𝑝 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (0g‘𝑅)) = 𝑍)
100	8, 95, 99	3eqtrd 2800	1 ⊢ (𝜑 → 𝐹 = 𝑍)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1568   ∈ wcel 2141  {crab 3414  Vcvv 3453   ∖ cdif 3901   ⊆ wss 3904  ∅c0 4285  {csn 4588  ⟨cop 4594   class class class wbr 5108   ↦ cmpt 5191   × cxp 5659  ^◡ccnv 5660   ↾ cres 5663   “ cima 5664   Fn wfn 6531  ‘cfv 6536  (class class class)co 7410  1_oc1o 8445   ↑_m cmap 8823  Fincfn 8942   finSupp cfsupp 9320  0cc0 11099  ℕcn 12232  ℕ₀cn0 12503  Basecbs 17268  0_gc0g 17491  Grpcgrp 18999  CRingccrg 20315   mPoly cmpl 22035   selectVars cslv 22246  Poly₁cpl1 22316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5237  ax-sep 5256  ax-nul 5268  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-cnex 11155  ax-resscn 11156  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-mulcom 11163  ax-addass 11164  ax-mulass 11165  ax-distr 11166  ax-i2m1 11167  ax-1ne0 11168  ax-1rid 11169  ax-rnegex 11170  ax-rrecex 11171  ax-cnre 11172  ax-pre-lttri 11173  ax-pre-lttrn 11174  ax-pre-ltadd 11175  ax-pre-mulgt0 11176

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4595  df-uni 4872  df-int 4912  df-iun 4957  df-iin 4958  df-br 5109  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-se 5615  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-isom 6545  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-of 7674  df-ofr 7675  df-om 7862  df-1st 7985  df-2nd 7986  df-supp 8156  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-1o 8452  df-2o 8453  df-er 8693  df-map 8825  df-pm 8826  df-ixp 8895  df-en 8943  df-dom 8944  df-sdom 8945  df-fin 8946  df-fsupp 9321  df-sup 9401  df-oi 9471  df-card 9924  df-pnf 11244  df-mnf 11245  df-xr 11246  df-ltxr 11247  df-le 11248  df-sub 11442  df-neg 11443  df-nn 12233  df-2 12302  df-3 12303  df-4 12304  df-5 12305  df-6 12306  df-7 12307  df-8 12308  df-9 12309  df-n0 12504  df-z 12591  df-dec 12711  df-uz 12862  df-fz 13535  df-fzo 13682  df-seq 14037  df-hash 14366  df-struct 17206  df-sets 17223  df-slot 17241  df-ndx 17253  df-base 17269  df-ress 17290  df-plusg 17322  df-mulr 17323  df-sca 17325  df-vsca 17326  df-ip 17327  df-tset 17328  df-ple 17329  df-ds 17331  df-hom 17333  df-cco 17334  df-0g 17493  df-gsum 17494  df-prds 17499  df-pws 17501  df-mre 17637  df-mrc 17638  df-acs 17640  df-mgm 18697  df-sgrp 18776  df-mnd 18792  df-mhm 18840  df-submnd 18841  df-grp 19002  df-minusg 19003  df-sbg 19004  df-mulg 19133  df-subg 19188  df-ghm 19283  df-cntz 19386  df-cmn 19851  df-abl 19852  df-mgp 20216  df-rng 20230  df-ur 20263  df-srg 20268  df-ring 20316  df-cring 20317  df-rhm 20553  df-subrng 20630  df-subrg 20654  df-lmod 20962  df-lss 21032  df-lsp 21072  df-assa 21982  df-asp 21983  df-ascl 21984  df-psr 22038  df-mvr 22039  df-mpl 22040  df-opsr 22042  df-evls 22204  df-evl 22205  df-selv 22247  df-psr1 22319  df-ply1 22321

This theorem is referenced by:  mplidomlem  33883