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	|- S = ( RSpan ` ZZring )
	znval2.u	|- U = ( ZZring /s ( ZZring ~QG ( S ` { N } ) ) )
	znval2.y	|- Y = ( Z/nZ ` N )
	znval2.l	|- .<_ = ( le ` Y )
Assertion	znval2	|- ( N e. NN0 -> Y = ( U sSet <. ( le ` ndx ) , .<_ >. ) )

Proof

Step	Hyp	Ref	Expression
1		znval2.s	|- S = ( RSpan ` ZZring )
2		znval2.u	|- U = ( ZZring /s ( ZZring ~QG ( S ` { N } ) ) )
3		znval2.y	|- Y = ( Z/nZ ` N )
4		znval2.l	|- .<_ = ( le ` Y )
5		eqid	|- ( ( ZRHom ` U ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) = ( ( ZRHom ` U ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) )
6		eqid	|- if ( N = 0 , ZZ , ( 0 ..^ N ) ) = if ( N = 0 , ZZ , ( 0 ..^ N ) )
7		eqid	|- ( ( ( ( ZRHom ` U ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) o. <_ ) o. `' ( ( ZRHom ` U ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) ) = ( ( ( ( ZRHom ` U ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) o. <_ ) o. `' ( ( ZRHom ` U ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) )
8	1 2 3 5 6 7	znval	|- ( N e. NN0 -> Y = ( U sSet <. ( le ` ndx ) , ( ( ( ( ZRHom ` U ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) o. <_ ) o. `' ( ( ZRHom ` U ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) ) >. ) )
9	1 2 3 5 6 4	znle	|- ( N e. NN0 -> .<_ = ( ( ( ( ZRHom ` U ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) o. <_ ) o. `' ( ( ZRHom ` U ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) ) )
10	9	opeq2d	|- ( N e. NN0 -> <. ( le ` ndx ) , .<_ >. = <. ( le ` ndx ) , ( ( ( ( ZRHom ` U ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) o. <_ ) o. `' ( ( ZRHom ` U ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) ) >. )
11	10	oveq2d	|- ( N e. NN0 -> ( U sSet <. ( le ` ndx ) , .<_ >. ) = ( U sSet <. ( le ` ndx ) , ( ( ( ( ZRHom ` U ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) o. <_ ) o. `' ( ( ZRHom ` U ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) ) >. ) )
12	8 11	eqtr4d	|- ( N e. NN0 -> Y = ( U sSet <. ( le ` ndx ) , .<_ >. ) )