Metamath Proof Explorer


Theorem psr1

Description: The identity element of the ring of power series. (Contributed by Mario Carneiro, 8-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 psrring.s 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psrring.i ( 𝜑𝐼𝑉 )
3 psrring.r ( 𝜑𝑅 ∈ Ring )
4 psr1.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
5 psr1.z 0 = ( 0g𝑅 )
6 psr1.o 1 = ( 1r𝑅 )
7 psr1.u 𝑈 = ( 1r𝑆 )
8 eqid ( 𝑥𝐷 ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) = ( 𝑥𝐷 ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) )
9 eqid ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
10 1 2 3 4 5 6 8 9 psr1cl ( 𝜑 → ( 𝑥𝐷 ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) ∈ ( Base ‘ 𝑆 ) )
11 2 adantr ( ( 𝜑𝑦 ∈ ( Base ‘ 𝑆 ) ) → 𝐼𝑉 )
12 3 adantr ( ( 𝜑𝑦 ∈ ( Base ‘ 𝑆 ) ) → 𝑅 ∈ Ring )
13 eqid ( .r𝑆 ) = ( .r𝑆 )
14 simpr ( ( 𝜑𝑦 ∈ ( Base ‘ 𝑆 ) ) → 𝑦 ∈ ( Base ‘ 𝑆 ) )
15 1 11 12 4 5 6 8 9 13 14 psrlidm ( ( 𝜑𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝑥𝐷 ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) ( .r𝑆 ) 𝑦 ) = 𝑦 )
16 1 11 12 4 5 6 8 9 13 14 psrridm ( ( 𝜑𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑦 ( .r𝑆 ) ( 𝑥𝐷 ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) ) = 𝑦 )
17 15 16 jca ( ( 𝜑𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( ( ( 𝑥𝐷 ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) ( .r𝑆 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r𝑆 ) ( 𝑥𝐷 ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) ) = 𝑦 ) )
18 17 ralrimiva ( 𝜑 → ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( ( ( 𝑥𝐷 ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) ( .r𝑆 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r𝑆 ) ( 𝑥𝐷 ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) ) = 𝑦 ) )
19 1 2 3 psrring ( 𝜑𝑆 ∈ Ring )
20 9 13 7 isringid ( 𝑆 ∈ Ring → ( ( ( 𝑥𝐷 ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) ∈ ( Base ‘ 𝑆 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( ( ( 𝑥𝐷 ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) ( .r𝑆 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r𝑆 ) ( 𝑥𝐷 ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) ) = 𝑦 ) ) ↔ 𝑈 = ( 𝑥𝐷 ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) ) )
21 19 20 syl ( 𝜑 → ( ( ( 𝑥𝐷 ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) ∈ ( Base ‘ 𝑆 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( ( ( 𝑥𝐷 ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) ( .r𝑆 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r𝑆 ) ( 𝑥𝐷 ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) ) = 𝑦 ) ) ↔ 𝑈 = ( 𝑥𝐷 ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) ) )
22 10 18 21 mpbi2and ( 𝜑𝑈 = ( 𝑥𝐷 ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) )