Step | Hyp | Ref
| Expression |
1 | | dchrmhm.g |
. . 3
β’ πΊ = (DChrβπ) |
2 | | dchrmhm.z |
. . 3
β’ π =
(β€/nβ€βπ) |
3 | | dchrmhm.b |
. . 3
β’ π· = (BaseβπΊ) |
4 | | dchrmul.t |
. . 3
β’ Β· =
(+gβπΊ) |
5 | | dchrmul.x |
. . 3
β’ (π β π β π·) |
6 | | dchrmul.y |
. . 3
β’ (π β π β π·) |
7 | 1, 2, 3, 4, 5, 6 | dchrmul 26612 |
. 2
β’ (π β (π Β· π) = (π βf Β· π)) |
8 | | mulcl 11142 |
. . . . 5
β’ ((π₯ β β β§ π¦ β β) β (π₯ Β· π¦) β β) |
9 | 8 | adantl 483 |
. . . 4
β’ ((π β§ (π₯ β β β§ π¦ β β)) β (π₯ Β· π¦) β β) |
10 | | eqid 2737 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
11 | 1, 2, 3, 10, 5 | dchrf 26606 |
. . . 4
β’ (π β π:(Baseβπ)βΆβ) |
12 | 1, 2, 3, 10, 6 | dchrf 26606 |
. . . 4
β’ (π β π:(Baseβπ)βΆβ) |
13 | | fvexd 6862 |
. . . 4
β’ (π β (Baseβπ) β V) |
14 | | inidm 4183 |
. . . 4
β’
((Baseβπ)
β© (Baseβπ)) =
(Baseβπ) |
15 | 9, 11, 12, 13, 13, 14 | off 7640 |
. . 3
β’ (π β (π βf Β· π):(Baseβπ)βΆβ) |
16 | | eqid 2737 |
. . . . . . . 8
β’
(Unitβπ) =
(Unitβπ) |
17 | 10, 16 | unitcl 20095 |
. . . . . . 7
β’ (π₯ β (Unitβπ) β π₯ β (Baseβπ)) |
18 | 10, 16 | unitcl 20095 |
. . . . . . 7
β’ (π¦ β (Unitβπ) β π¦ β (Baseβπ)) |
19 | 17, 18 | anim12i 614 |
. . . . . 6
β’ ((π₯ β (Unitβπ) β§ π¦ β (Unitβπ)) β (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) |
20 | 1, 3 | dchrrcl 26604 |
. . . . . . . . . . . . . 14
β’ (π β π· β π β β) |
21 | 5, 20 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
22 | 1, 2, 10, 16, 21, 3 | dchrelbas2 26601 |
. . . . . . . . . . . 12
β’ (π β (π β π· β (π β ((mulGrpβπ) MndHom
(mulGrpββfld)) β§ βπ₯ β (Baseβπ)((πβπ₯) β 0 β π₯ β (Unitβπ))))) |
23 | 5, 22 | mpbid 231 |
. . . . . . . . . . 11
β’ (π β (π β ((mulGrpβπ) MndHom
(mulGrpββfld)) β§ βπ₯ β (Baseβπ)((πβπ₯) β 0 β π₯ β (Unitβπ)))) |
24 | 23 | simpld 496 |
. . . . . . . . . 10
β’ (π β π β ((mulGrpβπ) MndHom
(mulGrpββfld))) |
25 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(mulGrpβπ) =
(mulGrpβπ) |
26 | 25, 10 | mgpbas 19909 |
. . . . . . . . . . . 12
β’
(Baseβπ) =
(Baseβ(mulGrpβπ)) |
27 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(.rβπ) = (.rβπ) |
28 | 25, 27 | mgpplusg 19907 |
. . . . . . . . . . . 12
β’
(.rβπ) = (+gβ(mulGrpβπ)) |
29 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(mulGrpββfld) =
(mulGrpββfld) |
30 | | cnfldmul 20818 |
. . . . . . . . . . . . 13
β’ Β·
= (.rββfld) |
31 | 29, 30 | mgpplusg 19907 |
. . . . . . . . . . . 12
β’ Β·
= (+gβ(mulGrpββfld)) |
32 | 26, 28, 31 | mhmlin 18616 |
. . . . . . . . . . 11
β’ ((π β ((mulGrpβπ) MndHom
(mulGrpββfld)) β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦))) |
33 | 32 | 3expb 1121 |
. . . . . . . . . 10
β’ ((π β ((mulGrpβπ) MndHom
(mulGrpββfld)) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β (πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦))) |
34 | 24, 33 | sylan 581 |
. . . . . . . . 9
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β (πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦))) |
35 | 1, 2, 10, 16, 21, 3 | dchrelbas2 26601 |
. . . . . . . . . . . 12
β’ (π β (π β π· β (π β ((mulGrpβπ) MndHom
(mulGrpββfld)) β§ βπ₯ β (Baseβπ)((πβπ₯) β 0 β π₯ β (Unitβπ))))) |
36 | 6, 35 | mpbid 231 |
. . . . . . . . . . 11
β’ (π β (π β ((mulGrpβπ) MndHom
(mulGrpββfld)) β§ βπ₯ β (Baseβπ)((πβπ₯) β 0 β π₯ β (Unitβπ)))) |
37 | 36 | simpld 496 |
. . . . . . . . . 10
β’ (π β π β ((mulGrpβπ) MndHom
(mulGrpββfld))) |
38 | 26, 28, 31 | mhmlin 18616 |
. . . . . . . . . . 11
β’ ((π β ((mulGrpβπ) MndHom
(mulGrpββfld)) β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦))) |
39 | 38 | 3expb 1121 |
. . . . . . . . . 10
β’ ((π β ((mulGrpβπ) MndHom
(mulGrpββfld)) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β (πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦))) |
40 | 37, 39 | sylan 581 |
. . . . . . . . 9
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β (πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦))) |
41 | 34, 40 | oveq12d 7380 |
. . . . . . . 8
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β ((πβ(π₯(.rβπ)π¦)) Β· (πβ(π₯(.rβπ)π¦))) = (((πβπ₯) Β· (πβπ¦)) Β· ((πβπ₯) Β· (πβπ¦)))) |
42 | 11 | ffvelcdmda 7040 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (Baseβπ)) β (πβπ₯) β β) |
43 | 42 | adantrr 716 |
. . . . . . . . 9
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β (πβπ₯) β β) |
44 | | simpr 486 |
. . . . . . . . . 10
β’ ((π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β π¦ β (Baseβπ)) |
45 | | ffvelcdm 7037 |
. . . . . . . . . 10
β’ ((π:(Baseβπ)βΆβ β§ π¦ β (Baseβπ)) β (πβπ¦) β β) |
46 | 11, 44, 45 | syl2an 597 |
. . . . . . . . 9
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β (πβπ¦) β β) |
47 | 12 | ffvelcdmda 7040 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (Baseβπ)) β (πβπ₯) β β) |
48 | 47 | adantrr 716 |
. . . . . . . . 9
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β (πβπ₯) β β) |
49 | | ffvelcdm 7037 |
. . . . . . . . . 10
β’ ((π:(Baseβπ)βΆβ β§ π¦ β (Baseβπ)) β (πβπ¦) β β) |
50 | 12, 44, 49 | syl2an 597 |
. . . . . . . . 9
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β (πβπ¦) β β) |
51 | 43, 46, 48, 50 | mul4d 11374 |
. . . . . . . 8
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β (((πβπ₯) Β· (πβπ¦)) Β· ((πβπ₯) Β· (πβπ¦))) = (((πβπ₯) Β· (πβπ₯)) Β· ((πβπ¦) Β· (πβπ¦)))) |
52 | 41, 51 | eqtrd 2777 |
. . . . . . 7
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β ((πβ(π₯(.rβπ)π¦)) Β· (πβ(π₯(.rβπ)π¦))) = (((πβπ₯) Β· (πβπ₯)) Β· ((πβπ¦) Β· (πβπ¦)))) |
53 | 11 | ffnd 6674 |
. . . . . . . . 9
β’ (π β π Fn (Baseβπ)) |
54 | 53 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β π Fn (Baseβπ)) |
55 | 12 | ffnd 6674 |
. . . . . . . . 9
β’ (π β π Fn (Baseβπ)) |
56 | 55 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β π Fn (Baseβπ)) |
57 | | fvexd 6862 |
. . . . . . . 8
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β (Baseβπ) β V) |
58 | 21 | nnnn0d 12480 |
. . . . . . . . . 10
β’ (π β π β
β0) |
59 | 2 | zncrng 20967 |
. . . . . . . . . 10
β’ (π β β0
β π β
CRing) |
60 | | crngring 19983 |
. . . . . . . . . 10
β’ (π β CRing β π β Ring) |
61 | 58, 59, 60 | 3syl 18 |
. . . . . . . . 9
β’ (π β π β Ring) |
62 | 10, 27 | ringcl 19988 |
. . . . . . . . . 10
β’ ((π β Ring β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (π₯(.rβπ)π¦) β (Baseβπ)) |
63 | 62 | 3expb 1121 |
. . . . . . . . 9
β’ ((π β Ring β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β (π₯(.rβπ)π¦) β (Baseβπ)) |
64 | 61, 63 | sylan 581 |
. . . . . . . 8
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β (π₯(.rβπ)π¦) β (Baseβπ)) |
65 | | fnfvof 7639 |
. . . . . . . 8
β’ (((π Fn (Baseβπ) β§ π Fn (Baseβπ)) β§ ((Baseβπ) β V β§ (π₯(.rβπ)π¦) β (Baseβπ))) β ((π βf Β· π)β(π₯(.rβπ)π¦)) = ((πβ(π₯(.rβπ)π¦)) Β· (πβ(π₯(.rβπ)π¦)))) |
66 | 54, 56, 57, 64, 65 | syl22anc 838 |
. . . . . . 7
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β ((π βf Β· π)β(π₯(.rβπ)π¦)) = ((πβ(π₯(.rβπ)π¦)) Β· (πβ(π₯(.rβπ)π¦)))) |
67 | 53 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (Baseβπ)) β π Fn (Baseβπ)) |
68 | 55 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (Baseβπ)) β π Fn (Baseβπ)) |
69 | | fvexd 6862 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (Baseβπ)) β (Baseβπ) β V) |
70 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (Baseβπ)) β π₯ β (Baseβπ)) |
71 | | fnfvof 7639 |
. . . . . . . . . 10
β’ (((π Fn (Baseβπ) β§ π Fn (Baseβπ)) β§ ((Baseβπ) β V β§ π₯ β (Baseβπ))) β ((π βf Β· π)βπ₯) = ((πβπ₯) Β· (πβπ₯))) |
72 | 67, 68, 69, 70, 71 | syl22anc 838 |
. . . . . . . . 9
β’ ((π β§ π₯ β (Baseβπ)) β ((π βf Β· π)βπ₯) = ((πβπ₯) Β· (πβπ₯))) |
73 | 72 | adantrr 716 |
. . . . . . . 8
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β ((π βf Β· π)βπ₯) = ((πβπ₯) Β· (πβπ₯))) |
74 | | simprr 772 |
. . . . . . . . 9
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β π¦ β (Baseβπ)) |
75 | | fnfvof 7639 |
. . . . . . . . 9
β’ (((π Fn (Baseβπ) β§ π Fn (Baseβπ)) β§ ((Baseβπ) β V β§ π¦ β (Baseβπ))) β ((π βf Β· π)βπ¦) = ((πβπ¦) Β· (πβπ¦))) |
76 | 54, 56, 57, 74, 75 | syl22anc 838 |
. . . . . . . 8
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β ((π βf Β· π)βπ¦) = ((πβπ¦) Β· (πβπ¦))) |
77 | 73, 76 | oveq12d 7380 |
. . . . . . 7
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β (((π βf Β· π)βπ₯) Β· ((π βf Β· π)βπ¦)) = (((πβπ₯) Β· (πβπ₯)) Β· ((πβπ¦) Β· (πβπ¦)))) |
78 | 52, 66, 77 | 3eqtr4d 2787 |
. . . . . 6
β’ ((π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β ((π βf Β· π)β(π₯(.rβπ)π¦)) = (((π βf Β· π)βπ₯) Β· ((π βf Β· π)βπ¦))) |
79 | 19, 78 | sylan2 594 |
. . . . 5
β’ ((π β§ (π₯ β (Unitβπ) β§ π¦ β (Unitβπ))) β ((π βf Β· π)β(π₯(.rβπ)π¦)) = (((π βf Β· π)βπ₯) Β· ((π βf Β· π)βπ¦))) |
80 | 79 | ralrimivva 3198 |
. . . 4
β’ (π β βπ₯ β (Unitβπ)βπ¦ β (Unitβπ)((π βf Β· π)β(π₯(.rβπ)π¦)) = (((π βf Β· π)βπ₯) Β· ((π βf Β· π)βπ¦))) |
81 | | eqid 2737 |
. . . . . . . 8
β’
(1rβπ) = (1rβπ) |
82 | 10, 81 | ringidcl 19996 |
. . . . . . 7
β’ (π β Ring β
(1rβπ)
β (Baseβπ)) |
83 | 61, 82 | syl 17 |
. . . . . 6
β’ (π β (1rβπ) β (Baseβπ)) |
84 | | fnfvof 7639 |
. . . . . 6
β’ (((π Fn (Baseβπ) β§ π Fn (Baseβπ)) β§ ((Baseβπ) β V β§ (1rβπ) β (Baseβπ))) β ((π βf Β· π)β(1rβπ)) = ((πβ(1rβπ)) Β· (πβ(1rβπ)))) |
85 | 53, 55, 13, 83, 84 | syl22anc 838 |
. . . . 5
β’ (π β ((π βf Β· π)β(1rβπ)) = ((πβ(1rβπ)) Β· (πβ(1rβπ)))) |
86 | 25, 81 | ringidval 19922 |
. . . . . . . . 9
β’
(1rβπ) = (0gβ(mulGrpβπ)) |
87 | | cnfld1 20838 |
. . . . . . . . . 10
β’ 1 =
(1rββfld) |
88 | 29, 87 | ringidval 19922 |
. . . . . . . . 9
β’ 1 =
(0gβ(mulGrpββfld)) |
89 | 86, 88 | mhm0 18617 |
. . . . . . . 8
β’ (π β ((mulGrpβπ) MndHom
(mulGrpββfld)) β (πβ(1rβπ)) = 1) |
90 | 24, 89 | syl 17 |
. . . . . . 7
β’ (π β (πβ(1rβπ)) = 1) |
91 | 86, 88 | mhm0 18617 |
. . . . . . . 8
β’ (π β ((mulGrpβπ) MndHom
(mulGrpββfld)) β (πβ(1rβπ)) = 1) |
92 | 37, 91 | syl 17 |
. . . . . . 7
β’ (π β (πβ(1rβπ)) = 1) |
93 | 90, 92 | oveq12d 7380 |
. . . . . 6
β’ (π β ((πβ(1rβπ)) Β· (πβ(1rβπ))) = (1 Β·
1)) |
94 | | 1t1e1 12322 |
. . . . . 6
β’ (1
Β· 1) = 1 |
95 | 93, 94 | eqtrdi 2793 |
. . . . 5
β’ (π β ((πβ(1rβπ)) Β· (πβ(1rβπ))) = 1) |
96 | 85, 95 | eqtrd 2777 |
. . . 4
β’ (π β ((π βf Β· π)β(1rβπ)) = 1) |
97 | 72 | neeq1d 3004 |
. . . . . . 7
β’ ((π β§ π₯ β (Baseβπ)) β (((π βf Β· π)βπ₯) β 0 β ((πβπ₯) Β· (πβπ₯)) β 0)) |
98 | 42, 47 | mulne0bd 11813 |
. . . . . . 7
β’ ((π β§ π₯ β (Baseβπ)) β (((πβπ₯) β 0 β§ (πβπ₯) β 0) β ((πβπ₯) Β· (πβπ₯)) β 0)) |
99 | 97, 98 | bitr4d 282 |
. . . . . 6
β’ ((π β§ π₯ β (Baseβπ)) β (((π βf Β· π)βπ₯) β 0 β ((πβπ₯) β 0 β§ (πβπ₯) β 0))) |
100 | 23 | simprd 497 |
. . . . . . . 8
β’ (π β βπ₯ β (Baseβπ)((πβπ₯) β 0 β π₯ β (Unitβπ))) |
101 | 100 | r19.21bi 3237 |
. . . . . . 7
β’ ((π β§ π₯ β (Baseβπ)) β ((πβπ₯) β 0 β π₯ β (Unitβπ))) |
102 | 101 | adantrd 493 |
. . . . . 6
β’ ((π β§ π₯ β (Baseβπ)) β (((πβπ₯) β 0 β§ (πβπ₯) β 0) β π₯ β (Unitβπ))) |
103 | 99, 102 | sylbid 239 |
. . . . 5
β’ ((π β§ π₯ β (Baseβπ)) β (((π βf Β· π)βπ₯) β 0 β π₯ β (Unitβπ))) |
104 | 103 | ralrimiva 3144 |
. . . 4
β’ (π β βπ₯ β (Baseβπ)(((π βf Β· π)βπ₯) β 0 β π₯ β (Unitβπ))) |
105 | 80, 96, 104 | 3jca 1129 |
. . 3
β’ (π β (βπ₯ β (Unitβπ)βπ¦ β (Unitβπ)((π βf Β· π)β(π₯(.rβπ)π¦)) = (((π βf Β· π)βπ₯) Β· ((π βf Β· π)βπ¦)) β§ ((π βf Β· π)β(1rβπ)) = 1 β§ βπ₯ β (Baseβπ)(((π βf Β· π)βπ₯) β 0 β π₯ β (Unitβπ)))) |
106 | 1, 2, 10, 16, 21, 3 | dchrelbas3 26602 |
. . 3
β’ (π β ((π βf Β· π) β π· β ((π βf Β· π):(Baseβπ)βΆβ β§ (βπ₯ β (Unitβπ)βπ¦ β (Unitβπ)((π βf Β· π)β(π₯(.rβπ)π¦)) = (((π βf Β· π)βπ₯) Β· ((π βf Β· π)βπ¦)) β§ ((π βf Β· π)β(1rβπ)) = 1 β§ βπ₯ β (Baseβπ)(((π βf Β· π)βπ₯) β 0 β π₯ β (Unitβπ)))))) |
107 | 15, 105, 106 | mpbir2and 712 |
. 2
β’ (π β (π βf Β· π) β π·) |
108 | 7, 107 | eqeltrd 2838 |
1
β’ (π β (π Β· π) β π·) |