Step | Hyp | Ref
| Expression |
1 | | fveq2 6847 |
. . . . . 6
β’ (π₯ = π΄ β (πβπ₯) = (πβπ΄)) |
2 | 1 | neeq1d 3004 |
. . . . 5
β’ (π₯ = π΄ β ((πβπ₯) β 0 β (πβπ΄) β 0)) |
3 | | eleq1 2826 |
. . . . 5
β’ (π₯ = π΄ β (π₯ β π β π΄ β π)) |
4 | 2, 3 | imbi12d 345 |
. . . 4
β’ (π₯ = π΄ β (((πβπ₯) β 0 β π₯ β π) β ((πβπ΄) β 0 β π΄ β π))) |
5 | | dchrn0.x |
. . . . . 6
β’ (π β π β π·) |
6 | | dchrmhm.g |
. . . . . . 7
β’ πΊ = (DChrβπ) |
7 | | dchrmhm.z |
. . . . . . 7
β’ π =
(β€/nβ€βπ) |
8 | | dchrn0.b |
. . . . . . 7
β’ π΅ = (Baseβπ) |
9 | | dchrn0.u |
. . . . . . 7
β’ π = (Unitβπ) |
10 | | dchrmhm.b |
. . . . . . . . 9
β’ π· = (BaseβπΊ) |
11 | 6, 10 | dchrrcl 26604 |
. . . . . . . 8
β’ (π β π· β π β β) |
12 | 5, 11 | syl 17 |
. . . . . . 7
β’ (π β π β β) |
13 | 6, 7, 8, 9, 12, 10 | dchrelbas2 26601 |
. . . . . 6
β’ (π β (π β π· β (π β ((mulGrpβπ) MndHom
(mulGrpββfld)) β§ βπ₯ β π΅ ((πβπ₯) β 0 β π₯ β π)))) |
14 | 5, 13 | mpbid 231 |
. . . . 5
β’ (π β (π β ((mulGrpβπ) MndHom
(mulGrpββfld)) β§ βπ₯ β π΅ ((πβπ₯) β 0 β π₯ β π))) |
15 | 14 | simprd 497 |
. . . 4
β’ (π β βπ₯ β π΅ ((πβπ₯) β 0 β π₯ β π)) |
16 | | dchrn0.a |
. . . 4
β’ (π β π΄ β π΅) |
17 | 4, 15, 16 | rspcdva 3585 |
. . 3
β’ (π β ((πβπ΄) β 0 β π΄ β π)) |
18 | 17 | imp 408 |
. 2
β’ ((π β§ (πβπ΄) β 0) β π΄ β π) |
19 | | ax-1ne0 11127 |
. . . . 5
β’ 1 β
0 |
20 | 19 | a1i 11 |
. . . 4
β’ ((π β§ π΄ β π) β 1 β 0) |
21 | 12 | nnnn0d 12480 |
. . . . . . . 8
β’ (π β π β
β0) |
22 | 7 | zncrng 20967 |
. . . . . . . 8
β’ (π β β0
β π β
CRing) |
23 | | crngring 19983 |
. . . . . . . 8
β’ (π β CRing β π β Ring) |
24 | 21, 22, 23 | 3syl 18 |
. . . . . . 7
β’ (π β π β Ring) |
25 | | eqid 2737 |
. . . . . . . 8
β’
(invrβπ) = (invrβπ) |
26 | | eqid 2737 |
. . . . . . . 8
β’
(.rβπ) = (.rβπ) |
27 | | eqid 2737 |
. . . . . . . 8
β’
(1rβπ) = (1rβπ) |
28 | 9, 25, 26, 27 | unitrinv 20114 |
. . . . . . 7
β’ ((π β Ring β§ π΄ β π) β (π΄(.rβπ)((invrβπ)βπ΄)) = (1rβπ)) |
29 | 24, 28 | sylan 581 |
. . . . . 6
β’ ((π β§ π΄ β π) β (π΄(.rβπ)((invrβπ)βπ΄)) = (1rβπ)) |
30 | 29 | fveq2d 6851 |
. . . . 5
β’ ((π β§ π΄ β π) β (πβ(π΄(.rβπ)((invrβπ)βπ΄))) = (πβ(1rβπ))) |
31 | 14 | simpld 496 |
. . . . . . 7
β’ (π β π β ((mulGrpβπ) MndHom
(mulGrpββfld))) |
32 | 31 | adantr 482 |
. . . . . 6
β’ ((π β§ π΄ β π) β π β ((mulGrpβπ) MndHom
(mulGrpββfld))) |
33 | 16 | adantr 482 |
. . . . . 6
β’ ((π β§ π΄ β π) β π΄ β π΅) |
34 | 9, 25, 8 | ringinvcl 20112 |
. . . . . . 7
β’ ((π β Ring β§ π΄ β π) β ((invrβπ)βπ΄) β π΅) |
35 | 24, 34 | sylan 581 |
. . . . . 6
β’ ((π β§ π΄ β π) β ((invrβπ)βπ΄) β π΅) |
36 | | eqid 2737 |
. . . . . . . 8
β’
(mulGrpβπ) =
(mulGrpβπ) |
37 | 36, 8 | mgpbas 19909 |
. . . . . . 7
β’ π΅ =
(Baseβ(mulGrpβπ)) |
38 | 36, 26 | mgpplusg 19907 |
. . . . . . 7
β’
(.rβπ) = (+gβ(mulGrpβπ)) |
39 | | eqid 2737 |
. . . . . . . 8
β’
(mulGrpββfld) =
(mulGrpββfld) |
40 | | cnfldmul 20818 |
. . . . . . . 8
β’ Β·
= (.rββfld) |
41 | 39, 40 | mgpplusg 19907 |
. . . . . . 7
β’ Β·
= (+gβ(mulGrpββfld)) |
42 | 37, 38, 41 | mhmlin 18616 |
. . . . . 6
β’ ((π β ((mulGrpβπ) MndHom
(mulGrpββfld)) β§ π΄ β π΅ β§ ((invrβπ)βπ΄) β π΅) β (πβ(π΄(.rβπ)((invrβπ)βπ΄))) = ((πβπ΄) Β· (πβ((invrβπ)βπ΄)))) |
43 | 32, 33, 35, 42 | syl3anc 1372 |
. . . . 5
β’ ((π β§ π΄ β π) β (πβ(π΄(.rβπ)((invrβπ)βπ΄))) = ((πβπ΄) Β· (πβ((invrβπ)βπ΄)))) |
44 | 36, 27 | ringidval 19922 |
. . . . . . 7
β’
(1rβπ) = (0gβ(mulGrpβπ)) |
45 | | cnfld1 20838 |
. . . . . . . 8
β’ 1 =
(1rββfld) |
46 | 39, 45 | ringidval 19922 |
. . . . . . 7
β’ 1 =
(0gβ(mulGrpββfld)) |
47 | 44, 46 | mhm0 18617 |
. . . . . 6
β’ (π β ((mulGrpβπ) MndHom
(mulGrpββfld)) β (πβ(1rβπ)) = 1) |
48 | 32, 47 | syl 17 |
. . . . 5
β’ ((π β§ π΄ β π) β (πβ(1rβπ)) = 1) |
49 | 30, 43, 48 | 3eqtr3d 2785 |
. . . 4
β’ ((π β§ π΄ β π) β ((πβπ΄) Β· (πβ((invrβπ)βπ΄))) = 1) |
50 | | cnfldbas 20816 |
. . . . . . . . 9
β’ β =
(Baseββfld) |
51 | 39, 50 | mgpbas 19909 |
. . . . . . . 8
β’ β =
(Baseβ(mulGrpββfld)) |
52 | 37, 51 | mhmf 18614 |
. . . . . . 7
β’ (π β ((mulGrpβπ) MndHom
(mulGrpββfld)) β π:π΅βΆβ) |
53 | 32, 52 | syl 17 |
. . . . . 6
β’ ((π β§ π΄ β π) β π:π΅βΆβ) |
54 | 53, 35 | ffvelcdmd 7041 |
. . . . 5
β’ ((π β§ π΄ β π) β (πβ((invrβπ)βπ΄)) β β) |
55 | 54 | mul02d 11360 |
. . . 4
β’ ((π β§ π΄ β π) β (0 Β· (πβ((invrβπ)βπ΄))) = 0) |
56 | 20, 49, 55 | 3netr4d 3022 |
. . 3
β’ ((π β§ π΄ β π) β ((πβπ΄) Β· (πβ((invrβπ)βπ΄))) β (0 Β· (πβ((invrβπ)βπ΄)))) |
57 | | oveq1 7369 |
. . . 4
β’ ((πβπ΄) = 0 β ((πβπ΄) Β· (πβ((invrβπ)βπ΄))) = (0 Β· (πβ((invrβπ)βπ΄)))) |
58 | 57 | necon3i 2977 |
. . 3
β’ (((πβπ΄) Β· (πβ((invrβπ)βπ΄))) β (0 Β· (πβ((invrβπ)βπ΄))) β (πβπ΄) β 0) |
59 | 56, 58 | syl 17 |
. 2
β’ ((π β§ π΄ β π) β (πβπ΄) β 0) |
60 | 18, 59 | impbida 800 |
1
β’ (π β ((πβπ΄) β 0 β π΄ β π)) |