Metamath Proof Explorer


Theorem issrg

Description: The predicate "is a semiring". (Contributed by Thierry Arnoux, 21-Mar-2018)

Ref Expression
Hypotheses issrg.b 𝐵 = ( Base ‘ 𝑅 )
issrg.g 𝐺 = ( mulGrp ‘ 𝑅 )
issrg.p + = ( +g𝑅 )
issrg.t · = ( .r𝑅 )
issrg.0 0 = ( 0g𝑅 )
Assertion issrg ( 𝑅 ∈ SRing ↔ ( 𝑅 ∈ CMnd ∧ 𝐺 ∈ Mnd ∧ ∀ 𝑥𝐵 ( ∀ 𝑦𝐵𝑧𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( 0 · 𝑥 ) = 0 ∧ ( 𝑥 · 0 ) = 0 ) ) ) )

Proof

Step Hyp Ref Expression
1 issrg.b 𝐵 = ( Base ‘ 𝑅 )
2 issrg.g 𝐺 = ( mulGrp ‘ 𝑅 )
3 issrg.p + = ( +g𝑅 )
4 issrg.t · = ( .r𝑅 )
5 issrg.0 0 = ( 0g𝑅 )
6 2 eleq1i ( 𝐺 ∈ Mnd ↔ ( mulGrp ‘ 𝑅 ) ∈ Mnd )
7 6 bicomi ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ↔ 𝐺 ∈ Mnd )
8 1 fvexi 𝐵 ∈ V
9 3 fvexi + ∈ V
10 4 fvexi · ∈ V
11 10 a1i ( ( 𝑏 = 𝐵𝑝 = + ) → · ∈ V )
12 5 fvexi 0 ∈ V
13 12 a1i ( ( ( 𝑏 = 𝐵𝑝 = + ) ∧ 𝑡 = · ) → 0 ∈ V )
14 simplll ( ( ( ( 𝑏 = 𝐵𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → 𝑏 = 𝐵 )
15 simplr ( ( ( ( 𝑏 = 𝐵𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → 𝑡 = · )
16 eqidd ( ( ( ( 𝑏 = 𝐵𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → 𝑥 = 𝑥 )
17 simpllr ( ( ( ( 𝑏 = 𝐵𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → 𝑝 = + )
18 17 oveqd ( ( ( ( 𝑏 = 𝐵𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → ( 𝑦 𝑝 𝑧 ) = ( 𝑦 + 𝑧 ) )
19 15 16 18 oveq123d ( ( ( ( 𝑏 = 𝐵𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( 𝑥 · ( 𝑦 + 𝑧 ) ) )
20 15 oveqd ( ( ( ( 𝑏 = 𝐵𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → ( 𝑥 𝑡 𝑦 ) = ( 𝑥 · 𝑦 ) )
21 15 oveqd ( ( ( ( 𝑏 = 𝐵𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → ( 𝑥 𝑡 𝑧 ) = ( 𝑥 · 𝑧 ) )
22 17 20 21 oveq123d ( ( ( ( 𝑏 = 𝐵𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) )
23 19 22 eqeq12d ( ( ( ( 𝑏 = 𝐵𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ↔ ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ) )
24 17 oveqd ( ( ( ( 𝑏 = 𝐵𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → ( 𝑥 𝑝 𝑦 ) = ( 𝑥 + 𝑦 ) )
25 eqidd ( ( ( ( 𝑏 = 𝐵𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → 𝑧 = 𝑧 )
26 15 24 25 oveq123d ( ( ( ( 𝑏 = 𝐵𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 + 𝑦 ) · 𝑧 ) )
27 15 oveqd ( ( ( ( 𝑏 = 𝐵𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → ( 𝑦 𝑡 𝑧 ) = ( 𝑦 · 𝑧 ) )
28 17 21 27 oveq123d ( ( ( ( 𝑏 = 𝐵𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) )
29 26 28 eqeq12d ( ( ( ( 𝑏 = 𝐵𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → ( ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ↔ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) )
30 23 29 anbi12d ( ( ( ( 𝑏 = 𝐵𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → ( ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ↔ ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) )
31 14 30 raleqbidv ( ( ( ( 𝑏 = 𝐵𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → ( ∀ 𝑧𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ↔ ∀ 𝑧𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) )
32 14 31 raleqbidv ( ( ( ( 𝑏 = 𝐵𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → ( ∀ 𝑦𝑏𝑧𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ↔ ∀ 𝑦𝐵𝑧𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) )
33 simpr ( ( ( ( 𝑏 = 𝐵𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → 𝑛 = 0 )
34 15 33 16 oveq123d ( ( ( ( 𝑏 = 𝐵𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → ( 𝑛 𝑡 𝑥 ) = ( 0 · 𝑥 ) )
35 34 33 eqeq12d ( ( ( ( 𝑏 = 𝐵𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → ( ( 𝑛 𝑡 𝑥 ) = 𝑛 ↔ ( 0 · 𝑥 ) = 0 ) )
36 15 16 33 oveq123d ( ( ( ( 𝑏 = 𝐵𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → ( 𝑥 𝑡 𝑛 ) = ( 𝑥 · 0 ) )
37 36 33 eqeq12d ( ( ( ( 𝑏 = 𝐵𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → ( ( 𝑥 𝑡 𝑛 ) = 𝑛 ↔ ( 𝑥 · 0 ) = 0 ) )
38 35 37 anbi12d ( ( ( ( 𝑏 = 𝐵𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → ( ( ( 𝑛 𝑡 𝑥 ) = 𝑛 ∧ ( 𝑥 𝑡 𝑛 ) = 𝑛 ) ↔ ( ( 0 · 𝑥 ) = 0 ∧ ( 𝑥 · 0 ) = 0 ) ) )
39 32 38 anbi12d ( ( ( ( 𝑏 = 𝐵𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → ( ( ∀ 𝑦𝑏𝑧𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ∧ ( ( 𝑛 𝑡 𝑥 ) = 𝑛 ∧ ( 𝑥 𝑡 𝑛 ) = 𝑛 ) ) ↔ ( ∀ 𝑦𝐵𝑧𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( 0 · 𝑥 ) = 0 ∧ ( 𝑥 · 0 ) = 0 ) ) ) )
40 14 39 raleqbidv ( ( ( ( 𝑏 = 𝐵𝑝 = + ) ∧ 𝑡 = · ) ∧ 𝑛 = 0 ) → ( ∀ 𝑥𝑏 ( ∀ 𝑦𝑏𝑧𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ∧ ( ( 𝑛 𝑡 𝑥 ) = 𝑛 ∧ ( 𝑥 𝑡 𝑛 ) = 𝑛 ) ) ↔ ∀ 𝑥𝐵 ( ∀ 𝑦𝐵𝑧𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( 0 · 𝑥 ) = 0 ∧ ( 𝑥 · 0 ) = 0 ) ) ) )
41 13 40 sbcied ( ( ( 𝑏 = 𝐵𝑝 = + ) ∧ 𝑡 = · ) → ( [ 0 / 𝑛 ]𝑥𝑏 ( ∀ 𝑦𝑏𝑧𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ∧ ( ( 𝑛 𝑡 𝑥 ) = 𝑛 ∧ ( 𝑥 𝑡 𝑛 ) = 𝑛 ) ) ↔ ∀ 𝑥𝐵 ( ∀ 𝑦𝐵𝑧𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( 0 · 𝑥 ) = 0 ∧ ( 𝑥 · 0 ) = 0 ) ) ) )
42 11 41 sbcied ( ( 𝑏 = 𝐵𝑝 = + ) → ( [ · / 𝑡 ] [ 0 / 𝑛 ]𝑥𝑏 ( ∀ 𝑦𝑏𝑧𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ∧ ( ( 𝑛 𝑡 𝑥 ) = 𝑛 ∧ ( 𝑥 𝑡 𝑛 ) = 𝑛 ) ) ↔ ∀ 𝑥𝐵 ( ∀ 𝑦𝐵𝑧𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( 0 · 𝑥 ) = 0 ∧ ( 𝑥 · 0 ) = 0 ) ) ) )
43 8 9 42 sbc2ie ( [ 𝐵 / 𝑏 ] [ + / 𝑝 ] [ · / 𝑡 ] [ 0 / 𝑛 ]𝑥𝑏 ( ∀ 𝑦𝑏𝑧𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ∧ ( ( 𝑛 𝑡 𝑥 ) = 𝑛 ∧ ( 𝑥 𝑡 𝑛 ) = 𝑛 ) ) ↔ ∀ 𝑥𝐵 ( ∀ 𝑦𝐵𝑧𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( 0 · 𝑥 ) = 0 ∧ ( 𝑥 · 0 ) = 0 ) ) )
44 7 43 anbi12i ( ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ [ 𝐵 / 𝑏 ] [ + / 𝑝 ] [ · / 𝑡 ] [ 0 / 𝑛 ]𝑥𝑏 ( ∀ 𝑦𝑏𝑧𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ∧ ( ( 𝑛 𝑡 𝑥 ) = 𝑛 ∧ ( 𝑥 𝑡 𝑛 ) = 𝑛 ) ) ) ↔ ( 𝐺 ∈ Mnd ∧ ∀ 𝑥𝐵 ( ∀ 𝑦𝐵𝑧𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( 0 · 𝑥 ) = 0 ∧ ( 𝑥 · 0 ) = 0 ) ) ) )
45 44 anbi2i ( ( 𝑅 ∈ CMnd ∧ ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ [ 𝐵 / 𝑏 ] [ + / 𝑝 ] [ · / 𝑡 ] [ 0 / 𝑛 ]𝑥𝑏 ( ∀ 𝑦𝑏𝑧𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ∧ ( ( 𝑛 𝑡 𝑥 ) = 𝑛 ∧ ( 𝑥 𝑡 𝑛 ) = 𝑛 ) ) ) ) ↔ ( 𝑅 ∈ CMnd ∧ ( 𝐺 ∈ Mnd ∧ ∀ 𝑥𝐵 ( ∀ 𝑦𝐵𝑧𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( 0 · 𝑥 ) = 0 ∧ ( 𝑥 · 0 ) = 0 ) ) ) ) )
46 fveq2 ( 𝑟 = 𝑅 → ( mulGrp ‘ 𝑟 ) = ( mulGrp ‘ 𝑅 ) )
47 46 eleq1d ( 𝑟 = 𝑅 → ( ( mulGrp ‘ 𝑟 ) ∈ Mnd ↔ ( mulGrp ‘ 𝑅 ) ∈ Mnd ) )
48 fveq2 ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
49 48 1 eqtr4di ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = 𝐵 )
50 fveq2 ( 𝑟 = 𝑅 → ( +g𝑟 ) = ( +g𝑅 ) )
51 50 3 eqtr4di ( 𝑟 = 𝑅 → ( +g𝑟 ) = + )
52 fveq2 ( 𝑟 = 𝑅 → ( .r𝑟 ) = ( .r𝑅 ) )
53 52 4 eqtr4di ( 𝑟 = 𝑅 → ( .r𝑟 ) = · )
54 fveq2 ( 𝑟 = 𝑅 → ( 0g𝑟 ) = ( 0g𝑅 ) )
55 54 5 eqtr4di ( 𝑟 = 𝑅 → ( 0g𝑟 ) = 0 )
56 55 sbceq1d ( 𝑟 = 𝑅 → ( [ ( 0g𝑟 ) / 𝑛 ]𝑥𝑏 ( ∀ 𝑦𝑏𝑧𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ∧ ( ( 𝑛 𝑡 𝑥 ) = 𝑛 ∧ ( 𝑥 𝑡 𝑛 ) = 𝑛 ) ) ↔ [ 0 / 𝑛 ]𝑥𝑏 ( ∀ 𝑦𝑏𝑧𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ∧ ( ( 𝑛 𝑡 𝑥 ) = 𝑛 ∧ ( 𝑥 𝑡 𝑛 ) = 𝑛 ) ) ) )
57 53 56 sbceqbid ( 𝑟 = 𝑅 → ( [ ( .r𝑟 ) / 𝑡 ] [ ( 0g𝑟 ) / 𝑛 ]𝑥𝑏 ( ∀ 𝑦𝑏𝑧𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ∧ ( ( 𝑛 𝑡 𝑥 ) = 𝑛 ∧ ( 𝑥 𝑡 𝑛 ) = 𝑛 ) ) ↔ [ · / 𝑡 ] [ 0 / 𝑛 ]𝑥𝑏 ( ∀ 𝑦𝑏𝑧𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ∧ ( ( 𝑛 𝑡 𝑥 ) = 𝑛 ∧ ( 𝑥 𝑡 𝑛 ) = 𝑛 ) ) ) )
58 51 57 sbceqbid ( 𝑟 = 𝑅 → ( [ ( +g𝑟 ) / 𝑝 ] [ ( .r𝑟 ) / 𝑡 ] [ ( 0g𝑟 ) / 𝑛 ]𝑥𝑏 ( ∀ 𝑦𝑏𝑧𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ∧ ( ( 𝑛 𝑡 𝑥 ) = 𝑛 ∧ ( 𝑥 𝑡 𝑛 ) = 𝑛 ) ) ↔ [ + / 𝑝 ] [ · / 𝑡 ] [ 0 / 𝑛 ]𝑥𝑏 ( ∀ 𝑦𝑏𝑧𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ∧ ( ( 𝑛 𝑡 𝑥 ) = 𝑛 ∧ ( 𝑥 𝑡 𝑛 ) = 𝑛 ) ) ) )
59 49 58 sbceqbid ( 𝑟 = 𝑅 → ( [ ( Base ‘ 𝑟 ) / 𝑏 ] [ ( +g𝑟 ) / 𝑝 ] [ ( .r𝑟 ) / 𝑡 ] [ ( 0g𝑟 ) / 𝑛 ]𝑥𝑏 ( ∀ 𝑦𝑏𝑧𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ∧ ( ( 𝑛 𝑡 𝑥 ) = 𝑛 ∧ ( 𝑥 𝑡 𝑛 ) = 𝑛 ) ) ↔ [ 𝐵 / 𝑏 ] [ + / 𝑝 ] [ · / 𝑡 ] [ 0 / 𝑛 ]𝑥𝑏 ( ∀ 𝑦𝑏𝑧𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ∧ ( ( 𝑛 𝑡 𝑥 ) = 𝑛 ∧ ( 𝑥 𝑡 𝑛 ) = 𝑛 ) ) ) )
60 47 59 anbi12d ( 𝑟 = 𝑅 → ( ( ( mulGrp ‘ 𝑟 ) ∈ Mnd ∧ [ ( Base ‘ 𝑟 ) / 𝑏 ] [ ( +g𝑟 ) / 𝑝 ] [ ( .r𝑟 ) / 𝑡 ] [ ( 0g𝑟 ) / 𝑛 ]𝑥𝑏 ( ∀ 𝑦𝑏𝑧𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ∧ ( ( 𝑛 𝑡 𝑥 ) = 𝑛 ∧ ( 𝑥 𝑡 𝑛 ) = 𝑛 ) ) ) ↔ ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ [ 𝐵 / 𝑏 ] [ + / 𝑝 ] [ · / 𝑡 ] [ 0 / 𝑛 ]𝑥𝑏 ( ∀ 𝑦𝑏𝑧𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ∧ ( ( 𝑛 𝑡 𝑥 ) = 𝑛 ∧ ( 𝑥 𝑡 𝑛 ) = 𝑛 ) ) ) ) )
61 df-srg SRing = { 𝑟 ∈ CMnd ∣ ( ( mulGrp ‘ 𝑟 ) ∈ Mnd ∧ [ ( Base ‘ 𝑟 ) / 𝑏 ] [ ( +g𝑟 ) / 𝑝 ] [ ( .r𝑟 ) / 𝑡 ] [ ( 0g𝑟 ) / 𝑛 ]𝑥𝑏 ( ∀ 𝑦𝑏𝑧𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ∧ ( ( 𝑛 𝑡 𝑥 ) = 𝑛 ∧ ( 𝑥 𝑡 𝑛 ) = 𝑛 ) ) ) }
62 60 61 elrab2 ( 𝑅 ∈ SRing ↔ ( 𝑅 ∈ CMnd ∧ ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ [ 𝐵 / 𝑏 ] [ + / 𝑝 ] [ · / 𝑡 ] [ 0 / 𝑛 ]𝑥𝑏 ( ∀ 𝑦𝑏𝑧𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ∧ ( ( 𝑛 𝑡 𝑥 ) = 𝑛 ∧ ( 𝑥 𝑡 𝑛 ) = 𝑛 ) ) ) ) )
63 3anass ( ( 𝑅 ∈ CMnd ∧ 𝐺 ∈ Mnd ∧ ∀ 𝑥𝐵 ( ∀ 𝑦𝐵𝑧𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( 0 · 𝑥 ) = 0 ∧ ( 𝑥 · 0 ) = 0 ) ) ) ↔ ( 𝑅 ∈ CMnd ∧ ( 𝐺 ∈ Mnd ∧ ∀ 𝑥𝐵 ( ∀ 𝑦𝐵𝑧𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( 0 · 𝑥 ) = 0 ∧ ( 𝑥 · 0 ) = 0 ) ) ) ) )
64 45 62 63 3bitr4i ( 𝑅 ∈ SRing ↔ ( 𝑅 ∈ CMnd ∧ 𝐺 ∈ Mnd ∧ ∀ 𝑥𝐵 ( ∀ 𝑦𝐵𝑧𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( 0 · 𝑥 ) = 0 ∧ ( 𝑥 · 0 ) = 0 ) ) ) )