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	$⊢ S = RSpan (ℤ_{ring})$
		znval2.u	$⊢ U = ℤ_{ring} /_{𝑠} (ℤ_{ring} ~_{QG} S (\{N\}))$
		znval2.y	$⊢ Y = ℤ / N ℤ$
		znbaslem.e	$⊢ E = Slot E (ndx)$
		znbaslem.n	$⊢ E (ndx) \neq \leq_{ndx}$
	Assertion	znbaslem	$⊢ N \in ℕ_{0} \to E (U) = E (Y)$

Proof

Step	Hyp	Ref	Expression
1		znval2.s	$⊢ S = RSpan (ℤ_{ring})$
2		znval2.u	$⊢ U = ℤ_{ring} /_{𝑠} (ℤ_{ring} ~_{QG} S (\{N\}))$
3		znval2.y	$⊢ Y = ℤ / N ℤ$
4		znbaslem.e	$⊢ E = Slot E (ndx)$
5		znbaslem.n	$⊢ E (ndx) \neq \leq_{ndx}$
6	4 5	setsnid	$⊢ E (U) = E (U sSet ⟨\leq_{ndx}, \leq_{Y}⟩)$
7		eqid	$⊢ \leq_{Y} = \leq_{Y}$
8	1 2 3 7	znval2	$⊢ N \in ℕ_{0} \to Y = U sSet ⟨\leq_{ndx}, \leq_{Y}⟩$
9	8	fveq2d	$⊢ N \in ℕ_{0} \to E (Y) = E (U sSet ⟨\leq_{ndx}, \leq_{Y}⟩)$
10	6 9	eqtr4id	$⊢ N \in ℕ_{0} \to E (U) = E (Y)$