Theorem psr0

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 )
	psr0.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
	psr0.o	⊢ 𝑂 = ( 0g ‘ 𝑅 )
	psr0.z	⊢ 0 = ( 0g ‘ 𝑆 )
Assertion	psr0	⊢ ( 𝜑 → 0 = ( 𝐷 × { 𝑂 } ) )

Proof

Step	Hyp	Ref	Expression
1		psrgrp.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2		psrgrp.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
3		psrgrp.r	⊢ ( 𝜑 → 𝑅 ∈ Grp )
4		psr0.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
5		psr0.o	⊢ 𝑂 = ( 0g ‘ 𝑅 )
6		psr0.z	⊢ 0 = ( 0g ‘ 𝑆 )
7		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
8		eqid	⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
9	1 2 3 4 5 7	psr0cl	⊢ ( 𝜑 → ( 𝐷 × { 𝑂 } ) ∈ ( Base ‘ 𝑆 ) )
10	1 2 3 4 5 7 8 9	psr0lid	⊢ ( 𝜑 → ( ( 𝐷 × { 𝑂 } ) ( +g ‘ 𝑆 ) ( 𝐷 × { 𝑂 } ) ) = ( 𝐷 × { 𝑂 } ) )
11	1 2 3	psrgrp	⊢ ( 𝜑 → 𝑆 ∈ Grp )
12	7 8 6	grpid	⊢ ( ( 𝑆 ∈ Grp ∧ ( 𝐷 × { 𝑂 } ) ∈ ( Base ‘ 𝑆 ) ) → ( ( ( 𝐷 × { 𝑂 } ) ( +g ‘ 𝑆 ) ( 𝐷 × { 𝑂 } ) ) = ( 𝐷 × { 𝑂 } ) ↔ 0 = ( 𝐷 × { 𝑂 } ) ) )
13	11 9 12	syl2anc	⊢ ( 𝜑 → ( ( ( 𝐷 × { 𝑂 } ) ( +g ‘ 𝑆 ) ( 𝐷 × { 𝑂 } ) ) = ( 𝐷 × { 𝑂 } ) ↔ 0 = ( 𝐷 × { 𝑂 } ) ) )
14	10 13	mpbid	⊢ ( 𝜑 → 0 = ( 𝐷 × { 𝑂 } ) )