Theorem selvply1rhmlem4 34088

Description: Lemma for selvply1rhm 34090: The mapping 𝐻 is linear. (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)
selvply1rhmlem4.f	⊢ (𝜑 → 𝐹 ∈ 𝐵)
selvply1rhmlem4.g	⊢ (𝜑 → 𝐺 ∈ 𝐵)

Assertion

Ref	Expression
selvply1rhmlem4	⊢ (𝜑 → (𝐻‘(𝐹(+g‘𝑃)𝐺)) = ((𝐻‘𝐹)(+g‘𝑄)(𝐻‘𝐺)))

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

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

Proof of Theorem selvply1rhmlem4

Dummy variable ℎ is distinct from all other variables.

Step	Hyp	Ref	Expression
1		selvply1rhm.1	. . . . . . . . 9 ⊢ 𝐵 = (Base‘𝑃)
2		selvply1rhm.2	. . . . . . . . 9 ⊢ 𝑃 = (𝐼 mPoly 𝑅)
3		selvply1rhm.3	. . . . . . . . 9 ⊢ 𝑈 = ((𝐼 ∖ {𝑋}) mPoly 𝑅)
4		selvply1rhm.4	. . . . . . . . 9 ⊢ 𝑄 = (Poly1‘𝑈)
5		selvply1rhm.5	. . . . . . . . 9 ⊢ 𝐻 = (𝑓 ∈ 𝐵 ↦ (𝑛 ∈ (ℕ0 ↑m 1o) ↦ ((((𝐼 selectVars 𝑅)‘{𝑋})‘𝑓)‘{⟨𝑋, (𝑛‘∅)⟩})))
6		selvply1rhm.6	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
7		selvply1rhm.7	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ 𝐼)
8		selvply1rhm.8	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ CRing)
9	1, 2, 3, 4, 5, 6, 7, 8	selvply1rhmlem1 34085	. . . . . . . 8 ⊢ (𝜑 → 𝐻:𝐵⟶(Base‘𝑄))
10		selvply1rhmlem4.f	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ 𝐵)
11	9, 10	ffvelcdmd 7073	. . . . . . 7 ⊢ (𝜑 → (𝐻‘𝐹) ∈ (Base‘𝑄))
12		eqid 2760	. . . . . . . 8 ⊢ (Base‘𝑄) = (Base‘𝑄)
13		eqid 2760	. . . . . . . 8 ⊢ (Base‘𝑈) = (Base‘𝑈)
14	4, 12, 13	ply1basf 22481	. . . . . . 7 ⊢ ((𝐻‘𝐹) ∈ (Base‘𝑄) → (𝐻‘𝐹):(ℕ0 ↑m 1o)⟶(Base‘𝑈))
15	11, 14	syl 18	. . . . . 6 ⊢ (𝜑 → (𝐻‘𝐹):(ℕ0 ↑m 1o)⟶(Base‘𝑈))
16	15	ffnd 6698	. . . . 5 ⊢ (𝜑 → (𝐻‘𝐹) Fn (ℕ0 ↑m 1o))
17		selvply1rhmlem4.g	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ 𝐵)
18	9, 17	ffvelcdmd 7073	. . . . . . 7 ⊢ (𝜑 → (𝐻‘𝐺) ∈ (Base‘𝑄))
19	4, 12, 13	ply1basf 22481	. . . . . . 7 ⊢ ((𝐻‘𝐺) ∈ (Base‘𝑄) → (𝐻‘𝐺):(ℕ0 ↑m 1o)⟶(Base‘𝑈))
20	18, 19	syl 18	. . . . . 6 ⊢ (𝜑 → (𝐻‘𝐺):(ℕ0 ↑m 1o)⟶(Base‘𝑈))
21	20	ffnd 6698	. . . . 5 ⊢ (𝜑 → (𝐻‘𝐺) Fn (ℕ0 ↑m 1o))
22		ovexd 7443	. . . . 5 ⊢ (𝜑 → (ℕ0 ↑m 1o) ∈ V)
23		inidm 4171	. . . . 5 ⊢ ((ℕ0 ↑m 1o) ∩ (ℕ0 ↑m 1o)) = (ℕ0 ↑m 1o)
24		eqidd 2761	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ0 ↑m 1o)) → ((𝐻‘𝐹)‘𝑛) = ((𝐻‘𝐹)‘𝑛))
25		eqidd 2761	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ0 ↑m 1o)) → ((𝐻‘𝐺)‘𝑛) = ((𝐻‘𝐺)‘𝑛))
26	16, 21, 22, 22, 23, 24, 25	ofval 7687	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ0 ↑m 1o)) → (((𝐻‘𝐹) ∘f (+g‘𝑈)(𝐻‘𝐺))‘𝑛) = (((𝐻‘𝐹)‘𝑛)(+g‘𝑈)((𝐻‘𝐺)‘𝑛)))
27		eqid 2760	. . . . . . 7 ⊢ (1o mPoly 𝑈) = (1o mPoly 𝑈)
28	4, 12	ply1bas 22474	. . . . . . 7 ⊢ (Base‘𝑄) = (Base‘(1o mPoly 𝑈))
29		eqid 2760	. . . . . . 7 ⊢ (+g‘𝑈) = (+g‘𝑈)
30		eqid 2760	. . . . . . . 8 ⊢ (+g‘𝑄) = (+g‘𝑄)
31	4, 27, 30	ply1plusg 22502	. . . . . . 7 ⊢ (+g‘𝑄) = (+g‘(1o mPoly 𝑈))
32	27, 28, 29, 31, 11, 18	mpladd 22277	. . . . . 6 ⊢ (𝜑 → ((𝐻‘𝐹)(+g‘𝑄)(𝐻‘𝐺)) = ((𝐻‘𝐹) ∘f (+g‘𝑈)(𝐻‘𝐺)))
33	32	fveq1d 6875	. . . . 5 ⊢ (𝜑 → (((𝐻‘𝐹)(+g‘𝑄)(𝐻‘𝐺))‘𝑛) = (((𝐻‘𝐹) ∘f (+g‘𝑈)(𝐻‘𝐺))‘𝑛))
34	33	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ0 ↑m 1o)) → (((𝐻‘𝐹)(+g‘𝑄)(𝐻‘𝐺))‘𝑛) = (((𝐻‘𝐹) ∘f (+g‘𝑈)(𝐻‘𝐺))‘𝑛))
35		eqid 2760	. . . . . . . . 9 ⊢ ({𝑋} mPoly 𝑈) = ({𝑋} mPoly 𝑈)
36		eqid 2760	. . . . . . . . 9 ⊢ (Base‘({𝑋} mPoly 𝑈)) = (Base‘({𝑋} mPoly 𝑈))
37		eqid 2760	. . . . . . . . 9 ⊢ {ℎ ∈ (ℕ0 ↑m {𝑋}) ∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0 ↑m {𝑋}) ∣ (◡ℎ “ ℕ) ∈ Fin}
38	7	snssd 4746	. . . . . . . . . 10 ⊢ (𝜑 → {𝑋} ⊆ 𝐼)
39	2, 1, 3, 35, 36, 8, 38, 10	selvcl 22410	. . . . . . . . 9 ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹) ∈ (Base‘({𝑋} mPoly 𝑈)))
40	35, 13, 36, 37, 39	mplelf 22266	. . . . . . . 8 ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹):{ℎ ∈ (ℕ0 ↑m {𝑋}) ∣ (◡ℎ “ ℕ) ∈ Fin}⟶(Base‘𝑈))
41	40	ffnd 6698	. . . . . . 7 ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹) Fn {ℎ ∈ (ℕ0 ↑m {𝑋}) ∣ (◡ℎ “ ℕ) ∈ Fin})
42	41	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ0 ↑m 1o)) → (((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹) Fn {ℎ ∈ (ℕ0 ↑m {𝑋}) ∣ (◡ℎ “ ℕ) ∈ Fin})
43	2, 1, 3, 35, 36, 8, 38, 17	selvcl 22410	. . . . . . . . 9 ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘{𝑋})‘𝐺) ∈ (Base‘({𝑋} mPoly 𝑈)))
44	35, 13, 36, 37, 43	mplelf 22266	. . . . . . . 8 ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘{𝑋})‘𝐺):{ℎ ∈ (ℕ0 ↑m {𝑋}) ∣ (◡ℎ “ ℕ) ∈ Fin}⟶(Base‘𝑈))
45	44	ffnd 6698	. . . . . . 7 ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘{𝑋})‘𝐺) Fn {ℎ ∈ (ℕ0 ↑m {𝑋}) ∣ (◡ℎ “ ℕ) ∈ Fin})
46	45	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ0 ↑m 1o)) → (((𝐼 selectVars 𝑅)‘{𝑋})‘𝐺) Fn {ℎ ∈ (ℕ0 ↑m {𝑋}) ∣ (◡ℎ “ ℕ) ∈ Fin})
47		ovex 7441	. . . . . . . 8 ⊢ (ℕ0 ↑m {𝑋}) ∈ V
48	47	rabex 5299	. . . . . . 7 ⊢ {ℎ ∈ (ℕ0 ↑m {𝑋}) ∣ (◡ℎ “ ℕ) ∈ Fin} ∈ V
49	48	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ0 ↑m 1o)) → {ℎ ∈ (ℕ0 ↑m {𝑋}) ∣ (◡ℎ “ ℕ) ∈ Fin} ∈ V)
50		breq1 5105	. . . . . . . 8 ⊢ (ℎ = {⟨𝑋, (𝑛‘∅)⟩} → (ℎ finSupp 0 ↔ {⟨𝑋, (𝑛‘∅)⟩} finSupp 0))
51		nn0ex 12581	. . . . . . . . . 10 ⊢ ℕ0 ∈ V
52	51	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ0 ↑m 1o)) → ℕ0 ∈ V)
53		snex 5396	. . . . . . . . . 10 ⊢ {𝑋} ∈ V
54	53	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ0 ↑m 1o)) → {𝑋} ∈ V)
55	7	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ0 ↑m 1o)) → 𝑋 ∈ 𝐼)
56		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ0 ↑m 1o)) → 𝑛 ∈ (ℕ0 ↑m 1o))
57	56	elmaprd 8848	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ0 ↑m 1o)) → 𝑛:1o⟶ℕ0)
58		0lt1o 8490	. . . . . . . . . . . 12 ⊢ ∅ ∈ 1o
59	58	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ0 ↑m 1o)) → ∅ ∈ 1o)
60	57, 59	ffvelcdmd 7073	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ0 ↑m 1o)) → (𝑛‘∅) ∈ ℕ0)
61	55, 60	fsnd 6857	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ0 ↑m 1o)) → {⟨𝑋, (𝑛‘∅)⟩}:{𝑋}⟶ℕ0)
62	52, 54, 61	elmapdd 8839	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ0 ↑m 1o)) → {⟨𝑋, (𝑛‘∅)⟩} ∈ (ℕ0 ↑m {𝑋}))
63		c0ex 11271	. . . . . . . . . 10 ⊢ 0 ∈ V
64	63	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ0 ↑m 1o)) → 0 ∈ V)
65		snopfsupp 9361	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝐼 ∧ (𝑛‘∅) ∈ ℕ0 ∧ 0 ∈ V) → {⟨𝑋, (𝑛‘∅)⟩} finSupp 0)
66	55, 60, 64, 65	syl3anc 1398	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ0 ↑m 1o)) → {⟨𝑋, (𝑛‘∅)⟩} finSupp 0)
67	50, 62, 66	elrabd 3646	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ0 ↑m 1o)) → {⟨𝑋, (𝑛‘∅)⟩} ∈ {ℎ ∈ (ℕ0 ↑m {𝑋}) ∣ ℎ finSupp 0})
68		eqid 2760	. . . . . . . 8 ⊢ {ℎ ∈ (ℕ0 ↑m {𝑋}) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ0 ↑m {𝑋}) ∣ ℎ finSupp 0}
69	68	psrbasfsupp 34076	. . . . . . 7 ⊢ {ℎ ∈ (ℕ0 ↑m {𝑋}) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ0 ↑m {𝑋}) ∣ (◡ℎ “ ℕ) ∈ Fin}
70	67, 69	eleqtrdi 2870	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ0 ↑m 1o)) → {⟨𝑋, (𝑛‘∅)⟩} ∈ {ℎ ∈ (ℕ0 ↑m {𝑋}) ∣ (◡ℎ “ ℕ) ∈ Fin})
71		fnfvof 7693	. . . . . 6 ⊢ ((((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹) Fn {ℎ ∈ (ℕ0 ↑m {𝑋}) ∣ (◡ℎ “ ℕ) ∈ Fin} ∧ (((𝐼 selectVars 𝑅)‘{𝑋})‘𝐺) Fn {ℎ ∈ (ℕ0 ↑m {𝑋}) ∣ (◡ℎ “ ℕ) ∈ Fin}) ∧ ({ℎ ∈ (ℕ0 ↑m {𝑋}) ∣ (◡ℎ “ ℕ) ∈ Fin} ∈ V ∧ {⟨𝑋, (𝑛‘∅)⟩} ∈ {ℎ ∈ (ℕ0 ↑m {𝑋}) ∣ (◡ℎ “ ℕ) ∈ Fin})) → (((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹) ∘f (+g‘𝑈)(((𝐼 selectVars 𝑅)‘{𝑋})‘𝐺))‘{⟨𝑋, (𝑛‘∅)⟩}) = (((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹)‘{⟨𝑋, (𝑛‘∅)⟩})(+g‘𝑈)((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐺)‘{⟨𝑋, (𝑛‘∅)⟩})))
72	42, 46, 49, 70, 71	syl22anc 852	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ0 ↑m 1o)) → (((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹) ∘f (+g‘𝑈)(((𝐼 selectVars 𝑅)‘{𝑋})‘𝐺))‘{⟨𝑋, (𝑛‘∅)⟩}) = (((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹)‘{⟨𝑋, (𝑛‘∅)⟩})(+g‘𝑈)((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐺)‘{⟨𝑋, (𝑛‘∅)⟩})))
73		eqid 2760	. . . . . . . 8 ⊢ (+g‘({𝑋} mPoly 𝑈)) = (+g‘({𝑋} mPoly 𝑈))
74	35, 36, 29, 73, 39, 43	mpladd 22277	. . . . . . 7 ⊢ (𝜑 → ((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹)(+g‘({𝑋} mPoly 𝑈))(((𝐼 selectVars 𝑅)‘{𝑋})‘𝐺)) = ((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹) ∘f (+g‘𝑈)(((𝐼 selectVars 𝑅)‘{𝑋})‘𝐺)))
75	74	fveq1d 6875	. . . . . 6 ⊢ (𝜑 → (((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹)(+g‘({𝑋} mPoly 𝑈))(((𝐼 selectVars 𝑅)‘{𝑋})‘𝐺))‘{⟨𝑋, (𝑛‘∅)⟩}) = (((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹) ∘f (+g‘𝑈)(((𝐼 selectVars 𝑅)‘{𝑋})‘𝐺))‘{⟨𝑋, (𝑛‘∅)⟩}))
76	75	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ0 ↑m 1o)) → (((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹)(+g‘({𝑋} mPoly 𝑈))(((𝐼 selectVars 𝑅)‘{𝑋})‘𝐺))‘{⟨𝑋, (𝑛‘∅)⟩}) = (((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹) ∘f (+g‘𝑈)(((𝐼 selectVars 𝑅)‘{𝑋})‘𝐺))‘{⟨𝑋, (𝑛‘∅)⟩}))
77	6	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ0 ↑m 1o)) → 𝐼 ∈ 𝑉)
78	8	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ0 ↑m 1o)) → 𝑅 ∈ CRing)
79	10	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ0 ↑m 1o)) → 𝐹 ∈ 𝐵)
80	1, 2, 3, 4, 5, 77, 55, 78, 79, 56	selvply1rhmlem3 34087	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ0 ↑m 1o)) → ((𝐻‘𝐹)‘𝑛) = ((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹)‘{⟨𝑋, (𝑛‘∅)⟩}))
81	17	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ0 ↑m 1o)) → 𝐺 ∈ 𝐵)
82	1, 2, 3, 4, 5, 77, 55, 78, 81, 56	selvply1rhmlem3 34087	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ0 ↑m 1o)) → ((𝐻‘𝐺)‘𝑛) = ((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐺)‘{⟨𝑋, (𝑛‘∅)⟩}))
83	80, 82	oveq12d 7426	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ0 ↑m 1o)) → (((𝐻‘𝐹)‘𝑛)(+g‘𝑈)((𝐻‘𝐺)‘𝑛)) = (((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹)‘{⟨𝑋, (𝑛‘∅)⟩})(+g‘𝑈)((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐺)‘{⟨𝑋, (𝑛‘∅)⟩})))
84	72, 76, 83	3eqtr4d 2805	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ0 ↑m 1o)) → (((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹)(+g‘({𝑋} mPoly 𝑈))(((𝐼 selectVars 𝑅)‘{𝑋})‘𝐺))‘{⟨𝑋, (𝑛‘∅)⟩}) = (((𝐻‘𝐹)‘𝑛)(+g‘𝑈)((𝐻‘𝐺)‘𝑛)))
85	26, 34, 84	3eqtr4rd 2806	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ0 ↑m 1o)) → (((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹)(+g‘({𝑋} mPoly 𝑈))(((𝐼 selectVars 𝑅)‘{𝑋})‘𝐺))‘{⟨𝑋, (𝑛‘∅)⟩}) = (((𝐻‘𝐹)(+g‘𝑄)(𝐻‘𝐺))‘𝑛))
86	85	mpteq2dva 5197	. 2 ⊢ (𝜑 → (𝑛 ∈ (ℕ0 ↑m 1o) ↦ (((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹)(+g‘({𝑋} mPoly 𝑈))(((𝐼 selectVars 𝑅)‘{𝑋})‘𝐺))‘{⟨𝑋, (𝑛‘∅)⟩})) = (𝑛 ∈ (ℕ0 ↑m 1o) ↦ (((𝐻‘𝐹)(+g‘𝑄)(𝐻‘𝐺))‘𝑛)))
87		fveq2 6873	. . . . . 6 ⊢ (𝑓 = (𝐹(+g‘𝑃)𝐺) → (((𝐼 selectVars 𝑅)‘{𝑋})‘𝑓) = (((𝐼 selectVars 𝑅)‘{𝑋})‘(𝐹(+g‘𝑃)𝐺)))
88		eqid 2760	. . . . . . 7 ⊢ (+g‘𝑃) = (+g‘𝑃)
89	2, 1, 88, 3, 35, 73, 6, 8, 38, 10, 17	selvadd 22413	. . . . . 6 ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘{𝑋})‘(𝐹(+g‘𝑃)𝐺)) = ((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹)(+g‘({𝑋} mPoly 𝑈))(((𝐼 selectVars 𝑅)‘{𝑋})‘𝐺)))
90	87, 89	sylan9eqr 2817	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 = (𝐹(+g‘𝑃)𝐺)) → (((𝐼 selectVars 𝑅)‘{𝑋})‘𝑓) = ((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹)(+g‘({𝑋} mPoly 𝑈))(((𝐼 selectVars 𝑅)‘{𝑋})‘𝐺)))
91	90	fveq1d 6875	. . . 4 ⊢ ((𝜑 ∧ 𝑓 = (𝐹(+g‘𝑃)𝐺)) → ((((𝐼 selectVars 𝑅)‘{𝑋})‘𝑓)‘{⟨𝑋, (𝑛‘∅)⟩}) = (((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹)(+g‘({𝑋} mPoly 𝑈))(((𝐼 selectVars 𝑅)‘{𝑋})‘𝐺))‘{⟨𝑋, (𝑛‘∅)⟩}))
92	91	mpteq2dv 5198	. . 3 ⊢ ((𝜑 ∧ 𝑓 = (𝐹(+g‘𝑃)𝐺)) → (𝑛 ∈ (ℕ0 ↑m 1o) ↦ ((((𝐼 selectVars 𝑅)‘{𝑋})‘𝑓)‘{⟨𝑋, (𝑛‘∅)⟩})) = (𝑛 ∈ (ℕ0 ↑m 1o) ↦ (((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹)(+g‘({𝑋} mPoly 𝑈))(((𝐼 selectVars 𝑅)‘{𝑋})‘𝐺))‘{⟨𝑋, (𝑛‘∅)⟩})))
93	8	crngringd 20434	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ Ring)
94	2, 6, 93	mplringd 22291	. . . . 5 ⊢ (𝜑 → 𝑃 ∈ Ring)
95	94	ringgrpd 20430	. . . 4 ⊢ (𝜑 → 𝑃 ∈ Grp)
96	1, 88, 95, 10, 17	grpcld 19119	. . 3 ⊢ (𝜑 → (𝐹(+g‘𝑃)𝐺) ∈ 𝐵)
97	22	mptexd 7218	. . 3 ⊢ (𝜑 → (𝑛 ∈ (ℕ0 ↑m 1o) ↦ (((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹)(+g‘({𝑋} mPoly 𝑈))(((𝐼 selectVars 𝑅)‘{𝑋})‘𝐺))‘{⟨𝑋, (𝑛‘∅)⟩})) ∈ V)
98	5, 92, 96, 97	fvmptd2 6990	. 2 ⊢ (𝜑 → (𝐻‘(𝐹(+g‘𝑃)𝐺)) = (𝑛 ∈ (ℕ0 ↑m 1o) ↦ (((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹)(+g‘({𝑋} mPoly 𝑈))(((𝐼 selectVars 𝑅)‘{𝑋})‘𝐺))‘{⟨𝑋, (𝑛‘∅)⟩})))
99	6	difexd 5292	. . . . . . . 8 ⊢ (𝜑 → (𝐼 ∖ {𝑋}) ∈ V)
100	3, 99, 93	mplringd 22291	. . . . . . 7 ⊢ (𝜑 → 𝑈 ∈ Ring)
101	4	ply1ring 22526	. . . . . . 7 ⊢ (𝑈 ∈ Ring → 𝑄 ∈ Ring)
102	100, 101	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑄 ∈ Ring)
103	102	ringgrpd 20430	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ Grp)
104	12, 30, 103, 11, 18	grpcld 19119	. . . 4 ⊢ (𝜑 → ((𝐻‘𝐹)(+g‘𝑄)(𝐻‘𝐺)) ∈ (Base‘𝑄))
105	4, 12, 13	ply1basf 22481	. . . 4 ⊢ (((𝐻‘𝐹)(+g‘𝑄)(𝐻‘𝐺)) ∈ (Base‘𝑄) → ((𝐻‘𝐹)(+g‘𝑄)(𝐻‘𝐺)):(ℕ0 ↑m 1o)⟶(Base‘𝑈))
106	104, 105	syl 18	. . 3 ⊢ (𝜑 → ((𝐻‘𝐹)(+g‘𝑄)(𝐻‘𝐺)):(ℕ0 ↑m 1o)⟶(Base‘𝑈))
107	106	feqmptd 6941	. 2 ⊢ (𝜑 → ((𝐻‘𝐹)(+g‘𝑄)(𝐻‘𝐺)) = (𝑛 ∈ (ℕ0 ↑m 1o) ↦ (((𝐻‘𝐹)(+g‘𝑄)(𝐻‘𝐺))‘𝑛)))
108	86, 98, 107	3eqtr4d 2805	1 ⊢ (𝜑 → (𝐻‘(𝐹(+g‘𝑃)𝐺)) = ((𝐻‘𝐹)(+g‘𝑄)(𝐻‘𝐺)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {crab 3412  Vcvv 3450   ∖ cdif 3895  ∅c0 4278  {csn 4583  ⟨cop 4589   class class class wbr 5102   ↦ cmpt 5185  ^◡ccnv 5646   “ cima 5650   Fn wfn 6522  ⟶wf 6523  ‘cfv 6527  (class class class)co 7408   ∘_f cof 7674  1_oc1o 8447   ↑_m cmap 8825  Fincfn 8951   finSupp cfsupp 9331  0cc0 11171  ℕcn 12304  ℕ₀cn0 12575  Basecbs 17348  +_gcplusg 17389  Ringcrg 20420  CRingccrg 20421   mPoly cmpl 22175   selectVars cslv 22386  Poly₁cpl1 22456

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7734  ax-cnex 11227  ax-resscn 11228  ax-1cn 11229  ax-icn 11230  ax-addcl 11231  ax-addrcl 11232  ax-mulcl 11233  ax-mulrcl 11234  ax-mulcom 11235  ax-addass 11236  ax-mulass 11237  ax-distr 11238  ax-i2m1 11239  ax-1ne0 11240  ax-1rid 11241  ax-rnegex 11242  ax-rrecex 11243  ax-cnre 11244  ax-pre-lttri 11245  ax-pre-lttrn 11246  ax-pre-ltadd 11247  ax-pre-mulgt0 11248

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-tp 4588  df-op 4590  df-uni 4867  df-int 4907  df-iun 4952  df-iin 4953  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-se 5601  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6293  df-ord 6354  df-on 6355  df-lim 6356  df-suc 6357  df-iota 6483  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-isom 6536  df-riota 7365  df-ov 7411  df-oprab 7412  df-mpo 7413  df-of 7676  df-ofr 7677  df-om 7861  df-1st 7984  df-2nd 7985  df-supp 8156  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-1o 8454  df-2o 8455  df-er 8695  df-map 8827  df-pm 8828  df-ixp 8904  df-en 8952  df-dom 8953  df-sdom 8954  df-fin 8955  df-fsupp 9332  df-sup 9412  df-oi 9482  df-card 9991  df-pnf 11316  df-mnf 11317  df-xr 11318  df-ltxr 11319  df-le 11320  df-sub 11514  df-neg 11515  df-nn 12305  df-2 12374  df-3 12375  df-4 12376  df-5 12377  df-6 12378  df-7 12379  df-8 12380  df-9 12381  df-n0 12576  df-z 12663  df-dec 12784  df-uz 12935  df-fz 13609  df-fzo 13757  df-seq 14113  df-hash 14442  df-struct 17286  df-sets 17303  df-slot 17321  df-ndx 17333  df-base 17349  df-ress 17370  df-plusg 17402  df-mulr 17403  df-sca 17405  df-vsca 17406  df-ip 17407  df-tset 17408  df-ple 17409  df-ds 17411  df-hom 17413  df-cco 17414  df-0g 17573  df-gsum 17574  df-prds 17579  df-pws 17581  df-mre 17717  df-mrc 17718  df-acs 17720  df-mgm 18777  df-sgrp 18869  df-mnd 18885  df-mhm 18939  df-submnd 18940  df-grp 19108  df-minusg 19109  df-sbg 19110  df-mulg 19239  df-subg 19294  df-ghm 19389  df-cntz 19492  df-cmn 19957  df-abl 19958  df-mgp 20322  df-rng 20336  df-ur 20369  df-srg 20374  df-ring 20422  df-cring 20423  df-rhm 20663  df-subrng 20759  df-subrg 20783  df-lmod 21098  df-lss 21168  df-lsp 21208  df-assa 22122  df-asp 22123  df-ascl 22124  df-psr 22178  df-mvr 22179  df-mpl 22180  df-opsr 22182  df-evls 22344  df-evl 22345  df-selv 22387  df-psr1 22459  df-ply1 22461

This theorem is used by:  selvply1rhm  34090