Step | Hyp | Ref
| Expression |
1 | | snex 5389 |
. . . 4
β’ {πΌ} β V |
2 | | mnd1.m |
. . . . 5
β’ π = {β¨(Baseβndx),
{πΌ}β©,
β¨(+gβndx), {β¨β¨πΌ, πΌβ©, πΌβ©}β©} |
3 | 2 | grpbase 17172 |
. . . 4
β’ ({πΌ} β V β {πΌ} = (Baseβπ)) |
4 | 1, 3 | ax-mp 5 |
. . 3
β’ {πΌ} = (Baseβπ) |
5 | | eqid 2733 |
. . 3
β’
(0gβπ) = (0gβπ) |
6 | | snex 5389 |
. . . 4
β’
{β¨β¨πΌ,
πΌβ©, πΌβ©} β V |
7 | 2 | grpplusg 17174 |
. . . 4
β’
({β¨β¨πΌ,
πΌβ©, πΌβ©} β V β {β¨β¨πΌ, πΌβ©, πΌβ©} = (+gβπ)) |
8 | 6, 7 | ax-mp 5 |
. . 3
β’
{β¨β¨πΌ,
πΌβ©, πΌβ©} = (+gβπ) |
9 | | snidg 4621 |
. . 3
β’ (πΌ β π β πΌ β {πΌ}) |
10 | | velsn 4603 |
. . . . 5
β’ (π β {πΌ} β π = πΌ) |
11 | | df-ov 7361 |
. . . . . . 7
β’ (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = ({β¨β¨πΌ, πΌβ©, πΌβ©}ββ¨πΌ, πΌβ©) |
12 | | opex 5422 |
. . . . . . . 8
β’
β¨πΌ, πΌβ© β V |
13 | | fvsng 7127 |
. . . . . . . 8
β’
((β¨πΌ, πΌβ© β V β§ πΌ β π) β ({β¨β¨πΌ, πΌβ©, πΌβ©}ββ¨πΌ, πΌβ©) = πΌ) |
14 | 12, 13 | mpan 689 |
. . . . . . 7
β’ (πΌ β π β ({β¨β¨πΌ, πΌβ©, πΌβ©}ββ¨πΌ, πΌβ©) = πΌ) |
15 | 11, 14 | eqtrid 2785 |
. . . . . 6
β’ (πΌ β π β (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = πΌ) |
16 | | oveq2 7366 |
. . . . . . 7
β’ (π = πΌ β (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}π) = (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ)) |
17 | | id 22 |
. . . . . . 7
β’ (π = πΌ β π = πΌ) |
18 | 16, 17 | eqeq12d 2749 |
. . . . . 6
β’ (π = πΌ β ((πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}π) = π β (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = πΌ)) |
19 | 15, 18 | syl5ibrcom 247 |
. . . . 5
β’ (πΌ β π β (π = πΌ β (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}π) = π)) |
20 | 10, 19 | biimtrid 241 |
. . . 4
β’ (πΌ β π β (π β {πΌ} β (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}π) = π)) |
21 | 20 | imp 408 |
. . 3
β’ ((πΌ β π β§ π β {πΌ}) β (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}π) = π) |
22 | | oveq1 7365 |
. . . . . . 7
β’ (π = πΌ β (π{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ)) |
23 | 22, 17 | eqeq12d 2749 |
. . . . . 6
β’ (π = πΌ β ((π{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = π β (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = πΌ)) |
24 | 15, 23 | syl5ibrcom 247 |
. . . . 5
β’ (πΌ β π β (π = πΌ β (π{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = π)) |
25 | 10, 24 | biimtrid 241 |
. . . 4
β’ (πΌ β π β (π β {πΌ} β (π{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = π)) |
26 | 25 | imp 408 |
. . 3
β’ ((πΌ β π β§ π β {πΌ}) β (π{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = π) |
27 | 4, 5, 8, 9, 21, 26 | ismgmid2 18528 |
. 2
β’ (πΌ β π β πΌ = (0gβπ)) |
28 | 27 | eqcomd 2739 |
1
β’ (πΌ β π β (0gβπ) = πΌ) |