Step |
Hyp |
Ref |
Expression |
1 |
|
isring.b |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
2 |
|
isring.g |
⊢ 𝐺 = ( mulGrp ‘ 𝑅 ) |
3 |
|
isring.p |
⊢ + = ( +g ‘ 𝑅 ) |
4 |
|
isring.t |
⊢ · = ( .r ‘ 𝑅 ) |
5 |
|
fveq2 |
⊢ ( 𝑟 = 𝑅 → ( mulGrp ‘ 𝑟 ) = ( mulGrp ‘ 𝑅 ) ) |
6 |
5 2
|
eqtr4di |
⊢ ( 𝑟 = 𝑅 → ( mulGrp ‘ 𝑟 ) = 𝐺 ) |
7 |
6
|
eleq1d |
⊢ ( 𝑟 = 𝑅 → ( ( mulGrp ‘ 𝑟 ) ∈ Mnd ↔ 𝐺 ∈ Mnd ) ) |
8 |
|
fvexd |
⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) ∈ V ) |
9 |
|
fveq2 |
⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) ) |
10 |
9 1
|
eqtr4di |
⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = 𝐵 ) |
11 |
|
fvexd |
⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) → ( +g ‘ 𝑟 ) ∈ V ) |
12 |
|
simpl |
⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) → 𝑟 = 𝑅 ) |
13 |
12
|
fveq2d |
⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) → ( +g ‘ 𝑟 ) = ( +g ‘ 𝑅 ) ) |
14 |
13 3
|
eqtr4di |
⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) → ( +g ‘ 𝑟 ) = + ) |
15 |
|
fvexd |
⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) → ( .r ‘ 𝑟 ) ∈ V ) |
16 |
|
simpll |
⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) → 𝑟 = 𝑅 ) |
17 |
16
|
fveq2d |
⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) → ( .r ‘ 𝑟 ) = ( .r ‘ 𝑅 ) ) |
18 |
17 4
|
eqtr4di |
⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) → ( .r ‘ 𝑟 ) = · ) |
19 |
|
simpllr |
⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑏 = 𝐵 ) |
20 |
|
simpr |
⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑡 = · ) |
21 |
|
eqidd |
⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑥 = 𝑥 ) |
22 |
|
simplr |
⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑝 = + ) |
23 |
22
|
oveqd |
⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( 𝑦 𝑝 𝑧 ) = ( 𝑦 + 𝑧 ) ) |
24 |
20 21 23
|
oveq123d |
⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( 𝑥 · ( 𝑦 + 𝑧 ) ) ) |
25 |
20
|
oveqd |
⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( 𝑥 𝑡 𝑦 ) = ( 𝑥 · 𝑦 ) ) |
26 |
20
|
oveqd |
⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( 𝑥 𝑡 𝑧 ) = ( 𝑥 · 𝑧 ) ) |
27 |
22 25 26
|
oveq123d |
⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ) |
28 |
24 27
|
eqeq12d |
⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ↔ ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ) ) |
29 |
22
|
oveqd |
⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( 𝑥 𝑝 𝑦 ) = ( 𝑥 + 𝑦 ) ) |
30 |
|
eqidd |
⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑧 = 𝑧 ) |
31 |
20 29 30
|
oveq123d |
⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 + 𝑦 ) · 𝑧 ) ) |
32 |
20
|
oveqd |
⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( 𝑦 𝑡 𝑧 ) = ( 𝑦 · 𝑧 ) ) |
33 |
22 26 32
|
oveq123d |
⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) |
34 |
31 33
|
eqeq12d |
⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ↔ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) |
35 |
28 34
|
anbi12d |
⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ↔ ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) ) |
36 |
19 35
|
raleqbidv |
⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ↔ ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) ) |
37 |
19 36
|
raleqbidv |
⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) ) |
38 |
19 37
|
raleqbidv |
⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) ) |
39 |
15 18 38
|
sbcied2 |
⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) → ( [ ( .r ‘ 𝑟 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) ) |
40 |
11 14 39
|
sbcied2 |
⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) → ( [ ( +g ‘ 𝑟 ) / 𝑝 ] [ ( .r ‘ 𝑟 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) ) |
41 |
8 10 40
|
sbcied2 |
⊢ ( 𝑟 = 𝑅 → ( [ ( Base ‘ 𝑟 ) / 𝑏 ] [ ( +g ‘ 𝑟 ) / 𝑝 ] [ ( .r ‘ 𝑟 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) ) |
42 |
7 41
|
anbi12d |
⊢ ( 𝑟 = 𝑅 → ( ( ( mulGrp ‘ 𝑟 ) ∈ Mnd ∧ [ ( Base ‘ 𝑟 ) / 𝑏 ] [ ( +g ‘ 𝑟 ) / 𝑝 ] [ ( .r ‘ 𝑟 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ) ↔ ( 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) ) ) |
43 |
|
df-ring |
⊢ Ring = { 𝑟 ∈ Grp ∣ ( ( mulGrp ‘ 𝑟 ) ∈ Mnd ∧ [ ( Base ‘ 𝑟 ) / 𝑏 ] [ ( +g ‘ 𝑟 ) / 𝑝 ] [ ( .r ‘ 𝑟 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ) } |
44 |
42 43
|
elrab2 |
⊢ ( 𝑅 ∈ Ring ↔ ( 𝑅 ∈ Grp ∧ ( 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) ) ) |
45 |
|
3anass |
⊢ ( ( 𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) ↔ ( 𝑅 ∈ Grp ∧ ( 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) ) ) |
46 |
44 45
|
bitr4i |
⊢ ( 𝑅 ∈ Ring ↔ ( 𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) ) |