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 = ( Z/nZ ` N )
cznrng.b 
|- B = ( Base ` Y )
cznrng.x 
|- X = ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. )
cznrng.0 
|- .0. = ( 0g ` Y )
Assertion cznnring 
|- ( ( N e. ( ZZ>= ` 2 ) /\ C e. B ) -> X e/ Ring )

Proof

Step Hyp Ref Expression
1 cznrng.y 
 |-  Y = ( Z/nZ ` N )
2 cznrng.b 
 |-  B = ( Base ` Y )
3 cznrng.x 
 |-  X = ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. )
4 cznrng.0 
 |-  .0. = ( 0g ` 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 <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. ) )
9 1 fvexi 
 |-  Y e. _V
10 2 fvexi 
 |-  B e. _V
11 10 10 mpoex 
 |-  ( x e. B , y e. B |-> C ) e. _V
12 mulrid 
 |-  .r = Slot ( .r ` ndx )
13 12 setsid 
 |-  ( ( Y e. _V /\ ( x e. B , y e. B |-> C ) e. _V ) -> ( x e. B , y e. B |-> C ) = ( .r ` ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. ) ) )
14 9 11 13 mp2an 
 |-  ( x e. B , y e. B |-> C ) = ( .r ` ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. ) )
15 8 14 mgpplusg 
 |-  ( x e. B , y e. B |-> C ) = ( +g ` ( mulGrp ` X ) )
16 15 eqcomi 
 |-  ( +g ` ( mulGrp ` X ) ) = ( x e. B , y e. B |-> C )
17 simpr 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ C e. B ) -> C e. B )
18 eluz2 
 |-  ( N e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ N e. ZZ /\ 2 <_ N ) )
19 1lt2 
 |-  1 < 2
20 1red 
 |-  ( N e. ZZ -> 1 e. RR )
21 2re 
 |-  2 e. RR
22 21 a1i 
 |-  ( N e. ZZ -> 2 e. RR )
23 zre 
 |-  ( N e. ZZ -> N e. RR )
24 ltletr 
 |-  ( ( 1 e. RR /\ 2 e. RR /\ N e. RR ) -> ( ( 1 < 2 /\ 2 <_ N ) -> 1 < N ) )
25 20 22 23 24 syl3anc 
 |-  ( N e. ZZ -> ( ( 1 < 2 /\ 2 <_ N ) -> 1 < N ) )
26 25 expcomd 
 |-  ( N e. ZZ -> ( 2 <_ N -> ( 1 < 2 -> 1 < N ) ) )
27 26 a1i 
 |-  ( 2 e. ZZ -> ( N e. ZZ -> ( 2 <_ N -> ( 1 < 2 -> 1 < N ) ) ) )
28 27 3imp 
 |-  ( ( 2 e. ZZ /\ N e. ZZ /\ 2 <_ N ) -> ( 1 < 2 -> 1 < N ) )
29 19 28 mpi 
 |-  ( ( 2 e. ZZ /\ N e. ZZ /\ 2 <_ N ) -> 1 < N )
30 18 29 sylbi 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 < N )
31 eluz2nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN )
32 1 2 znhash 
 |-  ( N e. NN -> ( # ` B ) = N )
33 31 32 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( # ` B ) = N )
34 30 33 breqtrrd 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 < ( # ` B ) )
35 34 adantr 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ C e. B ) -> 1 < ( # ` B ) )
36 7 16 17 35 copisnmnd 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ C e. B ) -> ( mulGrp ` X ) e/ Mnd )
37 df-nel 
 |-  ( ( mulGrp ` X ) e/ Mnd <-> -. ( mulGrp ` X ) e. Mnd )
38 36 37 sylib 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ C e. B ) -> -. ( mulGrp ` X ) e. Mnd )
39 38 intn3an2d 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ C e. B ) -> -. ( X e. Grp /\ ( mulGrp ` X ) e. Mnd /\ A. a e. B A. b e. B A. c e. B ( ( a ( .r ` ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. ) ) ( b ( +g ` X ) c ) ) = ( ( a ( .r ` ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. ) ) b ) ( +g ` X ) ( a ( .r ` ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. ) ) c ) ) /\ ( ( a ( +g ` X ) b ) ( .r ` ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. ) ) c ) = ( ( a ( .r ` ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. ) ) c ) ( +g ` X ) ( b ( .r ` ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. ) ) c ) ) ) ) )
40 eqid 
 |-  ( +g ` X ) = ( +g ` X )
41 3 eqcomi 
 |-  ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. ) = X
42 41 fveq2i 
 |-  ( .r ` ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. ) ) = ( .r ` X )
43 6 5 40 42 isring 
 |-  ( X e. Ring <-> ( X e. Grp /\ ( mulGrp ` X ) e. Mnd /\ A. a e. B A. b e. B A. c e. B ( ( a ( .r ` ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. ) ) ( b ( +g ` X ) c ) ) = ( ( a ( .r ` ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. ) ) b ) ( +g ` X ) ( a ( .r ` ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. ) ) c ) ) /\ ( ( a ( +g ` X ) b ) ( .r ` ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. ) ) c ) = ( ( a ( .r ` ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. ) ) c ) ( +g ` X ) ( b ( .r ` ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. ) ) c ) ) ) ) )
44 39 43 sylnibr 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ C e. B ) -> -. X e. Ring )
45 df-nel 
 |-  ( X e/ Ring <-> -. X e. Ring )
46 44 45 sylibr 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ C e. B ) -> X e/ Ring )