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

Metamath Proof Explorer

Theorem znval2

Description: Self-referential expression for the Z/nZ structure. (Contributed by Mario Carneiro, 14-Jun-2015) (Revised by AV, 13-Jun-2019)

Ref Expression
Hypotheses znval2.s ⊢ 𝑆 = ( RSpan ‘ ℤring )
znval2.u ⊢ 𝑈 = ( ℤring /s ( ℤring ~QG ( 𝑆 ‘ { 𝑁 } ) ) )
znval2.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
znval2.l ⊢ ≤ = ( le ‘ 𝑌 )
Assertion znval2 ( 𝑁 ∈ ℕ0 → 𝑌 = ( 𝑈 sSet ⟨ ( le ‘ ndx ) , ≤ ⟩ ) )

Proof

Step Hyp Ref Expression
1 znval2.s ⊢ 𝑆 = ( RSpan ‘ ℤring )
2 znval2.u ⊢ 𝑈 = ( ℤring /s ( ℤring ~QG ( 𝑆 ‘ { 𝑁 } ) ) )
3 znval2.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
4 znval2.l ⊢ ≤ = ( le ‘ 𝑌 )
5 eqid ⊢ ( ( ℤRHom ‘ 𝑈 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) = ( ( ℤRHom ‘ 𝑈 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) )
6 eqid ⊢ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) = if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) )
7 eqid ⊢ ( ( ( ( ℤRHom ‘ 𝑈 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) ∘ ≤ ) ∘ ◡ ( ( ℤRHom ‘ 𝑈 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) ) = ( ( ( ( ℤRHom ‘ 𝑈 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) ∘ ≤ ) ∘ ◡ ( ( ℤRHom ‘ 𝑈 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) )
8 1 2 3 5 6 7 znval ⊢ ( 𝑁 ∈ ℕ0 → 𝑌 = ( 𝑈 sSet ⟨ ( le ‘ ndx ) , ( ( ( ( ℤRHom ‘ 𝑈 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) ∘ ≤ ) ∘ ◡ ( ( ℤRHom ‘ 𝑈 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) ) ⟩ ) )
9 1 2 3 5 6 4 znle ⊢ ( 𝑁 ∈ ℕ0 → ≤ = ( ( ( ( ℤRHom ‘ 𝑈 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) ∘ ≤ ) ∘ ◡ ( ( ℤRHom ‘ 𝑈 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) ) )
10 9 opeq2d ⊢ ( 𝑁 ∈ ℕ0 → ⟨ ( le ‘ ndx ) , ≤ ⟩ = ⟨ ( le ‘ ndx ) , ( ( ( ( ℤRHom ‘ 𝑈 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) ∘ ≤ ) ∘ ◡ ( ( ℤRHom ‘ 𝑈 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) ) ⟩ )
11 10 oveq2d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑈 sSet ⟨ ( le ‘ ndx ) , ≤ ⟩ ) = ( 𝑈 sSet ⟨ ( le ‘ ndx ) , ( ( ( ( ℤRHom ‘ 𝑈 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) ∘ ≤ ) ∘ ◡ ( ( ℤRHom ‘ 𝑈 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) ) ⟩ ) )
12 8 11 eqtr4d ⊢ ( 𝑁 ∈ ℕ0 → 𝑌 = ( 𝑈 sSet ⟨ ( le ‘ ndx ) , ≤ ⟩ ) )