Step | Hyp | Ref
| Expression |
1 | | dchrpt.n1 |
. . . . 5
β’ (π β π΄ β 1 ) |
2 | | dchrpt.n |
. . . . . . . . . . . 12
β’ (π β π β β) |
3 | 2 | nnnn0d 12480 |
. . . . . . . . . . 11
β’ (π β π β
β0) |
4 | | dchrpt.z |
. . . . . . . . . . . 12
β’ π =
(β€/nβ€βπ) |
5 | 4 | zncrng 20967 |
. . . . . . . . . . 11
β’ (π β β0
β π β
CRing) |
6 | 3, 5 | syl 17 |
. . . . . . . . . 10
β’ (π β π β CRing) |
7 | | crngring 19983 |
. . . . . . . . . 10
β’ (π β CRing β π β Ring) |
8 | 6, 7 | syl 17 |
. . . . . . . . 9
β’ (π β π β Ring) |
9 | | dchrpt.u |
. . . . . . . . . 10
β’ π = (Unitβπ) |
10 | | dchrpt.h |
. . . . . . . . . 10
β’ π» = ((mulGrpβπ) βΎs π) |
11 | 9, 10 | unitgrp 20103 |
. . . . . . . . 9
β’ (π β Ring β π» β Grp) |
12 | 8, 11 | syl 17 |
. . . . . . . 8
β’ (π β π» β Grp) |
13 | 12 | grpmndd 18767 |
. . . . . . 7
β’ (π β π» β Mnd) |
14 | | dchrpt.w |
. . . . . . . 8
β’ (π β π β Word π) |
15 | 14 | dmexd 7847 |
. . . . . . 7
β’ (π β dom π β V) |
16 | | eqid 2737 |
. . . . . . . 8
β’
(0gβπ») = (0gβπ») |
17 | 16 | gsumz 18653 |
. . . . . . 7
β’ ((π» β Mnd β§ dom π β V) β (π» Ξ£g
(π β dom π β¦
(0gβπ»))) =
(0gβπ»)) |
18 | 13, 15, 17 | syl2anc 585 |
. . . . . 6
β’ (π β (π» Ξ£g (π β dom π β¦ (0gβπ»))) = (0gβπ»)) |
19 | | dchrpt.1 |
. . . . . . . . . 10
β’ 1 =
(1rβπ) |
20 | 9, 10, 19 | unitgrpid 20105 |
. . . . . . . . 9
β’ (π β Ring β 1 =
(0gβπ»)) |
21 | 8, 20 | syl 17 |
. . . . . . . 8
β’ (π β 1 =
(0gβπ»)) |
22 | 21 | mpteq2dv 5212 |
. . . . . . 7
β’ (π β (π β dom π β¦ 1 ) = (π β dom π β¦ (0gβπ»))) |
23 | 22 | oveq2d 7378 |
. . . . . 6
β’ (π β (π» Ξ£g (π β dom π β¦ 1 )) = (π» Ξ£g (π β dom π β¦ (0gβπ»)))) |
24 | 18, 23, 21 | 3eqtr4d 2787 |
. . . . 5
β’ (π β (π» Ξ£g (π β dom π β¦ 1 )) = 1 ) |
25 | 1, 24 | neeqtrrd 3019 |
. . . 4
β’ (π β π΄ β (π» Ξ£g (π β dom π β¦ 1 ))) |
26 | | dchrpt.2 |
. . . . . 6
β’ (π β π»dom DProd π) |
27 | | zex 12515 |
. . . . . . . . . 10
β’ β€
β V |
28 | 27 | mptex 7178 |
. . . . . . . . 9
β’ (π β β€ β¦ (π Β· (πβπ))) β V |
29 | 28 | rnex 7854 |
. . . . . . . 8
β’ ran
(π β β€ β¦
(π Β· (πβπ))) β V |
30 | | dchrpt.s |
. . . . . . . 8
β’ π = (π β dom π β¦ ran (π β β€ β¦ (π Β· (πβπ)))) |
31 | 29, 30 | dmmpti 6650 |
. . . . . . 7
β’ dom π = dom π |
32 | 31 | a1i 11 |
. . . . . 6
β’ (π β dom π = dom π) |
33 | | eqid 2737 |
. . . . . 6
β’ (π»dProjπ) = (π»dProjπ) |
34 | | dchrpt.au |
. . . . . . 7
β’ (π β π΄ β π) |
35 | | dchrpt.3 |
. . . . . . 7
β’ (π β (π» DProd π) = π) |
36 | 34, 35 | eleqtrrd 2841 |
. . . . . 6
β’ (π β π΄ β (π» DProd π)) |
37 | | eqid 2737 |
. . . . . 6
β’ {β β Xπ β
dom π(πβπ) β£ β finSupp (0gβπ»)} = {β β Xπ β dom π(πβπ) β£ β finSupp (0gβπ»)} |
38 | 21 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β dom π) β 1 =
(0gβπ»)) |
39 | 26, 32 | dprdf2 19793 |
. . . . . . . . . 10
β’ (π β π:dom πβΆ(SubGrpβπ»)) |
40 | 39 | ffvelcdmda 7040 |
. . . . . . . . 9
β’ ((π β§ π β dom π) β (πβπ) β (SubGrpβπ»)) |
41 | 16 | subg0cl 18943 |
. . . . . . . . 9
β’ ((πβπ) β (SubGrpβπ») β (0gβπ») β (πβπ)) |
42 | 40, 41 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β dom π) β (0gβπ») β (πβπ)) |
43 | 38, 42 | eqeltrd 2838 |
. . . . . . 7
β’ ((π β§ π β dom π) β 1 β (πβπ)) |
44 | 19 | fvexi 6861 |
. . . . . . . . . 10
β’ 1 β
V |
45 | 44 | a1i 11 |
. . . . . . . . 9
β’ (π β 1 β V) |
46 | 15, 45 | fczfsuppd 9330 |
. . . . . . . 8
β’ (π β (dom π Γ { 1 }) finSupp 1
) |
47 | | fconstmpt 5699 |
. . . . . . . . . 10
β’ (dom
π Γ { 1 }) = (π β dom π β¦ 1 ) |
48 | 47 | eqcomi 2746 |
. . . . . . . . 9
β’ (π β dom π β¦ 1 ) = (dom π Γ { 1 }) |
49 | 48 | a1i 11 |
. . . . . . . 8
β’ (π β (π β dom π β¦ 1 ) = (dom π Γ { 1 })) |
50 | 21 | eqcomd 2743 |
. . . . . . . 8
β’ (π β (0gβπ») = 1 ) |
51 | 46, 49, 50 | 3brtr4d 5142 |
. . . . . . 7
β’ (π β (π β dom π β¦ 1 ) finSupp
(0gβπ»)) |
52 | 37, 26, 32, 43, 51 | dprdwd 19797 |
. . . . . 6
β’ (π β (π β dom π β¦ 1 ) β {β β Xπ β
dom π(πβπ) β£ β finSupp (0gβπ»)}) |
53 | 26, 32, 33, 36, 16, 37, 52 | dpjeq 19845 |
. . . . 5
β’ (π β (π΄ = (π» Ξ£g (π β dom π β¦ 1 )) β βπ β dom π(((π»dProjπ)βπ)βπ΄) = 1 )) |
54 | 53 | necon3abid 2981 |
. . . 4
β’ (π β (π΄ β (π» Ξ£g (π β dom π β¦ 1 )) β Β¬
βπ β dom π(((π»dProjπ)βπ)βπ΄) = 1 )) |
55 | 25, 54 | mpbid 231 |
. . 3
β’ (π β Β¬ βπ β dom π(((π»dProjπ)βπ)βπ΄) = 1 ) |
56 | | rexnal 3104 |
. . 3
β’
(βπ β dom
π Β¬ (((π»dProjπ)βπ)βπ΄) = 1 β Β¬ βπ β dom π(((π»dProjπ)βπ)βπ΄) = 1 ) |
57 | 55, 56 | sylibr 233 |
. 2
β’ (π β βπ β dom π Β¬ (((π»dProjπ)βπ)βπ΄) = 1 ) |
58 | | df-ne 2945 |
. . . 4
β’ ((((π»dProjπ)βπ)βπ΄) β 1 β Β¬ (((π»dProjπ)βπ)βπ΄) = 1 ) |
59 | | dchrpt.g |
. . . . . 6
β’ πΊ = (DChrβπ) |
60 | | dchrpt.d |
. . . . . 6
β’ π· = (BaseβπΊ) |
61 | | dchrpt.b |
. . . . . 6
β’ π΅ = (Baseβπ) |
62 | 2 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β dom π β§ (((π»dProjπ)βπ)βπ΄) β 1 )) β π β
β) |
63 | 1 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β dom π β§ (((π»dProjπ)βπ)βπ΄) β 1 )) β π΄ β 1 ) |
64 | | dchrpt.m |
. . . . . 6
β’ Β· =
(.gβπ») |
65 | 34 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β dom π β§ (((π»dProjπ)βπ)βπ΄) β 1 )) β π΄ β π) |
66 | 14 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β dom π β§ (((π»dProjπ)βπ)βπ΄) β 1 )) β π β Word π) |
67 | 26 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β dom π β§ (((π»dProjπ)βπ)βπ΄) β 1 )) β π»dom DProd π) |
68 | 35 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β dom π β§ (((π»dProjπ)βπ)βπ΄) β 1 )) β (π» DProd π) = π) |
69 | | eqid 2737 |
. . . . . 6
β’
(odβπ») =
(odβπ») |
70 | | eqid 2737 |
. . . . . 6
β’
(-1βπ(2 / ((odβπ»)β(πβπ)))) = (-1βπ(2 /
((odβπ»)β(πβπ)))) |
71 | | simprl 770 |
. . . . . 6
β’ ((π β§ (π β dom π β§ (((π»dProjπ)βπ)βπ΄) β 1 )) β π β dom π) |
72 | | simprr 772 |
. . . . . 6
β’ ((π β§ (π β dom π β§ (((π»dProjπ)βπ)βπ΄) β 1 )) β (((π»dProjπ)βπ)βπ΄) β 1 ) |
73 | | eqid 2737 |
. . . . . 6
β’ (π’ β π β¦ (β©ββπ β β€ ((((π»dProjπ)βπ)βπ’) = (π Β· (πβπ)) β§ β = ((-1βπ(2 /
((odβπ»)β(πβπ))))βπ)))) = (π’ β π β¦ (β©ββπ β β€ ((((π»dProjπ)βπ)βπ’) = (π Β· (πβπ)) β§ β = ((-1βπ(2 /
((odβπ»)β(πβπ))))βπ)))) |
74 | 59, 4, 60, 61, 19, 62, 63, 9, 10, 64, 30, 65, 66, 67, 68, 33, 69, 70, 71, 72, 73 | dchrptlem2 26629 |
. . . . 5
β’ ((π β§ (π β dom π β§ (((π»dProjπ)βπ)βπ΄) β 1 )) β βπ₯ β π· (π₯βπ΄) β 1) |
75 | 74 | expr 458 |
. . . 4
β’ ((π β§ π β dom π) β ((((π»dProjπ)βπ)βπ΄) β 1 β βπ₯ β π· (π₯βπ΄) β 1)) |
76 | 58, 75 | biimtrrid 242 |
. . 3
β’ ((π β§ π β dom π) β (Β¬ (((π»dProjπ)βπ)βπ΄) = 1 β βπ₯ β π· (π₯βπ΄) β 1)) |
77 | 76 | rexlimdva 3153 |
. 2
β’ (π β (βπ β dom π Β¬ (((π»dProjπ)βπ)βπ΄) = 1 β βπ₯ β π· (π₯βπ΄) β 1)) |
78 | 57, 77 | mpd 15 |
1
β’ (π β βπ₯ β π· (π₯βπ΄) β 1) |