Metamath Proof Explorer


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 ( 𝑋𝐾 → ( { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } × { 𝑋 } ) : { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ⟶ 𝐾 )
13 6 12 syl ( 𝜑 → ( { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } × { 𝑋 } ) : { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ⟶ 𝐾 )
14 eqid { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
15 1 3 14 4 7 psrelbas ( 𝜑𝐹 : { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ⟶ 𝐾 )
16 ovex ( ℕ0m 𝐼 ) ∈ V
17 16 rabex { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∈ V
18 17 a1i ( 𝜑 → { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∈ V )
19 inidm ( { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∩ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
20 11 13 15 18 18 19 off ( 𝜑 → ( ( { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } × { 𝑋 } ) ∘f ( .r𝑅 ) 𝐹 ) : { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ⟶ 𝐾 )
21 3 fvexi 𝐾 ∈ V
22 21 17 elmap ( ( ( { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } × { 𝑋 } ) ∘f ( .r𝑅 ) 𝐹 ) ∈ ( 𝐾m { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ↔ ( ( { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } × { 𝑋 } ) ∘f ( .r𝑅 ) 𝐹 ) : { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ⟶ 𝐾 )
23 20 22 sylibr ( 𝜑 → ( ( { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } × { 𝑋 } ) ∘f ( .r𝑅 ) 𝐹 ) ∈ ( 𝐾m { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) )
24 1 2 3 4 8 14 6 7 psrvsca ( 𝜑 → ( 𝑋 · 𝐹 ) = ( ( { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ 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 { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) )
30 23 24 29 3eltr4d ( 𝜑 → ( 𝑋 · 𝐹 ) ∈ 𝐵 )