| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > mgpbas | Structured version Visualization version GIF version | ||
| Description: Base set of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014.) (Revised by Mario Carneiro, 5-Oct-2015.) |
| Ref | Expression |
|---|---|
| mgpbas.1 | ⊢ 𝑀 = (mulGrp‘𝑅) |
| mgpbas.2 | ⊢ 𝐵 = (Base‘𝑅) |
| Ref | Expression |
|---|---|
| mgpbas | ⊢ 𝐵 = (Base‘𝑀) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mgpbas.2 | . 2 ⊢ 𝐵 = (Base‘𝑅) | |
| 2 | mgpbas.1 | . . . 4 ⊢ 𝑀 = (mulGrp‘𝑅) | |
| 3 | eqid 2737 | . . . 4 ⊢ (.r‘𝑅) = (.r‘𝑅) | |
| 4 | 2, 3 | mgpval 20140 | . . 3 ⊢ 𝑀 = (𝑅 sSet 〈(+g‘ndx), (.r‘𝑅)〉) |
| 5 | baseid 17250 | . . 3 ⊢ Base = Slot (Base‘ndx) | |
| 6 | basendxnplusgndx 17327 | . . 3 ⊢ (Base‘ndx) ≠ (+g‘ndx) | |
| 7 | 4, 5, 6 | setsplusg 19368 | . 2 ⊢ (Base‘𝑅) = (Base‘𝑀) |
| 8 | 1, 7 | eqtri 2765 | 1 ⊢ 𝐵 = (Base‘𝑀) |
| Copyright terms: Public domain | W3C validator |