Metamath Proof Explorer

Theorem znzrhfo

Description: The ZZ ring homomorphism is a surjection onto ZZ / n ZZ . (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Hypotheses znzrhfo.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
znzrhfo.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
znzrhfo.2 ⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
Assertion znzrhfo ( 𝑁 ∈ ℕ0 → 𝐿 : ℤ –onto→ 𝐵 )

Proof

Step Hyp Ref Expression
1 znzrhfo.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
2 znzrhfo.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
3 znzrhfo.2 ⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
4 eqidd ⊢ ( 𝑁 ∈ ℕ0 → ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) = ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) )
5 zringbas ⊢ ℤ = ( Base ‘ ℤring )
6 5 a1i ⊢ ( 𝑁 ∈ ℕ0 → ℤ = ( Base ‘ ℤring ) )
7 eqid ⊢ ( 𝑥 ∈ ℤ ↦ [ 𝑥 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) = ( 𝑥 ∈ ℤ ↦ [ 𝑥 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) )
8 ovexd ⊢ ( 𝑁 ∈ ℕ0 → ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ∈ V )
9 zringring ⊢ ℤring ∈ Ring
10 9 a1i ⊢ ( 𝑁 ∈ ℕ0 → ℤring ∈ Ring )
11 4 6 7 8 10 quslem ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑥 ∈ ℤ ↦ [ 𝑥 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) : ℤ –onto→ ( ℤ / ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) )
12 eqid ⊢ ( RSpan ‘ ℤring ) = ( RSpan ‘ ℤring )
13 eqid ⊢ ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) = ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) )
14 12 1 13 znbas ⊢ ( 𝑁 ∈ ℕ0 → ( ℤ / ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) = ( Base ‘ 𝑌 ) )
15 14 2 eqtr4di ⊢ ( 𝑁 ∈ ℕ0 → ( ℤ / ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) = 𝐵 )
16 foeq3 ⊢ ( ( ℤ / ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) = 𝐵 → ( ( 𝑥 ∈ ℤ ↦ [ 𝑥 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) : ℤ –onto→ ( ℤ / ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ↔ ( 𝑥 ∈ ℤ ↦ [ 𝑥 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) : ℤ –onto→ 𝐵 ) )
17 15 16 syl ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑥 ∈ ℤ ↦ [ 𝑥 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) : ℤ –onto→ ( ℤ / ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ↔ ( 𝑥 ∈ ℤ ↦ [ 𝑥 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) : ℤ –onto→ 𝐵 ) )
18 11 17 mpbid ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑥 ∈ ℤ ↦ [ 𝑥 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) : ℤ –onto→ 𝐵 )
19 12 13 1 3 znzrh2 ⊢ ( 𝑁 ∈ ℕ0 → 𝐿 = ( 𝑥 ∈ ℤ ↦ [ 𝑥 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) )
20 foeq1 ⊢ ( 𝐿 = ( 𝑥 ∈ ℤ ↦ [ 𝑥 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) → ( 𝐿 : ℤ –onto→ 𝐵 ↔ ( 𝑥 ∈ ℤ ↦ [ 𝑥 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) : ℤ –onto→ 𝐵 ) )
21 19 20 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐿 : ℤ –onto→ 𝐵 ↔ ( 𝑥 ∈ ℤ ↦ [ 𝑥 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) : ℤ –onto→ 𝐵 ) )
22 18 21 mpbird ⊢ ( 𝑁 ∈ ℕ0 → 𝐿 : ℤ –onto→ 𝐵 )