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 ) , ≤ ⟩ ) )