Step | Hyp | Ref
| Expression |
1 | | rnglidlabl.l |
. . 3
⊢ 𝐿 = (LIdeal‘𝑅) |
2 | | rnglidlabl.i |
. . 3
⊢ 𝐼 = (𝑅 ↾s 𝑈) |
3 | | rnglidlabl.z |
. . 3
⊢ 0 =
(0g‘𝑅) |
4 | 1, 2, 3 | rnglidlmmgm 21134 |
. 2
⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) → (mulGrp‘𝐼) ∈ Mgm) |
5 | | eqid 2728 |
. . . . . . 7
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
6 | 5 | rngmgp 20090 |
. . . . . 6
⊢ (𝑅 ∈ Rng →
(mulGrp‘𝑅) ∈
Smgrp) |
7 | 6 | 3ad2ant1 1131 |
. . . . 5
⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) → (mulGrp‘𝑅) ∈ Smgrp) |
8 | 1, 2 | lidlssbas 21103 |
. . . . . . . . 9
⊢ (𝑈 ∈ 𝐿 → (Base‘𝐼) ⊆ (Base‘𝑅)) |
9 | 8 | sseld 3978 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝐿 → (𝑎 ∈ (Base‘𝐼) → 𝑎 ∈ (Base‘𝑅))) |
10 | 8 | sseld 3978 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝐿 → (𝑏 ∈ (Base‘𝐼) → 𝑏 ∈ (Base‘𝑅))) |
11 | 8 | sseld 3978 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝐿 → (𝑐 ∈ (Base‘𝐼) → 𝑐 ∈ (Base‘𝑅))) |
12 | 9, 10, 11 | 3anim123d 1440 |
. . . . . . 7
⊢ (𝑈 ∈ 𝐿 → ((𝑎 ∈ (Base‘𝐼) ∧ 𝑏 ∈ (Base‘𝐼) ∧ 𝑐 ∈ (Base‘𝐼)) → (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑐 ∈ (Base‘𝑅)))) |
13 | 12 | 3ad2ant2 1132 |
. . . . . 6
⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) → ((𝑎 ∈ (Base‘𝐼) ∧ 𝑏 ∈ (Base‘𝐼) ∧ 𝑐 ∈ (Base‘𝐼)) → (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑐 ∈ (Base‘𝑅)))) |
14 | 13 | imp 406 |
. . . . 5
⊢ (((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘𝐼) ∧ 𝑏 ∈ (Base‘𝐼) ∧ 𝑐 ∈ (Base‘𝐼))) → (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑐 ∈ (Base‘𝑅))) |
15 | | eqid 2728 |
. . . . . . 7
⊢
(Base‘𝑅) =
(Base‘𝑅) |
16 | 5, 15 | mgpbas 20074 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘(mulGrp‘𝑅)) |
17 | | eqid 2728 |
. . . . . . 7
⊢
(.r‘𝑅) = (.r‘𝑅) |
18 | 5, 17 | mgpplusg 20072 |
. . . . . 6
⊢
(.r‘𝑅) = (+g‘(mulGrp‘𝑅)) |
19 | 16, 18 | sgrpass 18679 |
. . . . 5
⊢
(((mulGrp‘𝑅)
∈ Smgrp ∧ (𝑎
∈ (Base‘𝑅) ∧
𝑏 ∈ (Base‘𝑅) ∧ 𝑐 ∈ (Base‘𝑅))) → ((𝑎(.r‘𝑅)𝑏)(.r‘𝑅)𝑐) = (𝑎(.r‘𝑅)(𝑏(.r‘𝑅)𝑐))) |
20 | 7, 14, 19 | syl2an2r 684 |
. . . 4
⊢ (((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘𝐼) ∧ 𝑏 ∈ (Base‘𝐼) ∧ 𝑐 ∈ (Base‘𝐼))) → ((𝑎(.r‘𝑅)𝑏)(.r‘𝑅)𝑐) = (𝑎(.r‘𝑅)(𝑏(.r‘𝑅)𝑐))) |
21 | 2, 17 | ressmulr 17282 |
. . . . . . . . 9
⊢ (𝑈 ∈ 𝐿 → (.r‘𝑅) = (.r‘𝐼)) |
22 | 21 | eqcomd 2734 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝐿 → (.r‘𝐼) = (.r‘𝑅)) |
23 | 22 | oveqd 7432 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝐿 → (𝑎(.r‘𝐼)𝑏) = (𝑎(.r‘𝑅)𝑏)) |
24 | | eqidd 2729 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝐿 → 𝑐 = 𝑐) |
25 | 22, 23, 24 | oveq123d 7436 |
. . . . . . 7
⊢ (𝑈 ∈ 𝐿 → ((𝑎(.r‘𝐼)𝑏)(.r‘𝐼)𝑐) = ((𝑎(.r‘𝑅)𝑏)(.r‘𝑅)𝑐)) |
26 | | eqidd 2729 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝐿 → 𝑎 = 𝑎) |
27 | 22 | oveqd 7432 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝐿 → (𝑏(.r‘𝐼)𝑐) = (𝑏(.r‘𝑅)𝑐)) |
28 | 22, 26, 27 | oveq123d 7436 |
. . . . . . 7
⊢ (𝑈 ∈ 𝐿 → (𝑎(.r‘𝐼)(𝑏(.r‘𝐼)𝑐)) = (𝑎(.r‘𝑅)(𝑏(.r‘𝑅)𝑐))) |
29 | 25, 28 | eqeq12d 2744 |
. . . . . 6
⊢ (𝑈 ∈ 𝐿 → (((𝑎(.r‘𝐼)𝑏)(.r‘𝐼)𝑐) = (𝑎(.r‘𝐼)(𝑏(.r‘𝐼)𝑐)) ↔ ((𝑎(.r‘𝑅)𝑏)(.r‘𝑅)𝑐) = (𝑎(.r‘𝑅)(𝑏(.r‘𝑅)𝑐)))) |
30 | 29 | 3ad2ant2 1132 |
. . . . 5
⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) → (((𝑎(.r‘𝐼)𝑏)(.r‘𝐼)𝑐) = (𝑎(.r‘𝐼)(𝑏(.r‘𝐼)𝑐)) ↔ ((𝑎(.r‘𝑅)𝑏)(.r‘𝑅)𝑐) = (𝑎(.r‘𝑅)(𝑏(.r‘𝑅)𝑐)))) |
31 | 30 | adantr 480 |
. . . 4
⊢ (((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘𝐼) ∧ 𝑏 ∈ (Base‘𝐼) ∧ 𝑐 ∈ (Base‘𝐼))) → (((𝑎(.r‘𝐼)𝑏)(.r‘𝐼)𝑐) = (𝑎(.r‘𝐼)(𝑏(.r‘𝐼)𝑐)) ↔ ((𝑎(.r‘𝑅)𝑏)(.r‘𝑅)𝑐) = (𝑎(.r‘𝑅)(𝑏(.r‘𝑅)𝑐)))) |
32 | 20, 31 | mpbird 257 |
. . 3
⊢ (((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘𝐼) ∧ 𝑏 ∈ (Base‘𝐼) ∧ 𝑐 ∈ (Base‘𝐼))) → ((𝑎(.r‘𝐼)𝑏)(.r‘𝐼)𝑐) = (𝑎(.r‘𝐼)(𝑏(.r‘𝐼)𝑐))) |
33 | 32 | ralrimivvva 3199 |
. 2
⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) → ∀𝑎 ∈ (Base‘𝐼)∀𝑏 ∈ (Base‘𝐼)∀𝑐 ∈ (Base‘𝐼)((𝑎(.r‘𝐼)𝑏)(.r‘𝐼)𝑐) = (𝑎(.r‘𝐼)(𝑏(.r‘𝐼)𝑐))) |
34 | | eqid 2728 |
. . . 4
⊢
(mulGrp‘𝐼) =
(mulGrp‘𝐼) |
35 | | eqid 2728 |
. . . 4
⊢
(Base‘𝐼) =
(Base‘𝐼) |
36 | 34, 35 | mgpbas 20074 |
. . 3
⊢
(Base‘𝐼) =
(Base‘(mulGrp‘𝐼)) |
37 | | eqid 2728 |
. . . 4
⊢
(.r‘𝐼) = (.r‘𝐼) |
38 | 34, 37 | mgpplusg 20072 |
. . 3
⊢
(.r‘𝐼) = (+g‘(mulGrp‘𝐼)) |
39 | 36, 38 | issgrp 18674 |
. 2
⊢
((mulGrp‘𝐼)
∈ Smgrp ↔ ((mulGrp‘𝐼) ∈ Mgm ∧ ∀𝑎 ∈ (Base‘𝐼)∀𝑏 ∈ (Base‘𝐼)∀𝑐 ∈ (Base‘𝐼)((𝑎(.r‘𝐼)𝑏)(.r‘𝐼)𝑐) = (𝑎(.r‘𝐼)(𝑏(.r‘𝐼)𝑐)))) |
40 | 4, 33, 39 | sylanbrc 582 |
1
⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) → (mulGrp‘𝐼) ∈ Smgrp) |