Theorem psr1cl

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

	Ref	Expression
Hypotheses	psrring.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
	psrring.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	psrring.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	psr1cl.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
	psr1cl.z	⊢ 0 = ( 0g ‘ 𝑅 )
	psr1cl.o	⊢ 1 = ( 1r ‘ 𝑅 )
	psr1cl.u	⊢ 𝑈 = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) )
	psr1cl.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
Assertion	psr1cl	⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		psrring.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2		psrring.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
3		psrring.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
4		psr1cl.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
5		psr1cl.z	⊢ 0 = ( 0g ‘ 𝑅 )
6		psr1cl.o	⊢ 1 = ( 1r ‘ 𝑅 )
7		psr1cl.u	⊢ 𝑈 = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) )
8		psr1cl.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
9		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
10	9 6	ringidcl	⊢ ( 𝑅 ∈ Ring → 1 ∈ ( Base ‘ 𝑅 ) )
11	9 5	ring0cl	⊢ ( 𝑅 ∈ Ring → 0 ∈ ( Base ‘ 𝑅 ) )
12	10 11	ifcld	⊢ ( 𝑅 ∈ Ring → if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) )
13	3 12	syl	⊢ ( 𝜑 → if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) )
14	13	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) )
15	14 7	fmptd	⊢ ( 𝜑 → 𝑈 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
16		fvex	⊢ ( Base ‘ 𝑅 ) ∈ V
17		ovex	⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
18	4 17	rabex2	⊢ 𝐷 ∈ V
19	16 18	elmap	⊢ ( 𝑈 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) ↔ 𝑈 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
20	15 19	sylibr	⊢ ( 𝜑 → 𝑈 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
21	1 9 4 8 2	psrbas	⊢ ( 𝜑 → 𝐵 = ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
22	20 21	eleqtrrd	⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )