Step | Hyp | Ref
| Expression |
1 | | simp1 1136 |
. . 3
β’ ((π· β Fin β§ π β (π΅ β π΄) β§ π β (π΅ β π΄)) β π· β Fin) |
2 | | simp2 1137 |
. . . . . 6
β’ ((π· β Fin β§ π β (π΅ β π΄) β§ π β (π΅ β π΄)) β π β (π΅ β π΄)) |
3 | 2 | eldifad 3956 |
. . . . 5
β’ ((π· β Fin β§ π β (π΅ β π΄) β§ π β (π΅ β π΄)) β π β π΅) |
4 | | simp3 1138 |
. . . . . 6
β’ ((π· β Fin β§ π β (π΅ β π΄) β§ π β (π΅ β π΄)) β π β (π΅ β π΄)) |
5 | 4 | eldifad 3956 |
. . . . 5
β’ ((π· β Fin β§ π β (π΅ β π΄) β§ π β (π΅ β π΄)) β π β π΅) |
6 | | odpmco.s |
. . . . . 6
β’ π = (SymGrpβπ·) |
7 | | odpmco.b |
. . . . . 6
β’ π΅ = (Baseβπ) |
8 | | eqid 2731 |
. . . . . 6
β’
(+gβπ) = (+gβπ) |
9 | 6, 7, 8 | symgov 19215 |
. . . . 5
β’ ((π β π΅ β§ π β π΅) β (π(+gβπ)π) = (π β π)) |
10 | 3, 5, 9 | syl2anc 584 |
. . . 4
β’ ((π· β Fin β§ π β (π΅ β π΄) β§ π β (π΅ β π΄)) β (π(+gβπ)π) = (π β π)) |
11 | 6, 7, 8 | symgcl 19216 |
. . . . 5
β’ ((π β π΅ β§ π β π΅) β (π(+gβπ)π) β π΅) |
12 | 3, 5, 11 | syl2anc 584 |
. . . 4
β’ ((π· β Fin β§ π β (π΅ β π΄) β§ π β (π΅ β π΄)) β (π(+gβπ)π) β π΅) |
13 | 10, 12 | eqeltrrd 2833 |
. . 3
β’ ((π· β Fin β§ π β (π΅ β π΄) β§ π β (π΅ β π΄)) β (π β π) β π΅) |
14 | | eqid 2731 |
. . . . . 6
β’
(pmSgnβπ·) =
(pmSgnβπ·) |
15 | 6, 14, 7 | psgnco 21069 |
. . . . 5
β’ ((π· β Fin β§ π β π΅ β§ π β π΅) β ((pmSgnβπ·)β(π β π)) = (((pmSgnβπ·)βπ) Β· ((pmSgnβπ·)βπ))) |
16 | 1, 3, 5, 15 | syl3anc 1371 |
. . . 4
β’ ((π· β Fin β§ π β (π΅ β π΄) β§ π β (π΅ β π΄)) β ((pmSgnβπ·)β(π β π)) = (((pmSgnβπ·)βπ) Β· ((pmSgnβπ·)βπ))) |
17 | | odpmco.a |
. . . . . . . . . 10
β’ π΄ = (pmEvenβπ·) |
18 | 17 | a1i 11 |
. . . . . . . . 9
β’ ((π· β Fin β§ π β (π΅ β π΄) β§ π β (π΅ β π΄)) β π΄ = (pmEvenβπ·)) |
19 | 18 | difeq2d 4118 |
. . . . . . . 8
β’ ((π· β Fin β§ π β (π΅ β π΄) β§ π β (π΅ β π΄)) β (π΅ β π΄) = (π΅ β (pmEvenβπ·))) |
20 | 2, 19 | eleqtrd 2834 |
. . . . . . 7
β’ ((π· β Fin β§ π β (π΅ β π΄) β§ π β (π΅ β π΄)) β π β (π΅ β (pmEvenβπ·))) |
21 | 6, 7, 14 | psgnodpm 21074 |
. . . . . . 7
β’ ((π· β Fin β§ π β (π΅ β (pmEvenβπ·))) β ((pmSgnβπ·)βπ) = -1) |
22 | 1, 20, 21 | syl2anc 584 |
. . . . . 6
β’ ((π· β Fin β§ π β (π΅ β π΄) β§ π β (π΅ β π΄)) β ((pmSgnβπ·)βπ) = -1) |
23 | 4, 19 | eleqtrd 2834 |
. . . . . . 7
β’ ((π· β Fin β§ π β (π΅ β π΄) β§ π β (π΅ β π΄)) β π β (π΅ β (pmEvenβπ·))) |
24 | 6, 7, 14 | psgnodpm 21074 |
. . . . . . 7
β’ ((π· β Fin β§ π β (π΅ β (pmEvenβπ·))) β ((pmSgnβπ·)βπ) = -1) |
25 | 1, 23, 24 | syl2anc 584 |
. . . . . 6
β’ ((π· β Fin β§ π β (π΅ β π΄) β§ π β (π΅ β π΄)) β ((pmSgnβπ·)βπ) = -1) |
26 | 22, 25 | oveq12d 7411 |
. . . . 5
β’ ((π· β Fin β§ π β (π΅ β π΄) β§ π β (π΅ β π΄)) β (((pmSgnβπ·)βπ) Β· ((pmSgnβπ·)βπ)) = (-1 Β· -1)) |
27 | | neg1mulneg1e1 12407 |
. . . . 5
β’ (-1
Β· -1) = 1 |
28 | 26, 27 | eqtrdi 2787 |
. . . 4
β’ ((π· β Fin β§ π β (π΅ β π΄) β§ π β (π΅ β π΄)) β (((pmSgnβπ·)βπ) Β· ((pmSgnβπ·)βπ)) = 1) |
29 | 16, 28 | eqtrd 2771 |
. . 3
β’ ((π· β Fin β§ π β (π΅ β π΄) β§ π β (π΅ β π΄)) β ((pmSgnβπ·)β(π β π)) = 1) |
30 | 6, 7, 14 | psgnevpmb 21073 |
. . . 4
β’ (π· β Fin β ((π β π) β (pmEvenβπ·) β ((π β π) β π΅ β§ ((pmSgnβπ·)β(π β π)) = 1))) |
31 | 30 | biimpar 478 |
. . 3
β’ ((π· β Fin β§ ((π β π) β π΅ β§ ((pmSgnβπ·)β(π β π)) = 1)) β (π β π) β (pmEvenβπ·)) |
32 | 1, 13, 29, 31 | syl12anc 835 |
. 2
β’ ((π· β Fin β§ π β (π΅ β π΄) β§ π β (π΅ β π΄)) β (π β π) β (pmEvenβπ·)) |
33 | 32, 17 | eleqtrrdi 2843 |
1
β’ ((π· β Fin β§ π β (π΅ β π΄) β§ π β (π΅ β π΄)) β (π β π) β π΄) |