Metamath Proof Explorer

Theorem cznrng

Description: The ring constructed from a Z/nZ structure by replacing the (multiplicative) ring operation by a constant operation is a non-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 cznrng 
|- ( ( N e. NN /\ C = .0. ) -> X e. Rng )

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 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
6 1 zncrng 
 |-  ( N e. NN0 -> Y e. CRing )
7 5 6 syl 
 |-  ( N e. NN -> Y e. CRing )
8 crngring 
 |-  ( Y e. CRing -> Y e. Ring )
9 2 4 ring0cl 
 |-  ( Y e. Ring -> .0. e. B )
10 eleq1a 
 |-  ( .0. e. B -> ( C = .0. -> C e. B ) )
11 9 10 syl 
 |-  ( Y e. Ring -> ( C = .0. -> C e. B ) )
12 8 11 syl 
 |-  ( Y e. CRing -> ( C = .0. -> C e. B ) )
13 7 12 syl 
 |-  ( N e. NN -> ( C = .0. -> C e. B ) )
14 13 imp 
 |-  ( ( N e. NN /\ C = .0. ) -> C e. B )
15 1 2 3 cznabel 
 |-  ( ( N e. NN /\ C e. B ) -> X e. Abel )
16 15 adantlr 
 |-  ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) -> X e. Abel )
17 eqid 
 |-  ( mulGrp ` X ) = ( mulGrp ` X )
18 1 2 3 cznrnglem 
 |-  B = ( Base ` X )
19 17 18 mgpbas 
 |-  B = ( Base ` ( mulGrp ` X ) )
20 3 fveq2i 
 |-  ( mulGrp ` X ) = ( mulGrp ` ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. ) )
21 1 fvexi 
 |-  Y e. _V
22 2 fvexi 
 |-  B e. _V
23 22 22 mpoex 
 |-  ( x e. B , y e. B |-> C ) e. _V
24 mulridx 
 |-  .r = Slot ( .r ` ndx )
25 24 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 ) >. ) ) )
26 21 23 25 mp2an 
 |-  ( x e. B , y e. B |-> C ) = ( .r ` ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. ) )
27 20 26 mgpplusg 
 |-  ( x e. B , y e. B |-> C ) = ( +g ` ( mulGrp ` X ) )
28 27 eqcomi 
 |-  ( +g ` ( mulGrp ` X ) ) = ( x e. B , y e. B |-> C )
29 ne0i 
 |-  ( C e. B -> B =/= (/) )
30 29 adantl 
 |-  ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) -> B =/= (/) )
31 simpr 
 |-  ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) -> C e. B )
32 19 28 30 31 copissgrp 
 |-  ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) -> ( mulGrp ` X ) e. Smgrp )
33 oveq1 
 |-  ( C = .0. -> ( C ( +g ` Y ) C ) = ( .0. ( +g ` Y ) C ) )
34 33 ad3antlr 
 |-  ( ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( C ( +g ` Y ) C ) = ( .0. ( +g ` Y ) C ) )
35 7 8 syl 
 |-  ( N e. NN -> Y e. Ring )
36 ringmnd 
 |-  ( Y e. Ring -> Y e. Mnd )
37 35 36 syl 
 |-  ( N e. NN -> Y e. Mnd )
38 37 adantr 
 |-  ( ( N e. NN /\ C = .0. ) -> Y e. Mnd )
39 38 anim1i 
 |-  ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) -> ( Y e. Mnd /\ C e. B ) )
40 39 adantr 
 |-  ( ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( Y e. Mnd /\ C e. B ) )
41 eqid 
 |-  ( +g ` Y ) = ( +g ` Y )
42 2 41 4 mndlid 
 |-  ( ( Y e. Mnd /\ C e. B ) -> ( .0. ( +g ` Y ) C ) = C )
43 40 42 syl 
 |-  ( ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( .0. ( +g ` Y ) C ) = C )
44 34 43 eqtrd 
 |-  ( ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( C ( +g ` Y ) C ) = C )
45 eqidd 
 |-  ( ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( x e. B , y e. B |-> C ) = ( x e. B , y e. B |-> C ) )
46 eqidd 
 |-  ( ( ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) /\ ( a e. B /\ b e. B /\ c e. B ) ) /\ ( x = a /\ y = b ) ) -> C = C )
47 simpr1 
 |-  ( ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) /\ ( a e. B /\ b e. B /\ c e. B ) ) -> a e. B )
48 simpr2 
 |-  ( ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) /\ ( a e. B /\ b e. B /\ c e. B ) ) -> b e. B )
49 31 adantr 
 |-  ( ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) /\ ( a e. B /\ b e. B /\ c e. B ) ) -> C e. B )
50 45 46 47 48 49 ovmpod 
 |-  ( ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( a ( x e. B , y e. B |-> C ) b ) = C )
51 eqidd 
 |-  ( ( ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) /\ ( a e. B /\ b e. B /\ c e. B ) ) /\ ( x = a /\ y = c ) ) -> C = C )
52 simpr3 
 |-  ( ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) /\ ( a e. B /\ b e. B /\ c e. B ) ) -> c e. B )
53 45 51 47 52 49 ovmpod 
 |-  ( ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( a ( x e. B , y e. B |-> C ) c ) = C )
54 50 53 oveq12d 
 |-  ( ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( ( a ( x e. B , y e. B |-> C ) b ) ( +g ` Y ) ( a ( x e. B , y e. B |-> C ) c ) ) = ( C ( +g ` Y ) C ) )
55 eqidd 
 |-  ( ( ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) /\ ( a e. B /\ b e. B /\ c e. B ) ) /\ ( x = a /\ y = ( b ( +g ` Y ) c ) ) ) -> C = C )
56 35 ad3antrrr 
 |-  ( ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) /\ ( a e. B /\ b e. B /\ c e. B ) ) -> Y e. Ring )
57 2 41 ringacl 
 |-  ( ( Y e. Ring /\ b e. B /\ c e. B ) -> ( b ( +g ` Y ) c ) e. B )
58 56 48 52 57 syl3anc 
 |-  ( ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( b ( +g ` Y ) c ) e. B )
59 45 55 47 58 49 ovmpod 
 |-  ( ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( a ( x e. B , y e. B |-> C ) ( b ( +g ` Y ) c ) ) = C )
60 44 54 59 3eqtr4rd 
 |-  ( ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( a ( x e. B , y e. B |-> C ) ( b ( +g ` Y ) c ) ) = ( ( a ( x e. B , y e. B |-> C ) b ) ( +g ` Y ) ( a ( x e. B , y e. B |-> C ) c ) ) )
61 eqidd 
 |-  ( ( ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) /\ ( a e. B /\ b e. B /\ c e. B ) ) /\ ( x = b /\ y = c ) ) -> C = C )
62 45 61 48 52 49 ovmpod 
 |-  ( ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( b ( x e. B , y e. B |-> C ) c ) = C )
63 53 62 oveq12d 
 |-  ( ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( ( a ( x e. B , y e. B |-> C ) c ) ( +g ` Y ) ( b ( x e. B , y e. B |-> C ) c ) ) = ( C ( +g ` Y ) C ) )
64 eqidd 
 |-  ( ( ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) /\ ( a e. B /\ b e. B /\ c e. B ) ) /\ ( x = ( a ( +g ` Y ) b ) /\ y = c ) ) -> C = C )
65 2 41 ringacl 
 |-  ( ( Y e. Ring /\ a e. B /\ b e. B ) -> ( a ( +g ` Y ) b ) e. B )
66 56 47 48 65 syl3anc 
 |-  ( ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( a ( +g ` Y ) b ) e. B )
67 45 64 66 52 49 ovmpod 
 |-  ( ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( ( a ( +g ` Y ) b ) ( x e. B , y e. B |-> C ) c ) = C )
68 44 63 67 3eqtr4rd 
 |-  ( ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( ( a ( +g ` Y ) b ) ( x e. B , y e. B |-> C ) c ) = ( ( a ( x e. B , y e. B |-> C ) c ) ( +g ` Y ) ( b ( x e. B , y e. B |-> C ) c ) ) )
69 60 68 jca 
 |-  ( ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( ( a ( x e. B , y e. B |-> C ) ( b ( +g ` Y ) c ) ) = ( ( a ( x e. B , y e. B |-> C ) b ) ( +g ` Y ) ( a ( x e. B , y e. B |-> C ) c ) ) /\ ( ( a ( +g ` Y ) b ) ( x e. B , y e. B |-> C ) c ) = ( ( a ( x e. B , y e. B |-> C ) c ) ( +g ` Y ) ( b ( x e. B , y e. B |-> C ) c ) ) ) )
70 69 ralrimivvva 
 |-  ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) -> A. a e. B A. b e. B A. c e. B ( ( a ( x e. B , y e. B |-> C ) ( b ( +g ` Y ) c ) ) = ( ( a ( x e. B , y e. B |-> C ) b ) ( +g ` Y ) ( a ( x e. B , y e. B |-> C ) c ) ) /\ ( ( a ( +g ` Y ) b ) ( x e. B , y e. B |-> C ) c ) = ( ( a ( x e. B , y e. B |-> C ) c ) ( +g ` Y ) ( b ( x e. B , y e. B |-> C ) c ) ) ) )
71 16 32 70 3jca 
 |-  ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) -> ( X e. Abel /\ ( mulGrp ` X ) e. Smgrp /\ A. a e. B A. b e. B A. c e. B ( ( a ( x e. B , y e. B |-> C ) ( b ( +g ` Y ) c ) ) = ( ( a ( x e. B , y e. B |-> C ) b ) ( +g ` Y ) ( a ( x e. B , y e. B |-> C ) c ) ) /\ ( ( a ( +g ` Y ) b ) ( x e. B , y e. B |-> C ) c ) = ( ( a ( x e. B , y e. B |-> C ) c ) ( +g ` Y ) ( b ( x e. B , y e. B |-> C ) c ) ) ) ) )
72 14 71 mpdan 
 |-  ( ( N e. NN /\ C = .0. ) -> ( X e. Abel /\ ( mulGrp ` X ) e. Smgrp /\ A. a e. B A. b e. B A. c e. B ( ( a ( x e. B , y e. B |-> C ) ( b ( +g ` Y ) c ) ) = ( ( a ( x e. B , y e. B |-> C ) b ) ( +g ` Y ) ( a ( x e. B , y e. B |-> C ) c ) ) /\ ( ( a ( +g ` Y ) b ) ( x e. B , y e. B |-> C ) c ) = ( ( a ( x e. B , y e. B |-> C ) c ) ( +g ` Y ) ( b ( x e. B , y e. B |-> C ) c ) ) ) ) )
73 plusgid 
 |-  +g = Slot ( +g ` ndx )
74 plusgndxnmulrndx 
 |-  ( +g ` ndx ) =/= ( .r ` ndx )
75 73 74 setsnid 
 |-  ( +g ` Y ) = ( +g ` ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. ) )
76 3 fveq2i 
 |-  ( +g ` X ) = ( +g ` ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. ) )
77 75 76 eqtr4i 
 |-  ( +g ` Y ) = ( +g ` X )
78 3 eqcomi 
 |-  ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. ) = X
79 78 fveq2i 
 |-  ( .r ` ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. ) ) = ( .r ` X )
80 26 79 eqtri 
 |-  ( x e. B , y e. B |-> C ) = ( .r ` X )
81 18 17 77 80 isrng 
 |-  ( X e. Rng <-> ( X e. Abel /\ ( mulGrp ` X ) e. Smgrp /\ A. a e. B A. b e. B A. c e. B ( ( a ( x e. B , y e. B |-> C ) ( b ( +g ` Y ) c ) ) = ( ( a ( x e. B , y e. B |-> C ) b ) ( +g ` Y ) ( a ( x e. B , y e. B |-> C ) c ) ) /\ ( ( a ( +g ` Y ) b ) ( x e. B , y e. B |-> C ) c ) = ( ( a ( x e. B , y e. B |-> C ) c ) ( +g ` Y ) ( b ( x e. B , y e. B |-> C ) c ) ) ) ) )
82 72 81 sylibr 
 |-  ( ( N e. NN /\ C = .0. ) -> X e. Rng )