Theorem mhpvarcl

Description: A power series variable is a polynomial of degree 1. (Contributed by SN, 25-May-2024)

	Ref	Expression
Hypotheses	mhpvarcl.h	⊢ 𝐻 = ( 𝐼 mHomP 𝑅 )
	mhpvarcl.v	⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
	mhpvarcl.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	mhpvarcl.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	mhpvarcl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
Assertion	mhpvarcl	⊢ ( 𝜑 → ( 𝑉 ‘ 𝑋 ) ∈ ( 𝐻 ‘ 1 ) )

Proof

Step	Hyp	Ref	Expression
1		mhpvarcl.h	⊢ 𝐻 = ( 𝐼 mHomP 𝑅 )
2		mhpvarcl.v	⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
3		mhpvarcl.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
4		mhpvarcl.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
5		mhpvarcl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
6		iffalse	⊢ ( ¬ 𝑑 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) → if ( 𝑑 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
7		eqid	⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
8		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
9		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
10	3	adantr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → 𝐼 ∈ 𝑊 )
11	4	adantr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → 𝑅 ∈ Ring )
12	5	adantr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → 𝑋 ∈ 𝐼 )
13		simpr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
14	2 7 8 9 10 11 12 13	mvrval2	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( 𝑉 ‘ 𝑋 ) ‘ 𝑑 ) = if ( 𝑑 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
15	14	eqeq1d	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( ( 𝑉 ‘ 𝑋 ) ‘ 𝑑 ) = ( 0g ‘ 𝑅 ) ↔ if ( 𝑑 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) ) )
16	6 15	syl5ibr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ¬ 𝑑 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) → ( ( 𝑉 ‘ 𝑋 ) ‘ 𝑑 ) = ( 0g ‘ 𝑅 ) ) )
17	16	necon1ad	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( ( 𝑉 ‘ 𝑋 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) → 𝑑 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) )
18		nn0subm	⊢ ℕ0 ∈ ( SubMnd ‘ ℂfld )
19		eqid	⊢ ( ℂfld ↾s ℕ0 ) = ( ℂfld ↾s ℕ0 )
20		cnfld0	⊢ 0 = ( 0g ‘ ℂfld )
21	19 20	subm0	⊢ ( ℕ0 ∈ ( SubMnd ‘ ℂfld ) → 0 = ( 0g ‘ ( ℂfld ↾s ℕ0 ) ) )
22	18 21	ax-mp	⊢ 0 = ( 0g ‘ ( ℂfld ↾s ℕ0 ) )
23	19	submmnd	⊢ ( ℕ0 ∈ ( SubMnd ‘ ℂfld ) → ( ℂfld ↾s ℕ0 ) ∈ Mnd )
24	18 23	mp1i	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ℂfld ↾s ℕ0 ) ∈ Mnd )
25		eqid	⊢ ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) )
26		1nn0	⊢ 1 ∈ ℕ0
27	19	submbas	⊢ ( ℕ0 ∈ ( SubMnd ‘ ℂfld ) → ℕ0 = ( Base ‘ ( ℂfld ↾s ℕ0 ) ) )
28	18 27	ax-mp	⊢ ℕ0 = ( Base ‘ ( ℂfld ↾s ℕ0 ) )
29	26 28	eleqtri	⊢ 1 ∈ ( Base ‘ ( ℂfld ↾s ℕ0 ) )
30	29	a1i	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → 1 ∈ ( Base ‘ ( ℂfld ↾s ℕ0 ) ) )
31	22 24 10 12 25 30	gsummptif1n0	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) = 1 )
32		oveq2	⊢ ( 𝑑 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) → ( ( ℂfld ↾s ℕ0 ) Σg 𝑑 ) = ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) )
33	32	eqeq1d	⊢ ( 𝑑 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) → ( ( ( ℂfld ↾s ℕ0 ) Σg 𝑑 ) = 1 ↔ ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) = 1 ) )
34	31 33	syl5ibrcom	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( 𝑑 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) → ( ( ℂfld ↾s ℕ0 ) Σg 𝑑 ) = 1 ) )
35	17 34	syld	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( ( 𝑉 ‘ 𝑋 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) → ( ( ℂfld ↾s ℕ0 ) Σg 𝑑 ) = 1 ) )
36	35	ralrimiva	⊢ ( 𝜑 → ∀ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ( ( ( 𝑉 ‘ 𝑋 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) → ( ( ℂfld ↾s ℕ0 ) Σg 𝑑 ) = 1 ) )
37		eqid	⊢ ( 𝐼 mPoly 𝑅 ) = ( 𝐼 mPoly 𝑅 )
38		eqid	⊢ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
39	26	a1i	⊢ ( 𝜑 → 1 ∈ ℕ0 )
40	37 2 38 3 4 5	mvrcl	⊢ ( 𝜑 → ( 𝑉 ‘ 𝑋 ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) )
41	1 37 38 8 7 3 4 39 40	ismhp3	⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝑋 ) ∈ ( 𝐻 ‘ 1 ) ↔ ∀ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ( ( ( 𝑉 ‘ 𝑋 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) → ( ( ℂfld ↾s ℕ0 ) Σg 𝑑 ) = 1 ) ) )
42	36 41	mpbird	⊢ ( 𝜑 → ( 𝑉 ‘ 𝑋 ) ∈ ( 𝐻 ‘ 1 ) )