Theorem znle2

Description: The ordering of the Z/nZ structure. (Contributed by Mario Carneiro, 15-Jun-2015) (Revised by AV, 13-Jun-2019)

	Ref	Expression
Hypotheses	znle2.y	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
	znle2.f	⊢ 𝐹 = ( ( ℤRHom ‘ 𝑌 ) ↾ 𝑊 )
	znle2.w	⊢ 𝑊 = if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) )
	znle2.l	⊢ ≤ = ( le ‘ 𝑌 )
Assertion	znle2	⊢ ( 𝑁 ∈ ℕ0 → ≤ = ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		znle2.y	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
2		znle2.f	⊢ 𝐹 = ( ( ℤRHom ‘ 𝑌 ) ↾ 𝑊 )
3		znle2.w	⊢ 𝑊 = if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) )
4		znle2.l	⊢ ≤ = ( le ‘ 𝑌 )
5		eqid	⊢ ( RSpan ‘ ℤring ) = ( RSpan ‘ ℤring )
6		eqid	⊢ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) = ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) )
7		eqid	⊢ ( ( ℤRHom ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) ↾ 𝑊 ) = ( ( ℤRHom ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) ↾ 𝑊 )
8	5 6 1 7 3 4	znle	⊢ ( 𝑁 ∈ ℕ0 → ≤ = ( ( ( ( ℤRHom ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) ↾ 𝑊 ) ∘ ≤ ) ∘ ◡ ( ( ℤRHom ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) ↾ 𝑊 ) ) )
9	5 6 1	znzrh	⊢ ( 𝑁 ∈ ℕ0 → ( ℤRHom ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) = ( ℤRHom ‘ 𝑌 ) )
10	9	reseq1d	⊢ ( 𝑁 ∈ ℕ0 → ( ( ℤRHom ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) ↾ 𝑊 ) = ( ( ℤRHom ‘ 𝑌 ) ↾ 𝑊 ) )
11	10 2	eqtr4di	⊢ ( 𝑁 ∈ ℕ0 → ( ( ℤRHom ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) ↾ 𝑊 ) = 𝐹 )
12	11	coeq1d	⊢ ( 𝑁 ∈ ℕ0 → ( ( ( ℤRHom ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) ↾ 𝑊 ) ∘ ≤ ) = ( 𝐹 ∘ ≤ ) )
13	11	cnveqd	⊢ ( 𝑁 ∈ ℕ0 → ◡ ( ( ℤRHom ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) ↾ 𝑊 ) = ◡ 𝐹 )
14	12 13	coeq12d	⊢ ( 𝑁 ∈ ℕ0 → ( ( ( ( ℤRHom ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) ↾ 𝑊 ) ∘ ≤ ) ∘ ◡ ( ( ℤRHom ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) ↾ 𝑊 ) ) = ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 ) )
15	8 14	eqtrd	⊢ ( 𝑁 ∈ ℕ0 → ≤ = ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 ) )