Step | Hyp | Ref
| Expression |
1 | | lidlabl.l |
. . 3
⊢ 𝐿 = (LIdeal‘𝑅) |
2 | | lidlabl.i |
. . 3
⊢ 𝐼 = (𝑅 ↾s 𝑈) |
3 | 1, 2 | lidlmmgm 45046 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → (mulGrp‘𝐼) ∈ Mgm) |
4 | | eqid 2738 |
. . . . . . 7
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
5 | 4 | ringmgp 19424 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(mulGrp‘𝑅) ∈
Mnd) |
6 | 5 | ad2antrr 726 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) ∧ (𝑎 ∈ (Base‘𝐼) ∧ 𝑏 ∈ (Base‘𝐼) ∧ 𝑐 ∈ (Base‘𝐼))) → (mulGrp‘𝑅) ∈ Mnd) |
7 | 1, 2 | lidlssbas 45043 |
. . . . . . . . 9
⊢ (𝑈 ∈ 𝐿 → (Base‘𝐼) ⊆ (Base‘𝑅)) |
8 | 7 | sseld 3876 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝐿 → (𝑎 ∈ (Base‘𝐼) → 𝑎 ∈ (Base‘𝑅))) |
9 | 7 | sseld 3876 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝐿 → (𝑏 ∈ (Base‘𝐼) → 𝑏 ∈ (Base‘𝑅))) |
10 | 7 | sseld 3876 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝐿 → (𝑐 ∈ (Base‘𝐼) → 𝑐 ∈ (Base‘𝑅))) |
11 | 8, 9, 10 | 3anim123d 1444 |
. . . . . . 7
⊢ (𝑈 ∈ 𝐿 → ((𝑎 ∈ (Base‘𝐼) ∧ 𝑏 ∈ (Base‘𝐼) ∧ 𝑐 ∈ (Base‘𝐼)) → (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑐 ∈ (Base‘𝑅)))) |
12 | 11 | adantl 485 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → ((𝑎 ∈ (Base‘𝐼) ∧ 𝑏 ∈ (Base‘𝐼) ∧ 𝑐 ∈ (Base‘𝐼)) → (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑐 ∈ (Base‘𝑅)))) |
13 | 12 | imp 410 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) ∧ (𝑎 ∈ (Base‘𝐼) ∧ 𝑏 ∈ (Base‘𝐼) ∧ 𝑐 ∈ (Base‘𝐼))) → (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑐 ∈ (Base‘𝑅))) |
14 | | eqid 2738 |
. . . . . . 7
⊢
(Base‘𝑅) =
(Base‘𝑅) |
15 | 4, 14 | mgpbas 19366 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘(mulGrp‘𝑅)) |
16 | | eqid 2738 |
. . . . . . 7
⊢
(.r‘𝑅) = (.r‘𝑅) |
17 | 4, 16 | mgpplusg 19364 |
. . . . . 6
⊢
(.r‘𝑅) = (+g‘(mulGrp‘𝑅)) |
18 | 15, 17 | mndass 18038 |
. . . . 5
⊢
(((mulGrp‘𝑅)
∈ Mnd ∧ (𝑎 ∈
(Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑐 ∈ (Base‘𝑅))) → ((𝑎(.r‘𝑅)𝑏)(.r‘𝑅)𝑐) = (𝑎(.r‘𝑅)(𝑏(.r‘𝑅)𝑐))) |
19 | 6, 13, 18 | syl2anc 587 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) ∧ (𝑎 ∈ (Base‘𝐼) ∧ 𝑏 ∈ (Base‘𝐼) ∧ 𝑐 ∈ (Base‘𝐼))) → ((𝑎(.r‘𝑅)𝑏)(.r‘𝑅)𝑐) = (𝑎(.r‘𝑅)(𝑏(.r‘𝑅)𝑐))) |
20 | 19 | ralrimivvva 3104 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → ∀𝑎 ∈ (Base‘𝐼)∀𝑏 ∈ (Base‘𝐼)∀𝑐 ∈ (Base‘𝐼)((𝑎(.r‘𝑅)𝑏)(.r‘𝑅)𝑐) = (𝑎(.r‘𝑅)(𝑏(.r‘𝑅)𝑐))) |
21 | 2, 16 | ressmulr 16730 |
. . . . . . . . 9
⊢ (𝑈 ∈ 𝐿 → (.r‘𝑅) = (.r‘𝐼)) |
22 | 21 | eqcomd 2744 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝐿 → (.r‘𝐼) = (.r‘𝑅)) |
23 | 22 | oveqd 7189 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝐿 → (𝑎(.r‘𝐼)𝑏) = (𝑎(.r‘𝑅)𝑏)) |
24 | | eqidd 2739 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝐿 → 𝑐 = 𝑐) |
25 | 22, 23, 24 | oveq123d 7193 |
. . . . . . 7
⊢ (𝑈 ∈ 𝐿 → ((𝑎(.r‘𝐼)𝑏)(.r‘𝐼)𝑐) = ((𝑎(.r‘𝑅)𝑏)(.r‘𝑅)𝑐)) |
26 | | eqidd 2739 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝐿 → 𝑎 = 𝑎) |
27 | 22 | oveqd 7189 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝐿 → (𝑏(.r‘𝐼)𝑐) = (𝑏(.r‘𝑅)𝑐)) |
28 | 22, 26, 27 | oveq123d 7193 |
. . . . . . 7
⊢ (𝑈 ∈ 𝐿 → (𝑎(.r‘𝐼)(𝑏(.r‘𝐼)𝑐)) = (𝑎(.r‘𝑅)(𝑏(.r‘𝑅)𝑐))) |
29 | 25, 28 | eqeq12d 2754 |
. . . . . 6
⊢ (𝑈 ∈ 𝐿 → (((𝑎(.r‘𝐼)𝑏)(.r‘𝐼)𝑐) = (𝑎(.r‘𝐼)(𝑏(.r‘𝐼)𝑐)) ↔ ((𝑎(.r‘𝑅)𝑏)(.r‘𝑅)𝑐) = (𝑎(.r‘𝑅)(𝑏(.r‘𝑅)𝑐)))) |
30 | 29 | adantl 485 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → (((𝑎(.r‘𝐼)𝑏)(.r‘𝐼)𝑐) = (𝑎(.r‘𝐼)(𝑏(.r‘𝐼)𝑐)) ↔ ((𝑎(.r‘𝑅)𝑏)(.r‘𝑅)𝑐) = (𝑎(.r‘𝑅)(𝑏(.r‘𝑅)𝑐)))) |
31 | 30 | ralbidv 3109 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → (∀𝑐 ∈ (Base‘𝐼)((𝑎(.r‘𝐼)𝑏)(.r‘𝐼)𝑐) = (𝑎(.r‘𝐼)(𝑏(.r‘𝐼)𝑐)) ↔ ∀𝑐 ∈ (Base‘𝐼)((𝑎(.r‘𝑅)𝑏)(.r‘𝑅)𝑐) = (𝑎(.r‘𝑅)(𝑏(.r‘𝑅)𝑐)))) |
32 | 31 | 2ralbidv 3111 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → (∀𝑎 ∈ (Base‘𝐼)∀𝑏 ∈ (Base‘𝐼)∀𝑐 ∈ (Base‘𝐼)((𝑎(.r‘𝐼)𝑏)(.r‘𝐼)𝑐) = (𝑎(.r‘𝐼)(𝑏(.r‘𝐼)𝑐)) ↔ ∀𝑎 ∈ (Base‘𝐼)∀𝑏 ∈ (Base‘𝐼)∀𝑐 ∈ (Base‘𝐼)((𝑎(.r‘𝑅)𝑏)(.r‘𝑅)𝑐) = (𝑎(.r‘𝑅)(𝑏(.r‘𝑅)𝑐)))) |
33 | 20, 32 | mpbird 260 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → ∀𝑎 ∈ (Base‘𝐼)∀𝑏 ∈ (Base‘𝐼)∀𝑐 ∈ (Base‘𝐼)((𝑎(.r‘𝐼)𝑏)(.r‘𝐼)𝑐) = (𝑎(.r‘𝐼)(𝑏(.r‘𝐼)𝑐))) |
34 | | eqid 2738 |
. . . 4
⊢
(mulGrp‘𝐼) =
(mulGrp‘𝐼) |
35 | | eqid 2738 |
. . . 4
⊢
(Base‘𝐼) =
(Base‘𝐼) |
36 | 34, 35 | mgpbas 19366 |
. . 3
⊢
(Base‘𝐼) =
(Base‘(mulGrp‘𝐼)) |
37 | | eqid 2738 |
. . . 4
⊢
(.r‘𝐼) = (.r‘𝐼) |
38 | 34, 37 | mgpplusg 19364 |
. . 3
⊢
(.r‘𝐼) = (+g‘(mulGrp‘𝐼)) |
39 | 36, 38 | issgrp 18020 |
. 2
⊢
((mulGrp‘𝐼)
∈ Smgrp ↔ ((mulGrp‘𝐼) ∈ Mgm ∧ ∀𝑎 ∈ (Base‘𝐼)∀𝑏 ∈ (Base‘𝐼)∀𝑐 ∈ (Base‘𝐼)((𝑎(.r‘𝐼)𝑏)(.r‘𝐼)𝑐) = (𝑎(.r‘𝐼)(𝑏(.r‘𝐼)𝑐)))) |
40 | 3, 33, 39 | sylanbrc 586 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → (mulGrp‘𝐼) ∈ Smgrp) |