Step | Hyp | Ref
| Expression |
1 | | lidlabl.l |
. . 3
⊢ 𝐿 = (LIdeal‘𝑅) |
2 | | lidlabl.i |
. . 3
⊢ 𝐼 = (𝑅 ↾s 𝑈) |
3 | 1, 2 | lidlabl 45155 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → 𝐼 ∈ Abel) |
4 | 1, 2 | lidlmsgrp 45157 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → (mulGrp‘𝐼) ∈ Smgrp) |
5 | | simpll 767 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) ∧ (𝑎 ∈ (Base‘𝐼) ∧ 𝑏 ∈ (Base‘𝐼) ∧ 𝑐 ∈ (Base‘𝐼))) → 𝑅 ∈ Ring) |
6 | 1, 2 | lidlssbas 45153 |
. . . . . . . . . 10
⊢ (𝑈 ∈ 𝐿 → (Base‘𝐼) ⊆ (Base‘𝑅)) |
7 | 6 | sseld 3900 |
. . . . . . . . 9
⊢ (𝑈 ∈ 𝐿 → (𝑎 ∈ (Base‘𝐼) → 𝑎 ∈ (Base‘𝑅))) |
8 | 6 | sseld 3900 |
. . . . . . . . 9
⊢ (𝑈 ∈ 𝐿 → (𝑏 ∈ (Base‘𝐼) → 𝑏 ∈ (Base‘𝑅))) |
9 | 6 | sseld 3900 |
. . . . . . . . 9
⊢ (𝑈 ∈ 𝐿 → (𝑐 ∈ (Base‘𝐼) → 𝑐 ∈ (Base‘𝑅))) |
10 | 7, 8, 9 | 3anim123d 1445 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝐿 → ((𝑎 ∈ (Base‘𝐼) ∧ 𝑏 ∈ (Base‘𝐼) ∧ 𝑐 ∈ (Base‘𝐼)) → (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑐 ∈ (Base‘𝑅)))) |
11 | 10 | adantl 485 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → ((𝑎 ∈ (Base‘𝐼) ∧ 𝑏 ∈ (Base‘𝐼) ∧ 𝑐 ∈ (Base‘𝐼)) → (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑐 ∈ (Base‘𝑅)))) |
12 | 11 | imp 410 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) ∧ (𝑎 ∈ (Base‘𝐼) ∧ 𝑏 ∈ (Base‘𝐼) ∧ 𝑐 ∈ (Base‘𝐼))) → (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑐 ∈ (Base‘𝑅))) |
13 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘𝑅) =
(Base‘𝑅) |
14 | | eqid 2737 |
. . . . . . 7
⊢
(+g‘𝑅) = (+g‘𝑅) |
15 | | eqid 2737 |
. . . . . . 7
⊢
(.r‘𝑅) = (.r‘𝑅) |
16 | 13, 14, 15 | ringdi 19584 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑐 ∈ (Base‘𝑅))) → (𝑎(.r‘𝑅)(𝑏(+g‘𝑅)𝑐)) = ((𝑎(.r‘𝑅)𝑏)(+g‘𝑅)(𝑎(.r‘𝑅)𝑐))) |
17 | 5, 12, 16 | syl2anc 587 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) ∧ (𝑎 ∈ (Base‘𝐼) ∧ 𝑏 ∈ (Base‘𝐼) ∧ 𝑐 ∈ (Base‘𝐼))) → (𝑎(.r‘𝑅)(𝑏(+g‘𝑅)𝑐)) = ((𝑎(.r‘𝑅)𝑏)(+g‘𝑅)(𝑎(.r‘𝑅)𝑐))) |
18 | 13, 14, 15 | ringdir 19585 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑐 ∈ (Base‘𝑅))) → ((𝑎(+g‘𝑅)𝑏)(.r‘𝑅)𝑐) = ((𝑎(.r‘𝑅)𝑐)(+g‘𝑅)(𝑏(.r‘𝑅)𝑐))) |
19 | 5, 12, 18 | syl2anc 587 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) ∧ (𝑎 ∈ (Base‘𝐼) ∧ 𝑏 ∈ (Base‘𝐼) ∧ 𝑐 ∈ (Base‘𝐼))) → ((𝑎(+g‘𝑅)𝑏)(.r‘𝑅)𝑐) = ((𝑎(.r‘𝑅)𝑐)(+g‘𝑅)(𝑏(.r‘𝑅)𝑐))) |
20 | 17, 19 | jca 515 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) ∧ (𝑎 ∈ (Base‘𝐼) ∧ 𝑏 ∈ (Base‘𝐼) ∧ 𝑐 ∈ (Base‘𝐼))) → ((𝑎(.r‘𝑅)(𝑏(+g‘𝑅)𝑐)) = ((𝑎(.r‘𝑅)𝑏)(+g‘𝑅)(𝑎(.r‘𝑅)𝑐)) ∧ ((𝑎(+g‘𝑅)𝑏)(.r‘𝑅)𝑐) = ((𝑎(.r‘𝑅)𝑐)(+g‘𝑅)(𝑏(.r‘𝑅)𝑐)))) |
21 | 20 | ralrimivvva 3113 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → ∀𝑎 ∈ (Base‘𝐼)∀𝑏 ∈ (Base‘𝐼)∀𝑐 ∈ (Base‘𝐼)((𝑎(.r‘𝑅)(𝑏(+g‘𝑅)𝑐)) = ((𝑎(.r‘𝑅)𝑏)(+g‘𝑅)(𝑎(.r‘𝑅)𝑐)) ∧ ((𝑎(+g‘𝑅)𝑏)(.r‘𝑅)𝑐) = ((𝑎(.r‘𝑅)𝑐)(+g‘𝑅)(𝑏(.r‘𝑅)𝑐)))) |
22 | 2, 15 | ressmulr 16848 |
. . . . . . . . . 10
⊢ (𝑈 ∈ 𝐿 → (.r‘𝑅) = (.r‘𝐼)) |
23 | 22 | eqcomd 2743 |
. . . . . . . . 9
⊢ (𝑈 ∈ 𝐿 → (.r‘𝐼) = (.r‘𝑅)) |
24 | | eqidd 2738 |
. . . . . . . . 9
⊢ (𝑈 ∈ 𝐿 → 𝑎 = 𝑎) |
25 | 2, 14 | ressplusg 16834 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ 𝐿 → (+g‘𝑅) = (+g‘𝐼)) |
26 | 25 | eqcomd 2743 |
. . . . . . . . . 10
⊢ (𝑈 ∈ 𝐿 → (+g‘𝐼) = (+g‘𝑅)) |
27 | 26 | oveqd 7230 |
. . . . . . . . 9
⊢ (𝑈 ∈ 𝐿 → (𝑏(+g‘𝐼)𝑐) = (𝑏(+g‘𝑅)𝑐)) |
28 | 23, 24, 27 | oveq123d 7234 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝐿 → (𝑎(.r‘𝐼)(𝑏(+g‘𝐼)𝑐)) = (𝑎(.r‘𝑅)(𝑏(+g‘𝑅)𝑐))) |
29 | 23 | oveqd 7230 |
. . . . . . . . 9
⊢ (𝑈 ∈ 𝐿 → (𝑎(.r‘𝐼)𝑏) = (𝑎(.r‘𝑅)𝑏)) |
30 | 23 | oveqd 7230 |
. . . . . . . . 9
⊢ (𝑈 ∈ 𝐿 → (𝑎(.r‘𝐼)𝑐) = (𝑎(.r‘𝑅)𝑐)) |
31 | 26, 29, 30 | oveq123d 7234 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝐿 → ((𝑎(.r‘𝐼)𝑏)(+g‘𝐼)(𝑎(.r‘𝐼)𝑐)) = ((𝑎(.r‘𝑅)𝑏)(+g‘𝑅)(𝑎(.r‘𝑅)𝑐))) |
32 | 28, 31 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑈 ∈ 𝐿 → ((𝑎(.r‘𝐼)(𝑏(+g‘𝐼)𝑐)) = ((𝑎(.r‘𝐼)𝑏)(+g‘𝐼)(𝑎(.r‘𝐼)𝑐)) ↔ (𝑎(.r‘𝑅)(𝑏(+g‘𝑅)𝑐)) = ((𝑎(.r‘𝑅)𝑏)(+g‘𝑅)(𝑎(.r‘𝑅)𝑐)))) |
33 | 26 | oveqd 7230 |
. . . . . . . . 9
⊢ (𝑈 ∈ 𝐿 → (𝑎(+g‘𝐼)𝑏) = (𝑎(+g‘𝑅)𝑏)) |
34 | | eqidd 2738 |
. . . . . . . . 9
⊢ (𝑈 ∈ 𝐿 → 𝑐 = 𝑐) |
35 | 23, 33, 34 | oveq123d 7234 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝐿 → ((𝑎(+g‘𝐼)𝑏)(.r‘𝐼)𝑐) = ((𝑎(+g‘𝑅)𝑏)(.r‘𝑅)𝑐)) |
36 | 23 | oveqd 7230 |
. . . . . . . . 9
⊢ (𝑈 ∈ 𝐿 → (𝑏(.r‘𝐼)𝑐) = (𝑏(.r‘𝑅)𝑐)) |
37 | 26, 30, 36 | oveq123d 7234 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝐿 → ((𝑎(.r‘𝐼)𝑐)(+g‘𝐼)(𝑏(.r‘𝐼)𝑐)) = ((𝑎(.r‘𝑅)𝑐)(+g‘𝑅)(𝑏(.r‘𝑅)𝑐))) |
38 | 35, 37 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑈 ∈ 𝐿 → (((𝑎(+g‘𝐼)𝑏)(.r‘𝐼)𝑐) = ((𝑎(.r‘𝐼)𝑐)(+g‘𝐼)(𝑏(.r‘𝐼)𝑐)) ↔ ((𝑎(+g‘𝑅)𝑏)(.r‘𝑅)𝑐) = ((𝑎(.r‘𝑅)𝑐)(+g‘𝑅)(𝑏(.r‘𝑅)𝑐)))) |
39 | 32, 38 | anbi12d 634 |
. . . . . 6
⊢ (𝑈 ∈ 𝐿 → (((𝑎(.r‘𝐼)(𝑏(+g‘𝐼)𝑐)) = ((𝑎(.r‘𝐼)𝑏)(+g‘𝐼)(𝑎(.r‘𝐼)𝑐)) ∧ ((𝑎(+g‘𝐼)𝑏)(.r‘𝐼)𝑐) = ((𝑎(.r‘𝐼)𝑐)(+g‘𝐼)(𝑏(.r‘𝐼)𝑐))) ↔ ((𝑎(.r‘𝑅)(𝑏(+g‘𝑅)𝑐)) = ((𝑎(.r‘𝑅)𝑏)(+g‘𝑅)(𝑎(.r‘𝑅)𝑐)) ∧ ((𝑎(+g‘𝑅)𝑏)(.r‘𝑅)𝑐) = ((𝑎(.r‘𝑅)𝑐)(+g‘𝑅)(𝑏(.r‘𝑅)𝑐))))) |
40 | 39 | adantl 485 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → (((𝑎(.r‘𝐼)(𝑏(+g‘𝐼)𝑐)) = ((𝑎(.r‘𝐼)𝑏)(+g‘𝐼)(𝑎(.r‘𝐼)𝑐)) ∧ ((𝑎(+g‘𝐼)𝑏)(.r‘𝐼)𝑐) = ((𝑎(.r‘𝐼)𝑐)(+g‘𝐼)(𝑏(.r‘𝐼)𝑐))) ↔ ((𝑎(.r‘𝑅)(𝑏(+g‘𝑅)𝑐)) = ((𝑎(.r‘𝑅)𝑏)(+g‘𝑅)(𝑎(.r‘𝑅)𝑐)) ∧ ((𝑎(+g‘𝑅)𝑏)(.r‘𝑅)𝑐) = ((𝑎(.r‘𝑅)𝑐)(+g‘𝑅)(𝑏(.r‘𝑅)𝑐))))) |
41 | 40 | ralbidv 3118 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → (∀𝑐 ∈ (Base‘𝐼)((𝑎(.r‘𝐼)(𝑏(+g‘𝐼)𝑐)) = ((𝑎(.r‘𝐼)𝑏)(+g‘𝐼)(𝑎(.r‘𝐼)𝑐)) ∧ ((𝑎(+g‘𝐼)𝑏)(.r‘𝐼)𝑐) = ((𝑎(.r‘𝐼)𝑐)(+g‘𝐼)(𝑏(.r‘𝐼)𝑐))) ↔ ∀𝑐 ∈ (Base‘𝐼)((𝑎(.r‘𝑅)(𝑏(+g‘𝑅)𝑐)) = ((𝑎(.r‘𝑅)𝑏)(+g‘𝑅)(𝑎(.r‘𝑅)𝑐)) ∧ ((𝑎(+g‘𝑅)𝑏)(.r‘𝑅)𝑐) = ((𝑎(.r‘𝑅)𝑐)(+g‘𝑅)(𝑏(.r‘𝑅)𝑐))))) |
42 | 41 | 2ralbidv 3120 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → (∀𝑎 ∈ (Base‘𝐼)∀𝑏 ∈ (Base‘𝐼)∀𝑐 ∈ (Base‘𝐼)((𝑎(.r‘𝐼)(𝑏(+g‘𝐼)𝑐)) = ((𝑎(.r‘𝐼)𝑏)(+g‘𝐼)(𝑎(.r‘𝐼)𝑐)) ∧ ((𝑎(+g‘𝐼)𝑏)(.r‘𝐼)𝑐) = ((𝑎(.r‘𝐼)𝑐)(+g‘𝐼)(𝑏(.r‘𝐼)𝑐))) ↔ ∀𝑎 ∈ (Base‘𝐼)∀𝑏 ∈ (Base‘𝐼)∀𝑐 ∈ (Base‘𝐼)((𝑎(.r‘𝑅)(𝑏(+g‘𝑅)𝑐)) = ((𝑎(.r‘𝑅)𝑏)(+g‘𝑅)(𝑎(.r‘𝑅)𝑐)) ∧ ((𝑎(+g‘𝑅)𝑏)(.r‘𝑅)𝑐) = ((𝑎(.r‘𝑅)𝑐)(+g‘𝑅)(𝑏(.r‘𝑅)𝑐))))) |
43 | 21, 42 | mpbird 260 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → ∀𝑎 ∈ (Base‘𝐼)∀𝑏 ∈ (Base‘𝐼)∀𝑐 ∈ (Base‘𝐼)((𝑎(.r‘𝐼)(𝑏(+g‘𝐼)𝑐)) = ((𝑎(.r‘𝐼)𝑏)(+g‘𝐼)(𝑎(.r‘𝐼)𝑐)) ∧ ((𝑎(+g‘𝐼)𝑏)(.r‘𝐼)𝑐) = ((𝑎(.r‘𝐼)𝑐)(+g‘𝐼)(𝑏(.r‘𝐼)𝑐)))) |
44 | | eqid 2737 |
. . 3
⊢
(Base‘𝐼) =
(Base‘𝐼) |
45 | | eqid 2737 |
. . 3
⊢
(mulGrp‘𝐼) =
(mulGrp‘𝐼) |
46 | | eqid 2737 |
. . 3
⊢
(+g‘𝐼) = (+g‘𝐼) |
47 | | eqid 2737 |
. . 3
⊢
(.r‘𝐼) = (.r‘𝐼) |
48 | 44, 45, 46, 47 | isrng 45107 |
. 2
⊢ (𝐼 ∈ Rng ↔ (𝐼 ∈ Abel ∧
(mulGrp‘𝐼) ∈
Smgrp ∧ ∀𝑎
∈ (Base‘𝐼)∀𝑏 ∈ (Base‘𝐼)∀𝑐 ∈ (Base‘𝐼)((𝑎(.r‘𝐼)(𝑏(+g‘𝐼)𝑐)) = ((𝑎(.r‘𝐼)𝑏)(+g‘𝐼)(𝑎(.r‘𝐼)𝑐)) ∧ ((𝑎(+g‘𝐼)𝑏)(.r‘𝐼)𝑐) = ((𝑎(.r‘𝐼)𝑐)(+g‘𝐼)(𝑏(.r‘𝐼)𝑐))))) |
49 | 3, 4, 43, 48 | syl3anbrc 1345 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → 𝐼 ∈ Rng) |