zsoring

Description: The surreal integers form an ordered ring. Note that we have to restrict the operations here since No is a proper class. (Contributed by Scott Fenton, 23-Dec-2025)

	Ref	Expression
Hypotheses	zsoring.1	$⊢ ℤ_{s} = {Base}_{K}$
	zsoring.2	$⊢ {+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})} = +_{K}$
	zsoring.3	$⊢ {\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})} = \cdot_{K}$
	zsoring.4	$⊢ \leq_{s} \cap (ℤ_{s} \times ℤ_{s}) = \leq_{K}$
	zsoring.5	$⊢ 0_{s} = 0_{K}$
Assertion	zsoring	$⊢ K \in oRing$

Proof

Step	Hyp	Ref	Expression
1		zsoring.1	$⊢ ℤ_{s} = {Base}_{K}$
2		zsoring.2	$⊢ {+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})} = +_{K}$
3		zsoring.3	$⊢ {\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})} = \cdot_{K}$
4		zsoring.4	$⊢ \leq_{s} \cap (ℤ_{s} \times ℤ_{s}) = \leq_{K}$
5		zsoring.5	$⊢ 0_{s} = 0_{K}$
6		ovres	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s}) \to x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y = x +_{s} y$
7		zaddscl	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s}) \to x +_{s} y \in ℤ_{s}$
8	6 7	eqeltrd	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s}) \to x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y \in ℤ_{s}$
9		zno	$⊢ x \in ℤ_{s} \to x \in No$
10		zno	$⊢ y \in ℤ_{s} \to y \in No$
11		zno	$⊢ z \in ℤ_{s} \to z \in No$
12		addsass	$⊢ (x \in No \land y \in No \land z \in No) \to (x +_{s} y) +_{s} z = x +_{s} (y +_{s} z)$
13	9 10 11 12	syl3an	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x +_{s} y) +_{s} z = x +_{s} (y +_{s} z)$
14	6	3adant3	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y = x +_{s} y$
15	14	oveq1d	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = (x +_{s} y) ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z$
16	7	3adant3	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to x +_{s} y \in ℤ_{s}$
17		simp3	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to z \in ℤ_{s}$
18	16 17	ovresd	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x +_{s} y) ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = (x +_{s} y) +_{s} z$
19	15 18	eqtrd	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = (x +_{s} y) +_{s} z$
20		ovres	$⊢ (y \in ℤ_{s} \land z \in ℤ_{s}) \to y ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = y +_{s} z$
21	20	3adant1	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to y ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = y +_{s} z$
22	21	oveq2d	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z) = x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y +_{s} z)$
23		simp1	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to x \in ℤ_{s}$
24		zaddscl	$⊢ (y \in ℤ_{s} \land z \in ℤ_{s}) \to y +_{s} z \in ℤ_{s}$
25	24	3adant1	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to y +_{s} z \in ℤ_{s}$
26	23 25	ovresd	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y +_{s} z) = x +_{s} (y +_{s} z)$
27	22 26	eqtrd	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z) = x +_{s} (y +_{s} z)$
28	13 19 27	3eqtr4d	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z)$
29		0zs	$⊢ 0_{s} \in ℤ_{s}$
30		ovres	$⊢ (0_{s} \in ℤ_{s} \land x \in ℤ_{s}) \to 0_{s} ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x = 0_{s} +_{s} x$
31	29 30	mpan	$⊢ x \in ℤ_{s} \to 0_{s} ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x = 0_{s} +_{s} x$
32		addslid	$⊢ x \in No \to 0_{s} +_{s} x = x$
33	9 32	syl	$⊢ x \in ℤ_{s} \to 0_{s} +_{s} x = x$
34	31 33	eqtrd	$⊢ x \in ℤ_{s} \to 0_{s} ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x = x$
35		znegscl	$⊢ x \in ℤ_{s} \to +_{s} (x) \in ℤ_{s}$
36		id	$⊢ x \in ℤ_{s} \to x \in ℤ_{s}$
37	35 36	ovresd	$⊢ x \in ℤ_{s} \to +_{s} (x) ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x = +_{s} (x) +_{s} x$
38	35	znod	$⊢ x \in ℤ_{s} \to +_{s} (x) \in No$
39	38 9	addscomd	$⊢ x \in ℤ_{s} \to +_{s} (x) +_{s} x = x +_{s} +_{s} (x)$
40	9	negsidd	$⊢ x \in ℤ_{s} \to x +_{s} +_{s} (x) = 0_{s}$
41	37 39 40	3eqtrd	$⊢ x \in ℤ_{s} \to +_{s} (x) ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x = 0_{s}$
42	1 2 8 28 29 34 35 41	isgrpi	$⊢ K \in Grp$
43		ovres	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s}) \to x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y = x \cdot_{s} y$
44		simpl	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s}) \to x \in ℤ_{s}$
45		simpr	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s}) \to y \in ℤ_{s}$
46	44 45	zmulscld	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s}) \to x \cdot_{s} y \in ℤ_{s}$
47	43 46	eqeltrd	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s}) \to x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y \in ℤ_{s}$
48		mulsass	$⊢ (x \in No \land y \in No \land z \in No) \to (x \cdot_{s} y) \cdot_{s} z = x \cdot_{s} (y \cdot_{s} z)$
49	9 10 11 48	syl3an	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x \cdot_{s} y) \cdot_{s} z = x \cdot_{s} (y \cdot_{s} z)$
50	43	3adant3	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y = x \cdot_{s} y$
51	50	oveq1d	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = (x \cdot_{s} y) ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z$
52		simp2	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to y \in ℤ_{s}$
53	23 52	zmulscld	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to x \cdot_{s} y \in ℤ_{s}$
54	53 17	ovresd	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x \cdot_{s} y) ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = (x \cdot_{s} y) \cdot_{s} z$
55	51 54	eqtrd	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = (x \cdot_{s} y) \cdot_{s} z$
56		ovres	$⊢ (y \in ℤ_{s} \land z \in ℤ_{s}) \to y ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = y \cdot_{s} z$
57	56	3adant1	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to y ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = y \cdot_{s} z$
58	57	oveq2d	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z) = x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y \cdot_{s} z)$
59	52 17	zmulscld	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to y \cdot_{s} z \in ℤ_{s}$
60	23 59	ovresd	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y \cdot_{s} z) = x \cdot_{s} (y \cdot_{s} z)$
61	58 60	eqtrd	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z) = x \cdot_{s} (y \cdot_{s} z)$
62	49 55 61	3eqtr4d	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z)$
63	62	3expa	$⊢ ((x \in ℤ_{s} \land y \in ℤ_{s}) \land z \in ℤ_{s}) \to (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z)$
64	63	ralrimiva	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s}) \to \forall z \in ℤ_{s} (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z)$
65	47 64	jca	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s}) \to (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y \in ℤ_{s} \land \forall z \in ℤ_{s} (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z))$
66	65	rgen2	$⊢ \forall x \in ℤ_{s} \forall y \in ℤ_{s} (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y \in ℤ_{s} \land \forall z \in ℤ_{s} (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z))$
67		1zs	$⊢ 1_{s} \in ℤ_{s}$
68		ovres	$⊢ (1_{s} \in ℤ_{s} \land x \in ℤ_{s}) \to 1_{s} ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x = 1_{s} \cdot_{s} x$
69	67 68	mpan	$⊢ x \in ℤ_{s} \to 1_{s} ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x = 1_{s} \cdot_{s} x$
70	9	mulslidd	$⊢ x \in ℤ_{s} \to 1_{s} \cdot_{s} x = x$
71	69 70	eqtrd	$⊢ x \in ℤ_{s} \to 1_{s} ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x = x$
72		ovres	$⊢ (x \in ℤ_{s} \land 1_{s} \in ℤ_{s}) \to x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) 1_{s} = x \cdot_{s} 1_{s}$
73	67 72	mpan2	$⊢ x \in ℤ_{s} \to x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) 1_{s} = x \cdot_{s} 1_{s}$
74	9	mulsridd	$⊢ x \in ℤ_{s} \to x \cdot_{s} 1_{s} = x$
75	73 74	eqtrd	$⊢ x \in ℤ_{s} \to x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) 1_{s} = x$
76	71 75	jca	$⊢ x \in ℤ_{s} \to (1_{s} ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x = x \land x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) 1_{s} = x)$
77	76	rgen	$⊢ \forall x \in ℤ_{s} (1_{s} ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x = x \land x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) 1_{s} = x)$
78		oveq1	$⊢ y = 1_{s} \to y ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x = 1_{s} ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x$
79	78	eqeq1d	$⊢ y = 1_{s} \to (y ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x = x \leftrightarrow 1_{s} ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x = x)$
80	79	ovanraleqv	$⊢ y = 1_{s} \to (\forall x \in ℤ_{s} (y ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x = x \land x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y = x) \leftrightarrow \forall x \in ℤ_{s} (1_{s} ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x = x \land x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) 1_{s} = x))$
81	80	rspcev	$⊢ (1_{s} \in ℤ_{s} \land \forall x \in ℤ_{s} (1_{s} ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x = x \land x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) 1_{s} = x)) \to \exists y \in ℤ_{s} \forall x \in ℤ_{s} (y ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x = x \land x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y = x)$
82	67 77 81	mp2an	$⊢ \exists y \in ℤ_{s} \forall x \in ℤ_{s} (y ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x = x \land x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y = x)$
83		eqid	$⊢ {mulGrp}_{K} = {mulGrp}_{K}$
84	83 1	mgpbas	$⊢ ℤ_{s} = {Base}_{{mulGrp}_{K}}$
85	83 3	mgpplusg	$⊢ {\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})} = +_{{mulGrp}_{K}}$
86	84 85	ismnd	$⊢ {mulGrp}_{K} \in Mnd \leftrightarrow (\forall x \in ℤ_{s} \forall y \in ℤ_{s} (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y \in ℤ_{s} \land \forall z \in ℤ_{s} (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z)) \land \exists y \in ℤ_{s} \forall x \in ℤ_{s} (y ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x = x \land x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y = x))$
87	66 82 86	mpbir2an	$⊢ {mulGrp}_{K} \in Mnd$
88		addsdi	$⊢ (x \in No \land y \in No \land z \in No) \to x \cdot_{s} (y +_{s} z) = (x \cdot_{s} y) +_{s} (x \cdot_{s} z)$
89	9 10 11 88	syl3an	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to x \cdot_{s} (y +_{s} z) = (x \cdot_{s} y) +_{s} (x \cdot_{s} z)$
90	21	oveq2d	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z) = x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y +_{s} z)$
91	23 25	ovresd	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y +_{s} z) = x \cdot_{s} (y +_{s} z)$
92	90 91	eqtrd	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z) = x \cdot_{s} (y +_{s} z)$
93		ovres	$⊢ (x \in ℤ_{s} \land z \in ℤ_{s}) \to x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = x \cdot_{s} z$
94	93	3adant2	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = x \cdot_{s} z$
95	50 94	oveq12d	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z) = (x \cdot_{s} y) ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (x \cdot_{s} z)$
96	23 17	zmulscld	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to x \cdot_{s} z \in ℤ_{s}$
97	53 96	ovresd	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x \cdot_{s} y) ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (x \cdot_{s} z) = (x \cdot_{s} y) +_{s} (x \cdot_{s} z)$
98	95 97	eqtrd	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z) = (x \cdot_{s} y) +_{s} (x \cdot_{s} z)$
99	89 92 98	3eqtr4d	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z) = (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z)$
100	23	znod	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to x \in No$
101	52	znod	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to y \in No$
102	17	znod	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to z \in No$
103	100 101 102	addsdird	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x +_{s} y) \cdot_{s} z = (x \cdot_{s} z) +_{s} (y \cdot_{s} z)$
104	14	oveq1d	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = (x +_{s} y) ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z$
105	16 17	ovresd	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x +_{s} y) ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = (x +_{s} y) \cdot_{s} z$
106	104 105	eqtrd	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = (x +_{s} y) \cdot_{s} z$
107	94 57	oveq12d	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z) ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z) = (x \cdot_{s} z) ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y \cdot_{s} z)$
108	96 59	ovresd	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x \cdot_{s} z) ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y \cdot_{s} z) = (x \cdot_{s} z) +_{s} (y \cdot_{s} z)$
109	107 108	eqtrd	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z) ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z) = (x \cdot_{s} z) +_{s} (y \cdot_{s} z)$
110	103 106 109	3eqtr4d	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z) ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z)$
111	99 110	jca	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z) = (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z) \land (x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z) ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z))$
112	111	rgen3	$⊢ \forall x \in ℤ_{s} \forall y \in ℤ_{s} \forall z \in ℤ_{s} (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z) = (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z) \land (x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z) ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z))$
113	1 83 2 3	isring	$⊢ K \in Ring \leftrightarrow (K \in Grp \land {mulGrp}_{K} \in Mnd \land \forall x \in ℤ_{s} \forall y \in ℤ_{s} \forall z \in ℤ_{s} (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z) = (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z) \land (x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z) ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z)))$
114	42 87 112 113	mpbir3an	$⊢ K \in Ring$
115	28	3expa	$⊢ ((x \in ℤ_{s} \land y \in ℤ_{s}) \land z \in ℤ_{s}) \to (x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z)$
116	115	ralrimiva	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s}) \to \forall z \in ℤ_{s} (x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z)$
117	8 116	jca	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s}) \to (x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y \in ℤ_{s} \land \forall z \in ℤ_{s} (x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z))$
118	117	rgen2	$⊢ \forall x \in ℤ_{s} \forall y \in ℤ_{s} (x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y \in ℤ_{s} \land \forall z \in ℤ_{s} (x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z))$
119		ovres	$⊢ (x \in ℤ_{s} \land 0_{s} \in ℤ_{s}) \to x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) 0_{s} = x +_{s} 0_{s}$
120	29 119	mpan2	$⊢ x \in ℤ_{s} \to x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) 0_{s} = x +_{s} 0_{s}$
121	9	addsridd	$⊢ x \in ℤ_{s} \to x +_{s} 0_{s} = x$
122	120 121	eqtrd	$⊢ x \in ℤ_{s} \to x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) 0_{s} = x$
123	34 122	jca	$⊢ x \in ℤ_{s} \to (0_{s} ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x = x \land x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) 0_{s} = x)$
124	123	rgen	$⊢ \forall x \in ℤ_{s} (0_{s} ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x = x \land x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) 0_{s} = x)$
125		oveq1	$⊢ y = 0_{s} \to y ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x = 0_{s} ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x$
126	125	eqeq1d	$⊢ y = 0_{s} \to (y ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x = x \leftrightarrow 0_{s} ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x = x)$
127	126	ovanraleqv	$⊢ y = 0_{s} \to (\forall x \in ℤ_{s} (y ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x = x \land x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y = x) \leftrightarrow \forall x \in ℤ_{s} (0_{s} ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x = x \land x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) 0_{s} = x))$
128	127	rspcev	$⊢ (0_{s} \in ℤ_{s} \land \forall x \in ℤ_{s} (0_{s} ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x = x \land x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) 0_{s} = x)) \to \exists y \in ℤ_{s} \forall x \in ℤ_{s} (y ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x = x \land x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y = x)$
129	29 124 128	mp2an	$⊢ \exists y \in ℤ_{s} \forall x \in ℤ_{s} (y ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x = x \land x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y = x)$
130	1 2	ismnd	$⊢ K \in Mnd \leftrightarrow (\forall x \in ℤ_{s} \forall y \in ℤ_{s} (x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y \in ℤ_{s} \land \forall z \in ℤ_{s} (x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) (y ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z)) \land \exists y \in ℤ_{s} \forall x \in ℤ_{s} (y ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) x = x \land x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y = x))$
131	118 129 130	mpbir2an	$⊢ K \in Mnd$
132	42	elexi	$⊢ K \in V$
133		lesid	$⊢ x \in No \to x \leq_{s} x$
134	9 133	syl	$⊢ x \in ℤ_{s} \to x \leq_{s} x$
135		brxp	$⊢ x (ℤ_{s} \times ℤ_{s}) x \leftrightarrow (x \in ℤ_{s} \land x \in ℤ_{s})$
136	135	biimpri	$⊢ (x \in ℤ_{s} \land x \in ℤ_{s}) \to x (ℤ_{s} \times ℤ_{s}) x$
137	136	anidms	$⊢ x \in ℤ_{s} \to x (ℤ_{s} \times ℤ_{s}) x$
138		brin	$⊢ x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) x \leftrightarrow (x \leq_{s} x \land x (ℤ_{s} \times ℤ_{s}) x)$
139	134 137 138	sylanbrc	$⊢ x \in ℤ_{s} \to x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) x$
140	139	3ad2ant1	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) x$
141		brin	$⊢ x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) y \leftrightarrow (x \leq_{s} y \land x (ℤ_{s} \times ℤ_{s}) y)$
142		brxp	$⊢ x (ℤ_{s} \times ℤ_{s}) y \leftrightarrow (x \in ℤ_{s} \land y \in ℤ_{s})$
143	142	biimpri	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s}) \to x (ℤ_{s} \times ℤ_{s}) y$
144	143	3adant3	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to x (ℤ_{s} \times ℤ_{s}) y$
145	144	biantrud	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x \leq_{s} y \leftrightarrow (x \leq_{s} y \land x (ℤ_{s} \times ℤ_{s}) y))$
146	141 145	bitr4id	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) y \leftrightarrow x \leq_{s} y)$
147		brin	$⊢ y (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) x \leftrightarrow (y \leq_{s} x \land y (ℤ_{s} \times ℤ_{s}) x)$
148		brxp	$⊢ y (ℤ_{s} \times ℤ_{s}) x \leftrightarrow (y \in ℤ_{s} \land x \in ℤ_{s})$
149	148	biimpri	$⊢ (y \in ℤ_{s} \land x \in ℤ_{s}) \to y (ℤ_{s} \times ℤ_{s}) x$
150	149	ancoms	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s}) \to y (ℤ_{s} \times ℤ_{s}) x$
151	150	biantrud	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s}) \to (y \leq_{s} x \leftrightarrow (y \leq_{s} x \land y (ℤ_{s} \times ℤ_{s}) x))$
152	147 151	bitr4id	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s}) \to (y (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) x \leftrightarrow y \leq_{s} x)$
153	152	3adant3	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (y (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) x \leftrightarrow y \leq_{s} x)$
154	146 153	anbi12d	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to ((x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) y \land y (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) x) \leftrightarrow (x \leq_{s} y \land y \leq_{s} x))$
155		lestri3	$⊢ (x \in No \land y \in No) \to (x = y \leftrightarrow (x \leq_{s} y \land y \leq_{s} x))$
156	9 10 155	syl2an	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s}) \to (x = y \leftrightarrow (x \leq_{s} y \land y \leq_{s} x))$
157	156	3adant3	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x = y \leftrightarrow (x \leq_{s} y \land y \leq_{s} x))$
158	157	biimprd	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to ((x \leq_{s} y \land y \leq_{s} x) \to x = y)$
159	154 158	sylbid	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to ((x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) y \land y (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) x) \to x = y)$
160		lestr	$⊢ (x \in No \land y \in No \land z \in No) \to ((x \leq_{s} y \land y \leq_{s} z) \to x \leq_{s} z)$
161	9 10 11 160	syl3an	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to ((x \leq_{s} y \land y \leq_{s} z) \to x \leq_{s} z)$
162	143	biantrud	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s}) \to (x \leq_{s} y \leftrightarrow (x \leq_{s} y \land x (ℤ_{s} \times ℤ_{s}) y))$
163	141 162	bitr4id	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s}) \to (x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) y \leftrightarrow x \leq_{s} y)$
164	163	3adant3	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) y \leftrightarrow x \leq_{s} y)$
165		brin	$⊢ y (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) z \leftrightarrow (y \leq_{s} z \land y (ℤ_{s} \times ℤ_{s}) z)$
166		brxp	$⊢ y (ℤ_{s} \times ℤ_{s}) z \leftrightarrow (y \in ℤ_{s} \land z \in ℤ_{s})$
167	166	biimpri	$⊢ (y \in ℤ_{s} \land z \in ℤ_{s}) \to y (ℤ_{s} \times ℤ_{s}) z$
168	167	3adant1	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to y (ℤ_{s} \times ℤ_{s}) z$
169	168	biantrud	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (y \leq_{s} z \leftrightarrow (y \leq_{s} z \land y (ℤ_{s} \times ℤ_{s}) z))$
170	165 169	bitr4id	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (y (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) z \leftrightarrow y \leq_{s} z)$
171	164 170	anbi12d	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to ((x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) y \land y (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) z) \leftrightarrow (x \leq_{s} y \land y \leq_{s} z))$
172		brin	$⊢ x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) z \leftrightarrow (x \leq_{s} z \land x (ℤ_{s} \times ℤ_{s}) z)$
173		brxp	$⊢ x (ℤ_{s} \times ℤ_{s}) z \leftrightarrow (x \in ℤ_{s} \land z \in ℤ_{s})$
174	173	biimpri	$⊢ (x \in ℤ_{s} \land z \in ℤ_{s}) \to x (ℤ_{s} \times ℤ_{s}) z$
175	174	3adant2	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to x (ℤ_{s} \times ℤ_{s}) z$
176	175	biantrud	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x \leq_{s} z \leftrightarrow (x \leq_{s} z \land x (ℤ_{s} \times ℤ_{s}) z))$
177	172 176	bitr4id	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) z \leftrightarrow x \leq_{s} z)$
178	161 171 177	3imtr4d	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to ((x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) y \land y (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) z) \to x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) z)$
179	140 159 178	3jca	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) x \land ((x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) y \land y (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) x) \to x = y) \land ((x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) y \land y (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) z) \to x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) z))$
180	179	rgen3	$⊢ \forall x \in ℤ_{s} \forall y \in ℤ_{s} \forall z \in ℤ_{s} (x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) x \land ((x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) y \land y (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) x) \to x = y) \land ((x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) y \land y (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) z) \to x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) z))$
181	1 4	ispos	$⊢ K \in Poset \leftrightarrow (K \in V \land \forall x \in ℤ_{s} \forall y \in ℤ_{s} \forall z \in ℤ_{s} (x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) x \land ((x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) y \land y (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) x) \to x = y) \land ((x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) y \land y (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) z) \to x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) z)))$
182	132 180 181	mpbir2an	$⊢ K \in Poset$
183		lestric	$⊢ (x \in No \land y \in No) \to (x \leq_{s} y \lor y \leq_{s} x)$
184	9 10 183	syl2an	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s}) \to (x \leq_{s} y \lor y \leq_{s} x)$
185	163 152	orbi12d	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s}) \to ((x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) y \lor y (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) x) \leftrightarrow (x \leq_{s} y \lor y \leq_{s} x))$
186	184 185	mpbird	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s}) \to (x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) y \lor y (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) x)$
187	186	rgen2	$⊢ \forall x \in ℤ_{s} \forall y \in ℤ_{s} (x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) y \lor y (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) x)$
188	1 4	istos	$⊢ K \in Toset \leftrightarrow (K \in Poset \land \forall x \in ℤ_{s} \forall y \in ℤ_{s} (x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) y \lor y (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) x))$
189	182 187 188	mpbir2an	$⊢ K \in Toset$
190		leadds1	$⊢ (x \in No \land y \in No \land z \in No) \to (x \leq_{s} y \leftrightarrow (x +_{s} z) \leq_{s} (y +_{s} z))$
191	9 10 11 190	syl3an	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x \leq_{s} y \leftrightarrow (x +_{s} z) \leq_{s} (y +_{s} z))$
192	191	biimpd	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x \leq_{s} y \to (x +_{s} z) \leq_{s} (y +_{s} z))$
193	23 17	ovresd	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = x +_{s} z$
194	52 17	ovresd	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to y ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z = y +_{s} z$
195	193 194	breq12d	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to ((x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z) (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) (y ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z) \leftrightarrow (x +_{s} z) (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) (y +_{s} z))$
196		brin	$⊢ (x +_{s} z) (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) (y +_{s} z) \leftrightarrow ((x +_{s} z) \leq_{s} (y +_{s} z) \land (x +_{s} z) (ℤ_{s} \times ℤ_{s}) (y +_{s} z))$
197		zaddscl	$⊢ (x \in ℤ_{s} \land z \in ℤ_{s}) \to x +_{s} z \in ℤ_{s}$
198	197	3adant2	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to x +_{s} z \in ℤ_{s}$
199		brxp	$⊢ (x +_{s} z) (ℤ_{s} \times ℤ_{s}) (y +_{s} z) \leftrightarrow (x +_{s} z \in ℤ_{s} \land y +_{s} z \in ℤ_{s})$
200	198 25 199	sylanbrc	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x +_{s} z) (ℤ_{s} \times ℤ_{s}) (y +_{s} z)$
201	200	biantrud	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to ((x +_{s} z) \leq_{s} (y +_{s} z) \leftrightarrow ((x +_{s} z) \leq_{s} (y +_{s} z) \land (x +_{s} z) (ℤ_{s} \times ℤ_{s}) (y +_{s} z)))$
202	196 201	bitr4id	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to ((x +_{s} z) (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) (y +_{s} z) \leftrightarrow (x +_{s} z) \leq_{s} (y +_{s} z))$
203	195 202	bitrd	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to ((x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z) (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) (y ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z) \leftrightarrow (x +_{s} z) \leq_{s} (y +_{s} z))$
204	192 146 203	3imtr4d	$⊢ (x \in ℤ_{s} \land y \in ℤ_{s} \land z \in ℤ_{s}) \to (x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) y \to (x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z) (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) (y ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z))$
205	204	rgen3	$⊢ \forall x \in ℤ_{s} \forall y \in ℤ_{s} \forall z \in ℤ_{s} (x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) y \to (x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z) (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) (y ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z))$
206	1 2 4	isomnd	$⊢ K \in oMnd \leftrightarrow (K \in Mnd \land K \in Toset \land \forall x \in ℤ_{s} \forall y \in ℤ_{s} \forall z \in ℤ_{s} (x (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) y \to (x ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z) (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) (y ({+_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) z)))$
207	131 189 205 206	mpbir3an	$⊢ K \in oMnd$
208		isogrp	$⊢ K \in oGrp \leftrightarrow (K \in Grp \land K \in oMnd)$
209	42 207 208	mpbir2an	$⊢ K \in oGrp$
210		simplr	$⊢ ((0_{s} \leq_{s} x \land x \in ℤ_{s}) \land (0_{s} \leq_{s} y \land y \in ℤ_{s})) \to x \in ℤ_{s}$
211	210	znod	$⊢ ((0_{s} \leq_{s} x \land x \in ℤ_{s}) \land (0_{s} \leq_{s} y \land y \in ℤ_{s})) \to x \in No$
212		simprr	$⊢ ((0_{s} \leq_{s} x \land x \in ℤ_{s}) \land (0_{s} \leq_{s} y \land y \in ℤ_{s})) \to y \in ℤ_{s}$
213	212	znod	$⊢ ((0_{s} \leq_{s} x \land x \in ℤ_{s}) \land (0_{s} \leq_{s} y \land y \in ℤ_{s})) \to y \in No$
214		simpll	$⊢ ((0_{s} \leq_{s} x \land x \in ℤ_{s}) \land (0_{s} \leq_{s} y \land y \in ℤ_{s})) \to 0_{s} \leq_{s} x$
215		simprl	$⊢ ((0_{s} \leq_{s} x \land x \in ℤ_{s}) \land (0_{s} \leq_{s} y \land y \in ℤ_{s})) \to 0_{s} \leq_{s} y$
216	211 213 214 215	mulsge0d	$⊢ ((0_{s} \leq_{s} x \land x \in ℤ_{s}) \land (0_{s} \leq_{s} y \land y \in ℤ_{s})) \to 0_{s} \leq_{s} (x \cdot_{s} y)$
217	210 212	ovresd	$⊢ ((0_{s} \leq_{s} x \land x \in ℤ_{s}) \land (0_{s} \leq_{s} y \land y \in ℤ_{s})) \to x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y = x \cdot_{s} y$
218	216 217	breqtrrd	$⊢ ((0_{s} \leq_{s} x \land x \in ℤ_{s}) \land (0_{s} \leq_{s} y \land y \in ℤ_{s})) \to 0_{s} \leq_{s} (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y)$
219	210 212	zmulscld	$⊢ ((0_{s} \leq_{s} x \land x \in ℤ_{s}) \land (0_{s} \leq_{s} y \land y \in ℤ_{s})) \to x \cdot_{s} y \in ℤ_{s}$
220	217 219	eqeltrd	$⊢ ((0_{s} \leq_{s} x \land x \in ℤ_{s}) \land (0_{s} \leq_{s} y \land y \in ℤ_{s})) \to x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y \in ℤ_{s}$
221	218 220	jca	$⊢ ((0_{s} \leq_{s} x \land x \in ℤ_{s}) \land (0_{s} \leq_{s} y \land y \in ℤ_{s})) \to (0_{s} \leq_{s} (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) \land x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y \in ℤ_{s})$
222		brin	$⊢ 0_{s} (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) x \leftrightarrow (0_{s} \leq_{s} x \land 0_{s} (ℤ_{s} \times ℤ_{s}) x)$
223		brxp	$⊢ 0_{s} (ℤ_{s} \times ℤ_{s}) x \leftrightarrow (0_{s} \in ℤ_{s} \land x \in ℤ_{s})$
224	29 223	mpbiran	$⊢ 0_{s} (ℤ_{s} \times ℤ_{s}) x \leftrightarrow x \in ℤ_{s}$
225	224	anbi2i	$⊢ (0_{s} \leq_{s} x \land 0_{s} (ℤ_{s} \times ℤ_{s}) x) \leftrightarrow (0_{s} \leq_{s} x \land x \in ℤ_{s})$
226	222 225	bitri	$⊢ 0_{s} (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) x \leftrightarrow (0_{s} \leq_{s} x \land x \in ℤ_{s})$
227		brin	$⊢ 0_{s} (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) y \leftrightarrow (0_{s} \leq_{s} y \land 0_{s} (ℤ_{s} \times ℤ_{s}) y)$
228		brxp	$⊢ 0_{s} (ℤ_{s} \times ℤ_{s}) y \leftrightarrow (0_{s} \in ℤ_{s} \land y \in ℤ_{s})$
229	29 228	mpbiran	$⊢ 0_{s} (ℤ_{s} \times ℤ_{s}) y \leftrightarrow y \in ℤ_{s}$
230	229	anbi2i	$⊢ (0_{s} \leq_{s} y \land 0_{s} (ℤ_{s} \times ℤ_{s}) y) \leftrightarrow (0_{s} \leq_{s} y \land y \in ℤ_{s})$
231	227 230	bitri	$⊢ 0_{s} (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) y \leftrightarrow (0_{s} \leq_{s} y \land y \in ℤ_{s})$
232	226 231	anbi12i	$⊢ (0_{s} (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) x \land 0_{s} (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) y) \leftrightarrow ((0_{s} \leq_{s} x \land x \in ℤ_{s}) \land (0_{s} \leq_{s} y \land y \in ℤ_{s}))$
233		brin	$⊢ 0_{s} (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) \leftrightarrow (0_{s} \leq_{s} (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) \land 0_{s} (ℤ_{s} \times ℤ_{s}) (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y))$
234		brxp	$⊢ 0_{s} (ℤ_{s} \times ℤ_{s}) (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) \leftrightarrow (0_{s} \in ℤ_{s} \land x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y \in ℤ_{s})$
235	29 234	mpbiran	$⊢ 0_{s} (ℤ_{s} \times ℤ_{s}) (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) \leftrightarrow x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y \in ℤ_{s}$
236	235	anbi2i	$⊢ (0_{s} \leq_{s} (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) \land 0_{s} (ℤ_{s} \times ℤ_{s}) (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y)) \leftrightarrow (0_{s} \leq_{s} (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) \land x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y \in ℤ_{s})$
237	233 236	bitri	$⊢ 0_{s} (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) \leftrightarrow (0_{s} \leq_{s} (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y) \land x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y \in ℤ_{s})$
238	221 232 237	3imtr4i	$⊢ (0_{s} (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) x \land 0_{s} (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) y) \to 0_{s} (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y)$
239	238	rgen2w	$⊢ \forall x \in ℤ_{s} \forall y \in ℤ_{s} ((0_{s} (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) x \land 0_{s} (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) y) \to 0_{s} (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y))$
240	1 5 3 4	isorng	$⊢ K \in oRing \leftrightarrow (K \in Ring \land K \in oGrp \land \forall x \in ℤ_{s} \forall y \in ℤ_{s} ((0_{s} (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) x \land 0_{s} (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) y) \to 0_{s} (\leq_{s} \cap (ℤ_{s} \times ℤ_{s})) (x ({\cdot_{s} ↾}_{(ℤ_{s} \times ℤ_{s})}) y)))$
241	114 209 239 240	mpbir3an	$⊢ K \in oRing$

Metamath Proof Explorer

Theorem zsoring

Proof