Metamath Proof Explorer

Theorem cznnring

Description: The ring constructed from a Z/nZ structure with 1 < n by replacing the (multiplicative) ring operation by a constant operation is not a unital ring. (Contributed by AV, 17-Feb-2020)

Ref Expression
Hypotheses cznrng.y ⊢ Y = ℤ/Nℤ
cznrng.b ⊢ B = Base Y
cznrng.x ⊢ X = Y sSet ⋅ ndx x ∈ B , y ∈ B ⟼ C
cznrng.0 ⊢ 0 ˙ = 0 Y
Assertion cznnring ⊢ N ∈ ℤ ≥ 2 ∧ C ∈ B → X ∉ Ring

Proof

Step Hyp Ref Expression
1 cznrng.y ⊢ Y = ℤ/Nℤ
2 cznrng.b ⊢ B = Base Y
3 cznrng.x ⊢ X = Y sSet ⋅ ndx x ∈ B , y ∈ B ⟼ C
4 cznrng.0 ⊢ 0 ˙ = 0 Y
5 eqid ⊢ mulGrp X = mulGrp X
6 1 2 3 cznrnglem ⊢ B = Base X
7 5 6 mgpbas ⊢ B = Base mulGrp X
8 3 fveq2i ⊢ mulGrp X = mulGrp Y sSet ⋅ ndx x ∈ B , y ∈ B ⟼ C
9 1 fvexi ⊢ Y ∈ V
10 2 fvexi ⊢ B ∈ V
11 10 10 mpoex ⊢ x ∈ B , y ∈ B ⟼ C ∈ V
12 mulridx ⊢ ⋅ 𝑟 = Slot ⋅ ndx
13 12 setsid ⊢ Y ∈ V ∧ x ∈ B , y ∈ B ⟼ C ∈ V → x ∈ B , y ∈ B ⟼ C = ⋅ Y sSet ⋅ ndx x ∈ B , y ∈ B ⟼ C
14 9 11 13 mp2an ⊢ x ∈ B , y ∈ B ⟼ C = ⋅ Y sSet ⋅ ndx x ∈ B , y ∈ B ⟼ C
15 8 14 mgpplusg ⊢ x ∈ B , y ∈ B ⟼ C = + mulGrp X
16 15 eqcomi ⊢ + mulGrp X = x ∈ B , y ∈ B ⟼ C
17 simpr ⊢ N ∈ ℤ ≥ 2 ∧ C ∈ B → C ∈ B
18 eluz2 ⊢ N ∈ ℤ ≥ 2 ↔ 2 ∈ ℤ ∧ N ∈ ℤ ∧ 2 ≤ N
19 1lt2 ⊢ 1 < 2
20 1red ⊢ N ∈ ℤ → 1 ∈ ℝ
21 2re ⊢ 2 ∈ ℝ
22 21 a1i ⊢ N ∈ ℤ → 2 ∈ ℝ
23 zre ⊢ N ∈ ℤ → N ∈ ℝ
24 ltletr ⊢ 1 ∈ ℝ ∧ 2 ∈ ℝ ∧ N ∈ ℝ → 1 < 2 ∧ 2 ≤ N → 1 < N
25 20 22 23 24 syl3anc ⊢ N ∈ ℤ → 1 < 2 ∧ 2 ≤ N → 1 < N
26 25 expcomd ⊢ N ∈ ℤ → 2 ≤ N → 1 < 2 → 1 < N
27 26 a1i ⊢ 2 ∈ ℤ → N ∈ ℤ → 2 ≤ N → 1 < 2 → 1 < N
28 27 3imp ⊢ 2 ∈ ℤ ∧ N ∈ ℤ ∧ 2 ≤ N → 1 < 2 → 1 < N
29 19 28 mpi ⊢ 2 ∈ ℤ ∧ N ∈ ℤ ∧ 2 ≤ N → 1 < N
30 18 29 sylbi ⊢ N ∈ ℤ ≥ 2 → 1 < N
31 eluz2nn ⊢ N ∈ ℤ ≥ 2 → N ∈ ℕ
32 1 2 znhash ⊢ N ∈ ℕ → B = N
33 31 32 syl ⊢ N ∈ ℤ ≥ 2 → B = N
34 30 33 breqtrrd ⊢ N ∈ ℤ ≥ 2 → 1 < B
35 34 adantr ⊢ N ∈ ℤ ≥ 2 ∧ C ∈ B → 1 < B
36 7 16 17 35 copisnmnd ⊢ N ∈ ℤ ≥ 2 ∧ C ∈ B → mulGrp X ∉ Mnd
37 df-nel ⊢ mulGrp X ∉ Mnd ↔ ¬ mulGrp X ∈ Mnd
38 36 37 sylib ⊢ N ∈ ℤ ≥ 2 ∧ C ∈ B → ¬ mulGrp X ∈ Mnd
39 38 intn3an2d ⊢ N ∈ ℤ ≥ 2 ∧ C ∈ B → ¬ X ∈ Grp ∧ mulGrp X ∈ Mnd ∧ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B a ⋅ Y sSet ⋅ ndx x ∈ B , y ∈ B ⟼ C b + X c = a ⋅ Y sSet ⋅ ndx x ∈ B , y ∈ B ⟼ C b + X a ⋅ Y sSet ⋅ ndx x ∈ B , y ∈ B ⟼ C c ∧ a + X b ⋅ Y sSet ⋅ ndx x ∈ B , y ∈ B ⟼ C c = a ⋅ Y sSet ⋅ ndx x ∈ B , y ∈ B ⟼ C c + X b ⋅ Y sSet ⋅ ndx x ∈ B , y ∈ B ⟼ C c
40 eqid ⊢ + X = + X
41 3 eqcomi ⊢ Y sSet ⋅ ndx x ∈ B , y ∈ B ⟼ C = X
42 41 fveq2i ⊢ ⋅ Y sSet ⋅ ndx x ∈ B , y ∈ B ⟼ C = ⋅ X
43 6 5 40 42 isring ⊢ X ∈ Ring ↔ X ∈ Grp ∧ mulGrp X ∈ Mnd ∧ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B a ⋅ Y sSet ⋅ ndx x ∈ B , y ∈ B ⟼ C b + X c = a ⋅ Y sSet ⋅ ndx x ∈ B , y ∈ B ⟼ C b + X a ⋅ Y sSet ⋅ ndx x ∈ B , y ∈ B ⟼ C c ∧ a + X b ⋅ Y sSet ⋅ ndx x ∈ B , y ∈ B ⟼ C c = a ⋅ Y sSet ⋅ ndx x ∈ B , y ∈ B ⟼ C c + X b ⋅ Y sSet ⋅ ndx x ∈ B , y ∈ B ⟼ C c
44 39 43 sylnibr ⊢ N ∈ ℤ ≥ 2 ∧ C ∈ B → ¬ X ∈ Ring
45 df-nel ⊢ X ∉ Ring ↔ ¬ X ∈ Ring
46 44 45 sylibr ⊢ N ∈ ℤ ≥ 2 ∧ C ∈ B → X ∉ Ring