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	⊢ ( 𝜑 → ( 𝑉 ‘ 𝑋 ) ∈ 𝐵 )