Step | Hyp | Ref
| Expression |
1 | | dchrinvcl.n |
. . 3
β’ πΎ = (π β π΅ β¦ if(π β π, (1 / (πβπ)), 0)) |
2 | | dchrmhm.g |
. . . 4
β’ πΊ = (DChrβπ) |
3 | | dchrmhm.z |
. . . 4
β’ π =
(β€/nβ€βπ) |
4 | | dchrn0.b |
. . . 4
β’ π΅ = (Baseβπ) |
5 | | dchrn0.u |
. . . 4
β’ π = (Unitβπ) |
6 | | dchrmulid2.x |
. . . . 5
β’ (π β π β π·) |
7 | | dchrmhm.b |
. . . . . 6
β’ π· = (BaseβπΊ) |
8 | 2, 7 | dchrrcl 26604 |
. . . . 5
β’ (π β π· β π β β) |
9 | 6, 8 | syl 17 |
. . . 4
β’ (π β π β β) |
10 | | fveq2 6847 |
. . . . 5
β’ (π = π₯ β (πβπ) = (πβπ₯)) |
11 | 10 | oveq2d 7378 |
. . . 4
β’ (π = π₯ β (1 / (πβπ)) = (1 / (πβπ₯))) |
12 | | fveq2 6847 |
. . . . 5
β’ (π = π¦ β (πβπ) = (πβπ¦)) |
13 | 12 | oveq2d 7378 |
. . . 4
β’ (π = π¦ β (1 / (πβπ)) = (1 / (πβπ¦))) |
14 | | fveq2 6847 |
. . . . 5
β’ (π = (π₯(.rβπ)π¦) β (πβπ) = (πβ(π₯(.rβπ)π¦))) |
15 | 14 | oveq2d 7378 |
. . . 4
β’ (π = (π₯(.rβπ)π¦) β (1 / (πβπ)) = (1 / (πβ(π₯(.rβπ)π¦)))) |
16 | | fveq2 6847 |
. . . . 5
β’ (π = (1rβπ) β (πβπ) = (πβ(1rβπ))) |
17 | 16 | oveq2d 7378 |
. . . 4
β’ (π = (1rβπ) β (1 / (πβπ)) = (1 / (πβ(1rβπ)))) |
18 | 2, 3, 7, 4, 6 | dchrf 26606 |
. . . . . 6
β’ (π β π:π΅βΆβ) |
19 | 4, 5 | unitss 20096 |
. . . . . . 7
β’ π β π΅ |
20 | 19 | sseli 3945 |
. . . . . 6
β’ (π β π β π β π΅) |
21 | | ffvelcdm 7037 |
. . . . . 6
β’ ((π:π΅βΆβ β§ π β π΅) β (πβπ) β β) |
22 | 18, 20, 21 | syl2an 597 |
. . . . 5
β’ ((π β§ π β π) β (πβπ) β β) |
23 | | simpr 486 |
. . . . . 6
β’ ((π β§ π β π) β π β π) |
24 | 6 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β π) β π β π·) |
25 | 20 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β π) β π β π΅) |
26 | 2, 3, 7, 4, 5, 24,
25 | dchrn0 26614 |
. . . . . 6
β’ ((π β§ π β π) β ((πβπ) β 0 β π β π)) |
27 | 23, 26 | mpbird 257 |
. . . . 5
β’ ((π β§ π β π) β (πβπ) β 0) |
28 | 22, 27 | reccld 11931 |
. . . 4
β’ ((π β§ π β π) β (1 / (πβπ)) β β) |
29 | | 1t1e1 12322 |
. . . . . . . 8
β’ (1
Β· 1) = 1 |
30 | 29 | eqcomi 2746 |
. . . . . . 7
β’ 1 = (1
Β· 1) |
31 | 30 | a1i 11 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π¦ β π)) β 1 = (1 Β·
1)) |
32 | 2, 3, 7 | dchrmhm 26605 |
. . . . . . . 8
β’ π· β ((mulGrpβπ) MndHom
(mulGrpββfld)) |
33 | 6 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π₯ β π β§ π¦ β π)) β π β π·) |
34 | 32, 33 | sselid 3947 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π)) β π β ((mulGrpβπ) MndHom
(mulGrpββfld))) |
35 | | simprl 770 |
. . . . . . . 8
β’ ((π β§ (π₯ β π β§ π¦ β π)) β π₯ β π) |
36 | 19, 35 | sselid 3947 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π)) β π₯ β π΅) |
37 | | simprr 772 |
. . . . . . . 8
β’ ((π β§ (π₯ β π β§ π¦ β π)) β π¦ β π) |
38 | 19, 37 | sselid 3947 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π)) β π¦ β π΅) |
39 | | eqid 2737 |
. . . . . . . . 9
β’
(mulGrpβπ) =
(mulGrpβπ) |
40 | 39, 4 | mgpbas 19909 |
. . . . . . . 8
β’ π΅ =
(Baseβ(mulGrpβπ)) |
41 | | eqid 2737 |
. . . . . . . . 9
β’
(.rβπ) = (.rβπ) |
42 | 39, 41 | mgpplusg 19907 |
. . . . . . . 8
β’
(.rβπ) = (+gβ(mulGrpβπ)) |
43 | | eqid 2737 |
. . . . . . . . 9
β’
(mulGrpββfld) =
(mulGrpββfld) |
44 | | cnfldmul 20818 |
. . . . . . . . 9
β’ Β·
= (.rββfld) |
45 | 43, 44 | mgpplusg 19907 |
. . . . . . . 8
β’ Β·
= (+gβ(mulGrpββfld)) |
46 | 40, 42, 45 | mhmlin 18616 |
. . . . . . 7
β’ ((π β ((mulGrpβπ) MndHom
(mulGrpββfld)) β§ π₯ β π΅ β§ π¦ β π΅) β (πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦))) |
47 | 34, 36, 38, 46 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦))) |
48 | 31, 47 | oveq12d 7380 |
. . . . 5
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (1 / (πβ(π₯(.rβπ)π¦))) = ((1 Β· 1) / ((πβπ₯) Β· (πβπ¦)))) |
49 | | 1cnd 11157 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π¦ β π)) β 1 β β) |
50 | 18 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π)) β π:π΅βΆβ) |
51 | 50, 36 | ffvelcdmd 7041 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (πβπ₯) β β) |
52 | 50, 38 | ffvelcdmd 7041 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (πβπ¦) β β) |
53 | 2, 3, 7, 4, 5, 33,
36 | dchrn0 26614 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π)) β ((πβπ₯) β 0 β π₯ β π)) |
54 | 35, 53 | mpbird 257 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (πβπ₯) β 0) |
55 | 2, 3, 7, 4, 5, 33,
38 | dchrn0 26614 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π)) β ((πβπ¦) β 0 β π¦ β π)) |
56 | 37, 55 | mpbird 257 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (πβπ¦) β 0) |
57 | 49, 51, 49, 52, 54, 56 | divmuldivd 11979 |
. . . . 5
β’ ((π β§ (π₯ β π β§ π¦ β π)) β ((1 / (πβπ₯)) Β· (1 / (πβπ¦))) = ((1 Β· 1) / ((πβπ₯) Β· (πβπ¦)))) |
58 | 48, 57 | eqtr4d 2780 |
. . . 4
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (1 / (πβ(π₯(.rβπ)π¦))) = ((1 / (πβπ₯)) Β· (1 / (πβπ¦)))) |
59 | 32, 6 | sselid 3947 |
. . . . . . 7
β’ (π β π β ((mulGrpβπ) MndHom
(mulGrpββfld))) |
60 | | eqid 2737 |
. . . . . . . . 9
β’
(1rβπ) = (1rβπ) |
61 | 39, 60 | ringidval 19922 |
. . . . . . . 8
β’
(1rβπ) = (0gβ(mulGrpβπ)) |
62 | | cnfld1 20838 |
. . . . . . . . 9
β’ 1 =
(1rββfld) |
63 | 43, 62 | ringidval 19922 |
. . . . . . . 8
β’ 1 =
(0gβ(mulGrpββfld)) |
64 | 61, 63 | mhm0 18617 |
. . . . . . 7
β’ (π β ((mulGrpβπ) MndHom
(mulGrpββfld)) β (πβ(1rβπ)) = 1) |
65 | 59, 64 | syl 17 |
. . . . . 6
β’ (π β (πβ(1rβπ)) = 1) |
66 | 65 | oveq2d 7378 |
. . . . 5
β’ (π β (1 / (πβ(1rβπ))) = (1 / 1)) |
67 | | 1div1e1 11852 |
. . . . 5
β’ (1 / 1) =
1 |
68 | 66, 67 | eqtrdi 2793 |
. . . 4
β’ (π β (1 / (πβ(1rβπ))) = 1) |
69 | 2, 3, 4, 5, 9, 7, 11, 13, 15, 17, 28, 58, 68 | dchrelbasd 26603 |
. . 3
β’ (π β (π β π΅ β¦ if(π β π, (1 / (πβπ)), 0)) β π·) |
70 | 1, 69 | eqeltrid 2842 |
. 2
β’ (π β πΎ β π·) |
71 | | dchrmulid2.t |
. . . 4
β’ Β· =
(+gβπΊ) |
72 | 2, 3, 7, 71, 70, 6 | dchrmul 26612 |
. . 3
β’ (π β (πΎ Β· π) = (πΎ βf Β· π)) |
73 | 4 | fvexi 6861 |
. . . . . 6
β’ π΅ β V |
74 | 73 | a1i 11 |
. . . . 5
β’ (π β π΅ β V) |
75 | | ovex 7395 |
. . . . . . 7
β’ (1 /
(πβπ)) β V |
76 | | c0ex 11156 |
. . . . . . 7
β’ 0 β
V |
77 | 75, 76 | ifex 4541 |
. . . . . 6
β’ if(π β π, (1 / (πβπ)), 0) β V |
78 | 77 | a1i 11 |
. . . . 5
β’ ((π β§ π β π΅) β if(π β π, (1 / (πβπ)), 0) β V) |
79 | 18 | ffvelcdmda 7040 |
. . . . 5
β’ ((π β§ π β π΅) β (πβπ) β β) |
80 | 1 | a1i 11 |
. . . . 5
β’ (π β πΎ = (π β π΅ β¦ if(π β π, (1 / (πβπ)), 0))) |
81 | 18 | feqmptd 6915 |
. . . . 5
β’ (π β π = (π β π΅ β¦ (πβπ))) |
82 | 74, 78, 79, 80, 81 | offval2 7642 |
. . . 4
β’ (π β (πΎ βf Β· π) = (π β π΅ β¦ (if(π β π, (1 / (πβπ)), 0) Β· (πβπ)))) |
83 | | dchr1cl.o |
. . . . 5
β’ 1 = (π β π΅ β¦ if(π β π, 1, 0)) |
84 | | ovif 7459 |
. . . . . . 7
β’ (if(π β π, (1 / (πβπ)), 0) Β· (πβπ)) = if(π β π, ((1 / (πβπ)) Β· (πβπ)), (0 Β· (πβπ))) |
85 | 79 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β π΅) β§ π β π) β (πβπ) β β) |
86 | 6 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΅) β π β π·) |
87 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΅) β π β π΅) |
88 | 2, 3, 7, 4, 5, 86,
87 | dchrn0 26614 |
. . . . . . . . . . 11
β’ ((π β§ π β π΅) β ((πβπ) β 0 β π β π)) |
89 | 88 | biimpar 479 |
. . . . . . . . . 10
β’ (((π β§ π β π΅) β§ π β π) β (πβπ) β 0) |
90 | 85, 89 | recid2d 11934 |
. . . . . . . . 9
β’ (((π β§ π β π΅) β§ π β π) β ((1 / (πβπ)) Β· (πβπ)) = 1) |
91 | 90 | ifeq1da 4522 |
. . . . . . . 8
β’ ((π β§ π β π΅) β if(π β π, ((1 / (πβπ)) Β· (πβπ)), (0 Β· (πβπ))) = if(π β π, 1, (0 Β· (πβπ)))) |
92 | 79 | mul02d 11360 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β (0 Β· (πβπ)) = 0) |
93 | 92 | ifeq2d 4511 |
. . . . . . . 8
β’ ((π β§ π β π΅) β if(π β π, 1, (0 Β· (πβπ))) = if(π β π, 1, 0)) |
94 | 91, 93 | eqtrd 2777 |
. . . . . . 7
β’ ((π β§ π β π΅) β if(π β π, ((1 / (πβπ)) Β· (πβπ)), (0 Β· (πβπ))) = if(π β π, 1, 0)) |
95 | 84, 94 | eqtrid 2789 |
. . . . . 6
β’ ((π β§ π β π΅) β (if(π β π, (1 / (πβπ)), 0) Β· (πβπ)) = if(π β π, 1, 0)) |
96 | 95 | mpteq2dva 5210 |
. . . . 5
β’ (π β (π β π΅ β¦ (if(π β π, (1 / (πβπ)), 0) Β· (πβπ))) = (π β π΅ β¦ if(π β π, 1, 0))) |
97 | 83, 96 | eqtr4id 2796 |
. . . 4
β’ (π β 1 = (π β π΅ β¦ (if(π β π, (1 / (πβπ)), 0) Β· (πβπ)))) |
98 | 82, 97 | eqtr4d 2780 |
. . 3
β’ (π β (πΎ βf Β· π) = 1 ) |
99 | 72, 98 | eqtrd 2777 |
. 2
β’ (π β (πΎ Β· π) = 1 ) |
100 | 70, 99 | jca 513 |
1
β’ (π β (πΎ β π· β§ (πΎ Β· π) = 1 )) |