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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )