Theorem znbas

Description: The base set of Z/nZ structure. (Contributed by Mario Carneiro, 15-Jun-2015) (Revised by AV, 13-Jun-2019)

	Ref	Expression
Hypotheses	znbas.s	⊢ 𝑆 = ( RSpan ‘ ℤring )
	znbas.y	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
	znbas.r	⊢ 𝑅 = ( ℤring ~QG ( 𝑆 ‘ { 𝑁 } ) )
Assertion	znbas	⊢ ( 𝑁 ∈ ℕ0 → ( ℤ / 𝑅 ) = ( Base ‘ 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		znbas.s	⊢ 𝑆 = ( RSpan ‘ ℤring )
2		znbas.y	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
3		znbas.r	⊢ 𝑅 = ( ℤring ~QG ( 𝑆 ‘ { 𝑁 } ) )
4		eqidd	⊢ ( 𝑁 ∈ ℕ0 → ( ℤring /s 𝑅 ) = ( ℤring /s 𝑅 ) )
5		zringbas	⊢ ℤ = ( Base ‘ ℤring )
6	5	a1i	⊢ ( 𝑁 ∈ ℕ0 → ℤ = ( Base ‘ ℤring ) )
7	3	ovexi	⊢ 𝑅 ∈ V
8	7	a1i	⊢ ( 𝑁 ∈ ℕ0 → 𝑅 ∈ V )
9		zringring	⊢ ℤring ∈ Ring
10	9	a1i	⊢ ( 𝑁 ∈ ℕ0 → ℤring ∈ Ring )
11	4 6 8 10	qusbas	⊢ ( 𝑁 ∈ ℕ0 → ( ℤ / 𝑅 ) = ( Base ‘ ( ℤring /s 𝑅 ) ) )
12	3	oveq2i	⊢ ( ℤring /s 𝑅 ) = ( ℤring /s ( ℤring ~QG ( 𝑆 ‘ { 𝑁 } ) ) )
13	1 12 2	znbas2	⊢ ( 𝑁 ∈ ℕ0 → ( Base ‘ ( ℤring /s 𝑅 ) ) = ( Base ‘ 𝑌 ) )
14	11 13	eqtrd	⊢ ( 𝑁 ∈ ℕ0 → ( ℤ / 𝑅 ) = ( Base ‘ 𝑌 ) )