| Step | Hyp | Ref
| Expression |
| 1 | | opprbas.1 |
. . . 4
⊢ 𝑂 =
(oppr‘𝑅) |
| 2 | | eqid 2737 |
. . . 4
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 3 | 1, 2 | opprbas 20341 |
. . 3
⊢
(Base‘𝑅) =
(Base‘𝑂) |
| 4 | 3 | a1i 11 |
. 2
⊢ (𝑅 ∈ Rng →
(Base‘𝑅) =
(Base‘𝑂)) |
| 5 | | eqid 2737 |
. . . 4
⊢
(+g‘𝑅) = (+g‘𝑅) |
| 6 | 1, 5 | oppradd 20343 |
. . 3
⊢
(+g‘𝑅) = (+g‘𝑂) |
| 7 | 6 | a1i 11 |
. 2
⊢ (𝑅 ∈ Rng →
(+g‘𝑅) =
(+g‘𝑂)) |
| 8 | | eqidd 2738 |
. 2
⊢ (𝑅 ∈ Rng →
(.r‘𝑂) =
(.r‘𝑂)) |
| 9 | | rngabl 20152 |
. . 3
⊢ (𝑅 ∈ Rng → 𝑅 ∈ Abel) |
| 10 | 3, 6 | ablprop 19811 |
. . 3
⊢ (𝑅 ∈ Abel ↔ 𝑂 ∈ Abel) |
| 11 | 9, 10 | sylib 218 |
. 2
⊢ (𝑅 ∈ Rng → 𝑂 ∈ Abel) |
| 12 | | eqid 2737 |
. . . 4
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 13 | | eqid 2737 |
. . . 4
⊢
(.r‘𝑂) = (.r‘𝑂) |
| 14 | 2, 12, 1, 13 | opprmul 20337 |
. . 3
⊢ (𝑥(.r‘𝑂)𝑦) = (𝑦(.r‘𝑅)𝑥) |
| 15 | 2, 12 | rngcl 20161 |
. . . 4
⊢ ((𝑅 ∈ Rng ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑦(.r‘𝑅)𝑥) ∈ (Base‘𝑅)) |
| 16 | 15 | 3com23 1127 |
. . 3
⊢ ((𝑅 ∈ Rng ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑦(.r‘𝑅)𝑥) ∈ (Base‘𝑅)) |
| 17 | 14, 16 | eqeltrid 2845 |
. 2
⊢ ((𝑅 ∈ Rng ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑂)𝑦) ∈ (Base‘𝑅)) |
| 18 | | simpl 482 |
. . . . 5
⊢ ((𝑅 ∈ Rng ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅))) → 𝑅 ∈ Rng) |
| 19 | | simpr3 1197 |
. . . . 5
⊢ ((𝑅 ∈ Rng ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅))) → 𝑧 ∈ (Base‘𝑅)) |
| 20 | | simpr2 1196 |
. . . . 5
⊢ ((𝑅 ∈ Rng ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅))) → 𝑦 ∈ (Base‘𝑅)) |
| 21 | | simpr1 1195 |
. . . . 5
⊢ ((𝑅 ∈ Rng ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅))) → 𝑥 ∈ (Base‘𝑅)) |
| 22 | 2, 12 | rngass 20156 |
. . . . 5
⊢ ((𝑅 ∈ Rng ∧ (𝑧 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅))) → ((𝑧(.r‘𝑅)𝑦)(.r‘𝑅)𝑥) = (𝑧(.r‘𝑅)(𝑦(.r‘𝑅)𝑥))) |
| 23 | 18, 19, 20, 21, 22 | syl13anc 1374 |
. . . 4
⊢ ((𝑅 ∈ Rng ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅))) → ((𝑧(.r‘𝑅)𝑦)(.r‘𝑅)𝑥) = (𝑧(.r‘𝑅)(𝑦(.r‘𝑅)𝑥))) |
| 24 | 23 | eqcomd 2743 |
. . 3
⊢ ((𝑅 ∈ Rng ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅))) → (𝑧(.r‘𝑅)(𝑦(.r‘𝑅)𝑥)) = ((𝑧(.r‘𝑅)𝑦)(.r‘𝑅)𝑥)) |
| 25 | 14 | oveq1i 7441 |
. . . 4
⊢ ((𝑥(.r‘𝑂)𝑦)(.r‘𝑂)𝑧) = ((𝑦(.r‘𝑅)𝑥)(.r‘𝑂)𝑧) |
| 26 | 2, 12, 1, 13 | opprmul 20337 |
. . . 4
⊢ ((𝑦(.r‘𝑅)𝑥)(.r‘𝑂)𝑧) = (𝑧(.r‘𝑅)(𝑦(.r‘𝑅)𝑥)) |
| 27 | 25, 26 | eqtri 2765 |
. . 3
⊢ ((𝑥(.r‘𝑂)𝑦)(.r‘𝑂)𝑧) = (𝑧(.r‘𝑅)(𝑦(.r‘𝑅)𝑥)) |
| 28 | 2, 12, 1, 13 | opprmul 20337 |
. . . . 5
⊢ (𝑦(.r‘𝑂)𝑧) = (𝑧(.r‘𝑅)𝑦) |
| 29 | 28 | oveq2i 7442 |
. . . 4
⊢ (𝑥(.r‘𝑂)(𝑦(.r‘𝑂)𝑧)) = (𝑥(.r‘𝑂)(𝑧(.r‘𝑅)𝑦)) |
| 30 | 2, 12, 1, 13 | opprmul 20337 |
. . . 4
⊢ (𝑥(.r‘𝑂)(𝑧(.r‘𝑅)𝑦)) = ((𝑧(.r‘𝑅)𝑦)(.r‘𝑅)𝑥) |
| 31 | 29, 30 | eqtri 2765 |
. . 3
⊢ (𝑥(.r‘𝑂)(𝑦(.r‘𝑂)𝑧)) = ((𝑧(.r‘𝑅)𝑦)(.r‘𝑅)𝑥) |
| 32 | 24, 27, 31 | 3eqtr4g 2802 |
. 2
⊢ ((𝑅 ∈ Rng ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅))) → ((𝑥(.r‘𝑂)𝑦)(.r‘𝑂)𝑧) = (𝑥(.r‘𝑂)(𝑦(.r‘𝑂)𝑧))) |
| 33 | 2, 5, 12 | rngdir 20158 |
. . . 4
⊢ ((𝑅 ∈ Rng ∧ (𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅))) → ((𝑦(+g‘𝑅)𝑧)(.r‘𝑅)𝑥) = ((𝑦(.r‘𝑅)𝑥)(+g‘𝑅)(𝑧(.r‘𝑅)𝑥))) |
| 34 | 18, 20, 19, 21, 33 | syl13anc 1374 |
. . 3
⊢ ((𝑅 ∈ Rng ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅))) → ((𝑦(+g‘𝑅)𝑧)(.r‘𝑅)𝑥) = ((𝑦(.r‘𝑅)𝑥)(+g‘𝑅)(𝑧(.r‘𝑅)𝑥))) |
| 35 | 2, 12, 1, 13 | opprmul 20337 |
. . 3
⊢ (𝑥(.r‘𝑂)(𝑦(+g‘𝑅)𝑧)) = ((𝑦(+g‘𝑅)𝑧)(.r‘𝑅)𝑥) |
| 36 | 2, 12, 1, 13 | opprmul 20337 |
. . . 4
⊢ (𝑥(.r‘𝑂)𝑧) = (𝑧(.r‘𝑅)𝑥) |
| 37 | 14, 36 | oveq12i 7443 |
. . 3
⊢ ((𝑥(.r‘𝑂)𝑦)(+g‘𝑅)(𝑥(.r‘𝑂)𝑧)) = ((𝑦(.r‘𝑅)𝑥)(+g‘𝑅)(𝑧(.r‘𝑅)𝑥)) |
| 38 | 34, 35, 37 | 3eqtr4g 2802 |
. 2
⊢ ((𝑅 ∈ Rng ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅))) → (𝑥(.r‘𝑂)(𝑦(+g‘𝑅)𝑧)) = ((𝑥(.r‘𝑂)𝑦)(+g‘𝑅)(𝑥(.r‘𝑂)𝑧))) |
| 39 | 2, 5, 12 | rngdi 20157 |
. . . 4
⊢ ((𝑅 ∈ Rng ∧ (𝑧 ∈ (Base‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) → (𝑧(.r‘𝑅)(𝑥(+g‘𝑅)𝑦)) = ((𝑧(.r‘𝑅)𝑥)(+g‘𝑅)(𝑧(.r‘𝑅)𝑦))) |
| 40 | 18, 19, 21, 20, 39 | syl13anc 1374 |
. . 3
⊢ ((𝑅 ∈ Rng ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅))) → (𝑧(.r‘𝑅)(𝑥(+g‘𝑅)𝑦)) = ((𝑧(.r‘𝑅)𝑥)(+g‘𝑅)(𝑧(.r‘𝑅)𝑦))) |
| 41 | 2, 12, 1, 13 | opprmul 20337 |
. . 3
⊢ ((𝑥(+g‘𝑅)𝑦)(.r‘𝑂)𝑧) = (𝑧(.r‘𝑅)(𝑥(+g‘𝑅)𝑦)) |
| 42 | 36, 28 | oveq12i 7443 |
. . 3
⊢ ((𝑥(.r‘𝑂)𝑧)(+g‘𝑅)(𝑦(.r‘𝑂)𝑧)) = ((𝑧(.r‘𝑅)𝑥)(+g‘𝑅)(𝑧(.r‘𝑅)𝑦)) |
| 43 | 40, 41, 42 | 3eqtr4g 2802 |
. 2
⊢ ((𝑅 ∈ Rng ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅))) → ((𝑥(+g‘𝑅)𝑦)(.r‘𝑂)𝑧) = ((𝑥(.r‘𝑂)𝑧)(+g‘𝑅)(𝑦(.r‘𝑂)𝑧))) |
| 44 | 4, 7, 8, 11, 17, 32, 38, 43 | isrngd 20170 |
1
⊢ (𝑅 ∈ Rng → 𝑂 ∈ Rng) |