| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . 4
⊢
{〈(Base‘ndx), {𝑍}〉, 〈(+g‘ndx),
{〈〈𝑍, 𝑍〉, 𝑍〉}〉} = {〈(Base‘ndx),
{𝑍}〉,
〈(+g‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉} |
| 2 | 1 | grp1 19065 |
. . 3
⊢ (𝑍 ∈ 𝑉 → {〈(Base‘ndx), {𝑍}〉,
〈(+g‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉} ∈ Grp) |
| 3 | | snex 5436 |
. . . . . 6
⊢ {𝑍} ∈ V |
| 4 | | ring1.m |
. . . . . . 7
⊢ 𝑀 = {〈(Base‘ndx),
{𝑍}〉,
〈(+g‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉,
〈(.r‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉} |
| 5 | 4 | rngbase 17343 |
. . . . . 6
⊢ ({𝑍} ∈ V → {𝑍} = (Base‘𝑀)) |
| 6 | 3, 5 | ax-mp 5 |
. . . . 5
⊢ {𝑍} = (Base‘𝑀) |
| 7 | 6 | eqcomi 2746 |
. . . 4
⊢
(Base‘𝑀) =
{𝑍} |
| 8 | | snex 5436 |
. . . . 5
⊢
{〈〈𝑍,
𝑍〉, 𝑍〉} ∈ V |
| 9 | 4 | rngplusg 17344 |
. . . . . 6
⊢
({〈〈𝑍,
𝑍〉, 𝑍〉} ∈ V → {〈〈𝑍, 𝑍〉, 𝑍〉} = (+g‘𝑀)) |
| 10 | 9 | eqcomd 2743 |
. . . . 5
⊢
({〈〈𝑍,
𝑍〉, 𝑍〉} ∈ V →
(+g‘𝑀) =
{〈〈𝑍, 𝑍〉, 𝑍〉}) |
| 11 | 8, 10 | ax-mp 5 |
. . . 4
⊢
(+g‘𝑀) = {〈〈𝑍, 𝑍〉, 𝑍〉} |
| 12 | 7, 11, 1 | grppropstr 18971 |
. . 3
⊢ (𝑀 ∈ Grp ↔
{〈(Base‘ndx), {𝑍}〉, 〈(+g‘ndx),
{〈〈𝑍, 𝑍〉, 𝑍〉}〉} ∈ Grp) |
| 13 | 2, 12 | sylibr 234 |
. 2
⊢ (𝑍 ∈ 𝑉 → 𝑀 ∈ Grp) |
| 14 | 1 | mnd1 18792 |
. . 3
⊢ (𝑍 ∈ 𝑉 → {〈(Base‘ndx), {𝑍}〉,
〈(+g‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉} ∈ Mnd) |
| 15 | | eqid 2737 |
. . . . . 6
⊢
(mulGrp‘𝑀) =
(mulGrp‘𝑀) |
| 16 | 15, 6 | mgpbas 20142 |
. . . . 5
⊢ {𝑍} =
(Base‘(mulGrp‘𝑀)) |
| 17 | 1 | grpbase 17330 |
. . . . . 6
⊢ ({𝑍} ∈ V → {𝑍} =
(Base‘{〈(Base‘ndx), {𝑍}〉, 〈(+g‘ndx),
{〈〈𝑍, 𝑍〉, 𝑍〉}〉})) |
| 18 | 3, 17 | ax-mp 5 |
. . . . 5
⊢ {𝑍} =
(Base‘{〈(Base‘ndx), {𝑍}〉, 〈(+g‘ndx),
{〈〈𝑍, 𝑍〉, 𝑍〉}〉}) |
| 19 | 16, 18 | eqtr3i 2767 |
. . . 4
⊢
(Base‘(mulGrp‘𝑀)) = (Base‘{〈(Base‘ndx),
{𝑍}〉,
〈(+g‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉}) |
| 20 | 4 | rngmulr 17345 |
. . . . . 6
⊢
({〈〈𝑍,
𝑍〉, 𝑍〉} ∈ V → {〈〈𝑍, 𝑍〉, 𝑍〉} = (.r‘𝑀)) |
| 21 | 8, 20 | ax-mp 5 |
. . . . 5
⊢
{〈〈𝑍,
𝑍〉, 𝑍〉} = (.r‘𝑀) |
| 22 | 1 | grpplusg 17332 |
. . . . . 6
⊢
({〈〈𝑍,
𝑍〉, 𝑍〉} ∈ V → {〈〈𝑍, 𝑍〉, 𝑍〉} =
(+g‘{〈(Base‘ndx), {𝑍}〉, 〈(+g‘ndx),
{〈〈𝑍, 𝑍〉, 𝑍〉}〉})) |
| 23 | 8, 22 | ax-mp 5 |
. . . . 5
⊢
{〈〈𝑍,
𝑍〉, 𝑍〉} =
(+g‘{〈(Base‘ndx), {𝑍}〉, 〈(+g‘ndx),
{〈〈𝑍, 𝑍〉, 𝑍〉}〉}) |
| 24 | | eqid 2737 |
. . . . . 6
⊢
(.r‘𝑀) = (.r‘𝑀) |
| 25 | 15, 24 | mgpplusg 20141 |
. . . . 5
⊢
(.r‘𝑀) = (+g‘(mulGrp‘𝑀)) |
| 26 | 21, 23, 25 | 3eqtr3ri 2774 |
. . . 4
⊢
(+g‘(mulGrp‘𝑀)) =
(+g‘{〈(Base‘ndx), {𝑍}〉, 〈(+g‘ndx),
{〈〈𝑍, 𝑍〉, 𝑍〉}〉}) |
| 27 | 19, 26 | mndprop 18773 |
. . 3
⊢
((mulGrp‘𝑀)
∈ Mnd ↔ {〈(Base‘ndx), {𝑍}〉, 〈(+g‘ndx),
{〈〈𝑍, 𝑍〉, 𝑍〉}〉} ∈ Mnd) |
| 28 | 14, 27 | sylibr 234 |
. 2
⊢ (𝑍 ∈ 𝑉 → (mulGrp‘𝑀) ∈ Mnd) |
| 29 | | df-ov 7434 |
. . . . . 6
⊢ (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍) = ({〈〈𝑍, 𝑍〉, 𝑍〉}‘〈𝑍, 𝑍〉) |
| 30 | | opex 5469 |
. . . . . . 7
⊢
〈𝑍, 𝑍〉 ∈ V |
| 31 | | fvsng 7200 |
. . . . . . 7
⊢
((〈𝑍, 𝑍〉 ∈ V ∧ 𝑍 ∈ 𝑉) → ({〈〈𝑍, 𝑍〉, 𝑍〉}‘〈𝑍, 𝑍〉) = 𝑍) |
| 32 | 30, 31 | mpan 690 |
. . . . . 6
⊢ (𝑍 ∈ 𝑉 → ({〈〈𝑍, 𝑍〉, 𝑍〉}‘〈𝑍, 𝑍〉) = 𝑍) |
| 33 | 29, 32 | eqtrid 2789 |
. . . . 5
⊢ (𝑍 ∈ 𝑉 → (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍) = 𝑍) |
| 34 | 33 | oveq2d 7447 |
. . . 4
⊢ (𝑍 ∈ 𝑉 → (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) = (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) |
| 35 | 33, 33 | oveq12d 7449 |
. . . 4
⊢ (𝑍 ∈ 𝑉 → ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) = (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) |
| 36 | 34, 35 | eqtr4d 2780 |
. . 3
⊢ (𝑍 ∈ 𝑉 → (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍))) |
| 37 | 33 | oveq1d 7446 |
. . . 4
⊢ (𝑍 ∈ 𝑉 → ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑍) = (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) |
| 38 | 37, 35 | eqtr4d 2780 |
. . 3
⊢ (𝑍 ∈ 𝑉 → ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑍) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍))) |
| 39 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑎 = 𝑍 → (𝑎{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))) |
| 40 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑎 = 𝑍 → (𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏) = (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏)) |
| 41 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑎 = 𝑍 → (𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) |
| 42 | 40, 41 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝑎 = 𝑍 → ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))) |
| 43 | 39, 42 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑎 = 𝑍 → ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ↔ (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)))) |
| 44 | 40 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑎 = 𝑍 → ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) |
| 45 | 41 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑎 = 𝑍 → ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))) |
| 46 | 44, 45 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑎 = 𝑍 → (((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ↔ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)))) |
| 47 | 43, 46 | anbi12d 632 |
. . . . . 6
⊢ (𝑎 = 𝑍 → (((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))) ↔ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))))) |
| 48 | 47 | 2ralbidv 3221 |
. . . . 5
⊢ (𝑎 = 𝑍 → (∀𝑏 ∈ {𝑍}∀𝑐 ∈ {𝑍} ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))) ↔ ∀𝑏 ∈ {𝑍}∀𝑐 ∈ {𝑍} ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))))) |
| 49 | 48 | ralsng 4675 |
. . . 4
⊢ (𝑍 ∈ 𝑉 → (∀𝑎 ∈ {𝑍}∀𝑏 ∈ {𝑍}∀𝑐 ∈ {𝑍} ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))) ↔ ∀𝑏 ∈ {𝑍}∀𝑐 ∈ {𝑍} ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))))) |
| 50 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑏 = 𝑍 → (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) |
| 51 | 50 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑏 = 𝑍 → (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))) |
| 52 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑏 = 𝑍 → (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏) = (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) |
| 53 | 52 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑏 = 𝑍 → ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))) |
| 54 | 51, 53 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑏 = 𝑍 → ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ↔ (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)))) |
| 55 | 52 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑏 = 𝑍 → ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) |
| 56 | 50 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑏 = 𝑍 → ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))) |
| 57 | 55, 56 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑏 = 𝑍 → (((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ↔ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)))) |
| 58 | 54, 57 | anbi12d 632 |
. . . . . 6
⊢ (𝑏 = 𝑍 → (((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))) ↔ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))))) |
| 59 | 58 | ralbidv 3178 |
. . . . 5
⊢ (𝑏 = 𝑍 → (∀𝑐 ∈ {𝑍} ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))) ↔ ∀𝑐 ∈ {𝑍} ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))))) |
| 60 | 59 | ralsng 4675 |
. . . 4
⊢ (𝑍 ∈ 𝑉 → (∀𝑏 ∈ {𝑍}∀𝑐 ∈ {𝑍} ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))) ↔ ∀𝑐 ∈ {𝑍} ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))))) |
| 61 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑐 = 𝑍 → (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) |
| 62 | 61 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑐 = 𝑍 → (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍))) |
| 63 | 61 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑐 = 𝑍 → ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍))) |
| 64 | 62, 63 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑐 = 𝑍 → ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ↔ (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)))) |
| 65 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑐 = 𝑍 → ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) |
| 66 | 61, 61 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑐 = 𝑍 → ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍))) |
| 67 | 65, 66 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑐 = 𝑍 → (((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ↔ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑍) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)))) |
| 68 | 64, 67 | anbi12d 632 |
. . . . 5
⊢ (𝑐 = 𝑍 → (((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))) ↔ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) ∧ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑍) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍))))) |
| 69 | 68 | ralsng 4675 |
. . . 4
⊢ (𝑍 ∈ 𝑉 → (∀𝑐 ∈ {𝑍} ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))) ↔ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) ∧ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑍) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍))))) |
| 70 | 49, 60, 69 | 3bitrd 305 |
. . 3
⊢ (𝑍 ∈ 𝑉 → (∀𝑎 ∈ {𝑍}∀𝑏 ∈ {𝑍}∀𝑐 ∈ {𝑍} ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))) ↔ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) ∧ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑍) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍))))) |
| 71 | 36, 38, 70 | mpbir2and 713 |
. 2
⊢ (𝑍 ∈ 𝑉 → ∀𝑎 ∈ {𝑍}∀𝑏 ∈ {𝑍}∀𝑐 ∈ {𝑍} ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)))) |
| 72 | 8, 9 | ax-mp 5 |
. . 3
⊢
{〈〈𝑍,
𝑍〉, 𝑍〉} = (+g‘𝑀) |
| 73 | 6, 15, 72, 21 | isring 20234 |
. 2
⊢ (𝑀 ∈ Ring ↔ (𝑀 ∈ Grp ∧
(mulGrp‘𝑀) ∈ Mnd
∧ ∀𝑎 ∈
{𝑍}∀𝑏 ∈ {𝑍}∀𝑐 ∈ {𝑍} ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))))) |
| 74 | 13, 28, 71, 73 | syl3anbrc 1344 |
1
⊢ (𝑍 ∈ 𝑉 → 𝑀 ∈ Ring) |