Theorem mhpvscacl

Description: Homogeneous polynomials are closed under scalar multiplication. (Contributed by SN, 25-Sep-2023)

	Ref	Expression
Hypotheses	mhpvscacl.h	⊢ 𝐻 = ( 𝐼 mHomP 𝑅 )
	mhpvscacl.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	mhpvscacl.t	⊢ · = ( ·𝑠 ‘ 𝑃 )
	mhpvscacl.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	mhpvscacl.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	mhpvscacl.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	mhpvscacl.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	mhpvscacl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
	mhpvscacl.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐻 ‘ 𝑁 ) )
Assertion	mhpvscacl	⊢ ( 𝜑 → ( 𝑋 · 𝐹 ) ∈ ( 𝐻 ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		mhpvscacl.h	⊢ 𝐻 = ( 𝐼 mHomP 𝑅 )
2		mhpvscacl.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
3		mhpvscacl.t	⊢ · = ( ·𝑠 ‘ 𝑃 )
4		mhpvscacl.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
5		mhpvscacl.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6		mhpvscacl.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
7		mhpvscacl.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
8		mhpvscacl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
9		mhpvscacl.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐻 ‘ 𝑁 ) )
10		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
11		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
12		eqid	⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
13	2	mpllmod	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → 𝑃 ∈ LMod )
14	5 6 13	syl2anc	⊢ ( 𝜑 → 𝑃 ∈ LMod )
15	8 4	eleqtrdi	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑅 ) )
16	2 5 6	mplsca	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
17	16	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
18	15 17	eleqtrd	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
19	1 2 10 5 6 7 9	mhpmpl	⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ 𝑃 ) )
20		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
21		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
22	10 20 3 21	lmodvscl	⊢ ( ( 𝑃 ∈ LMod ∧ 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝐹 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑋 · 𝐹 ) ∈ ( Base ‘ 𝑃 ) )
23	14 18 19 22	syl3anc	⊢ ( 𝜑 → ( 𝑋 · 𝐹 ) ∈ ( Base ‘ 𝑃 ) )
24	2 4 10 12 23	mplelf	⊢ ( 𝜑 → ( 𝑋 · 𝐹 ) : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ 𝐾 )
25		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
26	8	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∖ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ) → 𝑋 ∈ 𝐾 )
27	19	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∖ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ) → 𝐹 ∈ ( Base ‘ 𝑃 ) )
28		eldifi	⊢ ( 𝑘 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∖ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) → 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
29	28	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∖ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ) → 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
30	2 3 4 10 25 12 26 27 29	mplvscaval	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∖ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ) → ( ( 𝑋 · 𝐹 ) ‘ 𝑘 ) = ( 𝑋 ( .r ‘ 𝑅 ) ( 𝐹 ‘ 𝑘 ) ) )
31	2 4 10 12 19	mplelf	⊢ ( 𝜑 → 𝐹 : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ 𝐾 )
32		ssidd	⊢ ( 𝜑 → ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ⊆ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) )
33		ovexd	⊢ ( 𝜑 → ( ℕ0 ↑m 𝐼 ) ∈ V )
34	12 33	rabexd	⊢ ( 𝜑 → { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∈ V )
35		fvexd	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ V )
36	31 32 34 35	suppssr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∖ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ) → ( 𝐹 ‘ 𝑘 ) = ( 0g ‘ 𝑅 ) )
37	36	oveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∖ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ) → ( 𝑋 ( .r ‘ 𝑅 ) ( 𝐹 ‘ 𝑘 ) ) = ( 𝑋 ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) )
38	4 25 11	ringrz	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → ( 𝑋 ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
39	6 8 38	syl2anc	⊢ ( 𝜑 → ( 𝑋 ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
40	39	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∖ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ) → ( 𝑋 ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
41	30 37 40	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∖ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ) → ( ( 𝑋 · 𝐹 ) ‘ 𝑘 ) = ( 0g ‘ 𝑅 ) )
42	24 41	suppss	⊢ ( 𝜑 → ( ( 𝑋 · 𝐹 ) supp ( 0g ‘ 𝑅 ) ) ⊆ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) )
43	1 11 12 5 6 7 9	mhpdeg	⊢ ( 𝜑 → ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } )
44	42 43	sstrd	⊢ ( 𝜑 → ( ( 𝑋 · 𝐹 ) supp ( 0g ‘ 𝑅 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } )
45	1 2 10 11 12 5 6 7 23 44	ismhp2	⊢ ( 𝜑 → ( 𝑋 · 𝐹 ) ∈ ( 𝐻 ‘ 𝑁 ) )