Step | Hyp | Ref
| Expression |
1 | | simp1 999 |
. . . . . 6
⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) → 𝑅 ∈ Rng) |
2 | | rnglidlabl.l |
. . . . . . . . 9
⊢ 𝐿 = (LIdeal‘𝑅) |
3 | | rnglidlabl.i |
. . . . . . . . 9
⊢ 𝐼 = (𝑅 ↾s 𝑈) |
4 | 2, 3 | lidlbas 13974 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝐿 → (Base‘𝐼) = 𝑈) |
5 | | eleq1a 2265 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝐿 → ((Base‘𝐼) = 𝑈 → (Base‘𝐼) ∈ 𝐿)) |
6 | 4, 5 | mpd 13 |
. . . . . . 7
⊢ (𝑈 ∈ 𝐿 → (Base‘𝐼) ∈ 𝐿) |
7 | 6 | 3ad2ant2 1021 |
. . . . . 6
⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) → (Base‘𝐼) ∈ 𝐿) |
8 | 4 | eqcomd 2199 |
. . . . . . . . 9
⊢ (𝑈 ∈ 𝐿 → 𝑈 = (Base‘𝐼)) |
9 | 8 | eleq2d 2263 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝐿 → ( 0 ∈ 𝑈 ↔ 0 ∈ (Base‘𝐼))) |
10 | 9 | biimpa 296 |
. . . . . . 7
⊢ ((𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) → 0 ∈ (Base‘𝐼)) |
11 | 10 | 3adant1 1017 |
. . . . . 6
⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) → 0 ∈ (Base‘𝐼)) |
12 | 1, 7, 11 | 3jca 1179 |
. . . . 5
⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) → (𝑅 ∈ Rng ∧ (Base‘𝐼) ∈ 𝐿 ∧ 0 ∈ (Base‘𝐼))) |
13 | 2, 3 | lidlssbas 13973 |
. . . . . . . . 9
⊢ (𝑈 ∈ 𝐿 → (Base‘𝐼) ⊆ (Base‘𝑅)) |
14 | 13 | sseld 3178 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝐿 → (𝑎 ∈ (Base‘𝐼) → 𝑎 ∈ (Base‘𝑅))) |
15 | 14 | 3ad2ant2 1021 |
. . . . . . 7
⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) → (𝑎 ∈ (Base‘𝐼) → 𝑎 ∈ (Base‘𝑅))) |
16 | 15 | anim1d 336 |
. . . . . 6
⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) → ((𝑎 ∈ (Base‘𝐼) ∧ 𝑏 ∈ (Base‘𝐼)) → (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝐼)))) |
17 | 16 | imp 124 |
. . . . 5
⊢ (((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘𝐼) ∧ 𝑏 ∈ (Base‘𝐼))) → (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝐼))) |
18 | | rnglidlabl.z |
. . . . . 6
⊢ 0 =
(0g‘𝑅) |
19 | | eqid 2193 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) |
20 | | eqid 2193 |
. . . . . 6
⊢
(.r‘𝑅) = (.r‘𝑅) |
21 | 18, 19, 20, 2 | rnglidlmcl 13976 |
. . . . 5
⊢ (((𝑅 ∈ Rng ∧
(Base‘𝐼) ∈ 𝐿 ∧ 0 ∈ (Base‘𝐼)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝐼))) → (𝑎(.r‘𝑅)𝑏) ∈ (Base‘𝐼)) |
22 | 12, 17, 21 | syl2an2r 595 |
. . . 4
⊢ (((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘𝐼) ∧ 𝑏 ∈ (Base‘𝐼))) → (𝑎(.r‘𝑅)𝑏) ∈ (Base‘𝐼)) |
23 | | simp2 1000 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) → 𝑈 ∈ 𝐿) |
24 | 3, 20 | ressmulrg 12762 |
. . . . . . . . 9
⊢ ((𝑈 ∈ 𝐿 ∧ 𝑅 ∈ Rng) →
(.r‘𝑅) =
(.r‘𝐼)) |
25 | 23, 1, 24 | syl2anc 411 |
. . . . . . . 8
⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) → (.r‘𝑅) = (.r‘𝐼)) |
26 | 25 | eqcomd 2199 |
. . . . . . 7
⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) → (.r‘𝐼) = (.r‘𝑅)) |
27 | 26 | oveqd 5935 |
. . . . . 6
⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) → (𝑎(.r‘𝐼)𝑏) = (𝑎(.r‘𝑅)𝑏)) |
28 | 27 | eleq1d 2262 |
. . . . 5
⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) → ((𝑎(.r‘𝐼)𝑏) ∈ (Base‘𝐼) ↔ (𝑎(.r‘𝑅)𝑏) ∈ (Base‘𝐼))) |
29 | 28 | adantr 276 |
. . . 4
⊢ (((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘𝐼) ∧ 𝑏 ∈ (Base‘𝐼))) → ((𝑎(.r‘𝐼)𝑏) ∈ (Base‘𝐼) ↔ (𝑎(.r‘𝑅)𝑏) ∈ (Base‘𝐼))) |
30 | 22, 29 | mpbird 167 |
. . 3
⊢ (((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘𝐼) ∧ 𝑏 ∈ (Base‘𝐼))) → (𝑎(.r‘𝐼)𝑏) ∈ (Base‘𝐼)) |
31 | 30 | ralrimivva 2576 |
. 2
⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) → ∀𝑎 ∈ (Base‘𝐼)∀𝑏 ∈ (Base‘𝐼)(𝑎(.r‘𝐼)𝑏) ∈ (Base‘𝐼)) |
32 | | ressex 12683 |
. . . . . 6
⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿) → (𝑅 ↾s 𝑈) ∈ V) |
33 | 3, 32 | eqeltrid 2280 |
. . . . 5
⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿) → 𝐼 ∈ V) |
34 | 1, 23, 33 | syl2anc 411 |
. . . 4
⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) → 𝐼 ∈ V) |
35 | | eqid 2193 |
. . . . 5
⊢
(mulGrp‘𝐼) =
(mulGrp‘𝐼) |
36 | 35 | mgpex 13421 |
. . . 4
⊢ (𝐼 ∈ V →
(mulGrp‘𝐼) ∈
V) |
37 | | eqid 2193 |
. . . . 5
⊢
(Base‘(mulGrp‘𝐼)) = (Base‘(mulGrp‘𝐼)) |
38 | | eqid 2193 |
. . . . 5
⊢
(+g‘(mulGrp‘𝐼)) =
(+g‘(mulGrp‘𝐼)) |
39 | 37, 38 | ismgm 12940 |
. . . 4
⊢
((mulGrp‘𝐼)
∈ V → ((mulGrp‘𝐼) ∈ Mgm ↔ ∀𝑎 ∈
(Base‘(mulGrp‘𝐼))∀𝑏 ∈ (Base‘(mulGrp‘𝐼))(𝑎(+g‘(mulGrp‘𝐼))𝑏) ∈ (Base‘(mulGrp‘𝐼)))) |
40 | 34, 36, 39 | 3syl 17 |
. . 3
⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) → ((mulGrp‘𝐼) ∈ Mgm ↔ ∀𝑎 ∈
(Base‘(mulGrp‘𝐼))∀𝑏 ∈ (Base‘(mulGrp‘𝐼))(𝑎(+g‘(mulGrp‘𝐼))𝑏) ∈ (Base‘(mulGrp‘𝐼)))) |
41 | | eqid 2193 |
. . . . . 6
⊢
(Base‘𝐼) =
(Base‘𝐼) |
42 | 35, 41 | mgpbasg 13422 |
. . . . 5
⊢ (𝐼 ∈ V →
(Base‘𝐼) =
(Base‘(mulGrp‘𝐼))) |
43 | 34, 42 | syl 14 |
. . . 4
⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) → (Base‘𝐼) = (Base‘(mulGrp‘𝐼))) |
44 | | eqid 2193 |
. . . . . . . . 9
⊢
(.r‘𝐼) = (.r‘𝐼) |
45 | 35, 44 | mgpplusgg 13420 |
. . . . . . . 8
⊢ (𝐼 ∈ V →
(.r‘𝐼) =
(+g‘(mulGrp‘𝐼))) |
46 | 34, 45 | syl 14 |
. . . . . . 7
⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) → (.r‘𝐼) =
(+g‘(mulGrp‘𝐼))) |
47 | 46 | oveqd 5935 |
. . . . . 6
⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) → (𝑎(.r‘𝐼)𝑏) = (𝑎(+g‘(mulGrp‘𝐼))𝑏)) |
48 | 47, 43 | eleq12d 2264 |
. . . . 5
⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) → ((𝑎(.r‘𝐼)𝑏) ∈ (Base‘𝐼) ↔ (𝑎(+g‘(mulGrp‘𝐼))𝑏) ∈ (Base‘(mulGrp‘𝐼)))) |
49 | 43, 48 | raleqbidv 2706 |
. . . 4
⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) → (∀𝑏 ∈ (Base‘𝐼)(𝑎(.r‘𝐼)𝑏) ∈ (Base‘𝐼) ↔ ∀𝑏 ∈ (Base‘(mulGrp‘𝐼))(𝑎(+g‘(mulGrp‘𝐼))𝑏) ∈ (Base‘(mulGrp‘𝐼)))) |
50 | 43, 49 | raleqbidv 2706 |
. . 3
⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) → (∀𝑎 ∈ (Base‘𝐼)∀𝑏 ∈ (Base‘𝐼)(𝑎(.r‘𝐼)𝑏) ∈ (Base‘𝐼) ↔ ∀𝑎 ∈ (Base‘(mulGrp‘𝐼))∀𝑏 ∈ (Base‘(mulGrp‘𝐼))(𝑎(+g‘(mulGrp‘𝐼))𝑏) ∈ (Base‘(mulGrp‘𝐼)))) |
51 | 40, 50 | bitr4d 191 |
. 2
⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) → ((mulGrp‘𝐼) ∈ Mgm ↔ ∀𝑎 ∈ (Base‘𝐼)∀𝑏 ∈ (Base‘𝐼)(𝑎(.r‘𝐼)𝑏) ∈ (Base‘𝐼))) |
52 | 31, 51 | mpbird 167 |
1
⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) → (mulGrp‘𝐼) ∈ Mgm) |