Step | Hyp | Ref
| Expression |
1 | | rngabl 46249 |
. . . . . . 7
โข (๐
โ Rng โ ๐
โ Abel) |
2 | | ablgrp 19574 |
. . . . . . 7
โข (๐
โ Abel โ ๐
โ Grp) |
3 | 1, 2 | syl 17 |
. . . . . 6
โข (๐
โ Rng โ ๐
โ Grp) |
4 | | rngcl.b |
. . . . . . 7
โข ๐ต = (Baseโ๐
) |
5 | | rnglz.z |
. . . . . . 7
โข 0 =
(0gโ๐
) |
6 | 4, 5 | grpidcl 18785 |
. . . . . 6
โข (๐
โ Grp โ 0 โ ๐ต) |
7 | | eqid 2737 |
. . . . . . 7
โข
(+gโ๐
) = (+gโ๐
) |
8 | 4, 7, 5 | grplid 18787 |
. . . . . 6
โข ((๐
โ Grp โง 0 โ ๐ต) โ ( 0 (+gโ๐
) 0 ) = 0 ) |
9 | 3, 6, 8 | syl2anc2 586 |
. . . . 5
โข (๐
โ Rng โ ( 0
(+gโ๐
)
0 ) =
0
) |
10 | 9 | adantr 482 |
. . . 4
โข ((๐
โ Rng โง ๐ โ ๐ต) โ ( 0 (+gโ๐
) 0 ) = 0 ) |
11 | 10 | oveq1d 7377 |
. . 3
โข ((๐
โ Rng โง ๐ โ ๐ต) โ (( 0 (+gโ๐
) 0 ) ยท ๐) = ( 0 ยท ๐)) |
12 | | simpl 484 |
. . . 4
โข ((๐
โ Rng โง ๐ โ ๐ต) โ ๐
โ Rng) |
13 | 3, 6 | syl 17 |
. . . . . . 7
โข (๐
โ Rng โ 0 โ ๐ต) |
14 | 13, 13 | jca 513 |
. . . . . 6
โข (๐
โ Rng โ ( 0 โ ๐ต โง 0 โ ๐ต)) |
15 | 14 | anim1i 616 |
. . . . 5
โข ((๐
โ Rng โง ๐ โ ๐ต) โ (( 0 โ ๐ต โง 0 โ ๐ต) โง ๐ โ ๐ต)) |
16 | | df-3an 1090 |
. . . . 5
โข (( 0 โ ๐ต โง 0 โ ๐ต โง ๐ โ ๐ต) โ (( 0 โ ๐ต โง 0 โ ๐ต) โง ๐ โ ๐ต)) |
17 | 15, 16 | sylibr 233 |
. . . 4
โข ((๐
โ Rng โง ๐ โ ๐ต) โ ( 0 โ ๐ต โง 0 โ ๐ต โง ๐ โ ๐ต)) |
18 | | rngcl.t |
. . . . 5
โข ยท =
(.rโ๐
) |
19 | 4, 7, 18 | rngdir 46254 |
. . . 4
โข ((๐
โ Rng โง ( 0 โ ๐ต โง 0 โ ๐ต โง ๐ โ ๐ต)) โ (( 0 (+gโ๐
) 0 ) ยท ๐) = (( 0 ยท ๐)(+gโ๐
)( 0 ยท ๐))) |
20 | 12, 17, 19 | syl2anc 585 |
. . 3
โข ((๐
โ Rng โง ๐ โ ๐ต) โ (( 0 (+gโ๐
) 0 ) ยท ๐) = (( 0 ยท ๐)(+gโ๐
)( 0 ยท ๐))) |
21 | 3 | adantr 482 |
. . . 4
โข ((๐
โ Rng โง ๐ โ ๐ต) โ ๐
โ Grp) |
22 | 13 | adantr 482 |
. . . . 5
โข ((๐
โ Rng โง ๐ โ ๐ต) โ 0 โ ๐ต) |
23 | | simpr 486 |
. . . . 5
โข ((๐
โ Rng โง ๐ โ ๐ต) โ ๐ โ ๐ต) |
24 | 4, 18 | rngcl 46255 |
. . . . 5
โข ((๐
โ Rng โง 0 โ ๐ต โง ๐ โ ๐ต) โ ( 0 ยท ๐) โ ๐ต) |
25 | 12, 22, 23, 24 | syl3anc 1372 |
. . . 4
โข ((๐
โ Rng โง ๐ โ ๐ต) โ ( 0 ยท ๐) โ ๐ต) |
26 | 4, 7, 5 | grprid 18788 |
. . . . 5
โข ((๐
โ Grp โง ( 0 ยท ๐) โ ๐ต) โ (( 0 ยท ๐)(+gโ๐
) 0 ) = ( 0 ยท ๐)) |
27 | 26 | eqcomd 2743 |
. . . 4
โข ((๐
โ Grp โง ( 0 ยท ๐) โ ๐ต) โ ( 0 ยท ๐) = (( 0 ยท ๐)(+gโ๐
) 0 )) |
28 | 21, 25, 27 | syl2anc 585 |
. . 3
โข ((๐
โ Rng โง ๐ โ ๐ต) โ ( 0 ยท ๐) = (( 0 ยท ๐)(+gโ๐
) 0 )) |
29 | 11, 20, 28 | 3eqtr3d 2785 |
. 2
โข ((๐
โ Rng โง ๐ โ ๐ต) โ (( 0 ยท ๐)(+gโ๐
)( 0 ยท ๐)) = (( 0 ยท ๐)(+gโ๐
) 0 )) |
30 | 4, 7 | grplcan 18816 |
. . 3
โข ((๐
โ Grp โง (( 0 ยท ๐) โ ๐ต โง 0 โ ๐ต โง ( 0 ยท ๐) โ ๐ต)) โ ((( 0 ยท ๐)(+gโ๐
)( 0 ยท ๐)) = (( 0 ยท ๐)(+gโ๐
) 0 ) โ ( 0 ยท ๐) = 0 )) |
31 | 21, 25, 22, 25, 30 | syl13anc 1373 |
. 2
โข ((๐
โ Rng โง ๐ โ ๐ต) โ ((( 0 ยท ๐)(+gโ๐
)( 0 ยท ๐)) = (( 0 ยท ๐)(+gโ๐
) 0 ) โ ( 0 ยท ๐) = 0 )) |
32 | 29, 31 | mpbid 231 |
1
โข ((๐
โ Rng โง ๐ โ ๐ต) โ ( 0 ยท ๐) = 0 ) |