Step | Hyp | Ref
| Expression |
1 | | dchrabs.g |
. . . . . . . 8
β’ πΊ = (DChrβπ) |
2 | | eqid 2737 |
. . . . . . . 8
β’
(β€/nβ€βπ) = (β€/nβ€βπ) |
3 | | dchrabs.d |
. . . . . . . 8
β’ π· = (BaseβπΊ) |
4 | | eqid 2737 |
. . . . . . . 8
β’
(+gβπΊ) = (+gβπΊ) |
5 | | dchrabs.x |
. . . . . . . 8
β’ (π β π β π·) |
6 | | cjf 14996 |
. . . . . . . . . 10
β’
β:ββΆβ |
7 | | eqid 2737 |
. . . . . . . . . . 11
β’
(Baseβ(β€/nβ€βπ)) =
(Baseβ(β€/nβ€βπ)) |
8 | 1, 2, 3, 7, 5 | dchrf 26606 |
. . . . . . . . . 10
β’ (π β π:(Baseβ(β€/nβ€βπ))βΆβ) |
9 | | fco 6697 |
. . . . . . . . . 10
β’
((β:ββΆβ β§ π:(Baseβ(β€/nβ€βπ))βΆβ) β (β
β π):(Baseβ(β€/nβ€βπ))βΆβ) |
10 | 6, 8, 9 | sylancr 588 |
. . . . . . . . 9
β’ (π β (β β π):(Baseβ(β€/nβ€βπ))βΆβ) |
11 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(Unitβ(β€/nβ€βπ)) =
(Unitβ(β€/nβ€βπ)) |
12 | 1, 3 | dchrrcl 26604 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π· β π β β) |
13 | 5, 12 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β β) |
14 | 1, 2, 7, 11, 13, 3 | dchrelbas3 26602 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π β π· β (π:(Baseβ(β€/nβ€βπ))βΆβ β§
(βπ₯ β
(Unitβ(β€/nβ€βπ))βπ¦ β
(Unitβ(β€/nβ€βπ))(πβ(π₯(.rβ(β€/nβ€βπ))π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(1rβ(β€/nβ€βπ))) = 1 β§ βπ₯ β (Baseβ(β€/nβ€βπ))((πβπ₯)
β 0 β π₯ β
(Unitβ(β€/nβ€βπ))))))) |
15 | 5, 14 | mpbid 231 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π:(Baseβ(β€/nβ€βπ))βΆβ β§
(βπ₯ β
(Unitβ(β€/nβ€βπ))βπ¦ β
(Unitβ(β€/nβ€βπ))(πβ(π₯(.rβ(β€/nβ€βπ))π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(1rβ(β€/nβ€βπ))) = 1 β§ βπ₯ β (Baseβ(β€/nβ€βπ))((πβπ₯)
β 0 β π₯ β
(Unitβ(β€/nβ€βπ)))))) |
16 | 15 | simprd 497 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (βπ₯ β
(Unitβ(β€/nβ€βπ))βπ¦ β
(Unitβ(β€/nβ€βπ))(πβ(π₯(.rβ(β€/nβ€βπ))π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(1rβ(β€/nβ€βπ))) = 1 β§ βπ₯ β (Baseβ(β€/nβ€βπ))((πβπ₯)
β 0 β π₯ β
(Unitβ(β€/nβ€βπ))))) |
17 | 16 | simp1d 1143 |
. . . . . . . . . . . . . . . . 17
β’ (π β βπ₯ β
(Unitβ(β€/nβ€βπ))βπ¦ β
(Unitβ(β€/nβ€βπ))(πβ(π₯(.rβ(β€/nβ€βπ))π¦)) = ((πβπ₯) Β· (πβπ¦))) |
18 | 17 | r19.21bi 3237 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β
(Unitβ(β€/nβ€βπ))) β βπ¦ β
(Unitβ(β€/nβ€βπ))(πβ(π₯(.rβ(β€/nβ€βπ))π¦)) = ((πβπ₯) Β· (πβπ¦))) |
19 | 18 | r19.21bi 3237 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β
(Unitβ(β€/nβ€βπ))) β§ π¦ β
(Unitβ(β€/nβ€βπ))) β (πβ(π₯(.rβ(β€/nβ€βπ))π¦)) = ((πβπ₯) Β· (πβπ¦))) |
20 | 19 | anasss 468 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β
(Unitβ(β€/nβ€βπ)) β§ π¦ β
(Unitβ(β€/nβ€βπ)))) β (πβ(π₯(.rβ(β€/nβ€βπ))π¦)) = ((πβπ₯) Β· (πβπ¦))) |
21 | 20 | fveq2d 6851 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β
(Unitβ(β€/nβ€βπ)) β§ π¦ β
(Unitβ(β€/nβ€βπ)))) β (ββ(πβ(π₯(.rβ(β€/nβ€βπ))π¦))) = (ββ((πβπ₯) Β· (πβπ¦)))) |
22 | 8 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β
(Unitβ(β€/nβ€βπ)) β§ π¦ β
(Unitβ(β€/nβ€βπ)))) β π:(Baseβ(β€/nβ€βπ))βΆβ) |
23 | 7, 11 | unitss 20096 |
. . . . . . . . . . . . . . . 16
β’
(Unitβ(β€/nβ€βπ)) β
(Baseβ(β€/nβ€βπ)) |
24 | | simprl 770 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π₯ β
(Unitβ(β€/nβ€βπ)) β§ π¦ β
(Unitβ(β€/nβ€βπ)))) β π₯ β
(Unitβ(β€/nβ€βπ))) |
25 | 23, 24 | sselid 3947 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β
(Unitβ(β€/nβ€βπ)) β§ π¦ β
(Unitβ(β€/nβ€βπ)))) β π₯ β
(Baseβ(β€/nβ€βπ))) |
26 | 22, 25 | ffvelcdmd 7041 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β
(Unitβ(β€/nβ€βπ)) β§ π¦ β
(Unitβ(β€/nβ€βπ)))) β (πβπ₯) β β) |
27 | | simprr 772 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π₯ β
(Unitβ(β€/nβ€βπ)) β§ π¦ β
(Unitβ(β€/nβ€βπ)))) β π¦ β
(Unitβ(β€/nβ€βπ))) |
28 | 23, 27 | sselid 3947 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β
(Unitβ(β€/nβ€βπ)) β§ π¦ β
(Unitβ(β€/nβ€βπ)))) β π¦ β
(Baseβ(β€/nβ€βπ))) |
29 | 22, 28 | ffvelcdmd 7041 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β
(Unitβ(β€/nβ€βπ)) β§ π¦ β
(Unitβ(β€/nβ€βπ)))) β (πβπ¦) β β) |
30 | 26, 29 | cjmuld 15113 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β
(Unitβ(β€/nβ€βπ)) β§ π¦ β
(Unitβ(β€/nβ€βπ)))) β (ββ((πβπ₯) Β· (πβπ¦))) = ((ββ(πβπ₯)) Β· (ββ(πβπ¦)))) |
31 | 21, 30 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β
(Unitβ(β€/nβ€βπ)) β§ π¦ β
(Unitβ(β€/nβ€βπ)))) β (ββ(πβ(π₯(.rβ(β€/nβ€βπ))π¦))) = ((ββ(πβπ₯)) Β· (ββ(πβπ¦)))) |
32 | 13 | nnnn0d 12480 |
. . . . . . . . . . . . . . . 16
β’ (π β π β
β0) |
33 | 2 | zncrng 20967 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β (β€/nβ€βπ) β CRing) |
34 | | crngring 19983 |
. . . . . . . . . . . . . . . 16
β’
((β€/nβ€βπ) β CRing β
(β€/nβ€βπ) β Ring) |
35 | 32, 33, 34 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’ (π β
(β€/nβ€βπ) β Ring) |
36 | 35 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β
(Unitβ(β€/nβ€βπ)) β§ π¦ β
(Unitβ(β€/nβ€βπ)))) β
(β€/nβ€βπ) β Ring) |
37 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’
(.rβ(β€/nβ€βπ)) =
(.rβ(β€/nβ€βπ)) |
38 | 7, 37 | ringcl 19988 |
. . . . . . . . . . . . . 14
β’
(((β€/nβ€βπ) β Ring β§ π₯ β
(Baseβ(β€/nβ€βπ)) β§ π¦ β
(Baseβ(β€/nβ€βπ))) β (π₯(.rβ(β€/nβ€βπ))π¦) β (Baseβ(β€/nβ€βπ))) |
39 | 36, 25, 28, 38 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β
(Unitβ(β€/nβ€βπ)) β§ π¦ β
(Unitβ(β€/nβ€βπ)))) β (π₯(.rβ(β€/nβ€βπ))π¦) β (Baseβ(β€/nβ€βπ))) |
40 | | fvco3 6945 |
. . . . . . . . . . . . 13
β’ ((π:(Baseβ(β€/nβ€βπ))βΆβ β§ (π₯(.rβ(β€/nβ€βπ))π¦) β (Baseβ(β€/nβ€βπ))) β ((β β π)β(π₯(.rβ(β€/nβ€βπ))π¦)) = (ββ(πβ(π₯(.rβ(β€/nβ€βπ))π¦)))) |
41 | 22, 39, 40 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β
(Unitβ(β€/nβ€βπ)) β§ π¦ β
(Unitβ(β€/nβ€βπ)))) β ((β β π)β(π₯(.rβ(β€/nβ€βπ))π¦)) = (ββ(πβ(π₯(.rβ(β€/nβ€βπ))π¦)))) |
42 | | fvco3 6945 |
. . . . . . . . . . . . . 14
β’ ((π:(Baseβ(β€/nβ€βπ))βΆβ β§ π₯ β
(Baseβ(β€/nβ€βπ))) β ((β β π)βπ₯) = (ββ(πβπ₯))) |
43 | 22, 25, 42 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β
(Unitβ(β€/nβ€βπ)) β§ π¦ β
(Unitβ(β€/nβ€βπ)))) β ((β β π)βπ₯) = (ββ(πβπ₯))) |
44 | | fvco3 6945 |
. . . . . . . . . . . . . 14
β’ ((π:(Baseβ(β€/nβ€βπ))βΆβ β§ π¦ β
(Baseβ(β€/nβ€βπ))) β ((β β π)βπ¦) = (ββ(πβπ¦))) |
45 | 22, 28, 44 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β
(Unitβ(β€/nβ€βπ)) β§ π¦ β
(Unitβ(β€/nβ€βπ)))) β ((β β π)βπ¦) = (ββ(πβπ¦))) |
46 | 43, 45 | oveq12d 7380 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β
(Unitβ(β€/nβ€βπ)) β§ π¦ β
(Unitβ(β€/nβ€βπ)))) β (((β β π)βπ₯) Β· ((β β π)βπ¦)) = ((ββ(πβπ₯)) Β· (ββ(πβπ¦)))) |
47 | 31, 41, 46 | 3eqtr4d 2787 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β
(Unitβ(β€/nβ€βπ)) β§ π¦ β
(Unitβ(β€/nβ€βπ)))) β ((β β π)β(π₯(.rβ(β€/nβ€βπ))π¦)) = (((β β π)βπ₯) Β· ((β β π)βπ¦))) |
48 | 47 | ralrimivva 3198 |
. . . . . . . . . 10
β’ (π β βπ₯ β
(Unitβ(β€/nβ€βπ))βπ¦ β
(Unitβ(β€/nβ€βπ))((β β π)β(π₯(.rβ(β€/nβ€βπ))π¦)) = (((β β π)βπ₯) Β· ((β β π)βπ¦))) |
49 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’
(1rβ(β€/nβ€βπ)) =
(1rβ(β€/nβ€βπ)) |
50 | 7, 49 | ringidcl 19996 |
. . . . . . . . . . . . 13
β’
((β€/nβ€βπ) β Ring β
(1rβ(β€/nβ€βπ)) β
(Baseβ(β€/nβ€βπ))) |
51 | 35, 50 | syl 17 |
. . . . . . . . . . . 12
β’ (π β
(1rβ(β€/nβ€βπ)) β
(Baseβ(β€/nβ€βπ))) |
52 | | fvco3 6945 |
. . . . . . . . . . . 12
β’ ((π:(Baseβ(β€/nβ€βπ))βΆβ β§
(1rβ(β€/nβ€βπ)) β
(Baseβ(β€/nβ€βπ))) β ((β β π)β(1rβ(β€/nβ€βπ))) = (ββ(πβ(1rβ(β€/nβ€βπ))))) |
53 | 8, 51, 52 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β ((β β π)β(1rβ(β€/nβ€βπ))) = (ββ(πβ(1rβ(β€/nβ€βπ))))) |
54 | 16 | simp2d 1144 |
. . . . . . . . . . . . 13
β’ (π β (πβ(1rβ(β€/nβ€βπ))) = 1) |
55 | 54 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ (π β (ββ(πβ(1rβ(β€/nβ€βπ)))) = (ββ1)) |
56 | | 1re 11162 |
. . . . . . . . . . . . 13
β’ 1 β
β |
57 | | cjre 15031 |
. . . . . . . . . . . . 13
β’ (1 β
β β (ββ1) = 1) |
58 | 56, 57 | ax-mp 5 |
. . . . . . . . . . . 12
β’
(ββ1) = 1 |
59 | 55, 58 | eqtrdi 2793 |
. . . . . . . . . . 11
β’ (π β (ββ(πβ(1rβ(β€/nβ€βπ)))) = 1) |
60 | 53, 59 | eqtrd 2777 |
. . . . . . . . . 10
β’ (π β ((β β π)β(1rβ(β€/nβ€βπ))) = 1) |
61 | 16 | simp3d 1145 |
. . . . . . . . . . 11
β’ (π β βπ₯ β
(Baseβ(β€/nβ€βπ))((πβπ₯) β 0 β π₯ β
(Unitβ(β€/nβ€βπ)))) |
62 | 8, 42 | sylan 581 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β
(Baseβ(β€/nβ€βπ))) β ((β β π)βπ₯) = (ββ(πβπ₯))) |
63 | | cj0 15050 |
. . . . . . . . . . . . . . . . . 18
β’
(ββ0) = 0 |
64 | 63 | eqcomi 2746 |
. . . . . . . . . . . . . . . . 17
β’ 0 =
(ββ0) |
65 | 64 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β
(Baseβ(β€/nβ€βπ))) β 0 =
(ββ0)) |
66 | 62, 65 | eqeq12d 2753 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β
(Baseβ(β€/nβ€βπ))) β (((β β π)βπ₯) = 0 β (ββ(πβπ₯)) = (ββ0))) |
67 | 8 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β
(Baseβ(β€/nβ€βπ))) β (πβπ₯) β β) |
68 | | 0cn 11154 |
. . . . . . . . . . . . . . . 16
β’ 0 β
β |
69 | | cj11 15054 |
. . . . . . . . . . . . . . . 16
β’ (((πβπ₯) β β β§ 0 β β)
β ((ββ(πβπ₯)) = (ββ0) β (πβπ₯) = 0)) |
70 | 67, 68, 69 | sylancl 587 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β
(Baseβ(β€/nβ€βπ))) β ((ββ(πβπ₯)) = (ββ0) β (πβπ₯) = 0)) |
71 | 66, 70 | bitrd 279 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β
(Baseβ(β€/nβ€βπ))) β (((β β π)βπ₯) = 0 β (πβπ₯) = 0)) |
72 | 71 | necon3bid 2989 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β
(Baseβ(β€/nβ€βπ))) β (((β β π)βπ₯) β 0 β (πβπ₯) β 0)) |
73 | 72 | imbi1d 342 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β
(Baseβ(β€/nβ€βπ))) β ((((β β π)βπ₯) β 0 β π₯ β
(Unitβ(β€/nβ€βπ))) β ((πβπ₯) β 0 β π₯ β
(Unitβ(β€/nβ€βπ))))) |
74 | 73 | ralbidva 3173 |
. . . . . . . . . . 11
β’ (π β (βπ₯ β
(Baseβ(β€/nβ€βπ))(((β β π)βπ₯) β 0 β π₯ β
(Unitβ(β€/nβ€βπ))) β βπ₯ β
(Baseβ(β€/nβ€βπ))((πβπ₯) β 0 β π₯ β
(Unitβ(β€/nβ€βπ))))) |
75 | 61, 74 | mpbird 257 |
. . . . . . . . . 10
β’ (π β βπ₯ β
(Baseβ(β€/nβ€βπ))(((β β π)βπ₯) β 0 β π₯ β
(Unitβ(β€/nβ€βπ)))) |
76 | 48, 60, 75 | 3jca 1129 |
. . . . . . . . 9
β’ (π β (βπ₯ β
(Unitβ(β€/nβ€βπ))βπ¦ β
(Unitβ(β€/nβ€βπ))((β β π)β(π₯(.rβ(β€/nβ€βπ))π¦)) = (((β β π)βπ₯) Β· ((β β π)βπ¦)) β§ ((β β π)β(1rβ(β€/nβ€βπ))) = 1 β§ βπ₯ β (Baseβ(β€/nβ€βπ))(((β β π)βπ₯)
β 0 β π₯ β
(Unitβ(β€/nβ€βπ))))) |
77 | 1, 2, 7, 11, 13, 3 | dchrelbas3 26602 |
. . . . . . . . 9
β’ (π β ((β β π) β π· β ((β β π):(Baseβ(β€/nβ€βπ))βΆβ β§ (βπ₯ β
(Unitβ(β€/nβ€βπ))βπ¦ β
(Unitβ(β€/nβ€βπ))((β β π)β(π₯(.rβ(β€/nβ€βπ))π¦)) = (((β β π)βπ₯) Β· ((β β π)βπ¦)) β§ ((β β π)β(1rβ(β€/nβ€βπ))) = 1 β§ βπ₯ β (Baseβ(β€/nβ€βπ))(((β β π)βπ₯)
β 0 β π₯ β
(Unitβ(β€/nβ€βπ))))))) |
78 | 10, 76, 77 | mpbir2and 712 |
. . . . . . . 8
β’ (π β (β β π) β π·) |
79 | 1, 2, 3, 4, 5, 78 | dchrmul 26612 |
. . . . . . 7
β’ (π β (π(+gβπΊ)(β β π)) = (π βf Β· (β
β π))) |
80 | 79 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β
(Unitβ(β€/nβ€βπ))) β (π(+gβπΊ)(β β π)) = (π βf Β· (β
β π))) |
81 | 80 | fveq1d 6849 |
. . . . 5
β’ ((π β§ π₯ β
(Unitβ(β€/nβ€βπ))) β ((π(+gβπΊ)(β β π))βπ₯) = ((π βf Β· (β
β π))βπ₯)) |
82 | 23 | sseli 3945 |
. . . . . . . . 9
β’ (π₯ β
(Unitβ(β€/nβ€βπ)) β π₯ β
(Baseβ(β€/nβ€βπ))) |
83 | 82, 62 | sylan2 594 |
. . . . . . . 8
β’ ((π β§ π₯ β
(Unitβ(β€/nβ€βπ))) β ((β β π)βπ₯) = (ββ(πβπ₯))) |
84 | 83 | oveq2d 7378 |
. . . . . . 7
β’ ((π β§ π₯ β
(Unitβ(β€/nβ€βπ))) β ((πβπ₯) Β· ((β β π)βπ₯)) = ((πβπ₯) Β· (ββ(πβπ₯)))) |
85 | 82, 67 | sylan2 594 |
. . . . . . . 8
β’ ((π β§ π₯ β
(Unitβ(β€/nβ€βπ))) β (πβπ₯) β β) |
86 | 85 | absvalsqd 15334 |
. . . . . . 7
β’ ((π β§ π₯ β
(Unitβ(β€/nβ€βπ))) β ((absβ(πβπ₯))β2) = ((πβπ₯) Β· (ββ(πβπ₯)))) |
87 | 5 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β
(Unitβ(β€/nβ€βπ))) β π β π·) |
88 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π₯ β
(Unitβ(β€/nβ€βπ))) β π₯ β
(Unitβ(β€/nβ€βπ))) |
89 | 1, 3, 87, 2, 11, 88 | dchrabs 26624 |
. . . . . . . . 9
β’ ((π β§ π₯ β
(Unitβ(β€/nβ€βπ))) β (absβ(πβπ₯)) = 1) |
90 | 89 | oveq1d 7377 |
. . . . . . . 8
β’ ((π β§ π₯ β
(Unitβ(β€/nβ€βπ))) β ((absβ(πβπ₯))β2) = (1β2)) |
91 | | sq1 14106 |
. . . . . . . 8
β’
(1β2) = 1 |
92 | 90, 91 | eqtrdi 2793 |
. . . . . . 7
β’ ((π β§ π₯ β
(Unitβ(β€/nβ€βπ))) β ((absβ(πβπ₯))β2) = 1) |
93 | 84, 86, 92 | 3eqtr2d 2783 |
. . . . . 6
β’ ((π β§ π₯ β
(Unitβ(β€/nβ€βπ))) β ((πβπ₯) Β· ((β β π)βπ₯)) = 1) |
94 | 8 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β
(Unitβ(β€/nβ€βπ))) β π:(Baseβ(β€/nβ€βπ))βΆβ) |
95 | 94 | ffnd 6674 |
. . . . . . 7
β’ ((π β§ π₯ β
(Unitβ(β€/nβ€βπ))) β π Fn
(Baseβ(β€/nβ€βπ))) |
96 | 10 | ffnd 6674 |
. . . . . . . 8
β’ (π β (β β π) Fn
(Baseβ(β€/nβ€βπ))) |
97 | 96 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β
(Unitβ(β€/nβ€βπ))) β (β β π) Fn
(Baseβ(β€/nβ€βπ))) |
98 | | fvexd 6862 |
. . . . . . 7
β’ ((π β§ π₯ β
(Unitβ(β€/nβ€βπ))) β
(Baseβ(β€/nβ€βπ)) β V) |
99 | 82 | adantl 483 |
. . . . . . 7
β’ ((π β§ π₯ β
(Unitβ(β€/nβ€βπ))) β π₯ β
(Baseβ(β€/nβ€βπ))) |
100 | | fnfvof 7639 |
. . . . . . 7
β’ (((π Fn
(Baseβ(β€/nβ€βπ)) β§ (β β π) Fn
(Baseβ(β€/nβ€βπ))) β§
((Baseβ(β€/nβ€βπ)) β V β§ π₯ β
(Baseβ(β€/nβ€βπ)))) β ((π βf Β· (β
β π))βπ₯) = ((πβπ₯) Β· ((β β π)βπ₯))) |
101 | 95, 97, 98, 99, 100 | syl22anc 838 |
. . . . . 6
β’ ((π β§ π₯ β
(Unitβ(β€/nβ€βπ))) β ((π βf Β· (β
β π))βπ₯) = ((πβπ₯) Β· ((β β π)βπ₯))) |
102 | | eqid 2737 |
. . . . . . 7
β’
(0gβπΊ) = (0gβπΊ) |
103 | 13 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β
(Unitβ(β€/nβ€βπ))) β π β β) |
104 | 1, 2, 102, 11, 103, 88 | dchr1 26621 |
. . . . . 6
β’ ((π β§ π₯ β
(Unitβ(β€/nβ€βπ))) β ((0gβπΊ)βπ₯) = 1) |
105 | 93, 101, 104 | 3eqtr4d 2787 |
. . . . 5
β’ ((π β§ π₯ β
(Unitβ(β€/nβ€βπ))) β ((π βf Β· (β
β π))βπ₯) = ((0gβπΊ)βπ₯)) |
106 | 81, 105 | eqtrd 2777 |
. . . 4
β’ ((π β§ π₯ β
(Unitβ(β€/nβ€βπ))) β ((π(+gβπΊ)(β β π))βπ₯) = ((0gβπΊ)βπ₯)) |
107 | 106 | ralrimiva 3144 |
. . 3
β’ (π β βπ₯ β
(Unitβ(β€/nβ€βπ))((π(+gβπΊ)(β β π))βπ₯) = ((0gβπΊ)βπ₯)) |
108 | 1, 2, 3, 4, 5, 78 | dchrmulcl 26613 |
. . . 4
β’ (π β (π(+gβπΊ)(β β π)) β π·) |
109 | 1 | dchrabl 26618 |
. . . . . 6
β’ (π β β β πΊ β Abel) |
110 | | ablgrp 19574 |
. . . . . 6
β’ (πΊ β Abel β πΊ β Grp) |
111 | 13, 109, 110 | 3syl 18 |
. . . . 5
β’ (π β πΊ β Grp) |
112 | 3, 102 | grpidcl 18785 |
. . . . 5
β’ (πΊ β Grp β
(0gβπΊ)
β π·) |
113 | 111, 112 | syl 17 |
. . . 4
β’ (π β (0gβπΊ) β π·) |
114 | 1, 2, 3, 11, 108, 113 | dchreq 26622 |
. . 3
β’ (π β ((π(+gβπΊ)(β β π)) = (0gβπΊ) β βπ₯ β
(Unitβ(β€/nβ€βπ))((π(+gβπΊ)(β β π))βπ₯) = ((0gβπΊ)βπ₯))) |
115 | 107, 114 | mpbird 257 |
. 2
β’ (π β (π(+gβπΊ)(β β π)) = (0gβπΊ)) |
116 | | dchrinv.i |
. . . 4
β’ πΌ = (invgβπΊ) |
117 | 3, 4, 102, 116 | grpinvid1 18809 |
. . 3
β’ ((πΊ β Grp β§ π β π· β§ (β β π) β π·) β ((πΌβπ) = (β β π) β (π(+gβπΊ)(β β π)) = (0gβπΊ))) |
118 | 111, 5, 78, 117 | syl3anc 1372 |
. 2
β’ (π β ((πΌβπ) = (β β π) β (π(+gβπΊ)(β β π)) = (0gβπΊ))) |
119 | 115, 118 | mpbird 257 |
1
β’ (π β (πΌβπ) = (β β π)) |