Theorem 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	|- ZZ_s = ( Base ` K )
	zsoring.2	|- ( +s |` ( ZZ_s X. ZZ_s ) ) = ( +g ` K )
	zsoring.3	|- ( x.s |` ( ZZ_s X. ZZ_s ) ) = ( .r ` K )
	zsoring.4	|- ( <_s i^i ( ZZ_s X. ZZ_s ) ) = ( le ` K )
	zsoring.5	|- 0s = ( 0g ` K )
Assertion	zsoring	|- K e. oRing

Proof

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