Step | Hyp | Ref
| Expression |
1 | | isdomn3.b |
. . 3
β’ π΅ = (Baseβπ
) |
2 | | eqid 2733 |
. . 3
β’
(.rβπ
) = (.rβπ
) |
3 | | isdomn3.z |
. . 3
β’ 0 =
(0gβπ
) |
4 | 1, 2, 3 | isdomn 20780 |
. 2
β’ (π
β Domn β (π
β NzRing β§
βπ₯ β π΅ βπ¦ β π΅ ((π₯(.rβπ
)π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 )))) |
5 | | eqid 2733 |
. . . . . 6
β’
(1rβπ
) = (1rβπ
) |
6 | 5, 3 | isnzr 20745 |
. . . . 5
β’ (π
β NzRing β (π
β Ring β§
(1rβπ
)
β 0
)) |
7 | 6 | anbi1i 625 |
. . . 4
β’ ((π
β NzRing β§
βπ₯ β π΅ βπ¦ β π΅ ((π₯(.rβπ
)π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 ))) β ((π
β Ring β§
(1rβπ
)
β 0 )
β§ βπ₯ β
π΅ βπ¦ β π΅ ((π₯(.rβπ
)π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 )))) |
8 | | anass 470 |
. . . 4
β’ (((π
β Ring β§
(1rβπ
)
β 0 )
β§ βπ₯ β
π΅ βπ¦ β π΅ ((π₯(.rβπ
)π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 ))) β (π
β Ring β§
((1rβπ
)
β 0
β§ βπ₯ β
π΅ βπ¦ β π΅ ((π₯(.rβπ
)π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 ))))) |
9 | 7, 8 | bitri 275 |
. . 3
β’ ((π
β NzRing β§
βπ₯ β π΅ βπ¦ β π΅ ((π₯(.rβπ
)π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 ))) β (π
β Ring β§
((1rβπ
)
β 0
β§ βπ₯ β
π΅ βπ¦ β π΅ ((π₯(.rβπ
)π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 ))))) |
10 | 1, 5 | ringidcl 19994 |
. . . . . . 7
β’ (π
β Ring β
(1rβπ
)
β π΅) |
11 | | eldifsn 4748 |
. . . . . . . 8
β’
((1rβπ
) β (π΅ β { 0 }) β
((1rβπ
)
β π΅ β§
(1rβπ
)
β 0
)) |
12 | 11 | baibr 538 |
. . . . . . 7
β’
((1rβπ
) β π΅ β ((1rβπ
) β 0 β
(1rβπ
)
β (π΅ β { 0
}))) |
13 | 10, 12 | syl 17 |
. . . . . 6
β’ (π
β Ring β
((1rβπ
)
β 0
β (1rβπ
) β (π΅ β { 0 }))) |
14 | 1, 2 | ringcl 19986 |
. . . . . . . . . . . 12
β’ ((π
β Ring β§ π₯ β π΅ β§ π¦ β π΅) β (π₯(.rβπ
)π¦) β π΅) |
15 | 14 | 3expb 1121 |
. . . . . . . . . . 11
β’ ((π
β Ring β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(.rβπ
)π¦) β π΅) |
16 | 15 | biantrurd 534 |
. . . . . . . . . 10
β’ ((π
β Ring β§ (π₯ β π΅ β§ π¦ β π΅)) β ((π₯(.rβπ
)π¦) β 0 β ((π₯(.rβπ
)π¦) β π΅ β§ (π₯(.rβπ
)π¦) β 0 ))) |
17 | | eldifsn 4748 |
. . . . . . . . . 10
β’ ((π₯(.rβπ
)π¦) β (π΅ β { 0 }) β ((π₯(.rβπ
)π¦) β π΅ β§ (π₯(.rβπ
)π¦) β 0 )) |
18 | 16, 17 | bitr4di 289 |
. . . . . . . . 9
β’ ((π
β Ring β§ (π₯ β π΅ β§ π¦ β π΅)) β ((π₯(.rβπ
)π¦) β 0 β (π₯(.rβπ
)π¦) β (π΅ β { 0 }))) |
19 | 18 | imbi2d 341 |
. . . . . . . 8
β’ ((π
β Ring β§ (π₯ β π΅ β§ π¦ β π΅)) β (((π₯ β 0 β§ π¦ β 0 ) β (π₯(.rβπ
)π¦) β 0 ) β ((π₯ β 0 β§ π¦ β 0 ) β (π₯(.rβπ
)π¦) β (π΅ β { 0 })))) |
20 | 19 | 2ralbidva 3207 |
. . . . . . 7
β’ (π
β Ring β
(βπ₯ β π΅ βπ¦ β π΅ ((π₯ β 0 β§ π¦ β 0 ) β (π₯(.rβπ
)π¦) β 0 ) β βπ₯ β π΅ βπ¦ β π΅ ((π₯ β 0 β§ π¦ β 0 ) β (π₯(.rβπ
)π¦) β (π΅ β { 0 })))) |
21 | | con34b 316 |
. . . . . . . . 9
β’ (((π₯(.rβπ
)π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 )) β (Β¬ (π₯ = 0 β¨ π¦ = 0 ) β Β¬ (π₯(.rβπ
)π¦) = 0 )) |
22 | | neanior 3034 |
. . . . . . . . . 10
β’ ((π₯ β 0 β§ π¦ β 0 ) β Β¬ (π₯ = 0 β¨ π¦ = 0 )) |
23 | | df-ne 2941 |
. . . . . . . . . 10
β’ ((π₯(.rβπ
)π¦) β 0 β Β¬ (π₯(.rβπ
)π¦) = 0 ) |
24 | 22, 23 | imbi12i 351 |
. . . . . . . . 9
β’ (((π₯ β 0 β§ π¦ β 0 ) β (π₯(.rβπ
)π¦) β 0 ) β (Β¬ (π₯ = 0 β¨ π¦ = 0 ) β Β¬ (π₯(.rβπ
)π¦) = 0 )) |
25 | 21, 24 | bitr4i 278 |
. . . . . . . 8
β’ (((π₯(.rβπ
)π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 )) β ((π₯ β 0 β§ π¦ β 0 ) β (π₯(.rβπ
)π¦) β 0 )) |
26 | 25 | 2ralbii 3124 |
. . . . . . 7
β’
(βπ₯ β
π΅ βπ¦ β π΅ ((π₯(.rβπ
)π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 )) β βπ₯ β π΅ βπ¦ β π΅ ((π₯ β 0 β§ π¦ β 0 ) β (π₯(.rβπ
)π¦) β 0 )) |
27 | | impexp 452 |
. . . . . . . . . 10
β’ ((((π₯ β π΅ β§ π¦ β π΅) β§ (π₯ β 0 β§ π¦ β 0 )) β (π₯(.rβπ
)π¦) β (π΅ β { 0 })) β ((π₯ β π΅ β§ π¦ β π΅) β ((π₯ β 0 β§ π¦ β 0 ) β (π₯(.rβπ
)π¦) β (π΅ β { 0 })))) |
28 | | an4 655 |
. . . . . . . . . . . 12
β’ (((π₯ β π΅ β§ π¦ β π΅) β§ (π₯ β 0 β§ π¦ β 0 )) β ((π₯ β π΅ β§ π₯ β 0 ) β§ (π¦ β π΅ β§ π¦ β 0 ))) |
29 | | eldifsn 4748 |
. . . . . . . . . . . . 13
β’ (π₯ β (π΅ β { 0 }) β (π₯ β π΅ β§ π₯ β 0 )) |
30 | | eldifsn 4748 |
. . . . . . . . . . . . 13
β’ (π¦ β (π΅ β { 0 }) β (π¦ β π΅ β§ π¦ β 0 )) |
31 | 29, 30 | anbi12i 628 |
. . . . . . . . . . . 12
β’ ((π₯ β (π΅ β { 0 }) β§ π¦ β (π΅ β { 0 })) β ((π₯ β π΅ β§ π₯ β 0 ) β§ (π¦ β π΅ β§ π¦ β 0 ))) |
32 | 28, 31 | bitr4i 278 |
. . . . . . . . . . 11
β’ (((π₯ β π΅ β§ π¦ β π΅) β§ (π₯ β 0 β§ π¦ β 0 )) β (π₯ β (π΅ β { 0 }) β§ π¦ β (π΅ β { 0 }))) |
33 | 32 | imbi1i 350 |
. . . . . . . . . 10
β’ ((((π₯ β π΅ β§ π¦ β π΅) β§ (π₯ β 0 β§ π¦ β 0 )) β (π₯(.rβπ
)π¦) β (π΅ β { 0 })) β ((π₯ β (π΅ β { 0 }) β§ π¦ β (π΅ β { 0 })) β (π₯(.rβπ
)π¦) β (π΅ β { 0 }))) |
34 | 27, 33 | bitr3i 277 |
. . . . . . . . 9
β’ (((π₯ β π΅ β§ π¦ β π΅) β ((π₯ β 0 β§ π¦ β 0 ) β (π₯(.rβπ
)π¦) β (π΅ β { 0 }))) β ((π₯ β (π΅ β { 0 }) β§ π¦ β (π΅ β { 0 })) β (π₯(.rβπ
)π¦) β (π΅ β { 0 }))) |
35 | 34 | 2albii 1823 |
. . . . . . . 8
β’
(βπ₯βπ¦((π₯ β π΅ β§ π¦ β π΅) β ((π₯ β 0 β§ π¦ β 0 ) β (π₯(.rβπ
)π¦) β (π΅ β { 0 }))) β βπ₯βπ¦((π₯ β (π΅ β { 0 }) β§ π¦ β (π΅ β { 0 })) β (π₯(.rβπ
)π¦) β (π΅ β { 0 }))) |
36 | | r2al 3188 |
. . . . . . . 8
β’
(βπ₯ β
π΅ βπ¦ β π΅ ((π₯ β 0 β§ π¦ β 0 ) β (π₯(.rβπ
)π¦) β (π΅ β { 0 })) β βπ₯βπ¦((π₯ β π΅ β§ π¦ β π΅) β ((π₯ β 0 β§ π¦ β 0 ) β (π₯(.rβπ
)π¦) β (π΅ β { 0 })))) |
37 | | r2al 3188 |
. . . . . . . 8
β’
(βπ₯ β
(π΅ β { 0
})βπ¦ β (π΅ β { 0 })(π₯(.rβπ
)π¦) β (π΅ β { 0 }) β βπ₯βπ¦((π₯ β (π΅ β { 0 }) β§ π¦ β (π΅ β { 0 })) β (π₯(.rβπ
)π¦) β (π΅ β { 0 }))) |
38 | 35, 36, 37 | 3bitr4ri 304 |
. . . . . . 7
β’
(βπ₯ β
(π΅ β { 0
})βπ¦ β (π΅ β { 0 })(π₯(.rβπ
)π¦) β (π΅ β { 0 }) β βπ₯ β π΅ βπ¦ β π΅ ((π₯ β 0 β§ π¦ β 0 ) β (π₯(.rβπ
)π¦) β (π΅ β { 0 }))) |
39 | 20, 26, 38 | 3bitr4g 314 |
. . . . . 6
β’ (π
β Ring β
(βπ₯ β π΅ βπ¦ β π΅ ((π₯(.rβπ
)π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 )) β βπ₯ β (π΅ β { 0 })βπ¦ β (π΅ β { 0 })(π₯(.rβπ
)π¦) β (π΅ β { 0 }))) |
40 | 13, 39 | anbi12d 632 |
. . . . 5
β’ (π
β Ring β
(((1rβπ
)
β 0
β§ βπ₯ β
π΅ βπ¦ β π΅ ((π₯(.rβπ
)π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 ))) β
((1rβπ
)
β (π΅ β { 0 }) β§
βπ₯ β (π΅ β { 0 })βπ¦ β (π΅ β { 0 })(π₯(.rβπ
)π¦) β (π΅ β { 0 })))) |
41 | | isdomn3.u |
. . . . . . 7
β’ π = (mulGrpβπ
) |
42 | 41 | ringmgp 19975 |
. . . . . 6
β’ (π
β Ring β π β Mnd) |
43 | 41, 1 | mgpbas 19907 |
. . . . . . . . 9
β’ π΅ = (Baseβπ) |
44 | 41, 5 | ringidval 19920 |
. . . . . . . . 9
β’
(1rβπ
) = (0gβπ) |
45 | 41, 2 | mgpplusg 19905 |
. . . . . . . . 9
β’
(.rβπ
) = (+gβπ) |
46 | 43, 44, 45 | issubm 18619 |
. . . . . . . 8
β’ (π β Mnd β ((π΅ β { 0 }) β
(SubMndβπ) β
((π΅ β { 0 }) β
π΅ β§
(1rβπ
)
β (π΅ β { 0 }) β§
βπ₯ β (π΅ β { 0 })βπ¦ β (π΅ β { 0 })(π₯(.rβπ
)π¦) β (π΅ β { 0 })))) |
47 | | 3anass 1096 |
. . . . . . . 8
β’ (((π΅ β { 0 }) β π΅ β§
(1rβπ
)
β (π΅ β { 0 }) β§
βπ₯ β (π΅ β { 0 })βπ¦ β (π΅ β { 0 })(π₯(.rβπ
)π¦) β (π΅ β { 0 })) β ((π΅ β { 0 }) β π΅ β§
((1rβπ
)
β (π΅ β { 0 }) β§
βπ₯ β (π΅ β { 0 })βπ¦ β (π΅ β { 0 })(π₯(.rβπ
)π¦) β (π΅ β { 0 })))) |
48 | 46, 47 | bitrdi 287 |
. . . . . . 7
β’ (π β Mnd β ((π΅ β { 0 }) β
(SubMndβπ) β
((π΅ β { 0 }) β
π΅ β§
((1rβπ
)
β (π΅ β { 0 }) β§
βπ₯ β (π΅ β { 0 })βπ¦ β (π΅ β { 0 })(π₯(.rβπ
)π¦) β (π΅ β { 0 }))))) |
49 | | difss 4092 |
. . . . . . . 8
β’ (π΅ β { 0 }) β π΅ |
50 | 49 | biantrur 532 |
. . . . . . 7
β’
(((1rβπ
) β (π΅ β { 0 }) β§ βπ₯ β (π΅ β { 0 })βπ¦ β (π΅ β { 0 })(π₯(.rβπ
)π¦) β (π΅ β { 0 })) β ((π΅ β { 0 }) β π΅ β§
((1rβπ
)
β (π΅ β { 0 }) β§
βπ₯ β (π΅ β { 0 })βπ¦ β (π΅ β { 0 })(π₯(.rβπ
)π¦) β (π΅ β { 0 })))) |
51 | 48, 50 | bitr4di 289 |
. . . . . 6
β’ (π β Mnd β ((π΅ β { 0 }) β
(SubMndβπ) β
((1rβπ
)
β (π΅ β { 0 }) β§
βπ₯ β (π΅ β { 0 })βπ¦ β (π΅ β { 0 })(π₯(.rβπ
)π¦) β (π΅ β { 0 })))) |
52 | 42, 51 | syl 17 |
. . . . 5
β’ (π
β Ring β ((π΅ β { 0 }) β
(SubMndβπ) β
((1rβπ
)
β (π΅ β { 0 }) β§
βπ₯ β (π΅ β { 0 })βπ¦ β (π΅ β { 0 })(π₯(.rβπ
)π¦) β (π΅ β { 0 })))) |
53 | 40, 52 | bitr4d 282 |
. . . 4
β’ (π
β Ring β
(((1rβπ
)
β 0
β§ βπ₯ β
π΅ βπ¦ β π΅ ((π₯(.rβπ
)π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 ))) β (π΅ β { 0 }) β
(SubMndβπ))) |
54 | 53 | pm5.32i 576 |
. . 3
β’ ((π
β Ring β§
((1rβπ
)
β 0
β§ βπ₯ β
π΅ βπ¦ β π΅ ((π₯(.rβπ
)π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 )))) β (π
β Ring β§ (π΅ β { 0 }) β
(SubMndβπ))) |
55 | 9, 54 | bitri 275 |
. 2
β’ ((π
β NzRing β§
βπ₯ β π΅ βπ¦ β π΅ ((π₯(.rβπ
)π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 ))) β (π
β Ring β§ (π΅ β { 0 }) β
(SubMndβπ))) |
56 | 4, 55 | bitri 275 |
1
β’ (π
β Domn β (π
β Ring β§ (π΅ β { 0 }) β
(SubMndβπ))) |