Theorem psr0lid

Description: The zero element of the ring of power series is a left identity. (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 ‘ 𝑆 )
	psr0lid.p	⊢ + = ( +g ‘ 𝑆 )
	psr0lid.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	psr0lid	⊢ ( 𝜑 → ( ( 𝐷 × { 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		psr0lid.p	⊢ + = ( +g ‘ 𝑆 )
8		psr0lid.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
9		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
10	1 2 3 4 5 6	psr0cl	⊢ ( 𝜑 → ( 𝐷 × { 0 } ) ∈ 𝐵 )
11	1 6 9 7 10 8	psradd	⊢ ( 𝜑 → ( ( 𝐷 × { 0 } ) + 𝑋 ) = ( ( 𝐷 × { 0 } ) ∘f ( +g ‘ 𝑅 ) 𝑋 ) )
12		ovex	⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
13	4 12	rabex2	⊢ 𝐷 ∈ V
14	13	a1i	⊢ ( 𝜑 → 𝐷 ∈ V )
15		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
16	1 15 4 6 8	psrelbas	⊢ ( 𝜑 → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
17	5	fvexi	⊢ 0 ∈ V
18	17	a1i	⊢ ( 𝜑 → 0 ∈ V )
19	15 9 5	grplid	⊢ ( ( 𝑅 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 0 ( +g ‘ 𝑅 ) 𝑥 ) = 𝑥 )
20	3 19	sylan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 0 ( +g ‘ 𝑅 ) 𝑥 ) = 𝑥 )
21	14 16 18 20	caofid0l	⊢ ( 𝜑 → ( ( 𝐷 × { 0 } ) ∘f ( +g ‘ 𝑅 ) 𝑋 ) = 𝑋 )
22	11 21	eqtrd	⊢ ( 𝜑 → ( ( 𝐷 × { 0 } ) + 𝑋 ) = 𝑋 )