Step | Hyp | Ref
| Expression |
1 | | dfphi2 16654 |
. 2
β’ (π β β β
(Οβπ) =
(β―β{π₯ β
(0..^π) β£ (π₯ gcd π) = 1})) |
2 | | nnnn0 12428 |
. . . . . . . . 9
β’ (π β β β π β
β0) |
3 | | znchr.y |
. . . . . . . . . 10
β’ π =
(β€/nβ€βπ) |
4 | | eqid 2733 |
. . . . . . . . . 10
β’
(Baseβπ) =
(Baseβπ) |
5 | | eqid 2733 |
. . . . . . . . . 10
β’
((β€RHomβπ) βΎ if(π = 0, β€, (0..^π))) = ((β€RHomβπ) βΎ if(π = 0, β€, (0..^π))) |
6 | | eqid 2733 |
. . . . . . . . . 10
β’ if(π = 0, β€, (0..^π)) = if(π = 0, β€, (0..^π)) |
7 | 3, 4, 5, 6 | znf1o 20981 |
. . . . . . . . 9
β’ (π β β0
β ((β€RHomβπ) βΎ if(π = 0, β€, (0..^π))):if(π = 0, β€, (0..^π))β1-1-ontoβ(Baseβπ)) |
8 | 2, 7 | syl 17 |
. . . . . . . 8
β’ (π β β β
((β€RHomβπ)
βΎ if(π = 0, β€,
(0..^π))):if(π = 0, β€, (0..^π))β1-1-ontoβ(Baseβπ)) |
9 | | nnne0 12195 |
. . . . . . . . 9
β’ (π β β β π β 0) |
10 | | ifnefalse 4502 |
. . . . . . . . 9
β’ (π β 0 β if(π = 0, β€, (0..^π)) = (0..^π)) |
11 | | reseq2 5936 |
. . . . . . . . . . 11
β’ (if(π = 0, β€, (0..^π)) = (0..^π) β ((β€RHomβπ) βΎ if(π = 0, β€, (0..^π))) = ((β€RHomβπ) βΎ (0..^π))) |
12 | 11 | f1oeq1d 6783 |
. . . . . . . . . 10
β’ (if(π = 0, β€, (0..^π)) = (0..^π) β (((β€RHomβπ) βΎ if(π = 0, β€, (0..^π))):if(π = 0, β€, (0..^π))β1-1-ontoβ(Baseβπ) β ((β€RHomβπ) βΎ (0..^π)):if(π = 0, β€, (0..^π))β1-1-ontoβ(Baseβπ))) |
13 | | f1oeq2 6777 |
. . . . . . . . . 10
β’ (if(π = 0, β€, (0..^π)) = (0..^π) β (((β€RHomβπ) βΎ (0..^π)):if(π = 0, β€, (0..^π))β1-1-ontoβ(Baseβπ) β ((β€RHomβπ) βΎ (0..^π)):(0..^π)β1-1-ontoβ(Baseβπ))) |
14 | 12, 13 | bitrd 279 |
. . . . . . . . 9
β’ (if(π = 0, β€, (0..^π)) = (0..^π) β (((β€RHomβπ) βΎ if(π = 0, β€, (0..^π))):if(π = 0, β€, (0..^π))β1-1-ontoβ(Baseβπ) β ((β€RHomβπ) βΎ (0..^π)):(0..^π)β1-1-ontoβ(Baseβπ))) |
15 | 9, 10, 14 | 3syl 18 |
. . . . . . . 8
β’ (π β β β
(((β€RHomβπ)
βΎ if(π = 0, β€,
(0..^π))):if(π = 0, β€, (0..^π))β1-1-ontoβ(Baseβπ) β ((β€RHomβπ) βΎ (0..^π)):(0..^π)β1-1-ontoβ(Baseβπ))) |
16 | 8, 15 | mpbid 231 |
. . . . . . 7
β’ (π β β β
((β€RHomβπ)
βΎ (0..^π)):(0..^π)β1-1-ontoβ(Baseβπ)) |
17 | | f1ofn 6789 |
. . . . . . 7
β’
(((β€RHomβπ) βΎ (0..^π)):(0..^π)β1-1-ontoβ(Baseβπ) β ((β€RHomβπ) βΎ (0..^π)) Fn (0..^π)) |
18 | | elpreima 7012 |
. . . . . . 7
β’
(((β€RHomβπ) βΎ (0..^π)) Fn (0..^π) β (π₯ β (β‘((β€RHomβπ) βΎ (0..^π)) β π) β (π₯ β (0..^π) β§ (((β€RHomβπ) βΎ (0..^π))βπ₯) β π))) |
19 | 16, 17, 18 | 3syl 18 |
. . . . . 6
β’ (π β β β (π₯ β (β‘((β€RHomβπ) βΎ (0..^π)) β π) β (π₯ β (0..^π) β§ (((β€RHomβπ) βΎ (0..^π))βπ₯) β π))) |
20 | | fvres 6865 |
. . . . . . . . . 10
β’ (π₯ β (0..^π) β (((β€RHomβπ) βΎ (0..^π))βπ₯) = ((β€RHomβπ)βπ₯)) |
21 | 20 | adantl 483 |
. . . . . . . . 9
β’ ((π β β β§ π₯ β (0..^π)) β (((β€RHomβπ) βΎ (0..^π))βπ₯) = ((β€RHomβπ)βπ₯)) |
22 | 21 | eleq1d 2819 |
. . . . . . . 8
β’ ((π β β β§ π₯ β (0..^π)) β ((((β€RHomβπ) βΎ (0..^π))βπ₯) β π β ((β€RHomβπ)βπ₯) β π)) |
23 | | elfzoelz 13581 |
. . . . . . . . 9
β’ (π₯ β (0..^π) β π₯ β β€) |
24 | | znunit.u |
. . . . . . . . . 10
β’ π = (Unitβπ) |
25 | | eqid 2733 |
. . . . . . . . . 10
β’
(β€RHomβπ) = (β€RHomβπ) |
26 | 3, 24, 25 | znunit 20993 |
. . . . . . . . 9
β’ ((π β β0
β§ π₯ β β€)
β (((β€RHomβπ)βπ₯) β π β (π₯ gcd π) = 1)) |
27 | 2, 23, 26 | syl2an 597 |
. . . . . . . 8
β’ ((π β β β§ π₯ β (0..^π)) β (((β€RHomβπ)βπ₯) β π β (π₯ gcd π) = 1)) |
28 | 22, 27 | bitrd 279 |
. . . . . . 7
β’ ((π β β β§ π₯ β (0..^π)) β ((((β€RHomβπ) βΎ (0..^π))βπ₯) β π β (π₯ gcd π) = 1)) |
29 | 28 | pm5.32da 580 |
. . . . . 6
β’ (π β β β ((π₯ β (0..^π) β§ (((β€RHomβπ) βΎ (0..^π))βπ₯) β π) β (π₯ β (0..^π) β§ (π₯ gcd π) = 1))) |
30 | 19, 29 | bitrd 279 |
. . . . 5
β’ (π β β β (π₯ β (β‘((β€RHomβπ) βΎ (0..^π)) β π) β (π₯ β (0..^π) β§ (π₯ gcd π) = 1))) |
31 | 30 | abbi2dv 2868 |
. . . 4
β’ (π β β β (β‘((β€RHomβπ) βΎ (0..^π)) β π) = {π₯ β£ (π₯ β (0..^π) β§ (π₯ gcd π) = 1)}) |
32 | | df-rab 3407 |
. . . 4
β’ {π₯ β (0..^π) β£ (π₯ gcd π) = 1} = {π₯ β£ (π₯ β (0..^π) β§ (π₯ gcd π) = 1)} |
33 | 31, 32 | eqtr4di 2791 |
. . 3
β’ (π β β β (β‘((β€RHomβπ) βΎ (0..^π)) β π) = {π₯ β (0..^π) β£ (π₯ gcd π) = 1}) |
34 | 33 | fveq2d 6850 |
. 2
β’ (π β β β
(β―β(β‘((β€RHomβπ) βΎ (0..^π)) β π)) = (β―β{π₯ β (0..^π) β£ (π₯ gcd π) = 1})) |
35 | | f1ocnv 6800 |
. . . . 5
β’
(((β€RHomβπ) βΎ (0..^π)):(0..^π)β1-1-ontoβ(Baseβπ) β β‘((β€RHomβπ) βΎ (0..^π)):(Baseβπ)β1-1-ontoβ(0..^π)) |
36 | | f1of1 6787 |
. . . . 5
β’ (β‘((β€RHomβπ) βΎ (0..^π)):(Baseβπ)β1-1-ontoβ(0..^π) β β‘((β€RHomβπ) βΎ (0..^π)):(Baseβπ)β1-1β(0..^π)) |
37 | 16, 35, 36 | 3syl 18 |
. . . 4
β’ (π β β β β‘((β€RHomβπ) βΎ (0..^π)):(Baseβπ)β1-1β(0..^π)) |
38 | | ovexd 7396 |
. . . 4
β’ (π β β β
(0..^π) β
V) |
39 | 4, 24 | unitss 20097 |
. . . . 5
β’ π β (Baseβπ) |
40 | 39 | a1i 11 |
. . . 4
β’ (π β β β π β (Baseβπ)) |
41 | 24 | fvexi 6860 |
. . . . 5
β’ π β V |
42 | 41 | a1i 11 |
. . . 4
β’ (π β β β π β V) |
43 | | f1imaen2g 8961 |
. . . 4
β’ (((β‘((β€RHomβπ) βΎ (0..^π)):(Baseβπ)β1-1β(0..^π) β§ (0..^π) β V) β§ (π β (Baseβπ) β§ π β V)) β (β‘((β€RHomβπ) βΎ (0..^π)) β π) β π) |
44 | 37, 38, 40, 42, 43 | syl22anc 838 |
. . 3
β’ (π β β β (β‘((β€RHomβπ) βΎ (0..^π)) β π) β π) |
45 | | hasheni 14257 |
. . 3
β’ ((β‘((β€RHomβπ) βΎ (0..^π)) β π) β π β (β―β(β‘((β€RHomβπ) βΎ (0..^π)) β π)) = (β―βπ)) |
46 | 44, 45 | syl 17 |
. 2
β’ (π β β β
(β―β(β‘((β€RHomβπ) βΎ (0..^π)) β π)) = (β―βπ)) |
47 | 1, 34, 46 | 3eqtr2rd 2780 |
1
β’ (π β β β
(β―βπ) =
(Οβπ)) |