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

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 ⊢ ( 𝑋 ∈ 𝐾 → ( { 𝑓 ∈ ( ℕ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 ⊢ ( 𝜑 → ( 𝑋 · 𝐹 ) ∈ 𝐵 )