Step | Hyp | Ref
| Expression |
1 | | prhash2ex 14356 |
. 2
β’
(β―β{0, 1}) = 2 |
2 | | c0ex 11205 |
. . . . 5
β’ 0 β
V |
3 | | 1ex 11207 |
. . . . 5
β’ 1 β
V |
4 | 2, 3 | pm3.2i 472 |
. . . 4
β’ (0 β
V β§ 1 β V) |
5 | | eqid 2733 |
. . . . 5
β’ {0, 1} =
{0, 1} |
6 | | prex 5432 |
. . . . . . 7
β’ {0, 1}
β V |
7 | | eqeq1 2737 |
. . . . . . . . . . . . 13
β’ (π₯ = π’ β (π₯ = 0 β π’ = 0)) |
8 | 7 | anbi1d 631 |
. . . . . . . . . . . 12
β’ (π₯ = π’ β ((π₯ = 0 β§ π¦ = 0) β (π’ = 0 β§ π¦ = 0))) |
9 | 8 | ifbid 4551 |
. . . . . . . . . . 11
β’ (π₯ = π’ β if((π₯ = 0 β§ π¦ = 0), 1, 0) = if((π’ = 0 β§ π¦ = 0), 1, 0)) |
10 | | eqeq1 2737 |
. . . . . . . . . . . . 13
β’ (π¦ = π£ β (π¦ = 0 β π£ = 0)) |
11 | 10 | anbi2d 630 |
. . . . . . . . . . . 12
β’ (π¦ = π£ β ((π’ = 0 β§ π¦ = 0) β (π’ = 0 β§ π£ = 0))) |
12 | 11 | ifbid 4551 |
. . . . . . . . . . 11
β’ (π¦ = π£ β if((π’ = 0 β§ π¦ = 0), 1, 0) = if((π’ = 0 β§ π£ = 0), 1, 0)) |
13 | 9, 12 | cbvmpov 7501 |
. . . . . . . . . 10
β’ (π₯ β {0, 1}, π¦ β {0, 1} β¦ if((π₯ = 0 β§ π¦ = 0), 1, 0)) = (π’ β {0, 1}, π£ β {0, 1} β¦ if((π’ = 0 β§ π£ = 0), 1, 0)) |
14 | 13 | opeq2i 4877 |
. . . . . . . . 9
β’
β¨(+gβndx), (π₯ β {0, 1}, π¦ β {0, 1} β¦ if((π₯ = 0 β§ π¦ = 0), 1, 0))β© =
β¨(+gβndx), (π’ β {0, 1}, π£ β {0, 1} β¦ if((π’ = 0 β§ π£ = 0), 1, 0))β© |
15 | 14 | preq2i 4741 |
. . . . . . . 8
β’
{β¨(Baseβndx), {0, 1}β©, β¨(+gβndx),
(π₯ β {0, 1}, π¦ β {0, 1} β¦ if((π₯ = 0 β§ π¦ = 0), 1, 0))β©} =
{β¨(Baseβndx), {0, 1}β©, β¨(+gβndx), (π’ β {0, 1}, π£ β {0, 1} β¦ if((π’ = 0 β§ π£ = 0), 1, 0))β©} |
16 | 15 | grpbase 17228 |
. . . . . . 7
β’ ({0, 1}
β V β {0, 1} = (Baseβ{β¨(Baseβndx), {0, 1}β©,
β¨(+gβndx), (π₯ β {0, 1}, π¦ β {0, 1} β¦ if((π₯ = 0 β§ π¦ = 0), 1, 0))β©})) |
17 | 6, 16 | ax-mp 5 |
. . . . . 6
β’ {0, 1} =
(Baseβ{β¨(Baseβndx), {0, 1}β©,
β¨(+gβndx), (π₯ β {0, 1}, π¦ β {0, 1} β¦ if((π₯ = 0 β§ π¦ = 0), 1, 0))β©}) |
18 | 17 | eqcomi 2742 |
. . . . 5
β’
(Baseβ{β¨(Baseβndx), {0, 1}β©,
β¨(+gβndx), (π₯ β {0, 1}, π¦ β {0, 1} β¦ if((π₯ = 0 β§ π¦ = 0), 1, 0))β©}) = {0,
1} |
19 | 6, 6 | mpoex 8063 |
. . . . . . 7
β’ (π’ β {0, 1}, π£ β {0, 1} β¦ if((π’ = 0 β§ π£ = 0), 1, 0)) β V |
20 | 15 | grpplusg 17230 |
. . . . . . 7
β’ ((π’ β {0, 1}, π£ β {0, 1} β¦ if((π’ = 0 β§ π£ = 0), 1, 0)) β V β (π’ β {0, 1}, π£ β {0, 1} β¦ if((π’ = 0 β§ π£ = 0), 1, 0)) =
(+gβ{β¨(Baseβndx), {0, 1}β©,
β¨(+gβndx), (π₯ β {0, 1}, π¦ β {0, 1} β¦ if((π₯ = 0 β§ π¦ = 0), 1, 0))β©})) |
21 | 19, 20 | ax-mp 5 |
. . . . . 6
β’ (π’ β {0, 1}, π£ β {0, 1} β¦ if((π’ = 0 β§ π£ = 0), 1, 0)) =
(+gβ{β¨(Baseβndx), {0, 1}β©,
β¨(+gβndx), (π₯ β {0, 1}, π¦ β {0, 1} β¦ if((π₯ = 0 β§ π¦ = 0), 1, 0))β©}) |
22 | 21 | eqcomi 2742 |
. . . . 5
β’
(+gβ{β¨(Baseβndx), {0, 1}β©,
β¨(+gβndx), (π₯ β {0, 1}, π¦ β {0, 1} β¦ if((π₯ = 0 β§ π¦ = 0), 1, 0))β©}) = (π’ β {0, 1}, π£ β {0, 1} β¦ if((π’ = 0 β§ π£ = 0), 1, 0)) |
23 | 5, 18, 22 | mgm2nsgrplem1 18796 |
. . . 4
β’ ((0
β V β§ 1 β V) β {β¨(Baseβndx), {0, 1}β©,
β¨(+gβndx), (π₯ β {0, 1}, π¦ β {0, 1} β¦ if((π₯ = 0 β§ π¦ = 0), 1, 0))β©} β
Mgm) |
24 | 4, 23 | mp1i 13 |
. . 3
β’
((β―β{0, 1}) = 2 β {β¨(Baseβndx), {0,
1}β©, β¨(+gβndx), (π₯ β {0, 1}, π¦ β {0, 1} β¦ if((π₯ = 0 β§ π¦ = 0), 1, 0))β©} β
Mgm) |
25 | | neleq1 3053 |
. . . 4
β’ (π = {β¨(Baseβndx), {0,
1}β©, β¨(+gβndx), (π₯ β {0, 1}, π¦ β {0, 1} β¦ if((π₯ = 0 β§ π¦ = 0), 1, 0))β©} β (π β Smgrp β
{β¨(Baseβndx), {0, 1}β©, β¨(+gβndx), (π₯ β {0, 1}, π¦ β {0, 1} β¦ if((π₯ = 0 β§ π¦ = 0), 1, 0))β©} β
Smgrp)) |
26 | 25 | adantl 483 |
. . 3
β’
(((β―β{0, 1}) = 2 β§ π = {β¨(Baseβndx), {0, 1}β©,
β¨(+gβndx), (π₯ β {0, 1}, π¦ β {0, 1} β¦ if((π₯ = 0 β§ π¦ = 0), 1, 0))β©}) β (π β Smgrp β
{β¨(Baseβndx), {0, 1}β©, β¨(+gβndx), (π₯ β {0, 1}, π¦ β {0, 1} β¦ if((π₯ = 0 β§ π¦ = 0), 1, 0))β©} β
Smgrp)) |
27 | 5, 18, 22 | mgm2nsgrplem4 18799 |
. . 3
β’
((β―β{0, 1}) = 2 β {β¨(Baseβndx), {0,
1}β©, β¨(+gβndx), (π₯ β {0, 1}, π¦ β {0, 1} β¦ if((π₯ = 0 β§ π¦ = 0), 1, 0))β©} β
Smgrp) |
28 | 24, 26, 27 | rspcedvd 3615 |
. 2
β’
((β―β{0, 1}) = 2 β βπ β Mgm π β Smgrp) |
29 | 1, 28 | ax-mp 5 |
1
β’
βπ β Mgm
π β
Smgrp |