This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) ) )