Step |
Hyp |
Ref |
Expression |
1 |
|
cznrng.y |
⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 ) |
2 |
|
cznrng.b |
⊢ 𝐵 = ( Base ‘ 𝑌 ) |
3 |
|
cznrng.x |
⊢ 𝑋 = ( 𝑌 sSet 〈 ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 〉 ) |
4 |
|
cznrng.0 |
⊢ 0 = ( 0g ‘ 𝑌 ) |
5 |
|
eqid |
⊢ ( mulGrp ‘ 𝑋 ) = ( mulGrp ‘ 𝑋 ) |
6 |
1 2 3
|
cznrnglem |
⊢ 𝐵 = ( Base ‘ 𝑋 ) |
7 |
5 6
|
mgpbas |
⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑋 ) ) |
8 |
3
|
fveq2i |
⊢ ( mulGrp ‘ 𝑋 ) = ( mulGrp ‘ ( 𝑌 sSet 〈 ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 〉 ) ) |
9 |
1
|
fvexi |
⊢ 𝑌 ∈ V |
10 |
2
|
fvexi |
⊢ 𝐵 ∈ V |
11 |
10 10
|
mpoex |
⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ∈ V |
12 |
|
mulrid |
⊢ .r = Slot ( .r ‘ ndx ) |
13 |
12
|
setsid |
⊢ ( ( 𝑌 ∈ V ∧ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ∈ V ) → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( .r ‘ ( 𝑌 sSet 〈 ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 〉 ) ) ) |
14 |
9 11 13
|
mp2an |
⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( .r ‘ ( 𝑌 sSet 〈 ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 〉 ) ) |
15 |
8 14
|
mgpplusg |
⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( +g ‘ ( mulGrp ‘ 𝑋 ) ) |
16 |
15
|
eqcomi |
⊢ ( +g ‘ ( mulGrp ‘ 𝑋 ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) |
17 |
|
simpr |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐶 ∈ 𝐵 ) → 𝐶 ∈ 𝐵 ) |
18 |
|
eluz2 |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤ 𝑁 ) ) |
19 |
|
1lt2 |
⊢ 1 < 2 |
20 |
|
1red |
⊢ ( 𝑁 ∈ ℤ → 1 ∈ ℝ ) |
21 |
|
2re |
⊢ 2 ∈ ℝ |
22 |
21
|
a1i |
⊢ ( 𝑁 ∈ ℤ → 2 ∈ ℝ ) |
23 |
|
zre |
⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ ) |
24 |
|
ltletr |
⊢ ( ( 1 ∈ ℝ ∧ 2 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 1 < 2 ∧ 2 ≤ 𝑁 ) → 1 < 𝑁 ) ) |
25 |
20 22 23 24
|
syl3anc |
⊢ ( 𝑁 ∈ ℤ → ( ( 1 < 2 ∧ 2 ≤ 𝑁 ) → 1 < 𝑁 ) ) |
26 |
25
|
expcomd |
⊢ ( 𝑁 ∈ ℤ → ( 2 ≤ 𝑁 → ( 1 < 2 → 1 < 𝑁 ) ) ) |
27 |
26
|
a1i |
⊢ ( 2 ∈ ℤ → ( 𝑁 ∈ ℤ → ( 2 ≤ 𝑁 → ( 1 < 2 → 1 < 𝑁 ) ) ) ) |
28 |
27
|
3imp |
⊢ ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤ 𝑁 ) → ( 1 < 2 → 1 < 𝑁 ) ) |
29 |
19 28
|
mpi |
⊢ ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤ 𝑁 ) → 1 < 𝑁 ) |
30 |
18 29
|
sylbi |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝑁 ) |
31 |
|
eluz2nn |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℕ ) |
32 |
1 2
|
znhash |
⊢ ( 𝑁 ∈ ℕ → ( ♯ ‘ 𝐵 ) = 𝑁 ) |
33 |
31 32
|
syl |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ♯ ‘ 𝐵 ) = 𝑁 ) |
34 |
30 33
|
breqtrrd |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 1 < ( ♯ ‘ 𝐵 ) ) |
35 |
34
|
adantr |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐶 ∈ 𝐵 ) → 1 < ( ♯ ‘ 𝐵 ) ) |
36 |
7 16 17 35
|
copisnmnd |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐶 ∈ 𝐵 ) → ( mulGrp ‘ 𝑋 ) ∉ Mnd ) |
37 |
|
df-nel |
⊢ ( ( mulGrp ‘ 𝑋 ) ∉ Mnd ↔ ¬ ( mulGrp ‘ 𝑋 ) ∈ Mnd ) |
38 |
36 37
|
sylib |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐶 ∈ 𝐵 ) → ¬ ( mulGrp ‘ 𝑋 ) ∈ Mnd ) |
39 |
38
|
intn3an2d |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐶 ∈ 𝐵 ) → ¬ ( 𝑋 ∈ Grp ∧ ( mulGrp ‘ 𝑋 ) ∈ Mnd ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 ( .r ‘ ( 𝑌 sSet 〈 ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 〉 ) ) ( 𝑏 ( +g ‘ 𝑋 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ ( 𝑌 sSet 〈 ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 〉 ) ) 𝑏 ) ( +g ‘ 𝑋 ) ( 𝑎 ( .r ‘ ( 𝑌 sSet 〈 ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 〉 ) ) 𝑐 ) ) ∧ ( ( 𝑎 ( +g ‘ 𝑋 ) 𝑏 ) ( .r ‘ ( 𝑌 sSet 〈 ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 〉 ) ) 𝑐 ) = ( ( 𝑎 ( .r ‘ ( 𝑌 sSet 〈 ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 〉 ) ) 𝑐 ) ( +g ‘ 𝑋 ) ( 𝑏 ( .r ‘ ( 𝑌 sSet 〈 ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 〉 ) ) 𝑐 ) ) ) ) ) |
40 |
|
eqid |
⊢ ( +g ‘ 𝑋 ) = ( +g ‘ 𝑋 ) |
41 |
3
|
eqcomi |
⊢ ( 𝑌 sSet 〈 ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 〉 ) = 𝑋 |
42 |
41
|
fveq2i |
⊢ ( .r ‘ ( 𝑌 sSet 〈 ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 〉 ) ) = ( .r ‘ 𝑋 ) |
43 |
6 5 40 42
|
isring |
⊢ ( 𝑋 ∈ Ring ↔ ( 𝑋 ∈ Grp ∧ ( mulGrp ‘ 𝑋 ) ∈ Mnd ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 ( .r ‘ ( 𝑌 sSet 〈 ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 〉 ) ) ( 𝑏 ( +g ‘ 𝑋 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ ( 𝑌 sSet 〈 ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 〉 ) ) 𝑏 ) ( +g ‘ 𝑋 ) ( 𝑎 ( .r ‘ ( 𝑌 sSet 〈 ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 〉 ) ) 𝑐 ) ) ∧ ( ( 𝑎 ( +g ‘ 𝑋 ) 𝑏 ) ( .r ‘ ( 𝑌 sSet 〈 ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 〉 ) ) 𝑐 ) = ( ( 𝑎 ( .r ‘ ( 𝑌 sSet 〈 ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 〉 ) ) 𝑐 ) ( +g ‘ 𝑋 ) ( 𝑏 ( .r ‘ ( 𝑌 sSet 〈 ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 〉 ) ) 𝑐 ) ) ) ) ) |
44 |
39 43
|
sylnibr |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐶 ∈ 𝐵 ) → ¬ 𝑋 ∈ Ring ) |
45 |
|
df-nel |
⊢ ( 𝑋 ∉ Ring ↔ ¬ 𝑋 ∈ Ring ) |
46 |
44 45
|
sylibr |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐶 ∈ 𝐵 ) → 𝑋 ∉ Ring ) |