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) (Revised by AV, 3-Nov-2024)

	Ref	Expression
Hypotheses	znval2.s	⊢ 𝑆 = ( RSpan ‘ ℤring )
	znval2.u	⊢ 𝑈 = ( ℤring /s ( ℤring ~QG ( 𝑆 ‘ { 𝑁 } ) ) )
	znval2.y	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
	znbaslem.e	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
	znbaslem.n	⊢ ( 𝐸 ‘ ndx ) ≠ ( le ‘ ndx )
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 ( 𝐸 ‘ ndx )
5		znbaslem.n	⊢ ( 𝐸 ‘ ndx ) ≠ ( le ‘ ndx )
6	4 5	setsnid	⊢ ( 𝐸 ‘ 𝑈 ) = ( 𝐸 ‘ ( 𝑈 sSet ⟨ ( le ‘ ndx ) , ( le ‘ 𝑌 ) ⟩ ) )
7		eqid	⊢ ( le ‘ 𝑌 ) = ( le ‘ 𝑌 )
8	1 2 3 7	znval2	⊢ ( 𝑁 ∈ ℕ0 → 𝑌 = ( 𝑈 sSet ⟨ ( le ‘ ndx ) , ( le ‘ 𝑌 ) ⟩ ) )
9	8	fveq2d	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐸 ‘ 𝑌 ) = ( 𝐸 ‘ ( 𝑈 sSet ⟨ ( le ‘ ndx ) , ( le ‘ 𝑌 ) ⟩ ) ) )
10	6 9	eqtr4id	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐸 ‘ 𝑈 ) = ( 𝐸 ‘ 𝑌 ) )