Metamath Proof Explorer

Theorem mplmon

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

Ref Expression
Hypotheses mplmon.s ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
mplmon.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
mplmon.z ⊢ 0 = ( 0g ‘ 𝑅 )
mplmon.o ⊢ 1 = ( 1r ‘ 𝑅 )
mplmon.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
mplmon.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
mplmon.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
mplmon.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
Assertion mplmon ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 mplmon.s ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2 mplmon.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
3 mplmon.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 mplmon.o ⊢ 1 = ( 1r ‘ 𝑅 )
5 mplmon.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
6 mplmon.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
7 mplmon.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
8 mplmon.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
9 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
10 9 4 ringidcl ⊢ ( 𝑅 ∈ Ring → 1 ∈ ( Base ‘ 𝑅 ) )
11 9 3 ring0cl ⊢ ( 𝑅 ∈ Ring → 0 ∈ ( Base ‘ 𝑅 ) )
12 10 11 ifcld ⊢ ( 𝑅 ∈ Ring → if ( 𝑦 = 𝑋 , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) )
13 7 12 syl ⊢ ( 𝜑 → if ( 𝑦 = 𝑋 , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → if ( 𝑦 = 𝑋 , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) )
15 14 fmpttd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
16 fvex ⊢ ( Base ‘ 𝑅 ) ∈ V
17 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
18 5 17 rabex2 ⊢ 𝐷 ∈ V
19 16 18 elmap ⊢ ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) ↔ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
20 15 19 sylibr ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
21 eqid ⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
22 eqid ⊢ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
23 21 9 5 22 6 psrbas ⊢ ( 𝜑 → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
24 20 23 eleqtrrd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
25 18 mptex ⊢ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ V
26 funmpt ⊢ Fun ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) )
27 3 fvexi ⊢ 0 ∈ V
28 25 26 27 3pm3.2i ⊢ ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ V ∧ Fun ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∧ 0 ∈ V )
29 28 a1i ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ V ∧ Fun ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∧ 0 ∈ V ) )
30 snfi ⊢ { 𝑋 } ∈ Fin
31 30 a1i ⊢ ( 𝜑 → { 𝑋 } ∈ Fin )
32 eldifsni ⊢ ( 𝑦 ∈ ( 𝐷 ∖ { 𝑋 } ) → 𝑦 ≠ 𝑋 )
33 32 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐷 ∖ { 𝑋 } ) ) → 𝑦 ≠ 𝑋 )
34 33 neneqd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐷 ∖ { 𝑋 } ) ) → ¬ 𝑦 = 𝑋 )
35 34 iffalsed ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐷 ∖ { 𝑋 } ) ) → if ( 𝑦 = 𝑋 , 1 , 0 ) = 0 )
36 18 a1i ⊢ ( 𝜑 → 𝐷 ∈ V )
37 35 36 suppss2 ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) supp 0 ) ⊆ { 𝑋 } )
38 suppssfifsupp ⊢ ( ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ V ∧ Fun ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∧ 0 ∈ V ) ∧ ( { 𝑋 } ∈ Fin ∧ ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) supp 0 ) ⊆ { 𝑋 } ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) finSupp 0 )
39 29 31 37 38 syl12anc ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) finSupp 0 )
40 1 21 22 3 2 mplelbas ⊢ ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ 𝐵 ↔ ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) finSupp 0 ) )
41 24 39 40 sylanbrc ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ 𝐵 )