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

Metamath Proof Explorer

Theorem mvrcl

Description: A power series variable is a polynomial. (Contributed by Mario Carneiro, 9-Jan-2015)

Ref Expression
Hypotheses mvrcl.s ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
mvrcl.v ⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
mvrcl.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
mvrcl.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
mvrcl.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
mvrcl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
Assertion mvrcl ( 𝜑 → ( 𝑉 ‘ 𝑋 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 mvrcl.s ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2 mvrcl.v ⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
3 mvrcl.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
4 mvrcl.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
5 mvrcl.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
6 mvrcl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
7 eqid ⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
8 eqid ⊢ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
9 7 2 8 4 5 6 mvrcl2 ⊢ ( 𝜑 → ( 𝑉 ‘ 𝑋 ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
10 fvexd ⊢ ( 𝜑 → ( 𝑉 ‘ 𝑋 ) ∈ V )
11 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
12 eqid ⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
13 7 11 12 8 9 psrelbas ⊢ ( 𝜑 → ( 𝑉 ‘ 𝑋 ) : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
14 13 ffund ⊢ ( 𝜑 → Fun ( 𝑉 ‘ 𝑋 ) )
15 fvexd ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ V )
16 snfi ⊢ { ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) } ∈ Fin
17 16 a1i ⊢ ( 𝜑 → { ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) } ∈ Fin )
18 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
19 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
20 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∖ { ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) } ) ) → 𝐼 ∈ 𝑊 )
21 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∖ { ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) } ) ) → 𝑅 ∈ Ring )
22 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∖ { ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) } ) ) → 𝑋 ∈ 𝐼 )
23 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∖ { ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) } ) ) → 𝑥 ∈ ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∖ { ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) } ) )
24 eldifsn ⊢ ( 𝑥 ∈ ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∖ { ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) } ) ↔ ( 𝑥 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∧ 𝑥 ≠ ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) )
25 23 24 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∖ { ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) } ) ) → ( 𝑥 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∧ 𝑥 ≠ ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) )
26 25 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∖ { ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) } ) ) → 𝑥 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } )
27 2 12 18 19 20 21 22 26 mvrval2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∖ { ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) } ) ) → ( ( 𝑉 ‘ 𝑋 ) ‘ 𝑥 ) = if ( 𝑥 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
28 25 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∖ { ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) } ) ) → 𝑥 ≠ ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) )
29 28 neneqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∖ { ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) } ) ) → ¬ 𝑥 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) )
30 29 iffalsed ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∖ { ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) } ) ) → if ( 𝑥 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
31 27 30 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∖ { ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) } ) ) → ( ( 𝑉 ‘ 𝑋 ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) )
32 13 31 suppss ⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝑋 ) supp ( 0g ‘ 𝑅 ) ) ⊆ { ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) } )
33 suppssfifsupp ⊢ ( ( ( ( 𝑉 ‘ 𝑋 ) ∈ V ∧ Fun ( 𝑉 ‘ 𝑋 ) ∧ ( 0g ‘ 𝑅 ) ∈ V ) ∧ ( { ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) } ∈ Fin ∧ ( ( 𝑉 ‘ 𝑋 ) supp ( 0g ‘ 𝑅 ) ) ⊆ { ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) } ) ) → ( 𝑉 ‘ 𝑋 ) finSupp ( 0g ‘ 𝑅 ) )
34 10 14 15 17 32 33 syl32anc ⊢ ( 𝜑 → ( 𝑉 ‘ 𝑋 ) finSupp ( 0g ‘ 𝑅 ) )
35 1 7 8 18 3 mplelbas ⊢ ( ( 𝑉 ‘ 𝑋 ) ∈ 𝐵 ↔ ( ( 𝑉 ‘ 𝑋 ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ ( 𝑉 ‘ 𝑋 ) finSupp ( 0g ‘ 𝑅 ) ) )
36 9 34 35 sylanbrc ⊢ ( 𝜑 → ( 𝑉 ‘ 𝑋 ) ∈ 𝐵 )