Theorem selvply1rhmlem4

Description: Lemma for selvply1rhm : The mapping H is linear. (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 )
	selvply1rhmlem4.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	selvply1rhmlem4.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
Assertion	selvply1rhmlem4	⊢ ( 𝜑 → ( 𝐻 ‘ ( 𝐹 ( +g ‘ 𝑃 ) 𝐺 ) ) = ( ( 𝐻 ‘ 𝐹 ) ( +g ‘ 𝑄 ) ( 𝐻 ‘ 𝐺 ) ) )

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		selvply1rhmlem4.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
10		selvply1rhmlem4.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
11	1 2 3 4 5 6 7 8	selvply1rhmlem1	⊢ ( 𝜑 → 𝐻 : 𝐵 ⟶ ( Base ‘ 𝑄 ) )
12	11 9	ffvelcdmd	⊢ ( 𝜑 → ( 𝐻 ‘ 𝐹 ) ∈ ( Base ‘ 𝑄 ) )
13		eqid	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
14		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
15	4 13 14	ply1basf	⊢ ( ( 𝐻 ‘ 𝐹 ) ∈ ( Base ‘ 𝑄 ) → ( 𝐻 ‘ 𝐹 ) : ( ℕ0 ↑m 1o ) ⟶ ( Base ‘ 𝑈 ) )
16	12 15	syl	⊢ ( 𝜑 → ( 𝐻 ‘ 𝐹 ) : ( ℕ0 ↑m 1o ) ⟶ ( Base ‘ 𝑈 ) )
17	16	ffnd	⊢ ( 𝜑 → ( 𝐻 ‘ 𝐹 ) Fn ( ℕ0 ↑m 1o ) )
18	11 10	ffvelcdmd	⊢ ( 𝜑 → ( 𝐻 ‘ 𝐺 ) ∈ ( Base ‘ 𝑄 ) )
19	4 13 14	ply1basf	⊢ ( ( 𝐻 ‘ 𝐺 ) ∈ ( Base ‘ 𝑄 ) → ( 𝐻 ‘ 𝐺 ) : ( ℕ0 ↑m 1o ) ⟶ ( Base ‘ 𝑈 ) )
20	18 19	syl	⊢ ( 𝜑 → ( 𝐻 ‘ 𝐺 ) : ( ℕ0 ↑m 1o ) ⟶ ( Base ‘ 𝑈 ) )
21	20	ffnd	⊢ ( 𝜑 → ( 𝐻 ‘ 𝐺 ) Fn ( ℕ0 ↑m 1o ) )
22		ovexd	⊢ ( 𝜑 → ( ℕ0 ↑m 1o ) ∈ V )
23		inidm	⊢ ( ( ℕ0 ↑m 1o ) ∩ ( ℕ0 ↑m 1o ) ) = ( ℕ0 ↑m 1o )
24		eqidd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( ( 𝐻 ‘ 𝐹 ) ‘ 𝑛 ) = ( ( 𝐻 ‘ 𝐹 ) ‘ 𝑛 ) )
25		eqidd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( ( 𝐻 ‘ 𝐺 ) ‘ 𝑛 ) = ( ( 𝐻 ‘ 𝐺 ) ‘ 𝑛 ) )
26	17 21 22 22 23 24 25	ofval	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( ( ( 𝐻 ‘ 𝐹 ) ∘f ( +g ‘ 𝑈 ) ( 𝐻 ‘ 𝐺 ) ) ‘ 𝑛 ) = ( ( ( 𝐻 ‘ 𝐹 ) ‘ 𝑛 ) ( +g ‘ 𝑈 ) ( ( 𝐻 ‘ 𝐺 ) ‘ 𝑛 ) ) )
27		eqid	⊢ ( 1o mPoly 𝑈 ) = ( 1o mPoly 𝑈 )
28	4 13	ply1bas	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ ( 1o mPoly 𝑈 ) )
29		eqid	⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
30		eqid	⊢ ( +g ‘ 𝑄 ) = ( +g ‘ 𝑄 )
31	4 27 30	ply1plusg	⊢ ( +g ‘ 𝑄 ) = ( +g ‘ ( 1o mPoly 𝑈 ) )
32	27 28 29 31 12 18	mpladd	⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝐹 ) ( +g ‘ 𝑄 ) ( 𝐻 ‘ 𝐺 ) ) = ( ( 𝐻 ‘ 𝐹 ) ∘f ( +g ‘ 𝑈 ) ( 𝐻 ‘ 𝐺 ) ) )
33	32	fveq1d	⊢ ( 𝜑 → ( ( ( 𝐻 ‘ 𝐹 ) ( +g ‘ 𝑄 ) ( 𝐻 ‘ 𝐺 ) ) ‘ 𝑛 ) = ( ( ( 𝐻 ‘ 𝐹 ) ∘f ( +g ‘ 𝑈 ) ( 𝐻 ‘ 𝐺 ) ) ‘ 𝑛 ) )
34	33	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( ( ( 𝐻 ‘ 𝐹 ) ( +g ‘ 𝑄 ) ( 𝐻 ‘ 𝐺 ) ) ‘ 𝑛 ) = ( ( ( 𝐻 ‘ 𝐹 ) ∘f ( +g ‘ 𝑈 ) ( 𝐻 ‘ 𝐺 ) ) ‘ 𝑛 ) )
35		eqid	⊢ ( { 𝑋 } mPoly 𝑈 ) = ( { 𝑋 } mPoly 𝑈 )
36		eqid	⊢ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) = ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) )
37		eqid	⊢ { ℎ ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
38	7	snssd	⊢ ( 𝜑 → { 𝑋 } ⊆ 𝐼 )
39	2 1 3 35 36 8 38 9	selvcl	⊢ ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ∈ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) )
40	35 14 36 37 39	mplelf	⊢ ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) : { ℎ ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑈 ) )
41	40	ffnd	⊢ ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) Fn { ℎ ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
42	41	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) Fn { ℎ ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
43	2 1 3 35 36 8 38 10	selvcl	⊢ ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐺 ) ∈ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) )
44	35 14 36 37 43	mplelf	⊢ ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐺 ) : { ℎ ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑈 ) )
45	44	ffnd	⊢ ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐺 ) Fn { ℎ ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
46	45	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐺 ) Fn { ℎ ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
47		ovex	⊢ ( ℕ0 ↑m { 𝑋 } ) ∈ V
48	47	rabex	⊢ { ℎ ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∈ V
49	48	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { ℎ ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∈ V )
50		breq1	⊢ ( ℎ = { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } → ( ℎ finSupp 0 ↔ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } finSupp 0 ) )
51		nn0ex	⊢ ℕ0 ∈ V
52	51	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ℕ0 ∈ V )
53		snex	⊢ { 𝑋 } ∈ V
54	53	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { 𝑋 } ∈ V )
55	7	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → 𝑋 ∈ 𝐼 )
56		simpr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → 𝑛 ∈ ( ℕ0 ↑m 1o ) )
57	56	elmaprd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → 𝑛 : 1o ⟶ ℕ0 )
58		0lt1o	⊢ ∅ ∈ 1o
59	58	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ∅ ∈ 1o )
60	57 59	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝑛 ‘ ∅ ) ∈ ℕ0 )
61	55 60	fsnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } : { 𝑋 } ⟶ ℕ0 )
62	52 54 61	elmapdd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∈ ( ℕ0 ↑m { 𝑋 } ) )
63		c0ex	⊢ 0 ∈ V
64	63	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → 0 ∈ V )
65		snopfsupp	⊢ ( ( 𝑋 ∈ 𝐼 ∧ ( 𝑛 ‘ ∅ ) ∈ ℕ0 ∧ 0 ∈ V ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } finSupp 0 )
66	55 60 64 65	syl3anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } finSupp 0 )
67	50 62 66	elrabd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∈ { ℎ ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ℎ finSupp 0 } )
68		eqid	⊢ { ℎ ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ℎ finSupp 0 }
69	68	psrbasfsupp	⊢ { ℎ ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
70	67 69	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∈ { ℎ ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
71		fnfvof	⊢ ( ( ( ( ( ( 𝐼 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	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ∘f ( +g ‘ 𝑈 ) ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐺 ) ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) = ( ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ( +g ‘ 𝑈 ) ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐺 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
73		eqid	⊢ ( +g ‘ ( { 𝑋 } mPoly 𝑈 ) ) = ( +g ‘ ( { 𝑋 } mPoly 𝑈 ) )
74	35 36 29 73 39 43	mpladd	⊢ ( 𝜑 → ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ( +g ‘ ( { 𝑋 } mPoly 𝑈 ) ) ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐺 ) ) = ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ∘f ( +g ‘ 𝑈 ) ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐺 ) ) )
75	74	fveq1d	⊢ ( 𝜑 → ( ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ( +g ‘ ( { 𝑋 } mPoly 𝑈 ) ) ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐺 ) ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) = ( ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ∘f ( +g ‘ 𝑈 ) ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐺 ) ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) )
76	75	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ( +g ‘ ( { 𝑋 } mPoly 𝑈 ) ) ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐺 ) ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) = ( ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ∘f ( +g ‘ 𝑈 ) ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐺 ) ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) )
77	6	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → 𝐼 ∈ 𝑉 )
78	8	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → 𝑅 ∈ CRing )
79	9	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → 𝐹 ∈ 𝐵 )
80	1 2 3 4 5 77 55 78 79 56	selvply1rhmlem3	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( ( 𝐻 ‘ 𝐹 ) ‘ 𝑛 ) = ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) )
81	10	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → 𝐺 ∈ 𝐵 )
82	1 2 3 4 5 77 55 78 81 56	selvply1rhmlem3	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( ( 𝐻 ‘ 𝐺 ) ‘ 𝑛 ) = ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐺 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) )
83	80 82	oveq12d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( ( ( 𝐻 ‘ 𝐹 ) ‘ 𝑛 ) ( +g ‘ 𝑈 ) ( ( 𝐻 ‘ 𝐺 ) ‘ 𝑛 ) ) = ( ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ( +g ‘ 𝑈 ) ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐺 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
84	72 76 83	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ( +g ‘ ( { 𝑋 } mPoly 𝑈 ) ) ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐺 ) ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) = ( ( ( 𝐻 ‘ 𝐹 ) ‘ 𝑛 ) ( +g ‘ 𝑈 ) ( ( 𝐻 ‘ 𝐺 ) ‘ 𝑛 ) ) )
85	26 34 84	3eqtr4rd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ( +g ‘ ( { 𝑋 } mPoly 𝑈 ) ) ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐺 ) ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) = ( ( ( 𝐻 ‘ 𝐹 ) ( +g ‘ 𝑄 ) ( 𝐻 ‘ 𝐺 ) ) ‘ 𝑛 ) )
86	85	mpteq2dva	⊢ ( 𝜑 → ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ( +g ‘ ( { 𝑋 } mPoly 𝑈 ) ) ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐺 ) ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) = ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( 𝐻 ‘ 𝐹 ) ( +g ‘ 𝑄 ) ( 𝐻 ‘ 𝐺 ) ) ‘ 𝑛 ) ) )
87		fveq2	⊢ ( 𝑓 = ( 𝐹 ( +g ‘ 𝑃 ) 𝐺 ) → ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) = ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ ( 𝐹 ( +g ‘ 𝑃 ) 𝐺 ) ) )
88		eqid	⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
89	2 1 88 3 35 73 6 8 38 9 10	selvadd	⊢ ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ ( 𝐹 ( +g ‘ 𝑃 ) 𝐺 ) ) = ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ( +g ‘ ( { 𝑋 } mPoly 𝑈 ) ) ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐺 ) ) )
90	87 89	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑓 = ( 𝐹 ( +g ‘ 𝑃 ) 𝐺 ) ) → ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) = ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ( +g ‘ ( { 𝑋 } mPoly 𝑈 ) ) ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐺 ) ) )
91	90	fveq1d	⊢ ( ( 𝜑 ∧ 𝑓 = ( 𝐹 ( +g ‘ 𝑃 ) 𝐺 ) ) → ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) = ( ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ( +g ‘ ( { 𝑋 } mPoly 𝑈 ) ) ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐺 ) ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) )
92	91	mpteq2dv	⊢ ( ( 𝜑 ∧ 𝑓 = ( 𝐹 ( +g ‘ 𝑃 ) 𝐺 ) ) → ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) = ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ( +g ‘ ( { 𝑋 } mPoly 𝑈 ) ) ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐺 ) ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
93	8	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
94	2 6 93	mplringd	⊢ ( 𝜑 → 𝑃 ∈ Ring )
95	94	ringgrpd	⊢ ( 𝜑 → 𝑃 ∈ Grp )
96	1 88 95 9 10	grpcld	⊢ ( 𝜑 → ( 𝐹 ( +g ‘ 𝑃 ) 𝐺 ) ∈ 𝐵 )
97	22	mptexd	⊢ ( 𝜑 → ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ( +g ‘ ( { 𝑋 } mPoly 𝑈 ) ) ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐺 ) ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) ∈ V )
98	5 92 96 97	fvmptd2	⊢ ( 𝜑 → ( 𝐻 ‘ ( 𝐹 ( +g ‘ 𝑃 ) 𝐺 ) ) = ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ( +g ‘ ( { 𝑋 } mPoly 𝑈 ) ) ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐺 ) ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
99	6	difexd	⊢ ( 𝜑 → ( 𝐼 ∖ { 𝑋 } ) ∈ V )
100	3 99 93	mplringd	⊢ ( 𝜑 → 𝑈 ∈ Ring )
101	4	ply1ring	⊢ ( 𝑈 ∈ Ring → 𝑄 ∈ Ring )
102	100 101	syl	⊢ ( 𝜑 → 𝑄 ∈ Ring )
103	102	ringgrpd	⊢ ( 𝜑 → 𝑄 ∈ Grp )
104	13 30 103 12 18	grpcld	⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝐹 ) ( +g ‘ 𝑄 ) ( 𝐻 ‘ 𝐺 ) ) ∈ ( Base ‘ 𝑄 ) )
105	4 13 14	ply1basf	⊢ ( ( ( 𝐻 ‘ 𝐹 ) ( +g ‘ 𝑄 ) ( 𝐻 ‘ 𝐺 ) ) ∈ ( Base ‘ 𝑄 ) → ( ( 𝐻 ‘ 𝐹 ) ( +g ‘ 𝑄 ) ( 𝐻 ‘ 𝐺 ) ) : ( ℕ0 ↑m 1o ) ⟶ ( Base ‘ 𝑈 ) )
106	104 105	syl	⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝐹 ) ( +g ‘ 𝑄 ) ( 𝐻 ‘ 𝐺 ) ) : ( ℕ0 ↑m 1o ) ⟶ ( Base ‘ 𝑈 ) )
107	106	feqmptd	⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝐹 ) ( +g ‘ 𝑄 ) ( 𝐻 ‘ 𝐺 ) ) = ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( 𝐻 ‘ 𝐹 ) ( +g ‘ 𝑄 ) ( 𝐻 ‘ 𝐺 ) ) ‘ 𝑛 ) ) )
108	86 98 107	3eqtr4d	⊢ ( 𝜑 → ( 𝐻 ‘ ( 𝐹 ( +g ‘ 𝑃 ) 𝐺 ) ) = ( ( 𝐻 ‘ 𝐹 ) ( +g ‘ 𝑄 ) ( 𝐻 ‘ 𝐺 ) ) )