Step | Hyp | Ref
| Expression |
1 | | eqid 2739 |
. . . 4
⊢
{〈(Base‘ndx), {𝑍}〉, 〈(+g‘ndx),
{〈〈𝑍, 𝑍〉, 𝑍〉}〉} = {〈(Base‘ndx),
{𝑍}〉,
〈(+g‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉} |
2 | 1 | grp1 18337 |
. . 3
⊢ (𝑍 ∈ 𝑉 → {〈(Base‘ndx), {𝑍}〉,
〈(+g‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉} ∈ Grp) |
3 | | snex 5308 |
. . . . . 6
⊢ {𝑍} ∈ V |
4 | | ring1.m |
. . . . . . 7
⊢ 𝑀 = {〈(Base‘ndx),
{𝑍}〉,
〈(+g‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉,
〈(.r‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉} |
5 | 4 | rngbase 16736 |
. . . . . 6
⊢ ({𝑍} ∈ V → {𝑍} = (Base‘𝑀)) |
6 | 3, 5 | ax-mp 5 |
. . . . 5
⊢ {𝑍} = (Base‘𝑀) |
7 | 6 | eqcomi 2748 |
. . . 4
⊢
(Base‘𝑀) =
{𝑍} |
8 | | snex 5308 |
. . . . 5
⊢
{〈〈𝑍,
𝑍〉, 𝑍〉} ∈ V |
9 | 4 | rngplusg 16737 |
. . . . . 6
⊢
({〈〈𝑍,
𝑍〉, 𝑍〉} ∈ V → {〈〈𝑍, 𝑍〉, 𝑍〉} = (+g‘𝑀)) |
10 | 9 | eqcomd 2745 |
. . . . 5
⊢
({〈〈𝑍,
𝑍〉, 𝑍〉} ∈ V →
(+g‘𝑀) =
{〈〈𝑍, 𝑍〉, 𝑍〉}) |
11 | 8, 10 | ax-mp 5 |
. . . 4
⊢
(+g‘𝑀) = {〈〈𝑍, 𝑍〉, 𝑍〉} |
12 | 7, 11, 1 | grppropstr 18251 |
. . 3
⊢ (𝑀 ∈ Grp ↔
{〈(Base‘ndx), {𝑍}〉, 〈(+g‘ndx),
{〈〈𝑍, 𝑍〉, 𝑍〉}〉} ∈ Grp) |
13 | 2, 12 | sylibr 237 |
. 2
⊢ (𝑍 ∈ 𝑉 → 𝑀 ∈ Grp) |
14 | 1 | mnd1 18081 |
. . 3
⊢ (𝑍 ∈ 𝑉 → {〈(Base‘ndx), {𝑍}〉,
〈(+g‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉} ∈ Mnd) |
15 | | eqid 2739 |
. . . . . 6
⊢
(mulGrp‘𝑀) =
(mulGrp‘𝑀) |
16 | 15, 6 | mgpbas 19377 |
. . . . 5
⊢ {𝑍} =
(Base‘(mulGrp‘𝑀)) |
17 | 1 | grpbase 16726 |
. . . . . 6
⊢ ({𝑍} ∈ V → {𝑍} =
(Base‘{〈(Base‘ndx), {𝑍}〉, 〈(+g‘ndx),
{〈〈𝑍, 𝑍〉, 𝑍〉}〉})) |
18 | 3, 17 | ax-mp 5 |
. . . . 5
⊢ {𝑍} =
(Base‘{〈(Base‘ndx), {𝑍}〉, 〈(+g‘ndx),
{〈〈𝑍, 𝑍〉, 𝑍〉}〉}) |
19 | 16, 18 | eqtr3i 2764 |
. . . 4
⊢
(Base‘(mulGrp‘𝑀)) = (Base‘{〈(Base‘ndx),
{𝑍}〉,
〈(+g‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉}) |
20 | 4 | rngmulr 16738 |
. . . . . 6
⊢
({〈〈𝑍,
𝑍〉, 𝑍〉} ∈ V → {〈〈𝑍, 𝑍〉, 𝑍〉} = (.r‘𝑀)) |
21 | 8, 20 | ax-mp 5 |
. . . . 5
⊢
{〈〈𝑍,
𝑍〉, 𝑍〉} = (.r‘𝑀) |
22 | 1 | grpplusg 16727 |
. . . . . 6
⊢
({〈〈𝑍,
𝑍〉, 𝑍〉} ∈ V → {〈〈𝑍, 𝑍〉, 𝑍〉} =
(+g‘{〈(Base‘ndx), {𝑍}〉, 〈(+g‘ndx),
{〈〈𝑍, 𝑍〉, 𝑍〉}〉})) |
23 | 8, 22 | ax-mp 5 |
. . . . 5
⊢
{〈〈𝑍,
𝑍〉, 𝑍〉} =
(+g‘{〈(Base‘ndx), {𝑍}〉, 〈(+g‘ndx),
{〈〈𝑍, 𝑍〉, 𝑍〉}〉}) |
24 | | eqid 2739 |
. . . . . 6
⊢
(.r‘𝑀) = (.r‘𝑀) |
25 | 15, 24 | mgpplusg 19375 |
. . . . 5
⊢
(.r‘𝑀) = (+g‘(mulGrp‘𝑀)) |
26 | 21, 23, 25 | 3eqtr3ri 2771 |
. . . 4
⊢
(+g‘(mulGrp‘𝑀)) =
(+g‘{〈(Base‘ndx), {𝑍}〉, 〈(+g‘ndx),
{〈〈𝑍, 𝑍〉, 𝑍〉}〉}) |
27 | 19, 26 | mndprop 18066 |
. . 3
⊢
((mulGrp‘𝑀)
∈ Mnd ↔ {〈(Base‘ndx), {𝑍}〉, 〈(+g‘ndx),
{〈〈𝑍, 𝑍〉, 𝑍〉}〉} ∈ Mnd) |
28 | 14, 27 | sylibr 237 |
. 2
⊢ (𝑍 ∈ 𝑉 → (mulGrp‘𝑀) ∈ Mnd) |
29 | | df-ov 7186 |
. . . . . 6
⊢ (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍) = ({〈〈𝑍, 𝑍〉, 𝑍〉}‘〈𝑍, 𝑍〉) |
30 | | opex 5332 |
. . . . . . 7
⊢
〈𝑍, 𝑍〉 ∈ V |
31 | | fvsng 6965 |
. . . . . . 7
⊢
((〈𝑍, 𝑍〉 ∈ V ∧ 𝑍 ∈ 𝑉) → ({〈〈𝑍, 𝑍〉, 𝑍〉}‘〈𝑍, 𝑍〉) = 𝑍) |
32 | 30, 31 | mpan 690 |
. . . . . 6
⊢ (𝑍 ∈ 𝑉 → ({〈〈𝑍, 𝑍〉, 𝑍〉}‘〈𝑍, 𝑍〉) = 𝑍) |
33 | 29, 32 | syl5eq 2786 |
. . . . 5
⊢ (𝑍 ∈ 𝑉 → (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍) = 𝑍) |
34 | 33 | oveq2d 7199 |
. . . 4
⊢ (𝑍 ∈ 𝑉 → (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) = (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) |
35 | 33, 33 | oveq12d 7201 |
. . . 4
⊢ (𝑍 ∈ 𝑉 → ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) = (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) |
36 | 34, 35 | eqtr4d 2777 |
. . 3
⊢ (𝑍 ∈ 𝑉 → (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍))) |
37 | 33 | oveq1d 7198 |
. . . 4
⊢ (𝑍 ∈ 𝑉 → ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑍) = (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) |
38 | 37, 35 | eqtr4d 2777 |
. . 3
⊢ (𝑍 ∈ 𝑉 → ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑍) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍))) |
39 | | oveq1 7190 |
. . . . . . . 8
⊢ (𝑎 = 𝑍 → (𝑎{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))) |
40 | | oveq1 7190 |
. . . . . . . . 9
⊢ (𝑎 = 𝑍 → (𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏) = (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏)) |
41 | | oveq1 7190 |
. . . . . . . . 9
⊢ (𝑎 = 𝑍 → (𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) |
42 | 40, 41 | oveq12d 7201 |
. . . . . . . 8
⊢ (𝑎 = 𝑍 → ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))) |
43 | 39, 42 | eqeq12d 2755 |
. . . . . . 7
⊢ (𝑎 = 𝑍 → ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ↔ (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)))) |
44 | 40 | oveq1d 7198 |
. . . . . . . 8
⊢ (𝑎 = 𝑍 → ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) |
45 | 41 | oveq1d 7198 |
. . . . . . . 8
⊢ (𝑎 = 𝑍 → ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))) |
46 | 44, 45 | eqeq12d 2755 |
. . . . . . 7
⊢ (𝑎 = 𝑍 → (((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ↔ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)))) |
47 | 43, 46 | anbi12d 634 |
. . . . . 6
⊢ (𝑎 = 𝑍 → (((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))) ↔ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))))) |
48 | 47 | 2ralbidv 3112 |
. . . . 5
⊢ (𝑎 = 𝑍 → (∀𝑏 ∈ {𝑍}∀𝑐 ∈ {𝑍} ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))) ↔ ∀𝑏 ∈ {𝑍}∀𝑐 ∈ {𝑍} ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))))) |
49 | 48 | ralsng 4574 |
. . . 4
⊢ (𝑍 ∈ 𝑉 → (∀𝑎 ∈ {𝑍}∀𝑏 ∈ {𝑍}∀𝑐 ∈ {𝑍} ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))) ↔ ∀𝑏 ∈ {𝑍}∀𝑐 ∈ {𝑍} ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))))) |
50 | | oveq1 7190 |
. . . . . . . . 9
⊢ (𝑏 = 𝑍 → (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) |
51 | 50 | oveq2d 7199 |
. . . . . . . 8
⊢ (𝑏 = 𝑍 → (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))) |
52 | | oveq2 7191 |
. . . . . . . . 9
⊢ (𝑏 = 𝑍 → (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏) = (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) |
53 | 52 | oveq1d 7198 |
. . . . . . . 8
⊢ (𝑏 = 𝑍 → ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))) |
54 | 51, 53 | eqeq12d 2755 |
. . . . . . 7
⊢ (𝑏 = 𝑍 → ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ↔ (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)))) |
55 | 52 | oveq1d 7198 |
. . . . . . . 8
⊢ (𝑏 = 𝑍 → ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) |
56 | 50 | oveq2d 7199 |
. . . . . . . 8
⊢ (𝑏 = 𝑍 → ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))) |
57 | 55, 56 | eqeq12d 2755 |
. . . . . . 7
⊢ (𝑏 = 𝑍 → (((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ↔ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)))) |
58 | 54, 57 | anbi12d 634 |
. . . . . 6
⊢ (𝑏 = 𝑍 → (((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))) ↔ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))))) |
59 | 58 | ralbidv 3110 |
. . . . 5
⊢ (𝑏 = 𝑍 → (∀𝑐 ∈ {𝑍} ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))) ↔ ∀𝑐 ∈ {𝑍} ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))))) |
60 | 59 | ralsng 4574 |
. . . 4
⊢ (𝑍 ∈ 𝑉 → (∀𝑏 ∈ {𝑍}∀𝑐 ∈ {𝑍} ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))) ↔ ∀𝑐 ∈ {𝑍} ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))))) |
61 | | oveq2 7191 |
. . . . . . . 8
⊢ (𝑐 = 𝑍 → (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) |
62 | 61 | oveq2d 7199 |
. . . . . . 7
⊢ (𝑐 = 𝑍 → (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍))) |
63 | 61 | oveq2d 7199 |
. . . . . . 7
⊢ (𝑐 = 𝑍 → ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍))) |
64 | 62, 63 | eqeq12d 2755 |
. . . . . 6
⊢ (𝑐 = 𝑍 → ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ↔ (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)))) |
65 | | oveq2 7191 |
. . . . . . 7
⊢ (𝑐 = 𝑍 → ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) |
66 | 61, 61 | oveq12d 7201 |
. . . . . . 7
⊢ (𝑐 = 𝑍 → ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍))) |
67 | 65, 66 | eqeq12d 2755 |
. . . . . 6
⊢ (𝑐 = 𝑍 → (((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ↔ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑍) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)))) |
68 | 64, 67 | anbi12d 634 |
. . . . 5
⊢ (𝑐 = 𝑍 → (((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))) ↔ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) ∧ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑍) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍))))) |
69 | 68 | ralsng 4574 |
. . . 4
⊢ (𝑍 ∈ 𝑉 → (∀𝑐 ∈ {𝑍} ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))) ↔ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) ∧ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑍) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍))))) |
70 | 49, 60, 69 | 3bitrd 308 |
. . 3
⊢ (𝑍 ∈ 𝑉 → (∀𝑎 ∈ {𝑍}∀𝑏 ∈ {𝑍}∀𝑐 ∈ {𝑍} ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))) ↔ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍)) ∧ ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉}𝑍) = ((𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑍{〈〈𝑍, 𝑍〉, 𝑍〉}𝑍))))) |
71 | 36, 38, 70 | mpbir2and 713 |
. 2
⊢ (𝑍 ∈ 𝑉 → ∀𝑎 ∈ {𝑍}∀𝑏 ∈ {𝑍}∀𝑐 ∈ {𝑍} ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)))) |
72 | 8, 9 | ax-mp 5 |
. . 3
⊢
{〈〈𝑍,
𝑍〉, 𝑍〉} = (+g‘𝑀) |
73 | 6, 15, 72, 21 | isring 19433 |
. 2
⊢ (𝑀 ∈ Ring ↔ (𝑀 ∈ Grp ∧
(mulGrp‘𝑀) ∈ Mnd
∧ ∀𝑎 ∈
{𝑍}∀𝑏 ∈ {𝑍}∀𝑐 ∈ {𝑍} ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) = ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐)) ∧ ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑏){〈〈𝑍, 𝑍〉, 𝑍〉}𝑐) = ((𝑎{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐){〈〈𝑍, 𝑍〉, 𝑍〉} (𝑏{〈〈𝑍, 𝑍〉, 𝑍〉}𝑐))))) |
74 | 13, 28, 71, 73 | syl3anbrc 1344 |
1
⊢ (𝑍 ∈ 𝑉 → 𝑀 ∈ Ring) |