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 } ) ∈ 𝐵 )