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 = ℤ / N ℤ$
	cznrng.b	$⊢ B = {Base}_{Y}$
	cznrng.x	$⊢ X = Y sSet ⟨\cdot_{ndx}, (x \in B, y \in B ⟼ C)⟩$
	cznrng.0	$⊢ \underset{˙}{0} = 0_{Y}$
Assertion	cznrng	$⊢ (N \in ℕ \land C = \underset{˙}{0}) \to X \in Rng$

Proof

Step	Hyp	Ref	Expression
1		cznrng.y	$⊢ Y = ℤ / N ℤ$
2		cznrng.b	$⊢ B = {Base}_{Y}$
3		cznrng.x	$⊢ X = Y sSet ⟨\cdot_{ndx}, (x \in B, y \in B ⟼ C)⟩$
4		cznrng.0	$⊢ \underset{˙}{0} = 0_{Y}$
5		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
6	1	zncrng	$⊢ N \in ℕ_{0} \to Y \in CRing$
7	5 6	syl	$⊢ N \in ℕ \to Y \in CRing$
8		crngring	$⊢ Y \in CRing \to Y \in Ring$
9	2 4	ring0cl	$⊢ Y \in Ring \to \underset{˙}{0} \in B$
10		eleq1a	$⊢ \underset{˙}{0} \in B \to (C = \underset{˙}{0} \to C \in B)$
11	9 10	syl	$⊢ Y \in Ring \to (C = \underset{˙}{0} \to C \in B)$
12	8 11	syl	$⊢ Y \in CRing \to (C = \underset{˙}{0} \to C \in B)$
13	7 12	syl	$⊢ N \in ℕ \to (C = \underset{˙}{0} \to C \in B)$
14	13	imp	$⊢ (N \in ℕ \land C = \underset{˙}{0}) \to C \in B$
15	1 2 3	cznabel	$⊢ (N \in ℕ \land C \in B) \to X \in Abel$
16	15	adantlr	$⊢ ((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \to X \in 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 ⟨\cdot_{ndx}, (x \in B, y \in B ⟼ C)⟩)}$
21	1	fvexi	$⊢ Y \in V$
22	2	fvexi	$⊢ B \in V$
23	22 22	mpoex	$⊢ (x \in B, y \in B ⟼ C) \in V$
24		mulrid	$⊢ \cdot_{𝑟} = Slot \cdot_{ndx}$
25	24	setsid	$⊢ (Y \in V \land (x \in B, y \in B ⟼ C) \in V) \to (x \in B, y \in B ⟼ C) = \cdot_{(Y sSet ⟨\cdot_{ndx}, (x \in B, y \in B ⟼ C)⟩)}$
26	21 23 25	mp2an	$⊢ (x \in B, y \in B ⟼ C) = \cdot_{(Y sSet ⟨\cdot_{ndx}, (x \in B, y \in B ⟼ C)⟩)}$
27	20 26	mgpplusg	$⊢ (x \in B, y \in B ⟼ C) = +_{{mulGrp}_{X}}$
28	27	eqcomi	$⊢ +_{{mulGrp}_{X}} = (x \in B, y \in B ⟼ C)$
29		ne0i	$⊢ C \in B \to B \neq \emptyset$
30	29	adantl	$⊢ ((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \to B \neq \emptyset$
31		simpr	$⊢ ((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \to C \in B$
32	19 28 30 31	copissgrp	Could not format ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) -> ( mulGrp ` X ) e. Smgrp ) : No typesetting found for \|- ( ( ( N e. NN /\ C = .0. ) /\ C e. B ) -> ( mulGrp ` X ) e. Smgrp ) with typecode \|-
33		oveq1	$⊢ C = \underset{˙}{0} \to C +_{Y} C = \underset{˙}{0} +_{Y} C$
34	33	ad3antlr	$⊢ (((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \land (a \in B \land b \in B \land c \in B)) \to C +_{Y} C = \underset{˙}{0} +_{Y} C$
35	7 8	syl	$⊢ N \in ℕ \to Y \in Ring$
36		ringmnd	$⊢ Y \in Ring \to Y \in Mnd$
37	35 36	syl	$⊢ N \in ℕ \to Y \in Mnd$
38	37	adantr	$⊢ (N \in ℕ \land C = \underset{˙}{0}) \to Y \in Mnd$
39	38	anim1i	$⊢ ((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \to (Y \in Mnd \land C \in B)$
40	39	adantr	$⊢ (((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \land (a \in B \land b \in B \land c \in B)) \to (Y \in Mnd \land C \in B)$
41		eqid	$⊢ +_{Y} = +_{Y}$
42	2 41 4	mndlid	$⊢ (Y \in Mnd \land C \in B) \to \underset{˙}{0} +_{Y} C = C$
43	40 42	syl	$⊢ (((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \land (a \in B \land b \in B \land c \in B)) \to \underset{˙}{0} +_{Y} C = C$
44	34 43	eqtrd	$⊢ (((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \land (a \in B \land b \in B \land c \in B)) \to C +_{Y} C = C$
45		eqidd	$⊢ (((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \land (a \in B \land b \in B \land c \in B)) \to (x \in B, y \in B ⟼ C) = (x \in B, y \in B ⟼ C)$
46		eqidd	$⊢ ((((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \land (a \in B \land b \in B \land c \in B)) \land (x = a \land y = b)) \to C = C$
47		simpr1	$⊢ (((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \land (a \in B \land b \in B \land c \in B)) \to a \in B$
48		simpr2	$⊢ (((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \land (a \in B \land b \in B \land c \in B)) \to b \in B$
49	31	adantr	$⊢ (((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \land (a \in B \land b \in B \land c \in B)) \to C \in B$
50	45 46 47 48 49	ovmpod	$⊢ (((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \land (a \in B \land b \in B \land c \in B)) \to a (x \in B, y \in B ⟼ C) b = C$
51		eqidd	$⊢ ((((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \land (a \in B \land b \in B \land c \in B)) \land (x = a \land y = c)) \to C = C$
52		simpr3	$⊢ (((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \land (a \in B \land b \in B \land c \in B)) \to c \in B$
53	45 51 47 52 49	ovmpod	$⊢ (((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \land (a \in B \land b \in B \land c \in B)) \to a (x \in B, y \in B ⟼ C) c = C$
54	50 53	oveq12d	$⊢ (((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \land (a \in B \land b \in B \land c \in B)) \to (a (x \in B, y \in B ⟼ C) b) +_{Y} (a (x \in B, y \in B ⟼ C) c) = C +_{Y} C$
55		eqidd	$⊢ ((((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \land (a \in B \land b \in B \land c \in B)) \land (x = a \land y = b +_{Y} c)) \to C = C$
56	35	ad3antrrr	$⊢ (((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \land (a \in B \land b \in B \land c \in B)) \to Y \in Ring$
57	2 41	ringacl	$⊢ (Y \in Ring \land b \in B \land c \in B) \to b +_{Y} c \in B$
58	56 48 52 57	syl3anc	$⊢ (((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \land (a \in B \land b \in B \land c \in B)) \to b +_{Y} c \in B$
59	45 55 47 58 49	ovmpod	$⊢ (((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \land (a \in B \land b \in B \land c \in B)) \to a (x \in B, y \in B ⟼ C) (b +_{Y} c) = C$
60	44 54 59	3eqtr4rd	$⊢ (((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \land (a \in B \land b \in B \land c \in B)) \to a (x \in B, y \in B ⟼ C) (b +_{Y} c) = (a (x \in B, y \in B ⟼ C) b) +_{Y} (a (x \in B, y \in B ⟼ C) c)$
61		eqidd	$⊢ ((((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \land (a \in B \land b \in B \land c \in B)) \land (x = b \land y = c)) \to C = C$
62	45 61 48 52 49	ovmpod	$⊢ (((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \land (a \in B \land b \in B \land c \in B)) \to b (x \in B, y \in B ⟼ C) c = C$
63	53 62	oveq12d	$⊢ (((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \land (a \in B \land b \in B \land c \in B)) \to (a (x \in B, y \in B ⟼ C) c) +_{Y} (b (x \in B, y \in B ⟼ C) c) = C +_{Y} C$
64		eqidd	$⊢ ((((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \land (a \in B \land b \in B \land c \in B)) \land (x = a +_{Y} b \land y = c)) \to C = C$
65	2 41	ringacl	$⊢ (Y \in Ring \land a \in B \land b \in B) \to a +_{Y} b \in B$
66	56 47 48 65	syl3anc	$⊢ (((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \land (a \in B \land b \in B \land c \in B)) \to a +_{Y} b \in B$
67	45 64 66 52 49	ovmpod	$⊢ (((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \land (a \in B \land b \in B \land c \in B)) \to (a +_{Y} b) (x \in B, y \in B ⟼ C) c = C$
68	44 63 67	3eqtr4rd	$⊢ (((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \land (a \in B \land b \in B \land c \in B)) \to (a +_{Y} b) (x \in B, y \in B ⟼ C) c = (a (x \in B, y \in B ⟼ C) c) +_{Y} (b (x \in B, y \in B ⟼ C) c)$
69	60 68	jca	$⊢ (((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \land (a \in B \land b \in B \land c \in B)) \to (a (x \in B, y \in B ⟼ C) (b +_{Y} c) = (a (x \in B, y \in B ⟼ C) b) +_{Y} (a (x \in B, y \in B ⟼ C) c) \land (a +_{Y} b) (x \in B, y \in B ⟼ C) c = (a (x \in B, y \in B ⟼ C) c) +_{Y} (b (x \in B, y \in B ⟼ C) c))$
70	69	ralrimivvva	$⊢ ((N \in ℕ \land C = \underset{˙}{0}) \land C \in B) \to \forall a \in B \forall b \in B \forall c \in B (a (x \in B, y \in B ⟼ C) (b +_{Y} c) = (a (x \in B, y \in B ⟼ C) b) +_{Y} (a (x \in B, y \in B ⟼ C) c) \land (a +_{Y} b) (x \in B, y \in B ⟼ C) c = (a (x \in B, y \in B ⟼ C) c) +_{Y} (b (x \in B, y \in B ⟼ C) c))$
71	16 32 70	3jca	Could not format ( ( ( 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 ) ) ) ) ) : No typesetting found for \|- ( ( ( 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 ) ) ) ) ) with typecode \|-
72	14 71	mpdan	Could not format ( ( 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 ) ) ) ) ) : No typesetting found for \|- ( ( 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 ) ) ) ) ) with typecode \|-
73		plusgid	$⊢ +_{𝑔} = Slot +_{ndx}$
74		plusgndxnmulrndx	$⊢ +_{ndx} \neq \cdot_{ndx}$
75	73 74	setsnid	$⊢ +_{Y} = +_{(Y sSet ⟨\cdot_{ndx}, (x \in B, y \in B ⟼ C)⟩)}$
76	3	fveq2i	$⊢ +_{X} = +_{(Y sSet ⟨\cdot_{ndx}, (x \in B, y \in B ⟼ C)⟩)}$
77	75 76	eqtr4i	$⊢ +_{Y} = +_{X}$
78	3	eqcomi	$⊢ Y sSet ⟨\cdot_{ndx}, (x \in B, y \in B ⟼ C)⟩ = X$
79	78	fveq2i	$⊢ \cdot_{(Y sSet ⟨\cdot_{ndx}, (x \in B, y \in B ⟼ C)⟩)} = \cdot_{X}$
80	26 79	eqtri	$⊢ (x \in B, y \in B ⟼ C) = \cdot_{X}$
81	18 17 77 80	isrng	Could not format ( 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 ) ) ) ) ) : No typesetting found for \|- ( 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 ) ) ) ) ) with typecode \|-
82	72 81	sylibr	$⊢ (N \in ℕ \land C = \underset{˙}{0}) \to X \in Rng$

Metamath Proof Explorer

Theorem cznrng

Proof