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

Metamath Proof Explorer

Theorem selvply1rhmlem4

Proof