Metamath Proof Explorer

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 ⊢ ℤs = ( Base ‘ 𝐾 )
zsoring.2 ⊢ ( +s ↾ ( ℤs × ℤs ) ) = ( +g ‘ 𝐾 )
zsoring.3 ⊢ ( ·s ↾ ( ℤs × ℤs ) ) = ( .r ‘ 𝐾 )
zsoring.4 ⊢ ( ≤s ∩ ( ℤs × ℤs ) ) = ( le ‘ 𝐾 )
zsoring.5 ⊢ 0s = ( 0g ‘ 𝐾 )
Assertion zsoring 𝐾 ∈ oRing

Proof

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