Step | Hyp | Ref
| Expression |
1 | | isdomn2.b |
. . 3
β’ π΅ = (Baseβπ
) |
2 | | eqid 2733 |
. . 3
β’
(.rβπ
) = (.rβπ
) |
3 | | isdomn2.z |
. . 3
β’ 0 =
(0gβπ
) |
4 | 1, 2, 3 | isdomn 20780 |
. 2
β’ (π
β Domn β (π
β NzRing β§
βπ₯ β π΅ βπ¦ β π΅ ((π₯(.rβπ
)π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 )))) |
5 | | dfss3 3933 |
. . . 4
β’ ((π΅ β { 0 }) β πΈ β βπ₯ β (π΅ β { 0 })π₯ β πΈ) |
6 | | isdomn2.t |
. . . . . . . . 9
β’ πΈ = (RLRegβπ
) |
7 | 6, 1, 2, 3 | isrrg 20774 |
. . . . . . . 8
β’ (π₯ β πΈ β (π₯ β π΅ β§ βπ¦ β π΅ ((π₯(.rβπ
)π¦) = 0 β π¦ = 0 ))) |
8 | 7 | baib 537 |
. . . . . . 7
β’ (π₯ β π΅ β (π₯ β πΈ β βπ¦ β π΅ ((π₯(.rβπ
)π¦) = 0 β π¦ = 0 ))) |
9 | 8 | imbi2d 341 |
. . . . . 6
β’ (π₯ β π΅ β ((π₯ β 0 β π₯ β πΈ) β (π₯ β 0 β βπ¦ β π΅ ((π₯(.rβπ
)π¦) = 0 β π¦ = 0 )))) |
10 | 9 | ralbiia 3091 |
. . . . 5
β’
(βπ₯ β
π΅ (π₯ β 0 β π₯ β πΈ) β βπ₯ β π΅ (π₯ β 0 β βπ¦ β π΅ ((π₯(.rβπ
)π¦) = 0 β π¦ = 0 ))) |
11 | | eldifsn 4748 |
. . . . . . . 8
β’ (π₯ β (π΅ β { 0 }) β (π₯ β π΅ β§ π₯ β 0 )) |
12 | 11 | imbi1i 350 |
. . . . . . 7
β’ ((π₯ β (π΅ β { 0 }) β π₯ β πΈ) β ((π₯ β π΅ β§ π₯ β 0 ) β π₯ β πΈ)) |
13 | | impexp 452 |
. . . . . . 7
β’ (((π₯ β π΅ β§ π₯ β 0 ) β π₯ β πΈ) β (π₯ β π΅ β (π₯ β 0 β π₯ β πΈ))) |
14 | 12, 13 | bitri 275 |
. . . . . 6
β’ ((π₯ β (π΅ β { 0 }) β π₯ β πΈ) β (π₯ β π΅ β (π₯ β 0 β π₯ β πΈ))) |
15 | 14 | ralbii2 3089 |
. . . . 5
β’
(βπ₯ β
(π΅ β { 0 })π₯ β πΈ β βπ₯ β π΅ (π₯ β 0 β π₯ β πΈ)) |
16 | | con34b 316 |
. . . . . . . . 9
β’ (((π₯(.rβπ
)π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 )) β (Β¬ (π₯ = 0 β¨ π¦ = 0 ) β Β¬ (π₯(.rβπ
)π¦) = 0 )) |
17 | | impexp 452 |
. . . . . . . . . 10
β’ (((Β¬
π₯ = 0 β§ Β¬ π¦ = 0 ) β Β¬ (π₯(.rβπ
)π¦) = 0 ) β (Β¬ π₯ = 0 β (Β¬ π¦ = 0 β Β¬ (π₯(.rβπ
)π¦) = 0 ))) |
18 | | ioran 983 |
. . . . . . . . . . 11
β’ (Β¬
(π₯ = 0 β¨ π¦ = 0 ) β (Β¬ π₯ = 0 β§ Β¬ π¦ = 0 )) |
19 | 18 | imbi1i 350 |
. . . . . . . . . 10
β’ ((Β¬
(π₯ = 0 β¨ π¦ = 0 ) β Β¬ (π₯(.rβπ
)π¦) = 0 ) β ((Β¬ π₯ = 0 β§ Β¬ π¦ = 0 ) β Β¬ (π₯(.rβπ
)π¦) = 0 )) |
20 | | df-ne 2941 |
. . . . . . . . . . 11
β’ (π₯ β 0 β Β¬ π₯ = 0 ) |
21 | | con34b 316 |
. . . . . . . . . . 11
β’ (((π₯(.rβπ
)π¦) = 0 β π¦ = 0 ) β (Β¬ π¦ = 0 β Β¬ (π₯(.rβπ
)π¦) = 0 )) |
22 | 20, 21 | imbi12i 351 |
. . . . . . . . . 10
β’ ((π₯ β 0 β ((π₯(.rβπ
)π¦) = 0 β π¦ = 0 )) β (Β¬ π₯ = 0 β (Β¬ π¦ = 0 β Β¬ (π₯(.rβπ
)π¦) = 0 ))) |
23 | 17, 19, 22 | 3bitr4i 303 |
. . . . . . . . 9
β’ ((Β¬
(π₯ = 0 β¨ π¦ = 0 ) β Β¬ (π₯(.rβπ
)π¦) = 0 ) β (π₯ β 0 β ((π₯(.rβπ
)π¦) = 0 β π¦ = 0 ))) |
24 | 16, 23 | bitri 275 |
. . . . . . . 8
β’ (((π₯(.rβπ
)π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 )) β (π₯ β 0 β ((π₯(.rβπ
)π¦) = 0 β π¦ = 0 ))) |
25 | 24 | ralbii 3093 |
. . . . . . 7
β’
(βπ¦ β
π΅ ((π₯(.rβπ
)π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 )) β βπ¦ β π΅ (π₯ β 0 β ((π₯(.rβπ
)π¦) = 0 β π¦ = 0 ))) |
26 | | r19.21v 3173 |
. . . . . . 7
β’
(βπ¦ β
π΅ (π₯ β 0 β ((π₯(.rβπ
)π¦) = 0 β π¦ = 0 )) β (π₯ β 0 β βπ¦ β π΅ ((π₯(.rβπ
)π¦) = 0 β π¦ = 0 ))) |
27 | 25, 26 | bitri 275 |
. . . . . 6
β’
(βπ¦ β
π΅ ((π₯(.rβπ
)π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 )) β (π₯ β 0 β βπ¦ β π΅ ((π₯(.rβπ
)π¦) = 0 β π¦ = 0 ))) |
28 | 27 | ralbii 3093 |
. . . . 5
β’
(βπ₯ β
π΅ βπ¦ β π΅ ((π₯(.rβπ
)π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 )) β βπ₯ β π΅ (π₯ β 0 β βπ¦ β π΅ ((π₯(.rβπ
)π¦) = 0 β π¦ = 0 ))) |
29 | 10, 15, 28 | 3bitr4i 303 |
. . . 4
β’
(βπ₯ β
(π΅ β { 0 })π₯ β πΈ β βπ₯ β π΅ βπ¦ β π΅ ((π₯(.rβπ
)π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 ))) |
30 | 5, 29 | bitr2i 276 |
. . 3
β’
(βπ₯ β
π΅ βπ¦ β π΅ ((π₯(.rβπ
)π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 )) β (π΅ β { 0 }) β πΈ) |
31 | 30 | anbi2i 624 |
. 2
β’ ((π
β NzRing β§
βπ₯ β π΅ βπ¦ β π΅ ((π₯(.rβπ
)π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 ))) β (π
β NzRing β§ (π΅ β { 0 }) β πΈ)) |
32 | 4, 31 | bitri 275 |
1
β’ (π
β Domn β (π
β NzRing β§ (π΅ β { 0 }) β πΈ)) |