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

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 ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ 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 ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ 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 ) ) )