mhpsclcl

Description: A scalar (or constant) polynomial has degree 0. Compare deg1scl . In other contexts, there may be an exception for the zero polynomial, but under df-mhp the zero polynomial can be any degree (see mhp0cl ) so there is no exception. (Contributed by SN, 25-May-2024)

	Ref	Expression
Hypotheses	mhpsclcl.h	⊢ 𝐻 = ( 𝐼 mHomP 𝑅 )
	mhpsclcl.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	mhpsclcl.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
	mhpsclcl.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	mhpsclcl.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	mhpsclcl.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	mhpsclcl.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
Assertion	mhpsclcl	⊢ ( 𝜑 → ( 𝐴 ‘ 𝐶 ) ∈ ( 𝐻 ‘ 0 ) )

Proof

Step	Hyp	Ref	Expression
1		mhpsclcl.h	⊢ 𝐻 = ( 𝐼 mHomP 𝑅 )
2		mhpsclcl.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
3		mhpsclcl.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
4		mhpsclcl.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
5		mhpsclcl.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6		mhpsclcl.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
7		mhpsclcl.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
8		eqid	⊢ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin }
9		eqid	⊢ ( 0_g ‘ 𝑅 ) = ( 0_g ‘ 𝑅 )
10	5	adantr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } ) → 𝐼 ∈ 𝑉 )
11	6	adantr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } ) → 𝑅 ∈ Ring )
12	7	adantr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } ) → 𝐶 ∈ 𝐾 )
13	2 8 9 4 3 10 11 12	mplascl	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } ) → ( 𝐴 ‘ 𝐶 ) = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 𝐶 , ( 0_g ‘ 𝑅 ) ) ) )
14		eqeq1	⊢ ( 𝑦 = 𝑑 → ( 𝑦 = ( 𝐼 × { 0 } ) ↔ 𝑑 = ( 𝐼 × { 0 } ) ) )
15	14	ifbid	⊢ ( 𝑦 = 𝑑 → if ( 𝑦 = ( 𝐼 × { 0 } ) , 𝐶 , ( 0_g ‘ 𝑅 ) ) = if ( 𝑑 = ( 𝐼 × { 0 } ) , 𝐶 , ( 0_g ‘ 𝑅 ) ) )
16	15	adantl	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } ) ∧ 𝑦 = 𝑑 ) → if ( 𝑦 = ( 𝐼 × { 0 } ) , 𝐶 , ( 0_g ‘ 𝑅 ) ) = if ( 𝑑 = ( 𝐼 × { 0 } ) , 𝐶 , ( 0_g ‘ 𝑅 ) ) )
17		simpr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } ) → 𝑑 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } )
18		fvexd	⊢ ( 𝜑 → ( 0_g ‘ 𝑅 ) ∈ V )
19	7 18	ifexd	⊢ ( 𝜑 → if ( 𝑑 = ( 𝐼 × { 0 } ) , 𝐶 , ( 0_g ‘ 𝑅 ) ) ∈ V )
20	19	adantr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } ) → if ( 𝑑 = ( 𝐼 × { 0 } ) , 𝐶 , ( 0_g ‘ 𝑅 ) ) ∈ V )
21	13 16 17 20	fvmptd	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( 𝐴 ‘ 𝐶 ) ‘ 𝑑 ) = if ( 𝑑 = ( 𝐼 × { 0 } ) , 𝐶 , ( 0_g ‘ 𝑅 ) ) )
22	21	neeq1d	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( ( 𝐴 ‘ 𝐶 ) ‘ 𝑑 ) ≠ ( 0_g ‘ 𝑅 ) ↔ if ( 𝑑 = ( 𝐼 × { 0 } ) , 𝐶 , ( 0_g ‘ 𝑅 ) ) ≠ ( 0_g ‘ 𝑅 ) ) )
23		iffalse	⊢ ( ¬ 𝑑 = ( 𝐼 × { 0 } ) → if ( 𝑑 = ( 𝐼 × { 0 } ) , 𝐶 , ( 0_g ‘ 𝑅 ) ) = ( 0_g ‘ 𝑅 ) )
24	23	necon1ai	⊢ ( if ( 𝑑 = ( 𝐼 × { 0 } ) , 𝐶 , ( 0_g ‘ 𝑅 ) ) ≠ ( 0_g ‘ 𝑅 ) → 𝑑 = ( 𝐼 × { 0 } ) )
25		fconstmpt	⊢ ( 𝐼 × { 0 } ) = ( 𝑘 ∈ 𝐼 ↦ 0 )
26	25	oveq2i	⊢ ( ( ℂ_fld ↾_s ℕ₀ ) Σ_g ( 𝐼 × { 0 } ) ) = ( ( ℂ_fld ↾_s ℕ₀ ) Σ_g ( 𝑘 ∈ 𝐼 ↦ 0 ) )
27		nn0subm	⊢ ℕ₀ ∈ ( SubMnd ‘ ℂ_fld )
28		eqid	⊢ ( ℂ_fld ↾_s ℕ₀ ) = ( ℂ_fld ↾_s ℕ₀ )
29	28	submmnd	⊢ ( ℕ₀ ∈ ( SubMnd ‘ ℂ_fld ) → ( ℂ_fld ↾_s ℕ₀ ) ∈ Mnd )
30	27 29	ax-mp	⊢ ( ℂ_fld ↾_s ℕ₀ ) ∈ Mnd
31		cnfld0	⊢ 0 = ( 0_g ‘ ℂ_fld )
32	28 31	subm0	⊢ ( ℕ₀ ∈ ( SubMnd ‘ ℂ_fld ) → 0 = ( 0_g ‘ ( ℂ_fld ↾_s ℕ₀ ) ) )
33	27 32	ax-mp	⊢ 0 = ( 0_g ‘ ( ℂ_fld ↾_s ℕ₀ ) )
34	33	gsumz	⊢ ( ( ( ℂ_fld ↾_s ℕ₀ ) ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) → ( ( ℂ_fld ↾_s ℕ₀ ) Σ_g ( 𝑘 ∈ 𝐼 ↦ 0 ) ) = 0 )
35	30 10 34	sylancr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( ℂ_fld ↾_s ℕ₀ ) Σ_g ( 𝑘 ∈ 𝐼 ↦ 0 ) ) = 0 )
36	26 35	eqtrid	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( ℂ_fld ↾_s ℕ₀ ) Σ_g ( 𝐼 × { 0 } ) ) = 0 )
37		oveq2	⊢ ( 𝑑 = ( 𝐼 × { 0 } ) → ( ( ℂ_fld ↾_s ℕ₀ ) Σ_g 𝑑 ) = ( ( ℂ_fld ↾_s ℕ₀ ) Σ_g ( 𝐼 × { 0 } ) ) )
38	37	eqeq1d	⊢ ( 𝑑 = ( 𝐼 × { 0 } ) → ( ( ( ℂ_fld ↾_s ℕ₀ ) Σ_g 𝑑 ) = 0 ↔ ( ( ℂ_fld ↾_s ℕ₀ ) Σ_g ( 𝐼 × { 0 } ) ) = 0 ) )
39	36 38	syl5ibrcom	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } ) → ( 𝑑 = ( 𝐼 × { 0 } ) → ( ( ℂ_fld ↾_s ℕ₀ ) Σ_g 𝑑 ) = 0 ) )
40	24 39	syl5	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } ) → ( if ( 𝑑 = ( 𝐼 × { 0 } ) , 𝐶 , ( 0_g ‘ 𝑅 ) ) ≠ ( 0_g ‘ 𝑅 ) → ( ( ℂ_fld ↾_s ℕ₀ ) Σ_g 𝑑 ) = 0 ) )
41	22 40	sylbid	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( ( 𝐴 ‘ 𝐶 ) ‘ 𝑑 ) ≠ ( 0_g ‘ 𝑅 ) → ( ( ℂ_fld ↾_s ℕ₀ ) Σ_g 𝑑 ) = 0 ) )
42	41	ralrimiva	⊢ ( 𝜑 → ∀ 𝑑 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } ( ( ( 𝐴 ‘ 𝐶 ) ‘ 𝑑 ) ≠ ( 0_g ‘ 𝑅 ) → ( ( ℂ_fld ↾_s ℕ₀ ) Σ_g 𝑑 ) = 0 ) )
43		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
44		0nn0	⊢ 0 ∈ ℕ₀
45	44	a1i	⊢ ( 𝜑 → 0 ∈ ℕ₀ )
46	2 43 4 3 5 6	mplasclf	⊢ ( 𝜑 → 𝐴 : 𝐾 ⟶ ( Base ‘ 𝑃 ) )
47	46 7	ffvelcdmd	⊢ ( 𝜑 → ( 𝐴 ‘ 𝐶 ) ∈ ( Base ‘ 𝑃 ) )
48	1 2 43 9 8 45 47	ismhp3	⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝐶 ) ∈ ( 𝐻 ‘ 0 ) ↔ ∀ 𝑑 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } ( ( ( 𝐴 ‘ 𝐶 ) ‘ 𝑑 ) ≠ ( 0_g ‘ 𝑅 ) → ( ( ℂ_fld ↾_s ℕ₀ ) Σ_g 𝑑 ) = 0 ) ) )
49	42 48	mpbird	⊢ ( 𝜑 → ( 𝐴 ‘ 𝐶 ) ∈ ( 𝐻 ‘ 0 ) )

Metamath Proof Explorer

Theorem mhpsclcl

Proof