This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 → ( 𝐸 ‘ 𝑈 ) = ( 𝐸 ‘ 𝑌 ) )