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	⊢ 𝑆 = ( RSpan ‘ ℤring )
	znval2.u	⊢ 𝑈 = ( ℤring /s ( ℤring ~QG ( 𝑆 ‘ { 𝑁 } ) ) )
	znval2.y	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
	znbaslem.e	⊢ 𝐸 = Slot 𝐾
	znbaslem.k	⊢ 𝐾 ∈ ℕ
	znbaslem.l	⊢ 𝐾 < ; 1 0
Assertion	znbaslem	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐸 ‘ 𝑈 ) = ( 𝐸 ‘ 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		znval2.s	⊢ 𝑆 = ( RSpan ‘ ℤring )
2		znval2.u	⊢ 𝑈 = ( ℤring /s ( ℤring ~QG ( 𝑆 ‘ { 𝑁 } ) ) )
3		znval2.y	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
4		znbaslem.e	⊢ 𝐸 = Slot 𝐾
5		znbaslem.k	⊢ 𝐾 ∈ ℕ
6		znbaslem.l	⊢ 𝐾 < ; 1 0
7	4 5	ndxid	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
8	5	nnrei	⊢ 𝐾 ∈ ℝ
9	8 6	ltneii	⊢ 𝐾 ≠ ; 1 0
10	4 5	ndxarg	⊢ ( 𝐸 ‘ ndx ) = 𝐾
11		plendx	⊢ ( le ‘ ndx ) = ; 1 0
12	10 11	neeq12i	⊢ ( ( 𝐸 ‘ ndx ) ≠ ( le ‘ ndx ) ↔ 𝐾 ≠ ; 1 0 )
13	9 12	mpbir	⊢ ( 𝐸 ‘ ndx ) ≠ ( le ‘ ndx )
14	7 13	setsnid	⊢ ( 𝐸 ‘ 𝑈 ) = ( 𝐸 ‘ ( 𝑈 sSet ⟨ ( le ‘ ndx ) , ( le ‘ 𝑌 ) ⟩ ) )
15		eqid	⊢ ( le ‘ 𝑌 ) = ( le ‘ 𝑌 )
16	1 2 3 15	znval2	⊢ ( 𝑁 ∈ ℕ0 → 𝑌 = ( 𝑈 sSet ⟨ ( le ‘ ndx ) , ( le ‘ 𝑌 ) ⟩ ) )
17	16	fveq2d	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐸 ‘ 𝑌 ) = ( 𝐸 ‘ ( 𝑈 sSet ⟨ ( le ‘ ndx ) , ( le ‘ 𝑌 ) ⟩ ) ) )
18	14 17	eqtr4id	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐸 ‘ 𝑈 ) = ( 𝐸 ‘ 𝑌 ) )