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

Metamath Proof Explorer

Theorem psr0cl

Description: The zero element of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypotheses psrgrp.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
psrgrp.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
psrgrp.r ⊢ ( 𝜑 → 𝑅 ∈ Grp )
psr0cl.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
psr0cl.o ⊢ 0 = ( 0g ‘ 𝑅 )
psr0cl.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
Assertion psr0cl ( 𝜑 → ( 𝐷 × { 0 } ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 psrgrp.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psrgrp.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
3 psrgrp.r ⊢ ( 𝜑 → 𝑅 ∈ Grp )
4 psr0cl.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
5 psr0cl.o ⊢ 0 = ( 0g ‘ 𝑅 )
6 psr0cl.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
7 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
8 7 5 grpidcl ⊢ ( 𝑅 ∈ Grp → 0 ∈ ( Base ‘ 𝑅 ) )
9 fconst6g ⊢ ( 0 ∈ ( Base ‘ 𝑅 ) → ( 𝐷 × { 0 } ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
10 3 8 9 3syl ⊢ ( 𝜑 → ( 𝐷 × { 0 } ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
11 fvex ⊢ ( Base ‘ 𝑅 ) ∈ V
12 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
13 4 12 rabex2 ⊢ 𝐷 ∈ V
14 11 13 elmap ⊢ ( ( 𝐷 × { 0 } ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) ↔ ( 𝐷 × { 0 } ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
15 10 14 sylibr ⊢ ( 𝜑 → ( 𝐷 × { 0 } ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
16 1 7 4 6 2 psrbas ⊢ ( 𝜑 → 𝐵 = ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
17 15 16 eleqtrrd ⊢ ( 𝜑 → ( 𝐷 × { 0 } ) ∈ 𝐵 )