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		crngring	⊢ ( 𝑌 ∈ CRing → 𝑌 ∈ Ring )
8		ringabl	⊢ ( 𝑌 ∈ Ring → 𝑌 ∈ Abel )
9	5 6 7 8	4syl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐶 ∈ 𝐵 ) → 𝑌 ∈ Abel )
10	3	fveq2i	⊢ ( Base ‘ 𝑋 ) = ( Base ‘ ( 𝑌 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ⟩ ) )
11		baseid	⊢ Base = Slot ( Base ‘ ndx )
12		basendxnmulrndx	⊢ ( Base ‘ ndx ) ≠ ( .r ‘ ndx )
13	11 12	setsnid	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ ( 𝑌 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ⟩ ) )
14	10 13	eqtr4i	⊢ ( Base ‘ 𝑋 ) = ( Base ‘ 𝑌 )
15	3	fveq2i	⊢ ( +g ‘ 𝑋 ) = ( +g ‘ ( 𝑌 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ⟩ ) )
16		plusgid	⊢ +g = Slot ( +g ‘ ndx )
17		plusgndxnmulrndx	⊢ ( +g ‘ ndx ) ≠ ( .r ‘ ndx )
18	16 17	setsnid	⊢ ( +g ‘ 𝑌 ) = ( +g ‘ ( 𝑌 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ⟩ ) )
19	15 18	eqtr4i	⊢ ( +g ‘ 𝑋 ) = ( +g ‘ 𝑌 )
20	14 19	ablprop	⊢ ( 𝑋 ∈ Abel ↔ 𝑌 ∈ Abel )
21	9 20	sylibr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐶 ∈ 𝐵 ) → 𝑋 ∈ Abel )