Step | Hyp | Ref
| Expression |
1 | | df-ov 5877 |
. . . . . 6
β’ (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = ({β¨β¨πΌ, πΌβ©, πΌβ©}ββ¨πΌ, πΌβ©) |
2 | | opexg 4228 |
. . . . . . . 8
β’ ((πΌ β π β§ πΌ β π) β β¨πΌ, πΌβ© β V) |
3 | 2 | anidms 397 |
. . . . . . 7
β’ (πΌ β π β β¨πΌ, πΌβ© β V) |
4 | | fvsng 5712 |
. . . . . . 7
β’
((β¨πΌ, πΌβ© β V β§ πΌ β π) β ({β¨β¨πΌ, πΌβ©, πΌβ©}ββ¨πΌ, πΌβ©) = πΌ) |
5 | 3, 4 | mpancom 422 |
. . . . . 6
β’ (πΌ β π β ({β¨β¨πΌ, πΌβ©, πΌβ©}ββ¨πΌ, πΌβ©) = πΌ) |
6 | 1, 5 | eqtrid 2222 |
. . . . 5
β’ (πΌ β π β (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = πΌ) |
7 | | snidg 3621 |
. . . . 5
β’ (πΌ β π β πΌ β {πΌ}) |
8 | 6, 7 | eqeltrd 2254 |
. . . 4
β’ (πΌ β π β (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) β {πΌ}) |
9 | | oveq1 5881 |
. . . . . . . 8
β’ (π₯ = πΌ β (π₯{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}π¦)) |
10 | 9 | eleq1d 2246 |
. . . . . . 7
β’ (π₯ = πΌ β ((π₯{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) β {πΌ} β (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) β {πΌ})) |
11 | 10 | ralbidv 2477 |
. . . . . 6
β’ (π₯ = πΌ β (βπ¦ β {πΌ} (π₯{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) β {πΌ} β βπ¦ β {πΌ} (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) β {πΌ})) |
12 | 11 | ralsng 3632 |
. . . . 5
β’ (πΌ β π β (βπ₯ β {πΌ}βπ¦ β {πΌ} (π₯{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) β {πΌ} β βπ¦ β {πΌ} (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) β {πΌ})) |
13 | | oveq2 5882 |
. . . . . . 7
β’ (π¦ = πΌ β (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ)) |
14 | 13 | eleq1d 2246 |
. . . . . 6
β’ (π¦ = πΌ β ((πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) β {πΌ} β (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) β {πΌ})) |
15 | 14 | ralsng 3632 |
. . . . 5
β’ (πΌ β π β (βπ¦ β {πΌ} (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) β {πΌ} β (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) β {πΌ})) |
16 | 12, 15 | bitrd 188 |
. . . 4
β’ (πΌ β π β (βπ₯ β {πΌ}βπ¦ β {πΌ} (π₯{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) β {πΌ} β (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) β {πΌ})) |
17 | 8, 16 | mpbird 167 |
. . 3
β’ (πΌ β π β βπ₯ β {πΌ}βπ¦ β {πΌ} (π₯{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) β {πΌ}) |
18 | | snexg 4184 |
. . . . 5
β’ (πΌ β π β {πΌ} β V) |
19 | | opexg 4228 |
. . . . . . 7
β’
((β¨πΌ, πΌβ© β V β§ πΌ β π) β β¨β¨πΌ, πΌβ©, πΌβ© β V) |
20 | 3, 19 | mpancom 422 |
. . . . . 6
β’ (πΌ β π β β¨β¨πΌ, πΌβ©, πΌβ© β V) |
21 | | snexg 4184 |
. . . . . 6
β’
(β¨β¨πΌ,
πΌβ©, πΌβ© β V β {β¨β¨πΌ, πΌβ©, πΌβ©} β V) |
22 | 20, 21 | syl 14 |
. . . . 5
β’ (πΌ β π β {β¨β¨πΌ, πΌβ©, πΌβ©} β V) |
23 | | mgm1.m |
. . . . . 6
β’ π = {β¨(Baseβndx),
{πΌ}β©,
β¨(+gβndx), {β¨β¨πΌ, πΌβ©, πΌβ©}β©} |
24 | 23 | grpbaseg 12584 |
. . . . 5
β’ (({πΌ} β V β§
{β¨β¨πΌ, πΌβ©, πΌβ©} β V) β {πΌ} = (Baseβπ)) |
25 | 18, 22, 24 | syl2anc 411 |
. . . 4
β’ (πΌ β π β {πΌ} = (Baseβπ)) |
26 | 23 | grpplusgg 12585 |
. . . . . . . 8
β’ (({πΌ} β V β§
{β¨β¨πΌ, πΌβ©, πΌβ©} β V) β {β¨β¨πΌ, πΌβ©, πΌβ©} = (+gβπ)) |
27 | 18, 22, 26 | syl2anc 411 |
. . . . . . 7
β’ (πΌ β π β {β¨β¨πΌ, πΌβ©, πΌβ©} = (+gβπ)) |
28 | 27 | oveqd 5891 |
. . . . . 6
β’ (πΌ β π β (π₯{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = (π₯(+gβπ)π¦)) |
29 | 28, 25 | eleq12d 2248 |
. . . . 5
β’ (πΌ β π β ((π₯{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) β {πΌ} β (π₯(+gβπ)π¦) β (Baseβπ))) |
30 | 25, 29 | raleqbidv 2684 |
. . . 4
β’ (πΌ β π β (βπ¦ β {πΌ} (π₯{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) β {πΌ} β βπ¦ β (Baseβπ)(π₯(+gβπ)π¦) β (Baseβπ))) |
31 | 25, 30 | raleqbidv 2684 |
. . 3
β’ (πΌ β π β (βπ₯ β {πΌ}βπ¦ β {πΌ} (π₯{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) β {πΌ} β βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(π₯(+gβπ)π¦) β (Baseβπ))) |
32 | 17, 31 | mpbid 147 |
. 2
β’ (πΌ β π β βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(π₯(+gβπ)π¦) β (Baseβπ)) |
33 | 7, 25 | eleqtrd 2256 |
. . 3
β’ (πΌ β π β πΌ β (Baseβπ)) |
34 | | eqid 2177 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
35 | | eqid 2177 |
. . . 4
β’
(+gβπ) = (+gβπ) |
36 | 34, 35 | ismgmn0 12776 |
. . 3
β’ (πΌ β (Baseβπ) β (π β Mgm β βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(π₯(+gβπ)π¦) β (Baseβπ))) |
37 | 33, 36 | syl 14 |
. 2
β’ (πΌ β π β (π β Mgm β βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(π₯(+gβπ)π¦) β (Baseβπ))) |
38 | 32, 37 | mpbird 167 |
1
β’ (πΌ β π β π β Mgm) |