Step | Hyp | Ref
| Expression |
1 | | domnnzr 20765 |
. . 3
โข (๐
โ Domn โ ๐
โ NzRing) |
2 | | isdomn4.b |
. . . . . . . 8
โข ๐ต = (Baseโ๐
) |
3 | | isdomn4.x |
. . . . . . . 8
โข ยท =
(.rโ๐
) |
4 | | eqid 2736 |
. . . . . . . 8
โข
(-gโ๐
) = (-gโ๐
) |
5 | | domnring 20766 |
. . . . . . . . 9
โข (๐
โ Domn โ ๐
โ Ring) |
6 | 5 | adantr 481 |
. . . . . . . 8
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐
โ Ring) |
7 | | eldifi 4086 |
. . . . . . . . . 10
โข (๐ โ (๐ต โ { 0 }) โ ๐ โ ๐ต) |
8 | 7 | 3ad2ant1 1133 |
. . . . . . . . 9
โข ((๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต) โ ๐ โ ๐ต) |
9 | 8 | adantl 482 |
. . . . . . . 8
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ ๐ต) |
10 | | simpr2 1195 |
. . . . . . . 8
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ ๐ต) |
11 | | simpr3 1196 |
. . . . . . . 8
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ ๐ต) |
12 | 2, 3, 4, 6, 9, 10,
11 | ringsubdi 20023 |
. . . . . . 7
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท (๐(-gโ๐
)๐)) = ((๐ ยท ๐)(-gโ๐
)(๐ ยท ๐))) |
13 | 12 | eqeq1d 2738 |
. . . . . 6
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ ยท (๐(-gโ๐
)๐)) = 0 โ ((๐ ยท ๐)(-gโ๐
)(๐ ยท ๐)) = 0 )) |
14 | | simpll 765 |
. . . . . . . . 9
โข (((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐(-gโ๐
)๐) โ 0 ) โ ๐
โ Domn) |
15 | 9 | adantr 481 |
. . . . . . . . 9
โข (((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐(-gโ๐
)๐) โ 0 ) โ ๐ โ ๐ต) |
16 | | eldifsni 4750 |
. . . . . . . . . . 11
โข (๐ โ (๐ต โ { 0 }) โ ๐ โ 0 ) |
17 | 16 | 3ad2ant1 1133 |
. . . . . . . . . 10
โข ((๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต) โ ๐ โ 0 ) |
18 | 17 | ad2antlr 725 |
. . . . . . . . 9
โข (((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐(-gโ๐
)๐) โ 0 ) โ ๐ โ 0 ) |
19 | 5 | ringgrpd 19973 |
. . . . . . . . . . . 12
โข (๐
โ Domn โ ๐
โ Grp) |
20 | 2, 4 | grpsubcl 18827 |
. . . . . . . . . . . 12
โข ((๐
โ Grp โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐(-gโ๐
)๐) โ ๐ต) |
21 | 19, 20 | syl3an1 1163 |
. . . . . . . . . . 11
โข ((๐
โ Domn โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐(-gโ๐
)๐) โ ๐ต) |
22 | 21 | 3adant3r1 1182 |
. . . . . . . . . 10
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐(-gโ๐
)๐) โ ๐ต) |
23 | 22 | adantr 481 |
. . . . . . . . 9
โข (((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐(-gโ๐
)๐) โ 0 ) โ (๐(-gโ๐
)๐) โ ๐ต) |
24 | | simpr 485 |
. . . . . . . . 9
โข (((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐(-gโ๐
)๐) โ 0 ) โ (๐(-gโ๐
)๐) โ 0 ) |
25 | | isdomn4.0 |
. . . . . . . . . 10
โข 0 =
(0gโ๐
) |
26 | 2, 3, 25 | domnmuln0 20768 |
. . . . . . . . 9
โข ((๐
โ Domn โง (๐ โ ๐ต โง ๐ โ 0 ) โง ((๐(-gโ๐
)๐) โ ๐ต โง (๐(-gโ๐
)๐) โ 0 )) โ (๐ ยท (๐(-gโ๐
)๐)) โ 0 ) |
27 | 14, 15, 18, 23, 24, 26 | syl122anc 1379 |
. . . . . . . 8
โข (((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐(-gโ๐
)๐) โ 0 ) โ (๐ ยท (๐(-gโ๐
)๐)) โ 0 ) |
28 | 27 | ex 413 |
. . . . . . 7
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐(-gโ๐
)๐) โ 0 โ (๐ ยท (๐(-gโ๐
)๐)) โ 0 )) |
29 | 28 | necon4d 2967 |
. . . . . 6
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ ยท (๐(-gโ๐
)๐)) = 0 โ (๐(-gโ๐
)๐) = 0 )) |
30 | 13, 29 | sylbird 259 |
. . . . 5
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (((๐ ยท ๐)(-gโ๐
)(๐ ยท ๐)) = 0 โ (๐(-gโ๐
)๐) = 0 )) |
31 | 19 | adantr 481 |
. . . . . 6
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐
โ Grp) |
32 | | id 22 |
. . . . . . . 8
โข (๐ โ ๐ต โ ๐ โ ๐ต) |
33 | 2, 3 | ringcl 19981 |
. . . . . . . 8
โข ((๐
โ Ring โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) |
34 | 5, 7, 32, 33 | syl3an 1160 |
. . . . . . 7
โข ((๐
โ Domn โง ๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) |
35 | 34 | 3adant3r3 1184 |
. . . . . 6
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท ๐) โ ๐ต) |
36 | | id 22 |
. . . . . . . 8
โข (๐ โ ๐ต โ ๐ โ ๐ต) |
37 | 2, 3 | ringcl 19981 |
. . . . . . . 8
โข ((๐
โ Ring โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) |
38 | 5, 7, 36, 37 | syl3an 1160 |
. . . . . . 7
โข ((๐
โ Domn โง ๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) |
39 | 38 | 3adant3r2 1183 |
. . . . . 6
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท ๐) โ ๐ต) |
40 | 2, 25, 4 | grpsubeq0 18833 |
. . . . . 6
โข ((๐
โ Grp โง (๐ ยท ๐) โ ๐ต โง (๐ ยท ๐) โ ๐ต) โ (((๐ ยท ๐)(-gโ๐
)(๐ ยท ๐)) = 0 โ (๐ ยท ๐) = (๐ ยท ๐))) |
41 | 31, 35, 39, 40 | syl3anc 1371 |
. . . . 5
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (((๐ ยท ๐)(-gโ๐
)(๐ ยท ๐)) = 0 โ (๐ ยท ๐) = (๐ ยท ๐))) |
42 | 2, 25, 4 | grpsubeq0 18833 |
. . . . . 6
โข ((๐
โ Grp โง ๐ โ ๐ต โง ๐ โ ๐ต) โ ((๐(-gโ๐
)๐) = 0 โ ๐ = ๐)) |
43 | 31, 10, 11, 42 | syl3anc 1371 |
. . . . 5
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐(-gโ๐
)๐) = 0 โ ๐ = ๐)) |
44 | 30, 41, 43 | 3imtr3d 292 |
. . . 4
โข ((๐
โ Domn โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ ยท ๐) = (๐ ยท ๐) โ ๐ = ๐)) |
45 | 44 | ralrimivvva 3200 |
. . 3
โข (๐
โ Domn โ
โ๐ โ (๐ต โ { 0 })โ๐ โ ๐ต โ๐ โ ๐ต ((๐ ยท ๐) = (๐ ยท ๐) โ ๐ = ๐)) |
46 | 1, 45 | jca 512 |
. 2
โข (๐
โ Domn โ (๐
โ NzRing โง
โ๐ โ (๐ต โ { 0 })โ๐ โ ๐ต โ๐ โ ๐ต ((๐ ยท ๐) = (๐ ยท ๐) โ ๐ = ๐))) |
47 | | nzrring 20731 |
. . . . . . . . . . 11
โข (๐
โ NzRing โ ๐
โ Ring) |
48 | 47 | ringgrpd 19973 |
. . . . . . . . . 10
โข (๐
โ NzRing โ ๐
โ Grp) |
49 | 2, 25 | grpidcl 18778 |
. . . . . . . . . 10
โข (๐
โ Grp โ 0 โ ๐ต) |
50 | 48, 49 | syl 17 |
. . . . . . . . 9
โข (๐
โ NzRing โ 0 โ ๐ต) |
51 | 50 | adantr 481 |
. . . . . . . 8
โข ((๐
โ NzRing โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต)) โ 0 โ ๐ต) |
52 | | oveq2 7365 |
. . . . . . . . . . 11
โข (๐ = 0 โ (๐ ยท ๐) = (๐ ยท 0 )) |
53 | 52 | eqeq2d 2747 |
. . . . . . . . . 10
โข (๐ = 0 โ ((๐ ยท ๐) = (๐ ยท ๐) โ (๐ ยท ๐) = (๐ ยท 0 ))) |
54 | | eqeq2 2748 |
. . . . . . . . . 10
โข (๐ = 0 โ (๐ = ๐ โ ๐ = 0 )) |
55 | 53, 54 | imbi12d 344 |
. . . . . . . . 9
โข (๐ = 0 โ (((๐ ยท ๐) = (๐ ยท ๐) โ ๐ = ๐) โ ((๐ ยท ๐) = (๐ ยท 0 ) โ ๐ = 0 ))) |
56 | 55 | rspcv 3577 |
. . . . . . . 8
โข ( 0 โ ๐ต โ (โ๐ โ ๐ต ((๐ ยท ๐) = (๐ ยท ๐) โ ๐ = ๐) โ ((๐ ยท ๐) = (๐ ยท 0 ) โ ๐ = 0 ))) |
57 | 51, 56 | syl 17 |
. . . . . . 7
โข ((๐
โ NzRing โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต)) โ (โ๐ โ ๐ต ((๐ ยท ๐) = (๐ ยท ๐) โ ๐ = ๐) โ ((๐ ยท ๐) = (๐ ยท 0 ) โ ๐ = 0 ))) |
58 | 2, 3, 25 | ringrz 20012 |
. . . . . . . . . . 11
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (๐ ยท 0 ) = 0 ) |
59 | 47, 7, 58 | syl2an 596 |
. . . . . . . . . 10
โข ((๐
โ NzRing โง ๐ โ (๐ต โ { 0 })) โ (๐ ยท 0 ) = 0 ) |
60 | 59 | adantrr 715 |
. . . . . . . . 9
โข ((๐
โ NzRing โง (๐ โ (๐ต โ { 0 }) โง ๐ โ ๐ต)) โ (๐ ยท 0 ) = 0 ) |
61 | 60 | eqeq2d 2747 |
. . . . . . . 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 3201 |
. . . . 5
โข (๐
โ NzRing โ
(โ๐ โ (๐ต โ { 0 })โ๐ โ ๐ต โ๐ โ ๐ต ((๐ ยท ๐) = (๐ ยท ๐) โ ๐ = ๐) โ โ๐ โ (๐ต โ { 0 })โ๐ โ ๐ต ((๐ ยท ๐) = 0 โ ๐ = 0 ))) |
65 | | isdomn5 40623 |
. . . . 5
โข
(โ๐ โ
๐ต โ๐ โ ๐ต ((๐ ยท ๐) = 0 โ (๐ = 0 โจ ๐ = 0 )) โ โ๐ โ (๐ต โ { 0 })โ๐ โ ๐ต ((๐ ยท ๐) = 0 โ ๐ = 0 )) |
66 | 64, 65 | syl6ibr 251 |
. . . 4
โข (๐
โ NzRing โ
(โ๐ โ (๐ต โ { 0 })โ๐ โ ๐ต โ๐ โ ๐ต ((๐ ยท ๐) = (๐ ยท ๐) โ ๐ = ๐) โ โ๐ โ ๐ต โ๐ โ ๐ต ((๐ ยท ๐) = 0 โ (๐ = 0 โจ ๐ = 0 )))) |
67 | 66 | imdistani 569 |
. . 3
โข ((๐
โ NzRing โง
โ๐ โ (๐ต โ { 0 })โ๐ โ ๐ต โ๐ โ ๐ต ((๐ ยท ๐) = (๐ ยท ๐) โ ๐ = ๐)) โ (๐
โ NzRing โง โ๐ โ ๐ต โ๐ โ ๐ต ((๐ ยท ๐) = 0 โ (๐ = 0 โจ ๐ = 0 )))) |
68 | 2, 3, 25 | isdomn 20764 |
. . 3
โข (๐
โ Domn โ (๐
โ NzRing โง
โ๐ โ ๐ต โ๐ โ ๐ต ((๐ ยท ๐) = 0 โ (๐ = 0 โจ ๐ = 0 )))) |
69 | 67, 68 | sylibr 233 |
. 2
โข ((๐
โ NzRing โง
โ๐ โ (๐ต โ { 0 })โ๐ โ ๐ต โ๐ โ ๐ต ((๐ ยท ๐) = (๐ ยท ๐) โ ๐ = ๐)) โ ๐
โ Domn) |
70 | 46, 69 | impbii 208 |
1
โข (๐
โ Domn โ (๐
โ NzRing โง
โ๐ โ (๐ต โ { 0 })โ๐ โ ๐ต โ๐ โ ๐ต ((๐ ยท ๐) = (๐ ยท ๐) โ ๐ = ๐))) |