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

Metamath Proof Explorer

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 → ≤ = ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 ) )