Theorem znbaslem

Description: Lemma for znbas . (Contributed by Mario Carneiro, 14-Jun-2015) (Revised by Mario Carneiro, 14-Aug-2015) (Revised by AV, 13-Jun-2019) (Revised by AV, 9-Sep-2021)

	Ref	Expression
Hypotheses	znval2.s	|- S = ( RSpan ` ZZring )
	znval2.u	|- U = ( ZZring /s ( ZZring ~QG ( S ` { N } ) ) )
	znval2.y	|- Y = ( Z/nZ ` N )
	znbaslem.e	|- E = Slot K
	znbaslem.k	|- K e. NN
	znbaslem.l	|- K < ; 1 0
Assertion	znbaslem	|- ( N e. NN0 -> ( E ` U ) = ( E ` Y ) )

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		znbaslem.e	|- E = Slot K
5		znbaslem.k	|- K e. NN
6		znbaslem.l	|- K < ; 1 0
7	4 5	ndxid	|- E = Slot ( E ` ndx )
8	5	nnrei	|- K e. RR
9	8 6	ltneii	|- K =/= ; 1 0
10	4 5	ndxarg	|- ( E ` ndx ) = K
11		plendx	|- ( le ` ndx ) = ; 1 0
12	10 11	neeq12i	|- ( ( E ` ndx ) =/= ( le ` ndx ) <-> K =/= ; 1 0 )
13	9 12	mpbir	|- ( E ` ndx ) =/= ( le ` ndx )
14	7 13	setsnid	|- ( E ` U ) = ( E ` ( U sSet <. ( le ` ndx ) , ( le ` Y ) >. ) )
15		eqid	|- ( le ` Y ) = ( le ` Y )
16	1 2 3 15	znval2	|- ( N e. NN0 -> Y = ( U sSet <. ( le ` ndx ) , ( le ` Y ) >. ) )
17	16	fveq2d	|- ( N e. NN0 -> ( E ` Y ) = ( E ` ( U sSet <. ( le ` ndx ) , ( le ` Y ) >. ) ) )
18	14 17	eqtr4id	|- ( N e. NN0 -> ( E ` U ) = ( E ` Y ) )