Theorem cznabel

Description: The ring constructed from a Z/nZ structure by replacing the (multiplicative) ring operation by a constant operation is an abelian group. (Contributed by AV, 16-Feb-2020)

	Ref	Expression
Hypotheses	cznrng.y	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
	cznrng.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
	cznrng.x	⊢ 𝑋 = ( 𝑌 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ⟩ )
Assertion	cznabel	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐶 ∈ 𝐵 ) → 𝑋 ∈ Abel )

Proof

Step	Hyp	Ref	Expression
1		cznrng.y	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
2		cznrng.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
3		cznrng.x	⊢ 𝑋 = ( 𝑌 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ⟩ )
4		nnnn0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
5	4	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐶 ∈ 𝐵 ) → 𝑁 ∈ ℕ0 )
6	1	zncrng	⊢ ( 𝑁 ∈ ℕ0 → 𝑌 ∈ CRing )
7	5 6	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐶 ∈ 𝐵 ) → 𝑌 ∈ CRing )
8		crngring	⊢ ( 𝑌 ∈ CRing → 𝑌 ∈ Ring )
9		ringabl	⊢ ( 𝑌 ∈ Ring → 𝑌 ∈ Abel )
10	7 8 9	3syl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐶 ∈ 𝐵 ) → 𝑌 ∈ Abel )
11	3	fveq2i	⊢ ( Base ‘ 𝑋 ) = ( Base ‘ ( 𝑌 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ⟩ ) )
12		baseid	⊢ Base = Slot ( Base ‘ ndx )
13		basendxnmulrndx	⊢ ( Base ‘ ndx ) ≠ ( .r ‘ ndx )
14	12 13	setsnid	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ ( 𝑌 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ⟩ ) )
15	11 14	eqtr4i	⊢ ( Base ‘ 𝑋 ) = ( Base ‘ 𝑌 )
16	3	fveq2i	⊢ ( +g ‘ 𝑋 ) = ( +g ‘ ( 𝑌 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ⟩ ) )
17		plusgid	⊢ +g = Slot ( +g ‘ ndx )
18		plusgndxnmulrndx	⊢ ( +g ‘ ndx ) ≠ ( .r ‘ ndx )
19	17 18	setsnid	⊢ ( +g ‘ 𝑌 ) = ( +g ‘ ( 𝑌 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ⟩ ) )
20	16 19	eqtr4i	⊢ ( +g ‘ 𝑋 ) = ( +g ‘ 𝑌 )
21	15 20	ablprop	⊢ ( 𝑋 ∈ Abel ↔ 𝑌 ∈ Abel )
22	10 21	sylibr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐶 ∈ 𝐵 ) → 𝑋 ∈ Abel )