Theorem psrvscacl

Description: Closure of the power series scalar multiplication operation. (Contributed by Mario Carneiro, 29-Dec-2014)

	Ref	Expression
Hypotheses	psrvscacl.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
	psrvscacl.n	⊢ · = ( ·𝑠 ‘ 𝑆 )
	psrvscacl.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	psrvscacl.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	psrvscacl.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	psrvscacl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
	psrvscacl.y	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
Assertion	psrvscacl	⊢ ( 𝜑 → ( 𝑋 · 𝐹 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		psrvscacl.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2		psrvscacl.n	⊢ · = ( ·𝑠 ‘ 𝑆 )
3		psrvscacl.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
4		psrvscacl.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
5		psrvscacl.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
6		psrvscacl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
7		psrvscacl.y	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
8		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
9	3 8	ringcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐾 )
10	9	3expb	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐾 )
11	5 10	sylan	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐾 )
12		fconst6g	⊢ ( 𝑋 ∈ 𝐾 → ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑋 } ) : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ 𝐾 )
13	6 12	syl	⊢ ( 𝜑 → ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑋 } ) : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ 𝐾 )
14		eqid	⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
15	1 3 14 4 7	psrelbas	⊢ ( 𝜑 → 𝐹 : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ 𝐾 )
16		ovex	⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
17	16	rabex	⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∈ V
18	17	a1i	⊢ ( 𝜑 → { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∈ V )
19		inidm	⊢ ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∩ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
20	11 13 15 18 18 19	off	⊢ ( 𝜑 → ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) 𝐹 ) : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ 𝐾 )
21	3	fvexi	⊢ 𝐾 ∈ V
22	21 17	elmap	⊢ ( ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) 𝐹 ) ∈ ( 𝐾 ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ↔ ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) 𝐹 ) : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ 𝐾 )
23	20 22	sylibr	⊢ ( 𝜑 → ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) 𝐹 ) ∈ ( 𝐾 ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) )
24	1 2 3 4 8 14 6 7	psrvsca	⊢ ( 𝜑 → ( 𝑋 · 𝐹 ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) 𝐹 ) )
25		reldmpsr	⊢ Rel dom mPwSer
26	25 1 4	elbasov	⊢ ( 𝐹 ∈ 𝐵 → ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) )
27	7 26	syl	⊢ ( 𝜑 → ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) )
28	27	simpld	⊢ ( 𝜑 → 𝐼 ∈ V )
29	1 3 14 4 28	psrbas	⊢ ( 𝜑 → 𝐵 = ( 𝐾 ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) )
30	23 24 29	3eltr4d	⊢ ( 𝜑 → ( 𝑋 · 𝐹 ) ∈ 𝐵 )