Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (mulGrp‘𝑟) = (mulGrp‘𝑅)) |
2 | | isrng.g |
. . . . . 6
⊢ 𝐺 = (mulGrp‘𝑅) |
3 | 1, 2 | syl6eqr 2662 |
. . . . 5
⊢ (𝑟 = 𝑅 → (mulGrp‘𝑟) = 𝐺) |
4 | 3 | eleq1d 2672 |
. . . 4
⊢ (𝑟 = 𝑅 → ((mulGrp‘𝑟) ∈ SGrp ↔ 𝐺 ∈ SGrp)) |
5 | | fvex 6113 |
. . . . . 6
⊢
(Base‘𝑟)
∈ V |
6 | 5 | a1i 11 |
. . . . 5
⊢ (𝑟 = 𝑅 → (Base‘𝑟) ∈ V) |
7 | | fveq2 6103 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅)) |
8 | | isrng.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
9 | 7, 8 | syl6eqr 2662 |
. . . . 5
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵) |
10 | | fvex 6113 |
. . . . . . 7
⊢
(+g‘𝑟) ∈ V |
11 | 10 | a1i 11 |
. . . . . 6
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → (+g‘𝑟) ∈ V) |
12 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (+g‘𝑟) = (+g‘𝑅)) |
13 | 12 | adantr 480 |
. . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → (+g‘𝑟) = (+g‘𝑅)) |
14 | | isrng.p |
. . . . . . 7
⊢ + =
(+g‘𝑅) |
15 | 13, 14 | syl6eqr 2662 |
. . . . . 6
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → (+g‘𝑟) = + ) |
16 | | fvex 6113 |
. . . . . . . 8
⊢
(.r‘𝑟) ∈ V |
17 | 16 | a1i 11 |
. . . . . . 7
⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) →
(.r‘𝑟)
∈ V) |
18 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (.r‘𝑟) = (.r‘𝑅)) |
19 | 18 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → (.r‘𝑟) = (.r‘𝑅)) |
20 | 19 | adantr 480 |
. . . . . . . 8
⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) →
(.r‘𝑟) =
(.r‘𝑅)) |
21 | | isrng.t |
. . . . . . . 8
⊢ · =
(.r‘𝑅) |
22 | 20, 21 | syl6eqr 2662 |
. . . . . . 7
⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) →
(.r‘𝑟) =
·
) |
23 | | simpllr 795 |
. . . . . . . 8
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑏 = 𝐵) |
24 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑡 = · ) |
25 | | eqidd 2611 |
. . . . . . . . . . . . 13
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑥 = 𝑥) |
26 | | oveq 6555 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = + → (𝑦𝑝𝑧) = (𝑦 + 𝑧)) |
27 | 26 | ad2antlr 759 |
. . . . . . . . . . . . 13
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (𝑦𝑝𝑧) = (𝑦 + 𝑧)) |
28 | 24, 25, 27 | oveq123d 6570 |
. . . . . . . . . . . 12
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (𝑥𝑡(𝑦𝑝𝑧)) = (𝑥 · (𝑦 + 𝑧))) |
29 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) → 𝑝 = + ) |
30 | 29 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑝 = + ) |
31 | | oveq 6555 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = · → (𝑥𝑡𝑦) = (𝑥 · 𝑦)) |
32 | 31 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (𝑥𝑡𝑦) = (𝑥 · 𝑦)) |
33 | | oveq 6555 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = · → (𝑥𝑡𝑧) = (𝑥 · 𝑧)) |
34 | 33 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (𝑥𝑡𝑧) = (𝑥 · 𝑧)) |
35 | 30, 32, 34 | oveq123d 6570 |
. . . . . . . . . . . 12
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧))) |
36 | 28, 35 | eqeq12d 2625 |
. . . . . . . . . . 11
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ↔ (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)))) |
37 | | oveq 6555 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = + → (𝑥𝑝𝑦) = (𝑥 + 𝑦)) |
38 | 37 | ad2antlr 759 |
. . . . . . . . . . . . 13
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (𝑥𝑝𝑦) = (𝑥 + 𝑦)) |
39 | | eqidd 2611 |
. . . . . . . . . . . . 13
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑧 = 𝑧) |
40 | 24, 38, 39 | oveq123d 6570 |
. . . . . . . . . . . 12
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥 + 𝑦) · 𝑧)) |
41 | | oveq 6555 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = · → (𝑦𝑡𝑧) = (𝑦 · 𝑧)) |
42 | 41 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (𝑦𝑡𝑧) = (𝑦 · 𝑧)) |
43 | 30, 34, 42 | oveq123d 6570 |
. . . . . . . . . . . 12
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) |
44 | 40, 43 | eqeq12d 2625 |
. . . . . . . . . . 11
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)) ↔ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))) |
45 | 36, 44 | anbi12d 743 |
. . . . . . . . . 10
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))) |
46 | 23, 45 | raleqbidv 3129 |
. . . . . . . . 9
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) →
(∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))) |
47 | 23, 46 | raleqbidv 3129 |
. . . . . . . 8
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) →
(∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))) |
48 | 23, 47 | raleqbidv 3129 |
. . . . . . 7
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) →
(∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))) |
49 | 17, 22, 48 | sbcied2 3440 |
. . . . . 6
⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) →
([(.r‘𝑟) / 𝑡]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))) |
50 | 11, 15, 49 | sbcied2 3440 |
. . . . 5
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → ([(+g‘𝑟) / 𝑝][(.r‘𝑟) / 𝑡]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))) |
51 | 6, 9, 50 | sbcied2 3440 |
. . . 4
⊢ (𝑟 = 𝑅 → ([(Base‘𝑟) / 𝑏][(+g‘𝑟) / 𝑝][(.r‘𝑟) / 𝑡]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))) |
52 | 4, 51 | anbi12d 743 |
. . 3
⊢ (𝑟 = 𝑅 → (((mulGrp‘𝑟) ∈ SGrp ∧ [(Base‘𝑟) / 𝑏][(+g‘𝑟) / 𝑝][(.r‘𝑟) / 𝑡]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))) ↔ (𝐺 ∈ SGrp ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))) |
53 | | df-rng0 41665 |
. . 3
⊢ Rng =
{𝑟 ∈ Abel ∣
((mulGrp‘𝑟) ∈
SGrp ∧ [(Base‘𝑟) / 𝑏][(+g‘𝑟) / 𝑝][(.r‘𝑟) / 𝑡]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))))} |
54 | 52, 53 | elrab2 3333 |
. 2
⊢ (𝑅 ∈ Rng ↔ (𝑅 ∈ Abel ∧ (𝐺 ∈ SGrp ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))) |
55 | | 3anass 1035 |
. 2
⊢ ((𝑅 ∈ Abel ∧ 𝐺 ∈ SGrp ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))) ↔ (𝑅 ∈ Abel ∧ (𝐺 ∈ SGrp ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))) |
56 | 54, 55 | bitr4i 266 |
1
⊢ (𝑅 ∈ Rng ↔ (𝑅 ∈ Abel ∧ 𝐺 ∈ SGrp ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))) |