znle

Description: The value of the Z/nZ structure. It is defined as the quotient ring ZZ / n ZZ , with an "artificial" ordering added to make it a Toset . (In other words, Z/nZ is aring with anorder , but it is not anordered ring , which as a term implies that the order is compatible with the ring operations in some way.) (Contributed by Mario Carneiro, 14-Jun-2015) (Revised by AV, 13-Jun-2019)

	Ref	Expression
Hypotheses	znval.s	⊢ 𝑆 = ( RSpan ‘ ℤ_ring )
	znval.u	⊢ 𝑈 = ( ℤ_ring /_s ( ℤ_ring ~_QG ( 𝑆 ‘ { 𝑁 } ) ) )
	znval.y	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
	znval.f	⊢ 𝐹 = ( ( ℤRHom ‘ 𝑈 ) ↾ 𝑊 )
	znval.w	⊢ 𝑊 = if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) )
	znle.l	⊢ ≤ = ( le ‘ 𝑌 )
Assertion	znle	⊢ ( 𝑁 ∈ ℕ₀ → ≤ = ( ( 𝐹 ∘ ≤ ) ∘ ^◡ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		znval.s	⊢ 𝑆 = ( RSpan ‘ ℤ_ring )
2		znval.u	⊢ 𝑈 = ( ℤ_ring /_s ( ℤ_ring ~_QG ( 𝑆 ‘ { 𝑁 } ) ) )
3		znval.y	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
4		znval.f	⊢ 𝐹 = ( ( ℤRHom ‘ 𝑈 ) ↾ 𝑊 )
5		znval.w	⊢ 𝑊 = if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) )
6		znle.l	⊢ ≤ = ( le ‘ 𝑌 )
7		eqid	⊢ ( ( 𝐹 ∘ ≤ ) ∘ ^◡ 𝐹 ) = ( ( 𝐹 ∘ ≤ ) ∘ ^◡ 𝐹 )
8	1 2 3 4 5 7	znval	⊢ ( 𝑁 ∈ ℕ₀ → 𝑌 = ( 𝑈 sSet ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ≤ ) ∘ ^◡ 𝐹 ) ⟩ ) )
9	8	fveq2d	⊢ ( 𝑁 ∈ ℕ₀ → ( le ‘ 𝑌 ) = ( le ‘ ( 𝑈 sSet ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ≤ ) ∘ ^◡ 𝐹 ) ⟩ ) ) )
10	2	ovexi	⊢ 𝑈 ∈ V
11		fvex	⊢ ( ℤRHom ‘ 𝑈 ) ∈ V
12	11	resex	⊢ ( ( ℤRHom ‘ 𝑈 ) ↾ 𝑊 ) ∈ V
13	4 12	eqeltri	⊢ 𝐹 ∈ V
14		xrex	⊢ ℝ^* ∈ V
15	14 14	xpex	⊢ ( ℝ^* × ℝ^* ) ∈ V
16		lerelxr	⊢ ≤ ⊆ ( ℝ^* × ℝ^* )
17	15 16	ssexi	⊢ ≤ ∈ V
18	13 17	coex	⊢ ( 𝐹 ∘ ≤ ) ∈ V
19	13	cnvex	⊢ ^◡ 𝐹 ∈ V
20	18 19	coex	⊢ ( ( 𝐹 ∘ ≤ ) ∘ ^◡ 𝐹 ) ∈ V
21		pleid	⊢ le = Slot ( le ‘ ndx )
22	21	setsid	⊢ ( ( 𝑈 ∈ V ∧ ( ( 𝐹 ∘ ≤ ) ∘ ^◡ 𝐹 ) ∈ V ) → ( ( 𝐹 ∘ ≤ ) ∘ ^◡ 𝐹 ) = ( le ‘ ( 𝑈 sSet ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ≤ ) ∘ ^◡ 𝐹 ) ⟩ ) ) )
23	10 20 22	mp2an	⊢ ( ( 𝐹 ∘ ≤ ) ∘ ^◡ 𝐹 ) = ( le ‘ ( 𝑈 sSet ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ≤ ) ∘ ^◡ 𝐹 ) ⟩ ) )
24	9 6 23	3eqtr4g	⊢ ( 𝑁 ∈ ℕ₀ → ≤ = ( ( 𝐹 ∘ ≤ ) ∘ ^◡ 𝐹 ) )

Metamath Proof Explorer

Theorem znle

Proof