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