Theorem 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	|- S = ( RSpan ` ZZring )
	znval.u	|- U = ( ZZring /s ( ZZring ~QG ( S ` { N } ) ) )
	znval.y	|- Y = ( Z/nZ ` N )
	znval.f	|- F = ( ( ZRHom ` U ) |` W )
	znval.w	|- W = if ( N = 0 , ZZ , ( 0 ..^ N ) )
	znle.l	|- .<_ = ( le ` Y )
Assertion	znle	|- ( N e. NN0 -> .<_ = ( ( F o. <_ ) o. `' F ) )

Proof

Step	Hyp	Ref	Expression
1		znval.s	|- S = ( RSpan ` ZZring )
2		znval.u	|- U = ( ZZring /s ( ZZring ~QG ( S ` { N } ) ) )
3		znval.y	|- Y = ( Z/nZ ` N )
4		znval.f	|- F = ( ( ZRHom ` U ) |` W )
5		znval.w	|- W = if ( N = 0 , ZZ , ( 0 ..^ N ) )
6		znle.l	|- .<_ = ( le ` Y )
7		eqid	|- ( ( F o. <_ ) o. `' F ) = ( ( F o. <_ ) o. `' F )
8	1 2 3 4 5 7	znval	|- ( N e. NN0 -> Y = ( U sSet <. ( le ` ndx ) , ( ( F o. <_ ) o. `' F ) >. ) )
9	8	fveq2d	|- ( N e. NN0 -> ( le ` Y ) = ( le ` ( U sSet <. ( le ` ndx ) , ( ( F o. <_ ) o. `' F ) >. ) ) )
10	2	ovexi	|- U e. _V
11		fvex	|- ( ZRHom ` U ) e. _V
12	11	resex	|- ( ( ZRHom ` U ) |` W ) e. _V
13	4 12	eqeltri	|- F e. _V
14		xrex	|- RR* e. _V
15	14 14	xpex	|- ( RR* X. RR* ) e. _V
16		lerelxr	|- <_ C_ ( RR* X. RR* )
17	15 16	ssexi	|- <_ e. _V
18	13 17	coex	|- ( F o. <_ ) e. _V
19	13	cnvex	|- `' F e. _V
20	18 19	coex	|- ( ( F o. <_ ) o. `' F ) e. _V
21		pleid	|- le = Slot ( le ` ndx )
22	21	setsid	|- ( ( U e. _V /\ ( ( F o. <_ ) o. `' F ) e. _V ) -> ( ( F o. <_ ) o. `' F ) = ( le ` ( U sSet <. ( le ` ndx ) , ( ( F o. <_ ) o. `' F ) >. ) ) )
23	10 20 22	mp2an	|- ( ( F o. <_ ) o. `' F ) = ( le ` ( U sSet <. ( le ` ndx ) , ( ( F o. <_ ) o. `' F ) >. ) )
24	9 6 23	3eqtr4g	|- ( N e. NN0 -> .<_ = ( ( F o. <_ ) o. `' F ) )