Step | Hyp | Ref
| Expression |
1 | | domnnzr 21231 |
. . 3
โข (๐
โ Domn โ ๐
โ NzRing) |
2 | | isdomn4.b |
. . . . . . . 8
โข ๐ต = (Baseโ๐
) |
3 | | isdomn4.x |
. . . . . . . 8
โข ยท =
(.rโ๐
) |
4 | | eqid 2727 |
. . . . . . . 8
โข
(-gโ๐
) = (-gโ๐
) |
5 | | domnring 21232 |
. . . . . . . . 9
โข (๐
โ Domn โ ๐
โ Ring) |
6 | 5 | adantr 480 |
. . . . . . . 8
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐
โ Ring) |
7 | | eldifi 4122 |
. . . . . . . . . 10
โข (๐ โ (๐ต โ { 0 }) โ ๐ โ ๐ต) |
8 | 7 | 3ad2ant1 1131 |
. . . . . . . . 9
โข ((๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต) โ ๐ โ ๐ต) |
9 | 8 | adantl 481 |
. . . . . . . 8
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ ๐ต) |
10 | | simpr2 1193 |
. . . . . . . 8
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ ๐ต) |
11 | | simpr3 1194 |
. . . . . . . 8
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ ๐ต) |
12 | 2, 3, 4, 6, 9, 10,
11 | ringsubdi 20232 |
. . . . . . 7
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท (๐(-gโ๐
)๐)) = ((๐ ยท ๐)(-gโ๐
)(๐ ยท ๐))) |
13 | 12 | eqeq1d 2729 |
. . . . . 6
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ ยท (๐(-gโ๐
)๐)) = 0 โ ((๐ ยท ๐)(-gโ๐
)(๐ ยท ๐)) = 0 )) |
14 | | simpll 766 |
. . . . . . . . 9
โข (((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐(-gโ๐
)๐) โ 0 ) โ ๐
โ Domn) |
15 | 9 | adantr 480 |
. . . . . . . . 9
โข (((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐(-gโ๐
)๐) โ 0 ) โ ๐ โ ๐ต) |
16 | | eldifsni 4789 |
. . . . . . . . . . 11
โข (๐ โ (๐ต โ { 0 }) โ ๐ โ 0 ) |
17 | 16 | 3ad2ant1 1131 |
. . . . . . . . . 10
โข ((๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต) โ ๐ โ 0 ) |
18 | 17 | ad2antlr 726 |
. . . . . . . . 9
โข (((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐(-gโ๐
)๐) โ 0 ) โ ๐ โ 0 ) |
19 | 5 | ringgrpd 20173 |
. . . . . . . . . . . 12
โข (๐
โ Domn โ ๐
โ Grp) |
20 | 2, 4 | grpsubcl 18967 |
. . . . . . . . . . . 12
โข ((๐
โ Grp โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐(-gโ๐
)๐) โ ๐ต) |
21 | 19, 20 | syl3an1 1161 |
. . . . . . . . . . 11
โข ((๐
โ Domn โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐(-gโ๐
)๐) โ ๐ต) |
22 | 21 | 3adant3r1 1180 |
. . . . . . . . . 10
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐(-gโ๐
)๐) โ ๐ต) |
23 | 22 | adantr 480 |
. . . . . . . . 9
โข (((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐(-gโ๐
)๐) โ 0 ) โ (๐(-gโ๐
)๐) โ ๐ต) |
24 | | simpr 484 |
. . . . . . . . 9
โข (((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐(-gโ๐
)๐) โ 0 ) โ (๐(-gโ๐
)๐) โ 0 ) |
25 | | isdomn4.0 |
. . . . . . . . . 10
โข 0 =
(0gโ๐
) |
26 | 2, 3, 25 | domnmuln0 21234 |
. . . . . . . . 9
โข ((๐
โ Domn โง (๐ โ ๐ต โง ๐ โ 0 ) โง ((๐(-gโ๐
)๐) โ ๐ต โง (๐(-gโ๐
)๐) โ 0 )) โ (๐ ยท (๐(-gโ๐
)๐)) โ 0 ) |
27 | 14, 15, 18, 23, 24, 26 | syl122anc 1377 |
. . . . . . . 8
โข (((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐(-gโ๐
)๐) โ 0 ) โ (๐ ยท (๐(-gโ๐
)๐)) โ 0 ) |
28 | 27 | ex 412 |
. . . . . . 7
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐(-gโ๐
)๐) โ 0 โ (๐ ยท (๐(-gโ๐
)๐)) โ 0 )) |
29 | 28 | necon4d 2959 |
. . . . . 6
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ ยท (๐(-gโ๐
)๐)) = 0 โ (๐(-gโ๐
)๐) = 0 )) |
30 | 13, 29 | sylbird 260 |
. . . . 5
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (((๐ ยท ๐)(-gโ๐
)(๐ ยท ๐)) = 0 โ (๐(-gโ๐
)๐) = 0 )) |
31 | 19 | adantr 480 |
. . . . . 6
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐
โ Grp) |
32 | | id 22 |
. . . . . . . 8
โข (๐ โ ๐ต โ ๐ โ ๐ต) |
33 | 2, 3 | ringcl 20181 |
. . . . . . . 8
โข ((๐
โ Ring โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) |
34 | 5, 7, 32, 33 | syl3an 1158 |
. . . . . . 7
โข ((๐
โ Domn โง ๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) |
35 | 34 | 3adant3r3 1182 |
. . . . . 6
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท ๐) โ ๐ต) |
36 | | id 22 |
. . . . . . . 8
โข (๐ โ ๐ต โ ๐ โ ๐ต) |
37 | 2, 3 | ringcl 20181 |
. . . . . . . 8
โข ((๐
โ Ring โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) |
38 | 5, 7, 36, 37 | syl3an 1158 |
. . . . . . 7
โข ((๐
โ Domn โง ๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) |
39 | 38 | 3adant3r2 1181 |
. . . . . 6
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท ๐) โ ๐ต) |
40 | 2, 25, 4 | grpsubeq0 18973 |
. . . . . 6
โข ((๐
โ Grp โง (๐ ยท ๐) โ ๐ต โง (๐ ยท ๐) โ ๐ต) โ (((๐ ยท ๐)(-gโ๐
)(๐ ยท ๐)) = 0 โ (๐ ยท ๐) = (๐ ยท ๐))) |
41 | 31, 35, 39, 40 | syl3anc 1369 |
. . . . 5
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (((๐ ยท ๐)(-gโ๐
)(๐ ยท ๐)) = 0 โ (๐ ยท ๐) = (๐ ยท ๐))) |
42 | 2, 25, 4 | grpsubeq0 18973 |
. . . . . 6
โข ((๐
โ Grp โง ๐ โ ๐ต โง ๐ โ ๐ต) โ ((๐(-gโ๐
)๐) = 0 โ ๐ = ๐)) |
43 | 31, 10, 11, 42 | syl3anc 1369 |
. . . . 5
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐(-gโ๐
)๐) = 0 โ ๐ = ๐)) |
44 | 30, 41, 43 | 3imtr3d 293 |
. . . 4
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ ยท ๐) = (๐ ยท ๐) โ ๐ = ๐)) |
45 | 44 | ralrimivvva 3198 |
. . 3
โข (๐
โ Domn โ
โ๐ โ (๐ต โ { 0 })โ๐ โ ๐ต โ๐ โ ๐ต ((๐ ยท ๐) = (๐ ยท ๐) โ ๐ = ๐)) |
46 | 1, 45 | jca 511 |
. 2
โข (๐
โ Domn โ (๐
โ NzRing โง
โ๐ โ (๐ต โ { 0 })โ๐ โ ๐ต โ๐ โ ๐ต ((๐ ยท ๐) = (๐ ยท ๐) โ ๐ = ๐))) |
47 | | nzrring 20444 |
. . . . . . . . . . 11
โข (๐
โ NzRing โ ๐
โ Ring) |
48 | 47 | ringgrpd 20173 |
. . . . . . . . . 10
โข (๐
โ NzRing โ ๐
โ Grp) |
49 | 2, 25 | grpidcl 18913 |
. . . . . . . . . 10
โข (๐
โ Grp โ 0 โ ๐ต) |
50 | 48, 49 | syl 17 |
. . . . . . . . 9
โข (๐
โ NzRing โ 0 โ ๐ต) |
51 | 50 | adantr 480 |
. . . . . . . 8
โข ((๐
โ NzRing โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต)) โ 0 โ ๐ต) |
52 | | oveq2 7422 |
. . . . . . . . . . 11
โข (๐ = 0 โ (๐ ยท ๐) = (๐ ยท 0 )) |
53 | 52 | eqeq2d 2738 |
. . . . . . . . . 10
โข (๐ = 0 โ ((๐ ยท ๐) = (๐ ยท ๐) โ (๐ ยท ๐) = (๐ ยท 0 ))) |
54 | | eqeq2 2739 |
. . . . . . . . . 10
โข (๐ = 0 โ (๐ = ๐ โ ๐ = 0 )) |
55 | 53, 54 | imbi12d 344 |
. . . . . . . . 9
โข (๐ = 0 โ (((๐ ยท ๐) = (๐ ยท ๐) โ ๐ = ๐) โ ((๐ ยท ๐) = (๐ ยท 0 ) โ ๐ = 0 ))) |
56 | 55 | rspcv 3603 |
. . . . . . . 8
โข ( 0 โ ๐ต โ (โ๐ โ ๐ต ((๐ ยท ๐) = (๐ ยท ๐) โ ๐ = ๐) โ ((๐ ยท ๐) = (๐ ยท 0 ) โ ๐ = 0 ))) |
57 | 51, 56 | syl 17 |
. . . . . . 7
โข ((๐
โ NzRing โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต)) โ (โ๐ โ ๐ต ((๐ ยท ๐) = (๐ ยท ๐) โ ๐ = ๐) โ ((๐ ยท ๐) = (๐ ยท 0 ) โ ๐ = 0 ))) |
58 | 2, 3, 25 | ringrz 20219 |
. . . . . . . . . . 11
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (๐ ยท 0 ) = 0 ) |
59 | 47, 7, 58 | syl2an 595 |
. . . . . . . . . 10
โข ((๐
โ NzRing โง ๐ โ (๐ต โ { 0 })) โ (๐ ยท 0 ) = 0 ) |
60 | 59 | adantrr 716 |
. . . . . . . . 9
โข ((๐
โ NzRing โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต)) โ (๐ ยท 0 ) = 0 ) |
61 | 60 | eqeq2d 2738 |
. . . . . . . 8
โข ((๐
โ NzRing โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต)) โ ((๐ ยท ๐) = (๐ ยท 0 ) โ (๐ ยท ๐) = 0 )) |
62 | 61 | imbi1d 341 |
. . . . . . 7
โข ((๐
โ NzRing โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต)) โ (((๐ ยท ๐) = (๐ ยท 0 ) โ ๐ = 0 ) โ ((๐ ยท ๐) = 0 โ ๐ = 0 ))) |
63 | 57, 62 | sylibd 238 |
. . . . . 6
โข ((๐
โ NzRing โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต)) โ (โ๐ โ ๐ต ((๐ ยท ๐) = (๐ ยท ๐) โ ๐ = ๐) โ ((๐ ยท ๐) = 0 โ ๐ = 0 ))) |
64 | 63 | ralimdvva 3199 |
. . . . 5
โข (๐
โ NzRing โ
(โ๐ โ (๐ต โ { 0 })โ๐ โ ๐ต โ๐ โ ๐ต ((๐ ยท ๐) = (๐ ยท ๐) โ ๐ = ๐) โ โ๐ โ (๐ต โ { 0 })โ๐ โ ๐ต ((๐ ยท ๐) = 0 โ ๐ = 0 ))) |
65 | | isdomn5 21237 |
. . . . 5
โข
(โ๐ โ
๐ต โ๐ โ ๐ต ((๐ ยท ๐) = 0 โ (๐ = 0 โจ ๐ = 0 )) โ โ๐ โ (๐ต โ { 0 })โ๐ โ ๐ต ((๐ ยท ๐) = 0 โ ๐ = 0 )) |
66 | 64, 65 | imbitrrdi 251 |
. . . 4
โข (๐
โ NzRing โ
(โ๐ โ (๐ต โ { 0 })โ๐ โ ๐ต โ๐ โ ๐ต ((๐ ยท ๐) = (๐ ยท ๐) โ ๐ = ๐) โ โ๐ โ ๐ต โ๐ โ ๐ต ((๐ ยท ๐) = 0 โ (๐ = 0 โจ ๐ = 0 )))) |
67 | 66 | imdistani 568 |
. . 3
โข ((๐
โ NzRing โง
โ๐ โ (๐ต โ { 0 })โ๐ โ ๐ต โ๐ โ ๐ต ((๐ ยท ๐) = (๐ ยท ๐) โ ๐ = ๐)) โ (๐
โ NzRing โง โ๐ โ ๐ต โ๐ โ ๐ต ((๐ ยท ๐) = 0 โ (๐ = 0 โจ ๐ = 0 )))) |
68 | 2, 3, 25 | isdomn 21230 |
. . 3
โข (๐
โ Domn โ (๐
โ NzRing โง
โ๐ โ ๐ต โ๐ โ ๐ต ((๐ ยท ๐) = 0 โ (๐ = 0 โจ ๐ = 0 )))) |
69 | 67, 68 | sylibr 233 |
. 2
โข ((๐
โ NzRing โง
โ๐ โ (๐ต โ { 0 })โ๐ โ ๐ต โ๐ โ ๐ต ((๐ ยท ๐) = (๐ ยท ๐) โ ๐ = ๐)) โ ๐
โ Domn) |
70 | 46, 69 | impbii 208 |
1
โข (๐
โ Domn โ (๐
โ NzRing โง
โ๐ โ (๐ต โ { 0 })โ๐ โ ๐ต โ๐ โ ๐ต ((๐ ยท ๐) = (๐ ยท ๐) โ ๐ = ๐))) |