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