Step | Hyp | Ref
| Expression |
1 | | eqid 2177 |
. 2
⊢
(Base‘𝑀) =
(Base‘𝑀) |
2 | | eqid 2177 |
. 2
⊢
(0g‘𝑀) = (0g‘𝑀) |
3 | | eqid 2177 |
. 2
⊢
(+g‘𝑀) = (+g‘𝑀) |
4 | | simp3 999 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴) → 1 ∈ 𝐴) |
5 | | ringidss.g |
. . . . 5
⊢ 𝑀 = ((mulGrp‘𝑅) ↾s 𝐴) |
6 | 5 | a1i 9 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴) → 𝑀 = ((mulGrp‘𝑅) ↾s 𝐴)) |
7 | | eqid 2177 |
. . . . . 6
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
8 | | ringidss.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
9 | 7, 8 | mgpbasg 13089 |
. . . . 5
⊢ (𝑅 ∈ Ring → 𝐵 =
(Base‘(mulGrp‘𝑅))) |
10 | 9 | 3ad2ant1 1018 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴) → 𝐵 = (Base‘(mulGrp‘𝑅))) |
11 | 7 | mgpex 13088 |
. . . . 5
⊢ (𝑅 ∈ Ring →
(mulGrp‘𝑅) ∈
V) |
12 | 11 | 3ad2ant1 1018 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴) → (mulGrp‘𝑅) ∈ V) |
13 | | simp2 998 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴) → 𝐴 ⊆ 𝐵) |
14 | 6, 10, 12, 13 | ressbas2d 12522 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴) → 𝐴 = (Base‘𝑀)) |
15 | 4, 14 | eleqtrd 2256 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴) → 1 ∈ (Base‘𝑀)) |
16 | 14, 13 | eqsstrrd 3192 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴) → (Base‘𝑀) ⊆ 𝐵) |
17 | 16 | sselda 3155 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴) ∧ 𝑦 ∈ (Base‘𝑀)) → 𝑦 ∈ 𝐵) |
18 | | eqid 2177 |
. . . . . . . . 9
⊢
(.r‘𝑅) = (.r‘𝑅) |
19 | 7, 18 | mgpplusgg 13087 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
(.r‘𝑅) =
(+g‘(mulGrp‘𝑅))) |
20 | 19 | 3ad2ant1 1018 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴) → (.r‘𝑅) =
(+g‘(mulGrp‘𝑅))) |
21 | | basfn 12514 |
. . . . . . . . . 10
⊢ Base Fn
V |
22 | | simp1 997 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴) → 𝑅 ∈ Ring) |
23 | 22 | elexd 2750 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴) → 𝑅 ∈ V) |
24 | | funfvex 5532 |
. . . . . . . . . . 11
⊢ ((Fun
Base ∧ 𝑅 ∈ dom
Base) → (Base‘𝑅)
∈ V) |
25 | 24 | funfni 5316 |
. . . . . . . . . 10
⊢ ((Base Fn
V ∧ 𝑅 ∈ V) →
(Base‘𝑅) ∈
V) |
26 | 21, 23, 25 | sylancr 414 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴) → (Base‘𝑅) ∈ V) |
27 | 8, 26 | eqeltrid 2264 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴) → 𝐵 ∈ V) |
28 | 27, 13 | ssexd 4143 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴) → 𝐴 ∈ V) |
29 | 6, 20, 28, 12 | ressplusgd 12581 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴) → (.r‘𝑅) = (+g‘𝑀)) |
30 | 29 | adantr 276 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (.r‘𝑅) = (+g‘𝑀)) |
31 | 30 | oveqd 5891 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ( 1 (.r‘𝑅)𝑦) = ( 1 (+g‘𝑀)𝑦)) |
32 | | ringidss.u |
. . . . . 6
⊢ 1 =
(1r‘𝑅) |
33 | 8, 18, 32 | ringlidm 13159 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) → ( 1 (.r‘𝑅)𝑦) = 𝑦) |
34 | 33 | 3ad2antl1 1159 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ( 1 (.r‘𝑅)𝑦) = 𝑦) |
35 | 31, 34 | eqtr3d 2212 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ( 1 (+g‘𝑀)𝑦) = 𝑦) |
36 | 17, 35 | syldan 282 |
. 2
⊢ (((𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴) ∧ 𝑦 ∈ (Base‘𝑀)) → ( 1 (+g‘𝑀)𝑦) = 𝑦) |
37 | 30 | oveqd 5891 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝑦(.r‘𝑅) 1 ) = (𝑦(+g‘𝑀) 1 )) |
38 | 8, 18, 32 | ringridm 13160 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) → (𝑦(.r‘𝑅) 1 ) = 𝑦) |
39 | 38 | 3ad2antl1 1159 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝑦(.r‘𝑅) 1 ) = 𝑦) |
40 | 37, 39 | eqtr3d 2212 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝑦(+g‘𝑀) 1 ) = 𝑦) |
41 | 17, 40 | syldan 282 |
. 2
⊢ (((𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴) ∧ 𝑦 ∈ (Base‘𝑀)) → (𝑦(+g‘𝑀) 1 ) = 𝑦) |
42 | 1, 2, 3, 15, 36, 41 | ismgmid2 12753 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴) → 1 =
(0g‘𝑀)) |