Step | Hyp | Ref
| Expression |
1 | | idomodle.b |
. . . . 5
β’ π΅ = (BaseβπΊ) |
2 | 1 | fvexi 6857 |
. . . 4
β’ π΅ β V |
3 | 2 | rabex 5290 |
. . 3
β’ {π₯ β π΅ β£ (πβπ₯) β₯ π} β V |
4 | | hashxrcl 14263 |
. . 3
β’ ({π₯ β π΅ β£ (πβπ₯) β₯ π} β V β (β―β{π₯ β π΅ β£ (πβπ₯) β₯ π}) β
β*) |
5 | 3, 4 | mp1i 13 |
. 2
β’ ((π
β IDomn β§ π β β) β
(β―β{π₯ β
π΅ β£ (πβπ₯) β₯ π}) β
β*) |
6 | | fvex 6856 |
. . . 4
β’
(Baseβπ
)
β V |
7 | 6 | rabex 5290 |
. . 3
β’ {π₯ β (Baseβπ
) β£ (π(.gβ(mulGrpβπ
))π₯) = (1rβπ
)} β V |
8 | | hashxrcl 14263 |
. . 3
β’ ({π₯ β (Baseβπ
) β£ (π(.gβ(mulGrpβπ
))π₯) = (1rβπ
)} β V β (β―β{π₯ β (Baseβπ
) β£ (π(.gβ(mulGrpβπ
))π₯) = (1rβπ
)}) β
β*) |
9 | 7, 8 | mp1i 13 |
. 2
β’ ((π
β IDomn β§ π β β) β
(β―β{π₯ β
(Baseβπ
) β£
(π(.gβ(mulGrpβπ
))π₯) = (1rβπ
)}) β
β*) |
10 | | nnre 12165 |
. . . 4
β’ (π β β β π β
β) |
11 | 10 | rexrd 11210 |
. . 3
β’ (π β β β π β
β*) |
12 | 11 | adantl 483 |
. 2
β’ ((π
β IDomn β§ π β β) β π β
β*) |
13 | | isidom 20790 |
. . . . . . . . . . . 12
β’ (π
β IDomn β (π
β CRing β§ π
β Domn)) |
14 | 13 | simplbi 499 |
. . . . . . . . . . 11
β’ (π
β IDomn β π
β CRing) |
15 | 14 | adantr 482 |
. . . . . . . . . 10
β’ ((π
β IDomn β§ π β β) β π
β CRing) |
16 | | crngring 19981 |
. . . . . . . . . 10
β’ (π
β CRing β π
β Ring) |
17 | 15, 16 | syl 17 |
. . . . . . . . 9
β’ ((π
β IDomn β§ π β β) β π
β Ring) |
18 | 17 | adantr 482 |
. . . . . . . 8
β’ (((π
β IDomn β§ π β β) β§ π₯ β π΅) β π
β Ring) |
19 | | eqid 2733 |
. . . . . . . . 9
β’
(Unitβπ
) =
(Unitβπ
) |
20 | | idomodle.g |
. . . . . . . . 9
β’ πΊ = ((mulGrpβπ
) βΎs
(Unitβπ
)) |
21 | 19, 20 | unitgrp 20101 |
. . . . . . . 8
β’ (π
β Ring β πΊ β Grp) |
22 | 18, 21 | syl 17 |
. . . . . . 7
β’ (((π
β IDomn β§ π β β) β§ π₯ β π΅) β πΊ β Grp) |
23 | | simpr 486 |
. . . . . . 7
β’ (((π
β IDomn β§ π β β) β§ π₯ β π΅) β π₯ β π΅) |
24 | | nnz 12525 |
. . . . . . . 8
β’ (π β β β π β
β€) |
25 | 24 | ad2antlr 726 |
. . . . . . 7
β’ (((π
β IDomn β§ π β β) β§ π₯ β π΅) β π β β€) |
26 | | idomodle.o |
. . . . . . . 8
β’ π = (odβπΊ) |
27 | | eqid 2733 |
. . . . . . . 8
β’
(.gβπΊ) = (.gβπΊ) |
28 | | eqid 2733 |
. . . . . . . 8
β’
(0gβπΊ) = (0gβπΊ) |
29 | 1, 26, 27, 28 | oddvds 19334 |
. . . . . . 7
β’ ((πΊ β Grp β§ π₯ β π΅ β§ π β β€) β ((πβπ₯) β₯ π β (π(.gβπΊ)π₯) = (0gβπΊ))) |
30 | 22, 23, 25, 29 | syl3anc 1372 |
. . . . . 6
β’ (((π
β IDomn β§ π β β) β§ π₯ β π΅) β ((πβπ₯) β₯ π β (π(.gβπΊ)π₯) = (0gβπΊ))) |
31 | | eqid 2733 |
. . . . . . . . . 10
β’
(mulGrpβπ
) =
(mulGrpβπ
) |
32 | 19, 31 | unitsubm 20104 |
. . . . . . . . 9
β’ (π
β Ring β
(Unitβπ
) β
(SubMndβ(mulGrpβπ
))) |
33 | 18, 32 | syl 17 |
. . . . . . . 8
β’ (((π
β IDomn β§ π β β) β§ π₯ β π΅) β (Unitβπ
) β (SubMndβ(mulGrpβπ
))) |
34 | | nnnn0 12425 |
. . . . . . . . 9
β’ (π β β β π β
β0) |
35 | 34 | ad2antlr 726 |
. . . . . . . 8
β’ (((π
β IDomn β§ π β β) β§ π₯ β π΅) β π β
β0) |
36 | 19, 20 | unitgrpbas 20100 |
. . . . . . . . . 10
β’
(Unitβπ
) =
(BaseβπΊ) |
37 | 1, 36 | eqtr4i 2764 |
. . . . . . . . 9
β’ π΅ = (Unitβπ
) |
38 | 23, 37 | eleqtrdi 2844 |
. . . . . . . 8
β’ (((π
β IDomn β§ π β β) β§ π₯ β π΅) β π₯ β (Unitβπ
)) |
39 | | eqid 2733 |
. . . . . . . . 9
β’
(.gβ(mulGrpβπ
)) =
(.gβ(mulGrpβπ
)) |
40 | 39, 20, 27 | submmulg 18925 |
. . . . . . . 8
β’
(((Unitβπ
)
β (SubMndβ(mulGrpβπ
)) β§ π β β0 β§ π₯ β (Unitβπ
)) β (π(.gβ(mulGrpβπ
))π₯) = (π(.gβπΊ)π₯)) |
41 | 33, 35, 38, 40 | syl3anc 1372 |
. . . . . . 7
β’ (((π
β IDomn β§ π β β) β§ π₯ β π΅) β (π(.gβ(mulGrpβπ
))π₯) = (π(.gβπΊ)π₯)) |
42 | | eqid 2733 |
. . . . . . . . 9
β’
(1rβπ
) = (1rβπ
) |
43 | 19, 20, 42 | unitgrpid 20103 |
. . . . . . . 8
β’ (π
β Ring β
(1rβπ
) =
(0gβπΊ)) |
44 | 18, 43 | syl 17 |
. . . . . . 7
β’ (((π
β IDomn β§ π β β) β§ π₯ β π΅) β (1rβπ
) = (0gβπΊ)) |
45 | 41, 44 | eqeq12d 2749 |
. . . . . 6
β’ (((π
β IDomn β§ π β β) β§ π₯ β π΅) β ((π(.gβ(mulGrpβπ
))π₯) = (1rβπ
) β (π(.gβπΊ)π₯) = (0gβπΊ))) |
46 | 30, 45 | bitr4d 282 |
. . . . 5
β’ (((π
β IDomn β§ π β β) β§ π₯ β π΅) β ((πβπ₯) β₯ π β (π(.gβ(mulGrpβπ
))π₯) = (1rβπ
))) |
47 | 46 | rabbidva 3413 |
. . . 4
β’ ((π
β IDomn β§ π β β) β {π₯ β π΅ β£ (πβπ₯) β₯ π} = {π₯ β π΅ β£ (π(.gβ(mulGrpβπ
))π₯) = (1rβπ
)}) |
48 | 47 | fveq2d 6847 |
. . 3
β’ ((π
β IDomn β§ π β β) β
(β―β{π₯ β
π΅ β£ (πβπ₯) β₯ π}) = (β―β{π₯ β π΅ β£ (π(.gβ(mulGrpβπ
))π₯) = (1rβπ
)})) |
49 | | eqid 2733 |
. . . . . . 7
β’
(Baseβπ
) =
(Baseβπ
) |
50 | 49, 37 | unitss 20094 |
. . . . . 6
β’ π΅ β (Baseβπ
) |
51 | | rabss2 4036 |
. . . . . 6
β’ (π΅ β (Baseβπ
) β {π₯ β π΅ β£ (π(.gβ(mulGrpβπ
))π₯) = (1rβπ
)} β {π₯ β (Baseβπ
) β£ (π(.gβ(mulGrpβπ
))π₯) = (1rβπ
)}) |
52 | 50, 51 | mp1i 13 |
. . . . 5
β’ ((π
β IDomn β§ π β β) β {π₯ β π΅ β£ (π(.gβ(mulGrpβπ
))π₯) = (1rβπ
)} β {π₯ β (Baseβπ
) β£ (π(.gβ(mulGrpβπ
))π₯) = (1rβπ
)}) |
53 | | ssdomg 8943 |
. . . . 5
β’ ({π₯ β (Baseβπ
) β£ (π(.gβ(mulGrpβπ
))π₯) = (1rβπ
)} β V β ({π₯ β π΅ β£ (π(.gβ(mulGrpβπ
))π₯) = (1rβπ
)} β {π₯ β (Baseβπ
) β£ (π(.gβ(mulGrpβπ
))π₯) = (1rβπ
)} β {π₯ β π΅ β£ (π(.gβ(mulGrpβπ
))π₯) = (1rβπ
)} βΌ {π₯ β (Baseβπ
) β£ (π(.gβ(mulGrpβπ
))π₯) = (1rβπ
)})) |
54 | 7, 52, 53 | mpsyl 68 |
. . . 4
β’ ((π
β IDomn β§ π β β) β {π₯ β π΅ β£ (π(.gβ(mulGrpβπ
))π₯) = (1rβπ
)} βΌ {π₯ β (Baseβπ
) β£ (π(.gβ(mulGrpβπ
))π₯) = (1rβπ
)}) |
55 | | hashdomi 14286 |
. . . 4
β’ ({π₯ β π΅ β£ (π(.gβ(mulGrpβπ
))π₯) = (1rβπ
)} βΌ {π₯ β (Baseβπ
) β£ (π(.gβ(mulGrpβπ
))π₯) = (1rβπ
)} β (β―β{π₯ β π΅ β£ (π(.gβ(mulGrpβπ
))π₯) = (1rβπ
)}) β€ (β―β{π₯ β (Baseβπ
) β£ (π(.gβ(mulGrpβπ
))π₯) = (1rβπ
)})) |
56 | 54, 55 | syl 17 |
. . 3
β’ ((π
β IDomn β§ π β β) β
(β―β{π₯ β
π΅ β£ (π(.gβ(mulGrpβπ
))π₯) = (1rβπ
)}) β€ (β―β{π₯ β (Baseβπ
) β£ (π(.gβ(mulGrpβπ
))π₯) = (1rβπ
)})) |
57 | 48, 56 | eqbrtrd 5128 |
. 2
β’ ((π
β IDomn β§ π β β) β
(β―β{π₯ β
π΅ β£ (πβπ₯) β₯ π}) β€ (β―β{π₯ β (Baseβπ
) β£ (π(.gβ(mulGrpβπ
))π₯) = (1rβπ
)})) |
58 | | simpl 484 |
. . 3
β’ ((π
β IDomn β§ π β β) β π
β IDomn) |
59 | 49, 42 | ringidcl 19994 |
. . . 4
β’ (π
β Ring β
(1rβπ
)
β (Baseβπ
)) |
60 | 17, 59 | syl 17 |
. . 3
β’ ((π
β IDomn β§ π β β) β
(1rβπ
)
β (Baseβπ
)) |
61 | | simpr 486 |
. . 3
β’ ((π
β IDomn β§ π β β) β π β
β) |
62 | 49, 39 | idomrootle 41565 |
. . 3
β’ ((π
β IDomn β§
(1rβπ
)
β (Baseβπ
) β§
π β β) β
(β―β{π₯ β
(Baseβπ
) β£
(π(.gβ(mulGrpβπ
))π₯) = (1rβπ
)}) β€ π) |
63 | 58, 60, 61, 62 | syl3anc 1372 |
. 2
β’ ((π
β IDomn β§ π β β) β
(β―β{π₯ β
(Baseβπ
) β£
(π(.gβ(mulGrpβπ
))π₯) = (1rβπ
)}) β€ π) |
64 | 5, 9, 12, 57, 63 | xrletrd 13087 |
1
β’ ((π
β IDomn β§ π β β) β
(β―β{π₯ β
π΅ β£ (πβπ₯) β₯ π}) β€ π) |