Step | Hyp | Ref
| Expression |
1 | | mnd1.m |
. . 3
β’ π = {β¨(Baseβndx),
{πΌ}β©,
β¨(+gβndx), {β¨β¨πΌ, πΌβ©, πΌβ©}β©} |
2 | 1 | sgrp1 18560 |
. 2
β’ (πΌ β π β π β Smgrp) |
3 | | df-ov 7361 |
. . . . 5
β’ (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = ({β¨β¨πΌ, πΌβ©, πΌβ©}ββ¨πΌ, πΌβ©) |
4 | | opex 5422 |
. . . . . 6
β’
β¨πΌ, πΌβ© β V |
5 | | fvsng 7127 |
. . . . . 6
β’
((β¨πΌ, πΌβ© β V β§ πΌ β π) β ({β¨β¨πΌ, πΌβ©, πΌβ©}ββ¨πΌ, πΌβ©) = πΌ) |
6 | 4, 5 | mpan 689 |
. . . . 5
β’ (πΌ β π β ({β¨β¨πΌ, πΌβ©, πΌβ©}ββ¨πΌ, πΌβ©) = πΌ) |
7 | 3, 6 | eqtrid 2785 |
. . . 4
β’ (πΌ β π β (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = πΌ) |
8 | | oveq2 7366 |
. . . . . . 7
β’ (π¦ = πΌ β (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ)) |
9 | | id 22 |
. . . . . . 7
β’ (π¦ = πΌ β π¦ = πΌ) |
10 | 8, 9 | eqeq12d 2749 |
. . . . . 6
β’ (π¦ = πΌ β ((πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = π¦ β (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = πΌ)) |
11 | | oveq1 7365 |
. . . . . . 7
β’ (π¦ = πΌ β (π¦{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ)) |
12 | 11, 9 | eqeq12d 2749 |
. . . . . 6
β’ (π¦ = πΌ β ((π¦{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = π¦ β (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = πΌ)) |
13 | 10, 12 | anbi12d 632 |
. . . . 5
β’ (π¦ = πΌ β (((πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = π¦ β§ (π¦{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = π¦) β ((πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = πΌ β§ (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = πΌ))) |
14 | 13 | ralsng 4635 |
. . . 4
β’ (πΌ β π β (βπ¦ β {πΌ} ((πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = π¦ β§ (π¦{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = π¦) β ((πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = πΌ β§ (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = πΌ))) |
15 | 7, 7, 14 | mpbir2and 712 |
. . 3
β’ (πΌ β π β βπ¦ β {πΌ} ((πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = π¦ β§ (π¦{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = π¦)) |
16 | | oveq1 7365 |
. . . . . 6
β’ (π₯ = πΌ β (π₯{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}π¦)) |
17 | 16 | eqeq1d 2735 |
. . . . 5
β’ (π₯ = πΌ β ((π₯{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = π¦ β (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = π¦)) |
18 | 17 | ovanraleqv 7382 |
. . . 4
β’ (π₯ = πΌ β (βπ¦ β {πΌ} ((π₯{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = π¦ β§ (π¦{β¨β¨πΌ, πΌβ©, πΌβ©}π₯) = π¦) β βπ¦ β {πΌ} ((πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = π¦ β§ (π¦{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = π¦))) |
19 | 18 | rexsng 4636 |
. . 3
β’ (πΌ β π β (βπ₯ β {πΌ}βπ¦ β {πΌ} ((π₯{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = π¦ β§ (π¦{β¨β¨πΌ, πΌβ©, πΌβ©}π₯) = π¦) β βπ¦ β {πΌ} ((πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = π¦ β§ (π¦{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = π¦))) |
20 | 15, 19 | mpbird 257 |
. 2
β’ (πΌ β π β βπ₯ β {πΌ}βπ¦ β {πΌ} ((π₯{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = π¦ β§ (π¦{β¨β¨πΌ, πΌβ©, πΌβ©}π₯) = π¦)) |
21 | | snex 5389 |
. . . 4
β’ {πΌ} β V |
22 | 1 | grpbase 17172 |
. . . 4
β’ ({πΌ} β V β {πΌ} = (Baseβπ)) |
23 | 21, 22 | ax-mp 5 |
. . 3
β’ {πΌ} = (Baseβπ) |
24 | | snex 5389 |
. . . 4
β’
{β¨β¨πΌ,
πΌβ©, πΌβ©} β V |
25 | 1 | grpplusg 17174 |
. . . 4
β’
({β¨β¨πΌ,
πΌβ©, πΌβ©} β V β {β¨β¨πΌ, πΌβ©, πΌβ©} = (+gβπ)) |
26 | 24, 25 | ax-mp 5 |
. . 3
β’
{β¨β¨πΌ,
πΌβ©, πΌβ©} = (+gβπ) |
27 | 23, 26 | ismnddef 18563 |
. 2
β’ (π β Mnd β (π β Smgrp β§ βπ₯ β {πΌ}βπ¦ β {πΌ} ((π₯{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = π¦ β§ (π¦{β¨β¨πΌ, πΌβ©, πΌβ©}π₯) = π¦))) |
28 | 2, 20, 27 | sylanbrc 584 |
1
β’ (πΌ β π β π β Mnd) |