Step | Hyp | Ref
| Expression |
1 | | domnring 20782 |
. . . . 5
β’ (π
β Domn β π
β Ring) |
2 | 1 | adantl 483 |
. . . 4
β’ ((π΅ β Fin β§ π
β Domn) β π
β Ring) |
3 | | domnnzr 20781 |
. . . . . . . . . . 11
β’ (π
β Domn β π
β NzRing) |
4 | 3 | adantl 483 |
. . . . . . . . . 10
β’ ((π΅ β Fin β§ π
β Domn) β π
β NzRing) |
5 | | eqid 2733 |
. . . . . . . . . . 11
β’
(1rβπ
) = (1rβπ
) |
6 | | eqid 2733 |
. . . . . . . . . . 11
β’
(0gβπ
) = (0gβπ
) |
7 | 5, 6 | nzrnz 20746 |
. . . . . . . . . 10
β’ (π
β NzRing β
(1rβπ
)
β (0gβπ
)) |
8 | 4, 7 | syl 17 |
. . . . . . . . 9
β’ ((π΅ β Fin β§ π
β Domn) β
(1rβπ
)
β (0gβπ
)) |
9 | 8 | neneqd 2945 |
. . . . . . . 8
β’ ((π΅ β Fin β§ π
β Domn) β Β¬
(1rβπ
) =
(0gβπ
)) |
10 | | eqid 2733 |
. . . . . . . . . 10
β’
(Unitβπ
) =
(Unitβπ
) |
11 | 10, 6, 5 | 0unit 20114 |
. . . . . . . . 9
β’ (π
β Ring β
((0gβπ
)
β (Unitβπ
)
β (1rβπ
) = (0gβπ
))) |
12 | 2, 11 | syl 17 |
. . . . . . . 8
β’ ((π΅ β Fin β§ π
β Domn) β
((0gβπ
)
β (Unitβπ
)
β (1rβπ
) = (0gβπ
))) |
13 | 9, 12 | mtbird 325 |
. . . . . . 7
β’ ((π΅ β Fin β§ π
β Domn) β Β¬
(0gβπ
)
β (Unitβπ
)) |
14 | | disjsn 4673 |
. . . . . . 7
β’
(((Unitβπ
)
β© {(0gβπ
)}) = β
β Β¬
(0gβπ
)
β (Unitβπ
)) |
15 | 13, 14 | sylibr 233 |
. . . . . 6
β’ ((π΅ β Fin β§ π
β Domn) β
((Unitβπ
) β©
{(0gβπ
)})
= β
) |
16 | | fidomndrng.b |
. . . . . . . 8
β’ π΅ = (Baseβπ
) |
17 | 16, 10 | unitss 20094 |
. . . . . . 7
β’
(Unitβπ
)
β π΅ |
18 | | reldisj 4412 |
. . . . . . 7
β’
((Unitβπ
)
β π΅ β
(((Unitβπ
) β©
{(0gβπ
)})
= β
β (Unitβπ
) β (π΅ β {(0gβπ
)}))) |
19 | 17, 18 | ax-mp 5 |
. . . . . 6
β’
(((Unitβπ
)
β© {(0gβπ
)}) = β
β (Unitβπ
) β (π΅ β {(0gβπ
)})) |
20 | 15, 19 | sylib 217 |
. . . . 5
β’ ((π΅ β Fin β§ π
β Domn) β
(Unitβπ
) β
(π΅ β
{(0gβπ
)})) |
21 | | eqid 2733 |
. . . . . . 7
β’
(β₯rβπ
) = (β₯rβπ
) |
22 | | eqid 2733 |
. . . . . . 7
β’
(.rβπ
) = (.rβπ
) |
23 | | simplr 768 |
. . . . . . 7
β’ (((π΅ β Fin β§ π
β Domn) β§ π₯ β (π΅ β {(0gβπ
)})) β π
β Domn) |
24 | | simpll 766 |
. . . . . . 7
β’ (((π΅ β Fin β§ π
β Domn) β§ π₯ β (π΅ β {(0gβπ
)})) β π΅ β Fin) |
25 | | simpr 486 |
. . . . . . 7
β’ (((π΅ β Fin β§ π
β Domn) β§ π₯ β (π΅ β {(0gβπ
)})) β π₯ β (π΅ β {(0gβπ
)})) |
26 | | eqid 2733 |
. . . . . . 7
β’ (π¦ β π΅ β¦ (π¦(.rβπ
)π₯)) = (π¦ β π΅ β¦ (π¦(.rβπ
)π₯)) |
27 | 16, 6, 5, 21, 22, 23, 24, 25, 26 | fidomndrnglem 20793 |
. . . . . 6
β’ (((π΅ β Fin β§ π
β Domn) β§ π₯ β (π΅ β {(0gβπ
)})) β π₯(β₯rβπ
)(1rβπ
)) |
28 | | eqid 2733 |
. . . . . . . 8
β’
(opprβπ
) = (opprβπ
) |
29 | 28, 16 | opprbas 20061 |
. . . . . . 7
β’ π΅ =
(Baseβ(opprβπ
)) |
30 | 28, 6 | oppr0 20067 |
. . . . . . 7
β’
(0gβπ
) =
(0gβ(opprβπ
)) |
31 | 28, 5 | oppr1 20068 |
. . . . . . 7
β’
(1rβπ
) =
(1rβ(opprβπ
)) |
32 | | eqid 2733 |
. . . . . . 7
β’
(β₯rβ(opprβπ
)) =
(β₯rβ(opprβπ
)) |
33 | | eqid 2733 |
. . . . . . 7
β’
(.rβ(opprβπ
)) =
(.rβ(opprβπ
)) |
34 | 28 | opprdomn 20787 |
. . . . . . . 8
β’ (π
β Domn β
(opprβπ
) β Domn) |
35 | 23, 34 | syl 17 |
. . . . . . 7
β’ (((π΅ β Fin β§ π
β Domn) β§ π₯ β (π΅ β {(0gβπ
)})) β
(opprβπ
) β Domn) |
36 | | eqid 2733 |
. . . . . . 7
β’ (π¦ β π΅ β¦ (π¦(.rβ(opprβπ
))π₯)) = (π¦ β π΅ β¦ (π¦(.rβ(opprβπ
))π₯)) |
37 | 29, 30, 31, 32, 33, 35, 24, 25, 36 | fidomndrnglem 20793 |
. . . . . 6
β’ (((π΅ β Fin β§ π
β Domn) β§ π₯ β (π΅ β {(0gβπ
)})) β π₯(β₯rβ(opprβπ
))(1rβπ
)) |
38 | 10, 5, 21, 28, 32 | isunit 20091 |
. . . . . 6
β’ (π₯ β (Unitβπ
) β (π₯(β₯rβπ
)(1rβπ
) β§ π₯(β₯rβ(opprβπ
))(1rβπ
))) |
39 | 27, 37, 38 | sylanbrc 584 |
. . . . 5
β’ (((π΅ β Fin β§ π
β Domn) β§ π₯ β (π΅ β {(0gβπ
)})) β π₯ β (Unitβπ
)) |
40 | 20, 39 | eqelssd 3966 |
. . . 4
β’ ((π΅ β Fin β§ π
β Domn) β
(Unitβπ
) = (π΅ β
{(0gβπ
)})) |
41 | 16, 10, 6 | isdrng 20201 |
. . . 4
β’ (π
β DivRing β (π
β Ring β§
(Unitβπ
) = (π΅ β
{(0gβπ
)}))) |
42 | 2, 40, 41 | sylanbrc 584 |
. . 3
β’ ((π΅ β Fin β§ π
β Domn) β π
β
DivRing) |
43 | 42 | ex 414 |
. 2
β’ (π΅ β Fin β (π
β Domn β π
β
DivRing)) |
44 | | drngdomn 20789 |
. 2
β’ (π
β DivRing β π
β Domn) |
45 | 43, 44 | impbid1 224 |
1
β’ (π΅ β Fin β (π
β Domn β π
β
DivRing)) |