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

Metamath Proof Explorer

Theorem psrnzr

Description: The ring of power series over a nonzero ring form a nonzero ring. (Contributed by Thierry Arnoux, 4-May-2026)

Ref Expression
Hypotheses psrnzr.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
psrnzr.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
psrnzr.r ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
Assertion psrnzr ( 𝜑 → 𝑆 ∈ NzRing )

Proof

Step Hyp Ref Expression
1 psrnzr.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psrnzr.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
3 psrnzr.r ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
4 nzrring ⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
5 3 4 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
6 1 2 5 psrring ⊢ ( 𝜑 → 𝑆 ∈ Ring )
7 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
8 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
9 7 8 nzrnz ⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
10 3 9 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
11 eqid ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
12 eqid ⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
13 1 2 5 11 8 7 12 psr1 ⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
14 simpr ⊢ ( ( 𝜑 ∧ 𝑥 = ( 𝐼 × { 0 } ) ) → 𝑥 = ( 𝐼 × { 0 } ) )
15 14 iftrued ⊢ ( ( 𝜑 ∧ 𝑥 = ( 𝐼 × { 0 } ) ) → if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
16 11 psrbag0 ⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 × { 0 } ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
17 2 16 syl ⊢ ( 𝜑 → ( 𝐼 × { 0 } ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
18 fvexd ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ V )
19 13 15 17 18 fvmptd ⊢ ( 𝜑 → ( ( 1r ‘ 𝑆 ) ‘ ( 𝐼 × { 0 } ) ) = ( 1r ‘ 𝑅 ) )
20 5 ringgrpd ⊢ ( 𝜑 → 𝑅 ∈ Grp )
21 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
22 1 2 20 11 8 21 psr0 ⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) = ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( 0g ‘ 𝑅 ) } ) )
23 22 fveq1d ⊢ ( 𝜑 → ( ( 0g ‘ 𝑆 ) ‘ ( 𝐼 × { 0 } ) ) = ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( 0g ‘ 𝑅 ) } ) ‘ ( 𝐼 × { 0 } ) ) )
24 fvex ⊢ ( 0g ‘ 𝑅 ) ∈ V
25 24 fvconst2 ⊢ ( ( 𝐼 × { 0 } ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } → ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( 0g ‘ 𝑅 ) } ) ‘ ( 𝐼 × { 0 } ) ) = ( 0g ‘ 𝑅 ) )
26 17 25 syl ⊢ ( 𝜑 → ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( 0g ‘ 𝑅 ) } ) ‘ ( 𝐼 × { 0 } ) ) = ( 0g ‘ 𝑅 ) )
27 23 26 eqtrd ⊢ ( 𝜑 → ( ( 0g ‘ 𝑆 ) ‘ ( 𝐼 × { 0 } ) ) = ( 0g ‘ 𝑅 ) )
28 10 19 27 3netr4d ⊢ ( 𝜑 → ( ( 1r ‘ 𝑆 ) ‘ ( 𝐼 × { 0 } ) ) ≠ ( ( 0g ‘ 𝑆 ) ‘ ( 𝐼 × { 0 } ) ) )
29 fveq1 ⊢ ( ( 1r ‘ 𝑆 ) = ( 0g ‘ 𝑆 ) → ( ( 1r ‘ 𝑆 ) ‘ ( 𝐼 × { 0 } ) ) = ( ( 0g ‘ 𝑆 ) ‘ ( 𝐼 × { 0 } ) ) )
30 29 necon3i ⊢ ( ( ( 1r ‘ 𝑆 ) ‘ ( 𝐼 × { 0 } ) ) ≠ ( ( 0g ‘ 𝑆 ) ‘ ( 𝐼 × { 0 } ) ) → ( 1r ‘ 𝑆 ) ≠ ( 0g ‘ 𝑆 ) )
31 28 30 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) ≠ ( 0g ‘ 𝑆 ) )
32 12 21 isnzr ⊢ ( 𝑆 ∈ NzRing ↔ ( 𝑆 ∈ Ring ∧ ( 1r ‘ 𝑆 ) ≠ ( 0g ‘ 𝑆 ) ) )
33 6 31 32 sylanbrc ⊢ ( 𝜑 → 𝑆 ∈ NzRing )