Metamath Proof Explorer

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 
|- Y = ( Z/nZ ` N )
cznrng.b 
|- B = ( Base ` Y )
cznrng.x 
|- X = ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. )
Assertion cznabel 
|- ( ( N e. NN /\ C e. B ) -> X e. Abel )

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 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
5 4 adantr 
 |-  ( ( N e. NN /\ C e. B ) -> N e. NN0 )
6 1 zncrng 
 |-  ( N e. NN0 -> Y e. CRing )
7 5 6 syl 
 |-  ( ( N e. NN /\ C e. B ) -> Y e. CRing )
8 crngring 
 |-  ( Y e. CRing -> Y e. Ring )
9 ringabl 
 |-  ( Y e. Ring -> Y e. Abel )
10 7 8 9 3syl 
 |-  ( ( N e. NN /\ C e. B ) -> Y e. Abel )
11 3 fveq2i 
 |-  ( Base ` X ) = ( Base ` ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. ) )
12 baseid 
 |-  Base = Slot ( Base ` ndx )
13 basendxnmulrndx 
 |-  ( Base ` ndx ) =/= ( .r ` ndx )
14 12 13 setsnid 
 |-  ( Base ` Y ) = ( Base ` ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. ) )
15 11 14 eqtr4i 
 |-  ( Base ` X ) = ( Base ` Y )
16 3 fveq2i 
 |-  ( +g ` X ) = ( +g ` ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. ) )
17 plusgid 
 |-  +g = Slot ( +g ` ndx )
18 plusgndxnmulrndx 
 |-  ( +g ` ndx ) =/= ( .r ` ndx )
19 17 18 setsnid 
 |-  ( +g ` Y ) = ( +g ` ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. ) )
20 16 19 eqtr4i 
 |-  ( +g ` X ) = ( +g ` Y )
21 15 20 ablprop 
 |-  ( X e. Abel <-> Y e. Abel )
22 10 21 sylibr 
 |-  ( ( N e. NN /\ C e. B ) -> X e. Abel )