Step | Hyp | Ref
| Expression |
1 | | domnnzr 20781 |
. . 3
β’ (π
β Domn β π
β NzRing) |
2 | | abvn0b.b |
. . . . 5
β’ π΄ = (AbsValβπ
) |
3 | | eqid 2733 |
. . . . 5
β’
(Baseβπ
) =
(Baseβπ
) |
4 | | eqid 2733 |
. . . . 5
β’
(0gβπ
) = (0gβπ
) |
5 | | eqid 2733 |
. . . . 5
β’ (π₯ β (Baseβπ
) β¦ if(π₯ = (0gβπ
), 0, 1)) = (π₯ β (Baseβπ
) β¦ if(π₯ = (0gβπ
), 0, 1)) |
6 | | eqid 2733 |
. . . . 5
β’
(.rβπ
) = (.rβπ
) |
7 | | domnring 20782 |
. . . . 5
β’ (π
β Domn β π
β Ring) |
8 | 3, 6, 4 | domnmuln0 20784 |
. . . . 5
β’ ((π
β Domn β§ (π¦ β (Baseβπ
) β§ π¦ β (0gβπ
)) β§ (π§ β (Baseβπ
) β§ π§ β (0gβπ
))) β (π¦(.rβπ
)π§) β (0gβπ
)) |
9 | 2, 3, 4, 5, 6, 7, 8 | abvtrivd 20313 |
. . . 4
β’ (π
β Domn β (π₯ β (Baseβπ
) β¦ if(π₯ = (0gβπ
), 0, 1)) β π΄) |
10 | 9 | ne0d 4296 |
. . 3
β’ (π
β Domn β π΄ β β
) |
11 | 1, 10 | jca 513 |
. 2
β’ (π
β Domn β (π
β NzRing β§ π΄ β β
)) |
12 | | n0 4307 |
. . . . 5
β’ (π΄ β β
β
βπ₯ π₯ β π΄) |
13 | | neanior 3034 |
. . . . . . . . 9
β’ ((π¦ β (0gβπ
) β§ π§ β (0gβπ
)) β Β¬ (π¦ = (0gβπ
) β¨ π§ = (0gβπ
))) |
14 | | an4 655 |
. . . . . . . . . . 11
β’ (((π¦ β (Baseβπ
) β§ π§ β (Baseβπ
)) β§ (π¦ β (0gβπ
) β§ π§ β (0gβπ
))) β ((π¦ β (Baseβπ
) β§ π¦ β (0gβπ
)) β§ (π§ β (Baseβπ
) β§ π§ β (0gβπ
)))) |
15 | 2, 3, 4, 6 | abvdom 20311 |
. . . . . . . . . . . 12
β’ ((π₯ β π΄ β§ (π¦ β (Baseβπ
) β§ π¦ β (0gβπ
)) β§ (π§ β (Baseβπ
) β§ π§ β (0gβπ
))) β (π¦(.rβπ
)π§) β (0gβπ
)) |
16 | 15 | 3expib 1123 |
. . . . . . . . . . 11
β’ (π₯ β π΄ β (((π¦ β (Baseβπ
) β§ π¦ β (0gβπ
)) β§ (π§ β (Baseβπ
) β§ π§ β (0gβπ
))) β (π¦(.rβπ
)π§) β (0gβπ
))) |
17 | 14, 16 | biimtrid 241 |
. . . . . . . . . 10
β’ (π₯ β π΄ β (((π¦ β (Baseβπ
) β§ π§ β (Baseβπ
)) β§ (π¦ β (0gβπ
) β§ π§ β (0gβπ
))) β (π¦(.rβπ
)π§) β (0gβπ
))) |
18 | 17 | expdimp 454 |
. . . . . . . . 9
β’ ((π₯ β π΄ β§ (π¦ β (Baseβπ
) β§ π§ β (Baseβπ
))) β ((π¦ β (0gβπ
) β§ π§ β (0gβπ
)) β (π¦(.rβπ
)π§) β (0gβπ
))) |
19 | 13, 18 | biimtrrid 242 |
. . . . . . . 8
β’ ((π₯ β π΄ β§ (π¦ β (Baseβπ
) β§ π§ β (Baseβπ
))) β (Β¬ (π¦ = (0gβπ
) β¨ π§ = (0gβπ
)) β (π¦(.rβπ
)π§) β (0gβπ
))) |
20 | 19 | necon4bd 2960 |
. . . . . . 7
β’ ((π₯ β π΄ β§ (π¦ β (Baseβπ
) β§ π§ β (Baseβπ
))) β ((π¦(.rβπ
)π§) = (0gβπ
) β (π¦ = (0gβπ
) β¨ π§ = (0gβπ
)))) |
21 | 20 | ralrimivva 3194 |
. . . . . 6
β’ (π₯ β π΄ β βπ¦ β (Baseβπ
)βπ§ β (Baseβπ
)((π¦(.rβπ
)π§) = (0gβπ
) β (π¦ = (0gβπ
) β¨ π§ = (0gβπ
)))) |
22 | 21 | exlimiv 1934 |
. . . . 5
β’
(βπ₯ π₯ β π΄ β βπ¦ β (Baseβπ
)βπ§ β (Baseβπ
)((π¦(.rβπ
)π§) = (0gβπ
) β (π¦ = (0gβπ
) β¨ π§ = (0gβπ
)))) |
23 | 12, 22 | sylbi 216 |
. . . 4
β’ (π΄ β β
β
βπ¦ β
(Baseβπ
)βπ§ β (Baseβπ
)((π¦(.rβπ
)π§) = (0gβπ
) β (π¦ = (0gβπ
) β¨ π§ = (0gβπ
)))) |
24 | 23 | anim2i 618 |
. . 3
β’ ((π
β NzRing β§ π΄ β β
) β (π
β NzRing β§
βπ¦ β
(Baseβπ
)βπ§ β (Baseβπ
)((π¦(.rβπ
)π§) = (0gβπ
) β (π¦ = (0gβπ
) β¨ π§ = (0gβπ
))))) |
25 | 3, 6, 4 | isdomn 20780 |
. . 3
β’ (π
β Domn β (π
β NzRing β§
βπ¦ β
(Baseβπ
)βπ§ β (Baseβπ
)((π¦(.rβπ
)π§) = (0gβπ
) β (π¦ = (0gβπ
) β¨ π§ = (0gβπ
))))) |
26 | 24, 25 | sylibr 233 |
. 2
β’ ((π
β NzRing β§ π΄ β β
) β π
β Domn) |
27 | 11, 26 | impbii 208 |
1
β’ (π
β Domn β (π
β NzRing β§ π΄ β β
)) |