| Step | Hyp | Ref
| Expression |
| 1 | | fveq2 6906 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (mulGrp‘𝑟) = (mulGrp‘𝑅)) |
| 2 | | isrng.g |
. . . . . 6
⊢ 𝐺 = (mulGrp‘𝑅) |
| 3 | 1, 2 | eqtr4di 2795 |
. . . . 5
⊢ (𝑟 = 𝑅 → (mulGrp‘𝑟) = 𝐺) |
| 4 | 3 | eleq1d 2826 |
. . . 4
⊢ (𝑟 = 𝑅 → ((mulGrp‘𝑟) ∈ Smgrp ↔ 𝐺 ∈ Smgrp)) |
| 5 | | fvexd 6921 |
. . . . 5
⊢ (𝑟 = 𝑅 → (Base‘𝑟) ∈ V) |
| 6 | | fveq2 6906 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅)) |
| 7 | | isrng.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
| 8 | 6, 7 | eqtr4di 2795 |
. . . . 5
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵) |
| 9 | | fvexd 6921 |
. . . . . 6
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → (+g‘𝑟) ∈ V) |
| 10 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (+g‘𝑟) = (+g‘𝑅)) |
| 11 | 10 | adantr 480 |
. . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → (+g‘𝑟) = (+g‘𝑅)) |
| 12 | | isrng.p |
. . . . . . 7
⊢ + =
(+g‘𝑅) |
| 13 | 11, 12 | eqtr4di 2795 |
. . . . . 6
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → (+g‘𝑟) = + ) |
| 14 | | fvexd 6921 |
. . . . . . 7
⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) →
(.r‘𝑟)
∈ V) |
| 15 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (.r‘𝑟) = (.r‘𝑅)) |
| 16 | 15 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → (.r‘𝑟) = (.r‘𝑅)) |
| 17 | 16 | adantr 480 |
. . . . . . . 8
⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) →
(.r‘𝑟) =
(.r‘𝑅)) |
| 18 | | isrng.t |
. . . . . . . 8
⊢ · =
(.r‘𝑅) |
| 19 | 17, 18 | eqtr4di 2795 |
. . . . . . 7
⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) →
(.r‘𝑟) =
·
) |
| 20 | | simpllr 776 |
. . . . . . . 8
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑏 = 𝐵) |
| 21 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑡 = · ) |
| 22 | | eqidd 2738 |
. . . . . . . . . . . . 13
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑥 = 𝑥) |
| 23 | | oveq 7437 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = + → (𝑦𝑝𝑧) = (𝑦 + 𝑧)) |
| 24 | 23 | ad2antlr 727 |
. . . . . . . . . . . . 13
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (𝑦𝑝𝑧) = (𝑦 + 𝑧)) |
| 25 | 21, 22, 24 | oveq123d 7452 |
. . . . . . . . . . . 12
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (𝑥𝑡(𝑦𝑝𝑧)) = (𝑥 · (𝑦 + 𝑧))) |
| 26 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) → 𝑝 = + ) |
| 27 | 26 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑝 = + ) |
| 28 | | oveq 7437 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = · → (𝑥𝑡𝑦) = (𝑥 · 𝑦)) |
| 29 | 28 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (𝑥𝑡𝑦) = (𝑥 · 𝑦)) |
| 30 | | oveq 7437 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = · → (𝑥𝑡𝑧) = (𝑥 · 𝑧)) |
| 31 | 30 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (𝑥𝑡𝑧) = (𝑥 · 𝑧)) |
| 32 | 27, 29, 31 | oveq123d 7452 |
. . . . . . . . . . . 12
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧))) |
| 33 | 25, 32 | eqeq12d 2753 |
. . . . . . . . . . 11
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ↔ (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)))) |
| 34 | | oveq 7437 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = + → (𝑥𝑝𝑦) = (𝑥 + 𝑦)) |
| 35 | 34 | ad2antlr 727 |
. . . . . . . . . . . . 13
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (𝑥𝑝𝑦) = (𝑥 + 𝑦)) |
| 36 | | eqidd 2738 |
. . . . . . . . . . . . 13
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑧 = 𝑧) |
| 37 | 21, 35, 36 | oveq123d 7452 |
. . . . . . . . . . . 12
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥 + 𝑦) · 𝑧)) |
| 38 | | oveq 7437 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = · → (𝑦𝑡𝑧) = (𝑦 · 𝑧)) |
| 39 | 38 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (𝑦𝑡𝑧) = (𝑦 · 𝑧)) |
| 40 | 27, 31, 39 | oveq123d 7452 |
. . . . . . . . . . . 12
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) |
| 41 | 37, 40 | eqeq12d 2753 |
. . . . . . . . . . 11
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)) ↔ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))) |
| 42 | 33, 41 | anbi12d 632 |
. . . . . . . . . 10
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))) |
| 43 | 20, 42 | raleqbidv 3346 |
. . . . . . . . 9
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) →
(∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))) |
| 44 | 20, 43 | raleqbidv 3346 |
. . . . . . . 8
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) →
(∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))) |
| 45 | 20, 44 | raleqbidv 3346 |
. . . . . . 7
⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) →
(∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))) |
| 46 | 14, 19, 45 | sbcied2 3833 |
. . . . . 6
⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) →
([(.r‘𝑟) / 𝑡]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))) |
| 47 | 9, 13, 46 | sbcied2 3833 |
. . . . 5
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → ([(+g‘𝑟) / 𝑝][(.r‘𝑟) / 𝑡]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))) |
| 48 | 5, 8, 47 | sbcied2 3833 |
. . . 4
⊢ (𝑟 = 𝑅 → ([(Base‘𝑟) / 𝑏][(+g‘𝑟) / 𝑝][(.r‘𝑟) / 𝑡]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))) |
| 49 | 4, 48 | anbi12d 632 |
. . 3
⊢ (𝑟 = 𝑅 → (((mulGrp‘𝑟) ∈ Smgrp ∧
[(Base‘𝑟) /
𝑏][(+g‘𝑟) / 𝑝][(.r‘𝑟) / 𝑡]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))) ↔ (𝐺 ∈ Smgrp ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))) |
| 50 | | df-rng 20150 |
. . 3
⊢ Rng =
{𝑟 ∈ Abel ∣
((mulGrp‘𝑟) ∈
Smgrp ∧ [(Base‘𝑟) / 𝑏][(+g‘𝑟) / 𝑝][(.r‘𝑟) / 𝑡]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))))} |
| 51 | 49, 50 | elrab2 3695 |
. 2
⊢ (𝑅 ∈ Rng ↔ (𝑅 ∈ Abel ∧ (𝐺 ∈ Smgrp ∧
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))) |
| 52 | | 3anass 1095 |
. 2
⊢ ((𝑅 ∈ Abel ∧ 𝐺 ∈ Smgrp ∧
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))) ↔ (𝑅 ∈ Abel ∧ (𝐺 ∈ Smgrp ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))) |
| 53 | 51, 52 | bitr4i 278 |
1
⊢ (𝑅 ∈ Rng ↔ (𝑅 ∈ Abel ∧ 𝐺 ∈ Smgrp ∧
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))) |