This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 imbitrrid ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ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 39 40 ismhp3 ⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝑋 ) ∈ ( 𝐻 ‘ 1 ) ↔ ∀ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ( ( ( 𝑉 ‘ 𝑋 ) ‘ 𝑑 ) ≠ ( 0g ‘ 𝑅 ) → ( ( ℂfld ↾s ℕ0 ) Σg 𝑑 ) = 1 ) ) )
42 36 41 mpbird ⊢ ( 𝜑 → ( 𝑉 ‘ 𝑋 ) ∈ ( 𝐻 ‘ 1 ) )