Step | Hyp | Ref
| Expression |
1 | | mnd1.m |
. . . 4
β’ π = {β¨(Baseβndx),
{πΌ}β©,
β¨(+gβndx), {β¨β¨πΌ, πΌβ©, πΌβ©}β©} |
2 | 1 | sgrp1 12815 |
. . 3
β’ (πΌ β π β π β Smgrp) |
3 | | df-ov 5877 |
. . . . . 6
β’ (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = ({β¨β¨πΌ, πΌβ©, πΌβ©}ββ¨πΌ, πΌβ©) |
4 | | opexg 4228 |
. . . . . . . 8
β’ ((πΌ β π β§ πΌ β π) β β¨πΌ, πΌβ© β V) |
5 | 4 | anidms 397 |
. . . . . . 7
β’ (πΌ β π β β¨πΌ, πΌβ© β V) |
6 | | fvsng 5712 |
. . . . . . 7
β’
((β¨πΌ, πΌβ© β V β§ πΌ β π) β ({β¨β¨πΌ, πΌβ©, πΌβ©}ββ¨πΌ, πΌβ©) = πΌ) |
7 | 5, 6 | mpancom 422 |
. . . . . 6
β’ (πΌ β π β ({β¨β¨πΌ, πΌβ©, πΌβ©}ββ¨πΌ, πΌβ©) = πΌ) |
8 | 3, 7 | eqtrid 2222 |
. . . . 5
β’ (πΌ β π β (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = πΌ) |
9 | | oveq2 5882 |
. . . . . . . 8
β’ (π¦ = πΌ β (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ)) |
10 | | id 19 |
. . . . . . . 8
β’ (π¦ = πΌ β π¦ = πΌ) |
11 | 9, 10 | eqeq12d 2192 |
. . . . . . 7
β’ (π¦ = πΌ β ((πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = π¦ β (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = πΌ)) |
12 | | oveq1 5881 |
. . . . . . . 8
β’ (π¦ = πΌ β (π¦{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ)) |
13 | 12, 10 | eqeq12d 2192 |
. . . . . . 7
β’ (π¦ = πΌ β ((π¦{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = π¦ β (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = πΌ)) |
14 | 11, 13 | anbi12d 473 |
. . . . . 6
β’ (π¦ = πΌ β (((πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = π¦ β§ (π¦{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = π¦) β ((πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = πΌ β§ (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = πΌ))) |
15 | 14 | ralsng 3632 |
. . . . 5
β’ (πΌ β π β (βπ¦ β {πΌ} ((πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = π¦ β§ (π¦{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = π¦) β ((πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = πΌ β§ (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = πΌ))) |
16 | 8, 8, 15 | mpbir2and 944 |
. . . 4
β’ (πΌ β π β βπ¦ β {πΌ} ((πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = π¦ β§ (π¦{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = π¦)) |
17 | | oveq1 5881 |
. . . . . . 7
β’ (π₯ = πΌ β (π₯{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}π¦)) |
18 | 17 | eqeq1d 2186 |
. . . . . 6
β’ (π₯ = πΌ β ((π₯{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = π¦ β (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = π¦)) |
19 | 18 | ovanraleqv 5898 |
. . . . 5
β’ (π₯ = πΌ β (βπ¦ β {πΌ} ((π₯{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = π¦ β§ (π¦{β¨β¨πΌ, πΌβ©, πΌβ©}π₯) = π¦) β βπ¦ β {πΌ} ((πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = π¦ β§ (π¦{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = π¦))) |
20 | 19 | rexsng 3633 |
. . . 4
β’ (πΌ β π β (βπ₯ β {πΌ}βπ¦ β {πΌ} ((π₯{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = π¦ β§ (π¦{β¨β¨πΌ, πΌβ©, πΌβ©}π₯) = π¦) β βπ¦ β {πΌ} ((πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = π¦ β§ (π¦{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = π¦))) |
21 | 16, 20 | mpbird 167 |
. . 3
β’ (πΌ β π β βπ₯ β {πΌ}βπ¦ β {πΌ} ((π₯{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = π¦ β§ (π¦{β¨β¨πΌ, πΌβ©, πΌβ©}π₯) = π¦)) |
22 | | snexg 4184 |
. . . . . 6
β’ (πΌ β π β {πΌ} β V) |
23 | | opexg 4228 |
. . . . . . . 8
β’
((β¨πΌ, πΌβ© β V β§ πΌ β π) β β¨β¨πΌ, πΌβ©, πΌβ© β V) |
24 | 5, 23 | mpancom 422 |
. . . . . . 7
β’ (πΌ β π β β¨β¨πΌ, πΌβ©, πΌβ© β V) |
25 | | snexg 4184 |
. . . . . . 7
β’
(β¨β¨πΌ,
πΌβ©, πΌβ© β V β {β¨β¨πΌ, πΌβ©, πΌβ©} β V) |
26 | 24, 25 | syl 14 |
. . . . . 6
β’ (πΌ β π β {β¨β¨πΌ, πΌβ©, πΌβ©} β V) |
27 | 1 | grpbaseg 12584 |
. . . . . 6
β’ (({πΌ} β V β§
{β¨β¨πΌ, πΌβ©, πΌβ©} β V) β {πΌ} = (Baseβπ)) |
28 | 22, 26, 27 | syl2anc 411 |
. . . . 5
β’ (πΌ β π β {πΌ} = (Baseβπ)) |
29 | 1 | grpplusgg 12585 |
. . . . . . . . . 10
β’ (({πΌ} β V β§
{β¨β¨πΌ, πΌβ©, πΌβ©} β V) β {β¨β¨πΌ, πΌβ©, πΌβ©} = (+gβπ)) |
30 | 22, 26, 29 | syl2anc 411 |
. . . . . . . . 9
β’ (πΌ β π β {β¨β¨πΌ, πΌβ©, πΌβ©} = (+gβπ)) |
31 | 30 | oveqd 5891 |
. . . . . . . 8
β’ (πΌ β π β (π₯{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = (π₯(+gβπ)π¦)) |
32 | 31 | eqeq1d 2186 |
. . . . . . 7
β’ (πΌ β π β ((π₯{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = π¦ β (π₯(+gβπ)π¦) = π¦)) |
33 | 30 | oveqd 5891 |
. . . . . . . 8
β’ (πΌ β π β (π¦{β¨β¨πΌ, πΌβ©, πΌβ©}π₯) = (π¦(+gβπ)π₯)) |
34 | 33 | eqeq1d 2186 |
. . . . . . 7
β’ (πΌ β π β ((π¦{β¨β¨πΌ, πΌβ©, πΌβ©}π₯) = π¦ β (π¦(+gβπ)π₯) = π¦)) |
35 | 32, 34 | anbi12d 473 |
. . . . . 6
β’ (πΌ β π β (((π₯{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = π¦ β§ (π¦{β¨β¨πΌ, πΌβ©, πΌβ©}π₯) = π¦) β ((π₯(+gβπ)π¦) = π¦ β§ (π¦(+gβπ)π₯) = π¦))) |
36 | 28, 35 | raleqbidv 2684 |
. . . . 5
β’ (πΌ β π β (βπ¦ β {πΌ} ((π₯{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = π¦ β§ (π¦{β¨β¨πΌ, πΌβ©, πΌβ©}π₯) = π¦) β βπ¦ β (Baseβπ)((π₯(+gβπ)π¦) = π¦ β§ (π¦(+gβπ)π₯) = π¦))) |
37 | 28, 36 | rexeqbidv 2685 |
. . . 4
β’ (πΌ β π β (βπ₯ β {πΌ}βπ¦ β {πΌ} ((π₯{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = π¦ β§ (π¦{β¨β¨πΌ, πΌβ©, πΌβ©}π₯) = π¦) β βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)((π₯(+gβπ)π¦) = π¦ β§ (π¦(+gβπ)π₯) = π¦))) |
38 | 37 | anbi2d 464 |
. . 3
β’ (πΌ β π β ((π β Smgrp β§ βπ₯ β {πΌ}βπ¦ β {πΌ} ((π₯{β¨β¨πΌ, πΌβ©, πΌβ©}π¦) = π¦ β§ (π¦{β¨β¨πΌ, πΌβ©, πΌβ©}π₯) = π¦)) β (π β Smgrp β§ βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)((π₯(+gβπ)π¦) = π¦ β§ (π¦(+gβπ)π₯) = π¦)))) |
39 | 2, 21, 38 | mpbi2and 943 |
. 2
β’ (πΌ β π β (π β Smgrp β§ βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)((π₯(+gβπ)π¦) = π¦ β§ (π¦(+gβπ)π₯) = π¦))) |
40 | | eqid 2177 |
. . 3
β’
(Baseβπ) =
(Baseβπ) |
41 | | eqid 2177 |
. . 3
β’
(+gβπ) = (+gβπ) |
42 | 40, 41 | ismnddef 12818 |
. 2
β’ (π β Mnd β (π β Smgrp β§ βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)((π₯(+gβπ)π¦) = π¦ β§ (π¦(+gβπ)π₯) = π¦))) |
43 | 39, 42 | sylibr 134 |
1
β’ (πΌ β π β π β Mnd) |